sigmaSpread
plain-language theorem explainer
Sigma spread is defined as the sum of squared sigma values across a finite population of agents. Researchers analyzing ethical strategies for sigma reduction in Recognition Science cite it to measure global variance in decision discrepancies. The definition is a direct finite summation that supports later algebraic comparisons of strategy outcomes.
Claim. For a finite population of agents each carrying a real-valued sigma charge $σ_i$, the sigma spread is the sum $∑_i σ_i^2$.
background
In Recognition Science, sigma denotes the numerical gap between an agent's private preference and its public report. A population is a finite collection of agents, each assigned such a real sigma value. The module examines how strategies alter the distribution of these values, with the overarching requirement that the system must drive global sigma toward zero.
proof idea
The definition is a direct one-line summation of the squared sigma entries over the finite index set of agents.
why it matters
This definition supplies the variance measure used by the theorems showing that the love strategy reduces spread by a factor of four and achieves the fastest equilibration. It thereby supports the module's core claim that love is the optimal strategy for driving the population to global sigma equilibrium. The construction aligns with the meta-principle that sigma must reach zero and with the sigma-charge definition from decision analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.