spreadAfter
The function computing post-strategy sigma spread is defined as the sum of squares of the transformed sigma values over the finite population. Researchers analyzing ethical strategies in Recognition Science cite it when comparing how love versus selfish actions affect global equilibrium. It is realized directly as a summation after the strategy's apply map.
claimFor a strategy $s$ and population $p$ with sigma values $p = (n, (0 < n), (i : Fin n)mapsto sigma_i)$, the spread after application is $sum_{i} (s.apply(sigma)(i))^2$.
background
The module treats love as the strategy that minimizes sigma spread under the Recognition Science Meta-Principle requiring global sigma to approach zero. A SigmaPopulation is a finite positive collection of agents each carrying a real-valued sigma. A Strategy is any map that sends a vector of sigmas to another vector of the same length. The upstream love virtue signature supplies the concrete transformation with sigma effect -1, while sibling definitions supply the pre-application spread and the two concrete strategies.
proof idea
This is a definition. It is implemented as the Finset sum over the universe of the squared values obtained by applying the strategy's transformation to the population sigma vector.
why it matters in Recognition Science
The definition supplies the common quantity used by love_minimizes_sigma_spread, which shows the love strategy reduces spread by a factor of four, and by love_is_fastest_equilibration, which shows love is strictly fastest when any sigma is nonzero. It thereby operationalizes the module claim that love is the optimal equilibration drive, linking ethical strategy choice to the global sigma-zero requirement.
scope and limits
- Does not identify which concrete strategy achieves the minimum.
- Does not prove non-negativity or other inequalities.
- Does not extend to infinite or continuous populations.
- Does not compute numerical values for any specific strategy.
Lean usage
rw [spreadAfter] at hformal statement (Lean)
44def spreadAfter (s : Strategy) (pop : SigmaPopulation) : ℝ :=
proof body
Definition body.
45 Finset.sum Finset.univ fun i => (s.apply pop.sigmas i) ^ 2
46
47/-- A love strategy maps all sigmas toward zero uniformly. -/