SingleLatticeTransform
plain-language theorem explainer
SingleLatticeTransform defines a map on an agent's state that leaves the imbalance measure sigma unchanged. Researchers deriving the uniqueness of love among the fourteen virtues cite it to separate intra-lattice automorphisms from inter-agent couplings. The declaration is a direct structure with an apply function and an explicit preservation axiom for sigma.
Claim. A single-lattice transform is a function $f$ from an agent's state to itself such that $f(s).sigma = s.sigma$ for every state $s$, where the agent's state consists of an imbalance scalar $sigma$ in $mathbb{R}$ together with a positive lattice size.
background
AgentState is the structure carrying an imbalance scalar sigma in $mathbb{R}$, a lattice size in $mathbb{N}$, and the proof that the size is positive. The module sets the fourteen canonical virtue generators from the DREAM theorem against one another: thirteen act inside a single lattice while love couples two lattices. Upstream, sigma is the gap between private preference and public vote in the Abilene paradox definition, and the J-cost calibration appears in the LedgerFactorization structure.
proof idea
This is the structure definition itself. It introduces the apply map together with the forall statement that enforces sigma preservation; no lemmas or tactics are applied.
why it matters
The structure is the direct parent of the theorem automorphism_preserves_sigma, which states that any such transform leaves sigma invariant. It fills the classification slot in the module's derivation of love's uniqueness by identifying the thirteen sigma-preserving virtues with single-lattice automorphisms, in contrast to the cross-lattice redistribution performed by love. The surrounding argument rests on the Recognition Composition Law and the eight-tick octave that fixes the virtue count at fourteen.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.