sigmaSpread_nonneg
plain-language theorem explainer
Sigma spread, defined as the sum of squared sigma values over agents in a finite population, is nonnegative. Researchers modeling ethical equilibration strategies under Recognition Science's Meta-Principle cite it to treat spread as a valid nonnegative dispersion measure. The proof is a one-line term that applies Finset.sum_nonneg to the nonnegativity of squares.
Claim. For any finite population of agents with real sigma values $σ_i$, the sum of squares satisfies $∑_i σ_i^2 ≥ 0$.
background
The module develops Love as the strategy that minimizes sigma spread to drive global sigma to zero, per the Meta-Principle. SigmaPopulation is a structure with positive integer n and a map from Fin n to real sigma values. sigmaSpread is the Finset sum of squares of these values, serving as a variance proxy for dispersion across agents.
proof idea
The proof is a one-line term wrapper that applies Finset.sum_nonneg to the map sending each index to the square of the corresponding sigma value, invoking sq_nonneg on each term.
why it matters
This anchors the nonnegative spread measure that the module uses to compare love and selfish strategies. It supplies the elementary nonnegativity step required for claims that love minimizes spread and achieves fastest equilibration. The result is consistent with Recognition Science's global drive toward sigma equilibrium.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.