[BS26b]: Causation and Causal Relations

[BS26b] [BBS25] [BBS20]

Formalization of the door-opening scenario from [BS26b] Figure 1: a structural equation model with two alternative sufficient sets for a single effect (the door opening).

The Door-Opening Model

Variables:

• handle: handle is turned
• lock: lock is engaged (effect needs ¬lock)
• circuit: circuit is closed
• electricity: electricity is running
• button: button is pressed
• doorOpens: door opens (the effect)

Mechanism: doorOpens = (handle ∧ ¬lock) ∨ (circuit ∧ electricity ∧ ¬lock), plus circuit := button for the automatic pathway. Two sufficient sets:

• Manual (handle ∧ ¬lock) ⊨ doorOpens
• Automatic (circuit ∧ electricity ∧ ¬lock) ⊨ doorOpens

Key Result

The model demonstrates CC-selection at work — completion mode (CoS verbs like open) succeeds when handle alone is the active pathway, but FAILS under overdetermination (both pathways active simultaneously). This captures [BS26b]'s point that open is infelicitous when an alternative explanation exists.

Member-mode (Def 10b causally-necessary) divergence between open and cause awaits substrate support for multi-parent disjunctive mechanisms.

Sufficiency/completion predicates are imported from the substrate (BoolSEM.causallySufficient, CCSelection.completesForEffect) rather than re-stipulated locally — see CLAUDE.md "Theory-hub denotation as study-file constraint."

inductive BarAsherSiegal2026.V : Type

Six-vertex door scenario. Inductive enum so Fintype.elems gives a fixed canonical order and developDet reduces structurally.

• handle : V
• lock : V
• circuit : V
• electricity : V
• button : V
• doorOpens : V

@[implicit_reducible]

instance BarAsherSiegal2026.instDecidableEqV : DecidableEq V

Equations

• BarAsherSiegal2026.instDecidableEqV x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BarAsherSiegal2026.instFintypeV : Fintype V

Equations

• BarAsherSiegal2026.instFintypeV = { elems := { val := ↑BarAsherSiegal2026.V.enumList, nodup := BarAsherSiegal2026.V.enumList_nodup }, complete := BarAsherSiegal2026.instFintypeV._proof_1 }

def BarAsherSiegal2026.instReprV.repr : V → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• BarAsherSiegal2026.instReprV.repr BarAsherSiegal2026.V.lock prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BarAsherSiegal2026.V.lock")).group prec✝

@[implicit_reducible]

instance BarAsherSiegal2026.instReprV : Repr V

Equations

• BarAsherSiegal2026.instReprV = { reprPrec := BarAsherSiegal2026.instReprV.repr }

def BarAsherSiegal2026.varList : List V

Equations

• One or more equations did not get rendered due to their size.

def BarAsherSiegal2026.fullGraph : Causation.CausalGraph V

Full graph: button → circuit; (handle, lock) → doorOpens (manual); (circuit, electricity, lock) → doorOpens (automatic).

Equations

• One or more equations did not get rendered due to their size.

def BarAsherSiegal2026.manualGraph : Causation.CausalGraph V

Manual-only graph: drops the automatic pathway entirely.

Equations

• One or more equations did not get rendered due to their size.

def BarAsherSiegal2026.fullDepth : V → ℕ

Depth certificate for the full graph.

Equations

• BarAsherSiegal2026.fullDepth BarAsherSiegal2026.V.circuit = 1
• BarAsherSiegal2026.fullDepth BarAsherSiegal2026.V.doorOpens = 2
• BarAsherSiegal2026.fullDepth x✝ = 0

instance BarAsherSiegal2026.instIsDAGVFullGraph : fullGraph.IsDAG

def BarAsherSiegal2026.manualDepth : V → ℕ

Depth certificate for the manual graph.

Equations

• BarAsherSiegal2026.manualDepth BarAsherSiegal2026.V.doorOpens = 1
• BarAsherSiegal2026.manualDepth x✝ = 0

instance BarAsherSiegal2026.instIsDAGVManualGraph : manualGraph.IsDAG

noncomputable def BarAsherSiegal2026.doorOpensFullMech : Causation.Mechanism fullGraph (fun (x : V) => Bool) V.doorOpens

Door-opens mechanism (full model): manual OR automatic, both need ¬lock.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BarAsherSiegal2026.doorOpensManualMech : Causation.Mechanism manualGraph (fun (x : V) => Bool) V.doorOpens

Door-opens mechanism (manual model): just handle ∧ ¬lock.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BarAsherSiegal2026.fullModel : Causation.BoolSEM V

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BarAsherSiegal2026.manualModel : Causation.BoolSEM V

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance BarAsherSiegal2026.instIsDeterministicVBoolFullModel : Causation.SEM.IsDeterministic fullModel

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance BarAsherSiegal2026.instIsDeterministicVBoolManualModel : Causation.SEM.IsDeterministic manualModel

Equations

• One or more equations did not get rendered due to their size.

instance BarAsherSiegal2026.instIsDAGVGraphBoolFullModel : fullModel.graph.IsDAG

instance BarAsherSiegal2026.instIsDAGVGraphBoolManualModel : manualModel.graph.IsDAG

def BarAsherSiegal2026.unlocked : Causation.Valuation fun (x : V) => Bool

Background: lock disengaged.

Equations

• BarAsherSiegal2026.unlocked = Causation.Valuation.empty.extend BarAsherSiegal2026.V.lock false

theorem BarAsherSiegal2026.handle_completes_manual : Causation.CCSelection.completesForEffect manualModel unlocked V.handle true false V.doorOpens true

Manual-only model: handle completes the sufficient set for doorOpens (full open and cause felicity, per [BS26b]). Both completion and member modes succeed because there's no alternative pathway.

theorem BarAsherSiegal2026.handle_completes_full : Causation.CCSelection.completesForEffect fullModel unlocked V.handle true false V.doorOpens true

Full model with handle alone: handle completes the manual sufficient set, satisfying open-style completion CC-selection. The automatic pathway doesn't fire because button=false in unlocked.

theorem BarAsherSiegal2026.handle_no_completion_overdetermined : ¬Causation.CCSelection.completesForEffect fullModel ((unlocked.extend V.button true).extend V.electricity true) V.handle true false V.doorOpens true

Overdetermination in the full model: when both pathways are independently activated (button=true, electricity=true alongside handle=true), removing handle still leaves doorOpens true via the automatic pathway — the but-for half of completion CC-selection FAILS for handle. This captures [BS26b]'s point that open is infelicitous under overdetermination.