totalAbsSigma
plain-language theorem explainer
totalAbsSigma defines the L1 norm of the sigma vector over a finite population of agents. Researchers comparing equilibration strategies in Recognition Science cite it to quantify total deviation from global σ = 0. The definition is a direct Finset sum of absolute values with no additional lemmas.
Claim. For a population $p$ of $n$ agents with sigma values $σ_i$, the total absolute sigma is $∑_i |σ_i|$.
background
The module examines strategies for driving global sigma to zero under the Meta-Principle. SigmaPopulation is the structure holding a positive integer $n$ and a map from Fin $n$ to real sigma values for each agent. The sibling doc-comment notes that global sigma spread is the sum of squares, proportional to variance.
proof idea
One-line definition that applies Finset.sum over Finset.univ to the absolute value of each pop.sigmas i.
why it matters
Supplies the L1 measure of total sigma used by sibling results such as love_minimizes_sigma_spread and sigmaSpread_nonneg. It operationalizes the global deviation needed to distinguish love (which minimizes spread) from selfish strategies (which increase it) in the ethics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.