Observed-Break Decomposition
Abstract
Observed symmetry breaking splits into observer and intrinsic defects.
Theorem 1.1 (Observed breaking has two exact sources).
Proof. Machine-checked in Lean as D5/S3/Observer/Naturality/ObservedBreakDecomposition.observed_break_decomposition (✓ std3). ∎
Source. Repository-derived.
Commentary.
The observer term measures failure of the readout to intertwine the object update with the observed update. The second term reads the object’s intrinsic update defect.
The source writes the readout as an ordinary function, but the displayed identity requires preservation of subtraction. Lean records that repair by typing the readout as an AddMonoidHom.
After applying map_sub, additive cancellation gives the exact split. This declaration is the bind-only companion of the explicit nonadditive counterexample below.
Theorem 1.2 (Additivity cannot be dropped).
Proof. Machine-checked in Lean as D5/S3/Observer/Naturality/ObservedBreakDecomposition.nonadditive_observer_break_counterexample (✓ std3). ∎
Source. Repository-derived.
Commentary.
On the integers, the quadratic readout O(z)=z z, the successor object update, and the identity observed update violate the decomposition at z=1.
This concrete computation is the module’s escape witness: it establishes that the repaired additivity hypothesis is mathematically necessary, rather than a Lean convenience.
References
- Truth anchor:
D5/S3/Observer/Naturality/ObservedBreakDecomposition.nonadditive_observer_break_counterexample - Truth anchor:
D5/S3/Observer/Naturality/ObservedBreakDecomposition.observed_break_decomposition