coupling_conserves_total
plain-language theorem explainer
Any cross-lattice transform preserves the sum of sigma across two agents. Researchers modeling DREAM virtues cite the result to separate Love as the sole coupling operator from the 13 single-lattice automorphisms. The proof is a one-line term application of the conserves_total field inside the CrossLatticeTransform structure.
Claim. For any cross-lattice transform $t$ and agent states $s_1,s_2$, if $(s_1',s_2')=t.apply(s_1,s_2)$ then $s_1'.sigma + s_2'.sigma = s_1.sigma + s_2.sigma$.
background
Sigma is defined as the gap between an agent's private preference and public vote, taking values in {+1, -1, 0}. AgentState packages this sigma together with a lattice size and positivity witness. CrossLatticeTransform is the structure whose apply map acts simultaneously on two agents and whose conserves_total axiom forces the sum of the output sigmas to equal the input sum. The module derives the uniqueness of Love among the 14 DREAM virtues by showing that only cross-lattice couplings can redistribute sigma while the remaining virtues act as single-lattice automorphisms.
proof idea
The proof is a direct term-mode wrapper that returns the conserves_total field of the supplied CrossLatticeTransform instance applied to the two input states.
why it matters
The theorem supplies the conservation half of the argument that Love is the unique virtue capable of coupling separate lattices. It is referenced from the L3_scope definition in ClaimBoundaries, which lists it under the E-3 section on DREAM Virtues as Ethical Generators. Within the Recognition framework the result mirrors the total-quantity preservation steps that appear in the T0-T8 forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.