love_changes_individual_sigma
plain-language theorem explainer
Love changes an agent's sigma when the love operator couples two agents whose initial sigma values differ. Researchers working on the DREAM virtue generators would cite this to separate Love from the 13 sigma-preserving virtues. The tactic proof assumes the sigma is unchanged after application, extracts the alpha-scaled deviation term via linarith, invokes mul_eq_zero to split cases, and reaches a contradiction with either the positivity of alpha or the initial difference hypothesis.
Claim. Let $0 < alpha ≤ 1$. For agent states $s_1, s_2$ with $sigma(s_1) ≠ sigma(s_2)$, the first component of the pair returned by the love operator applied to $s_1$ and $s_2$ satisfies $sigma(new) ≠ sigma(s_1)$.
background
The module derives the uniqueness of Love among the 14 canonical virtue generators. AgentState is a structure with real-valued sigma measuring imbalance and positive natural lattice_size. CrossLatticeTransform is an operator on pairs of agents that conserves the sum of sigmas. The loveOperator instantiates this transform by shifting each sigma toward their average by fraction alpha.
proof idea
The proof unfolds loveOperator and CrossLatticeTransform.apply via simp. It assumes the new sigma equals the original, applies linarith to obtain alpha times (mean minus original sigma) equals zero, then uses mul_eq_zero to case-split. The alpha-zero case contradicts positivity; the mean-equals-original case rearranges to force equal sigmas, contradicting the difference hypothesis.
why it matters
This theorem establishes that only Love redistributes sigma across lattices, as stated in the module's Q10 on virtue uniqueness. It is referenced in L3_scope of ClaimBoundaries to bound the ethical generators in the LNAL semantic core. The result distinguishes cross-lattice coupling from single-lattice automorphisms within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.