loveOperator
The Love operator constructs the explicit action of Love as a cross-lattice transform that shifts each agent's sigma toward their pairwise mean by a factor alpha. Ethicists or decision theorists modeling virtue uniqueness would reference this definition to instantiate the coupling that redistributes imbalance between agents. The construction directly encodes the equilibration rule and confirms total sigma conservation through ring arithmetic.
claimLet $0 < alpha ≤ 1$. The Love operator maps a pair of agent states with sigmas $σ_1, σ_2$ to the updated pair where each new sigma equals the original plus $alpha$ times the deviation from the mean: $σ_i' = σ_i + alpha ((σ_1 + σ_2)/2 - σ_i)$. The resulting map preserves the sum of the two sigmas.
background
In this module sigma denotes the charge measuring the gap between an agent's private preference and public vote. A CrossLatticeTransform is a structure that applies a joint update to two AgentState records while enforcing that the total sigma remains unchanged. The module contrasts this with SingleLatticeTransform, which are automorphisms preserving individual sigma. The local setting derives from the DREAM theorem's 14 virtues, isolating Love as the sole operator that couples separate lattices rather than acting within one. Upstream, the alpha constant enters as the weighting parameter, drawn from the fine-structure constant definition.
proof idea
The definition supplies the apply function by computing the mean sigma and adding the proportional adjustment alpha times the difference to each agent. Conservation of total sigma follows immediately from the algebraic identity that the adjustments cancel, verified by the ring tactic after simplification.
why it matters in Recognition Science
This definition supplies the concrete coupling used by the theorems love_changes_individual_sigma and love_equilibrates, which establish that Love alters individual sigmas and reduces their difference. It completes the cross-lattice half of the argument that Love is the unique virtue among the 14 that redistributes sigma between agents, as outlined in the module's Q10 derivation. The construction directly supports the claim that only cross-lattice operations can change individual sigma values.
scope and limits
- Does not prove that Love is the only possible cross-lattice transform.
- Does not derive the value of alpha from first principles within this module.
- Does not address multi-agent extensions beyond pairs.
- Does not connect to the J-cost or phi-ladder structures from the foundation.
formal statement (Lean)
62def loveOperator (alpha : ℝ) (ha : 0 < alpha) (ha1 : alpha ≤ 1) :
63 CrossLatticeTransform where
64 apply := fun s₁ s₂ =>
proof body
Definition body.
65 let mean := (s₁.sigma + s₂.sigma) / 2
66 let s₁' := { s₁ with sigma := s₁.sigma + alpha * (mean - s₁.sigma) }
67 let s₂' := { s₂ with sigma := s₂.sigma + alpha * (mean - s₂.sigma) }
68 (s₁', s₂')
69 conserves_total := by
70 intro s₁ s₂; simp; ring
71
72/-- Love changes individual sigma when agents have different sigma:
73 the new sigma differs from the old. -/