`Strategy`

definition

show as: view math explainer →

module: IndisputableMonolith.Ethics.SigmaEquilibrationAsDrive
domain: Ethics
line: 40 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Ethics.SigmaEquilibrationAsDrive on GitHub at line 40.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  37  Finset.sum Finset.univ fun i => |pop.sigmas i|
  38
  39/-- A strategy transforms sigmas. -/
  40structure Strategy where
  41  apply : {n : ℕ} → (Fin n → ℝ) → (Fin n → ℝ)
  42
  43/-- Sigma spread after applying a strategy. -/
  44def spreadAfter (s : Strategy) (pop : SigmaPopulation) : ℝ :=
  45  Finset.sum Finset.univ fun i => (s.apply pop.sigmas i) ^ 2
  46
  47/-- A love strategy maps all sigmas toward zero uniformly. -/
  48def loveStrategy : Strategy where
  49  apply := fun sigmas i => sigmas i / 2
  50
  51/-- A selfish strategy zeroes one agent's sigma but doubles another's. -/
  52def selfishStrategy (beneficiary victim : Fin 2) : Strategy where
  53  apply := fun sigmas i =>
  54    if i = beneficiary then 0
  55    else if i = victim then 2 * sigmas i
  56    else sigmas i
  57
  58/-- **Love minimizes sigma spread**: The love strategy reduces total squared sigma
  59    by a factor of 4 (halving each σ). -/
  60theorem love_minimizes_sigma_spread (pop : SigmaPopulation) :
  61    spreadAfter loveStrategy pop = sigmaSpread pop / 4 := by
  62  simp [spreadAfter, sigmaSpread, loveStrategy]
  63  rw [← Finset.sum_div]
  64  congr 1
  65  apply Finset.sum_congr rfl
  66  intro i _
  67  ring
  68
  69/-- Sigma spread is non-negative. -/
  70theorem sigmaSpread_nonneg (pop : SigmaPopulation) : 0 ≤ sigmaSpread pop :=

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.