Forced development

Developing a partial valuation in Kleene's three-valued way. A vertex the valuation leaves undetermined is forced to x when every completion of its parents' forced values yields x under its mechanism, so a turned handle on an unlocked door forces the door open while the circuit is still undetermined. ForcedFuel M s n v x is the n-step approximation and Forced M s v x its limit, which is reached at any fuel above a ranking of the graph. The strict development developDetVtxFuel settles a vertex only once all its parents are settled, so whatever it settles is forced.

References

• [bar-asher-siegal-2026]
• [baglini-bar-asher-siegal-2025]

def Causation.SEM.ForcedFuel {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.IsDeterministic] (s : Valuation α) : ℕ → (v : V) → α v → Prop

v is forced to x within n steps: settled by s, or, for an inner vertex, every completion of its parents' values forced within n - 1 steps yields x.

Equations

• One or more equations did not get rendered due to their size.
• M.ForcedFuel s 0 x✝¹ x✝ = (s.get x✝¹ = some x✝)

def Causation.SEM.Forced {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.IsDeterministic] (s : Valuation α) (v : V) (x : α v) : Prop

v is forced to x: within some number of steps.

Equations

• M.Forced s v x = ∃ (n : ℕ), M.ForcedFuel s n v x

def Causation.SEM.decidableForcedFuel {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.IsDeterministic] (s : Valuation α) [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (n : ℕ) (v : V) (x : α v) : Decidable (M.ForcedFuel s n v x)

Deciding ForcedFuel by recursion on the fuel.

Equations

• M.decidableForcedFuel s 0 x✝¹ x✝ = Causation.SEM.decidableForcedFuel._aux_1 M s x✝¹ x✝
• M.decidableForcedFuel s n.succ x✝¹ x✝ = ⋯.mpr inferInstance

@[instance_reducible]

instance Causation.SEM.instDecidableForcedFuel {V : Type u_1} {α : V → Type u_2} (M : SEM V α) [M.IsDeterministic] (s : Valuation α) [DecidableEq V] [DecidableValuation α] [(v : V) → Fintype (α v)] (n : ℕ) (v : V) (x : α v) : Decidable (M.ForcedFuel s n v x)

Equations

• M.instDecidableForcedFuel s n v x = M.decidableForcedFuel s n v x

theorem Causation.SEM.ForcedFuel.succ {V : Type u_1} {α : V → Type u_2} {M : SEM V α} [M.IsDeterministic] {s : Valuation α} {n : ℕ} {v : V} {x : α v} : M.ForcedFuel s n v x → M.ForcedFuel s (n + 1) v x

theorem Causation.SEM.ForcedFuel.mono {V : Type u_1} {α : V → Type u_2} {M : SEM V α} [M.IsDeterministic] {s : Valuation α} {m n : ℕ} (h : m ≤ n) {v : V} {x : α v} (hf : M.ForcedFuel s m v x) : M.ForcedFuel s n v x

theorem Causation.SEM.ForcedFuel.forced {V : Type u_1} {α : V → Type u_2} {M : SEM V α} [M.IsDeterministic] {s : Valuation α} {n : ℕ} {v : V} {x : α v} (h : M.ForcedFuel s n v x) : M.Forced s v x

theorem Causation.SEM.forcedFuel_iff_of_lt {V : Type u_1} {α : V → Type u_2} {M : SEM V α} [M.IsDeterministic] {s : Valuation α} (r : M.graph.Ranking) {v : V} {n : ℕ} (hn : r v < n) {x : α v} : M.ForcedFuel s n v x ↔ M.ForcedFuel s (r v + 1) v x

Above a ranking of the graph, more fuel forces nothing new.

theorem Causation.SEM.forced_iff_fuel {V : Type u_1} {α : V → Type u_2} {M : SEM V α} [M.IsDeterministic] {s : Valuation α} (r : M.graph.Ranking) {v : V} {n : ℕ} (hn : r v < n) {x : α v} : M.Forced s v x ↔ M.ForcedFuel s n v x

The limit is reached at any fuel above a ranking.

theorem Causation.SEM.ForcedFuel.of_developDetVtxFuel {V : Type u_1} {α : V → Type u_2} {M : SEM V α} [M.IsDeterministic] {s : Valuation α} [DecidableEq V] {n : ℕ} {v : V} {x : α v} : M.developDetVtxFuel s n v = some x → M.ForcedFuel s n v x

Whatever the strict development settles is forced.