Interaction Witness from Noncommuting Interventions

Abstract

Independent translations commute, so an observed order defect excludes that model.

Theorem 1.1 (Independent translations commute and defects exclude them).

$$\begin{gathered} \forall X,U,Y:\mathrm{Type},[\mathrm{AddCommGroup}(X)],F:U\to X\to X,\forall a:U\to X,\forall u:U,x:X,F_u(x)=x+a_u\Rightarrow \\ \forall u,v:U,F_u\circ F_v=F_v\circ F_u\wedge \forall T:X\to Y,u,v:U,\mathrm{Nonempty}(\{x:X\mid T(F_u(F_v(x)))\ne T(F_v(F_u(x)))\})\Rightarrow \\ \neg \exists a:U\to X,\forall w:U,x:X,F_w(x)=x+a_w. \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let X be an abelian group, U an intervention-index type, and F_u the intervention at u. The first public clause assumes the interventions are constructed from independently indexed displacements and proves that every pair commutes.

For a canonical concept readout T, the second public clause says that a nonempty set of states distinguished by the two intervention orders rules out every independent additive-translation representation.

This state-level mechanism is the rigorous interaction witness behind the source’s drug-order, legal-measure, course-order, trauma-and-repair, and multiple-cause examples.

References

• Truth anchor: D5/S3/ConceptDynamics/Interventions/AbelianTranslationInteraction.abelian_translation_commutation_and_defect_exclusion
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition