AgentState
plain-language theorem explainer
AgentState records an agent's imbalance sigma together with its lattice size. Researchers deriving the uniqueness of Love among the 14 virtues cite this structure as the carrier object on which both sigma-preserving automorphisms and cross-lattice couplings act. The definition is a direct record type whose only constraint is positivity of the lattice size.
Claim. An agent's state consists of a real number $sigma in mathbb{R}$ measuring imbalance, a natural number $n in mathbb{N}$ for lattice size, and the assertion $0 < n$.
background
Sigma is the imbalance charge defined upstream as the gap between private preference and public report: sigma equals +1 when an agent privately prefers stay but publicly votes go, -1 for the reverse, and 0 for truthful reporting. The module distinguishes single-lattice transforms (the 13 sigma-preserving virtues) from cross-lattice couplings (Love), which alone can redistribute imbalance between agents. The local theoretical setting is the DREAM theorem's 14 canonical virtue generators, with the explicit claim that only Love creates bonds between previously separate lattices.
proof idea
Direct structure definition with no proof body. The three fields sigma, lattice_size, and lattice_pos are declared explicitly; the positivity constraint is part of the record syntax and carries no computational content.
why it matters
AgentState supplies the domain type for SingleLatticeTransform and CrossLatticeTransform, which in turn support the downstream theorems automorphism_preserves_sigma and coupling_conserves_total. It fills the basic object role in the derivation that Love is the unique virtue changing individual sigma while conserving total sigma. The construction connects directly to the Recognition Science claim that the 13 other virtues act as lattice automorphisms whereas Love acts as a coupling operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.