@cite{bar-asher-siegal-2026}: Causation and Causal Relations

@cite{bar-asher-siegal-2026} @cite{baglini-bar-asher-siegal-2025} @cite{baglini-bar-asher-siegal-2020}

Formalization of the door-opening scenario from @cite{bar-asher-siegal-2026} 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 @cite{bar-asher-siegal-2026}'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 Core.Causal.BoolSEM (causallySufficientOn, completesForEffectOn) 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 : Core.Causal.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 : Core.Causal.CausalGraph V

Manual-only graph: drops the automatic pathway entirely.

Equations

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

noncomputable def BarAsherSiegal2026.doorOpensFullMech : Core.Causal.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 : Core.Causal.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 : Core.Causal.BoolSEM V

Equations

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

noncomputable def BarAsherSiegal2026.manualModel : Core.Causal.BoolSEM V

Equations

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

@[implicit_reducible]

noncomputable instance BarAsherSiegal2026.instIsDeterministicVBoolFullModel : Core.Causal.SEM.IsDeterministic fullModel

Equations

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

@[implicit_reducible]

noncomputable instance BarAsherSiegal2026.instIsDeterministicVBoolManualModel : Core.Causal.SEM.IsDeterministic manualModel

Equations

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

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

Background: lock disengaged.

Equations

• BarAsherSiegal2026.unlocked = Core.Causal.Valuation.empty.extend BarAsherSiegal2026.V.lock false

theorem BarAsherSiegal2026.handle_completes_manual : manualModel.completesForEffectOn varList unlocked 1 V.handle V.doorOpens

Manual-only model: handle completes the sufficient set for doorOpens (full open and cause felicity, per @cite{bar-asher-siegal-2026}). Both completion and member modes succeed because there's no alternative pathway.

theorem BarAsherSiegal2026.handle_completes_full : fullModel.completesForEffectOn varList unlocked 2 V.handle V.doorOpens

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 : ¬fullModel.completesForEffectOn varList ((unlocked.extend V.button true).extend V.electricity true) 2 V.handle V.doorOpens

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 — completion CC-selection FAILS for handle. This captures @cite{bar-asher-siegal-2026}'s point that open is infelicitous under overdetermination.