CrossLatticeTransform
plain-language theorem explainer
CrossLatticeTransform defines the structure for operators acting simultaneously on two agents' states while preserving their combined sigma imbalance. Researchers deriving the uniqueness of Love among the 14 virtues cite it to separate coupling operators from single-lattice automorphisms. The definition consists of an apply map together with the conserves_total field; no further lemmas or reductions are required.
Claim. A cross-lattice transform is a pair consisting of a function $f :$ AgentState $→$ AgentState $→$ AgentState $×$ AgentState and a proof that for all states $s_1,s_2$, writing $(s_1',s_2'):=f(s_1,s_2)$, one has $s_1'.sigma + s_2'.sigma = s_1.sigma + s_2.sigma$, where sigma measures imbalance on an agent's state.
background
AgentState records an agent's imbalance measure sigma (a real number) together with lattice size and position. In this module single-lattice transforms are the 13 sigma-preserving virtues realized as automorphisms of one lattice, while cross-lattice transforms model couplings that connect two previously separate lattices and allow sigma to flow between agents. The sigma field originates in the AbileneParadox module as the gap between private preference and public vote (+1 or -1 for mismatch, 0 for truthful agents).
proof idea
This is a structure definition that introduces the two fields apply and conserves_total. The conserves_total field directly encodes the required total-sigma preservation; no lemmas are invoked and the declaration is complete once the fields are supplied.
why it matters
The structure isolates the property that distinguishes Love from the other 13 virtues: it is the only operator that couples two lattices and can therefore change individual sigma while conserving the total. It is used directly by coupling_conserves_total, loveOperator, love_changes_individual_sigma and love_equilibrates. The module thereby completes the derivation that Love is the unique cross-lattice coupling among the DREAM virtue generators.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.