Block Causal Quotient Decomposition

Abstract

Block-product intervention channels decompose causal equivalence and its quotient.

Theorem 1.1 (Causal equivalence and the causal quotient decompose by blocks).

$$\left(\forall M\in \mathrm{BlockModel}\left(I\right),N\in \mathrm{BlockModel}\left(I\right),\left(\forall a\in \mathrm{JointIntervention}\left(I\right),\mathrm{blockInterventionalOutcome}\left(a,M\right)=\mathrm{blockInterventionalOutcome}\left(a,N\right)\right)\iff \left(\forall i\in I,\forall u\in \mathrm{Action}\left(i\right),\mathrm{apply}\left(M,i,u\right)=\mathrm{apply}\left(N,i,u\right)\right)\right)\wedge \left(\forall M\in \mathrm{BlockModel}\left(I\right),\mathrm{causalQuotientEquiv}\left(\mathrm{globalClass}\left(M\right)\right)=\mathrm{localClasses}\left(M\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Interventions/BlockCausalQuotientDecomposition.causal_equivalence_block_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let the block index be finite. Each block has a nonempty allowed intervention type and a local response channel. A joint intervention is the unrestricted product of those local interventions, and its response is assembled coordinatewise.

Two block models agree under every joint intervention exactly when their local channels agree under every intervention in every block. The reverse direction inserts a chosen local action into a baseline joint intervention.

The global and local causal quotients use the existing empirical setoid. The named canonical equivalence is Mathlib’s indexed quotient-product equivalence after transporting along the first clause, and it sends each global class to its family of local classes.

References

• Truth anchor: D5/S3/ConceptDynamics/Interventions/BlockCausalQuotientDecomposition.causal_equivalence_block_decomposition
• Dependency: D5/S3/ConceptDynamics/EmpiricalIdentifiability