Strategy
plain-language theorem explainer
Strategy is the structure type for maps that send any finite collection of real sigmas to another collection of the same length. It is instantiated by loveStrategy and selfishStrategy in the ethics module to model how actions affect global sigma equilibration under the Meta-Principle. The declaration is a direct structure with a single polymorphic apply field and no proof body.
Claim. A strategy is a map $S$ such that for every natural number $n$, $S$ sends any function from the finite set of $n$ elements to the reals to another such function: $S : (n : ℕ) → (Fin n → ℝ) → (Fin n → ℝ)$.
background
In Recognition Science the Meta-Principle requires global sigma to tend to zero. This module studies how different transformations of individual sigma values alter the spread across a population of agents. Sigma spread is the dispersion of these values; love is the transformation that reduces every entry uniformly while selfish transformations reduce one entry at the expense of another.
proof idea
Direct structure definition. The single field apply is declared with the required polymorphic type and no further obligations or lemmas are invoked.
why it matters
The definition supplies the common interface used by loveStrategy, which halves every sigma, and selfishStrategy, which zeros one entry and doubles another. These instances support the module theorems that love minimizes spread and drives the fastest global equilibration, consistent with the Meta-Principle. The same interface appears in downstream results on population tiers and cost representations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.