SigmaPopulation
plain-language theorem explainer
The structure models a finite population of n agents each carrying a real sigma charge that quantifies the gap between private preference and public report. Researchers analyzing sigma equilibration in Recognition Science cite it when proving properties of love versus selfish strategies. It is introduced as a plain structure definition with three fields: population size, positivity witness, and the assignment function.
Claim. A finite population of $n>0$ agents equipped with an assignment of real numbers $s_i$ ($i=1$ to $n$) representing each agent's sigma charge.
background
In Recognition Science the Meta-Principle requires global sigma to tend to zero. Sigma itself is the real charge measuring the discrepancy between an agent's private preference and its public vote, taking values in {+1, -1, 0} as defined in the Abilene Paradox module. The present structure collects a finite collection of such charges so that global spread (sum of squares) and its reduction under different strategies can be stated precisely. Upstream structures supply the J-cost convexity and 8-tick local dynamics that underwrite the broader claim that sigma minimization is convex and locally realizable.
proof idea
Structure definition with three fields: natural number n, proof that n is positive, and function from Fin n to the reals assigning the sigma values.
why it matters
This definition supplies the data type required by the downstream theorems love_minimizes_sigma_spread and love_is_fastest_equilibration, which establish that the love strategy halves global sigma spread and is strictly fastest when any sigma is nonzero. It thereby fills the concrete data layer for the module claim that love is the unique strategy consistent with the Meta-Principle's demand that global sigma reach zero. The construction sits inside the ethics module whose goal is to derive ethical optimality from the same J-cost and phi-forcing apparatus used in the physics and information modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.