Recursive Intervention Composition

Abstract

A recursively realized node value makes its additional intervention redundant.

Theorem 1.1 (A realized intervention composes without changing the outcome).

$$\forall n:\mathbb{N},X,U:\mathrm{Type},model:\mathrm{StructuralModel}(n,X,U),intervention:\mathrm{Finset}(\mathrm{Fin}(n)),assigned:\mathrm{Fin}(n)\to X,u:U,baseResult,expandedResult:\mathrm{Fin}(n)\to X,w,y:\mathrm{Fin}(n),\mathrm{EvaluationWitness}(model,intervention,assigned,u,\mathrm{order}(model),\mathrm{initial}(model,u),baseResult)\wedge \mathrm{EvaluationWitness}(model,\mathrm{insert}(w,intervention),assigned,u,\mathrm{order}(model),\mathrm{initial}(model,u),expandedResult)\wedge baseResult(w)=assigned(w)\Rightarrow expandedResult(y)=baseResult(y).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Causal/RecursiveInterventionComposition.recursive_intervention_composition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both worlds use the repository’s parent-ordered structural model, the same external state, and the same assignment. The second world additionally intervenes at one node.

When the first evaluation already realizes the value assigned at that node, the inserted intervention performs the same update. Determinism of all later recursive updates then gives the same value at every queried outcome node.

References

• Truth anchor: D5/S3/ConceptDynamics/Causal/RecursiveInterventionComposition.recursive_intervention_composition
• Dependency: D5/S3/ConceptDynamics/Causal/ParentOrderedStructuralEvaluationSemantics