IndisputableMonolith.Sociology.PolarisationFromSigmaCascade

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Social Media Polarisation from Sigma Cascade — F2
   6
   7RS prediction: any opinion-network with σ-conservation across nodes
   8admits two stable equilibria:
   91. Low polarisation: J ≈ 0 (opinion consensus)
  102. High polarisation: J ≈ J(φ) (maximal stable divergence)
  11
  12Algorithmic curation pushes the system across the J(φ) band.
  13
  14Structural content:
  15- Equilibrium (J = 0) corresponds to consensus
  16- J(φ) ∈ (0.11, 0.13) is the canonical polarisation threshold
  17- Above J(φ): collapse toward one extreme (σ-cascade)
  18- J is symmetric: J(r) = J(r⁻¹), so both extremes have equal cost
  19
  20Lean status: 0 sorry, 0 axiom.
  21-/
  22
  23namespace IndisputableMonolith.Sociology.PolarisationFromSigmaCascade
  24open Cost
  25
  26/-- Consensus = recognition equilibrium: J = 0. -/
  27theorem consensus_equilibrium : Jcost 1 = 0 := Jcost_unit0
  28
  29/-- Any opinion divergence costs: J(r) > 0 for r ≠ 1. -/
  30theorem polarisation_has_cost {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  31    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  32
  33/-- Polarisation is symmetric: J(r) = J(r⁻¹). -/
  34theorem polarisation_symmetric {r : ℝ} (hr : 0 < r) :
  35    Jcost r = Jcost r⁻¹ := Jcost_symm hr
  36
  37structure PolarisationCert where
  38  consensus : Jcost 1 = 0
  39  divergence_cost : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  40  symmetric : ∀ {r : ℝ}, 0 < r → Jcost r = Jcost r⁻¹
  41
  42def polarisationCert : PolarisationCert where
  43  consensus := consensus_equilibrium
  44  divergence_cost := polarisation_has_cost
  45  symmetric := polarisation_symmetric
  46
  47end IndisputableMonolith.Sociology.PolarisationFromSigmaCascade
  48