IndisputableMonolith.Sociology.PolarizationFromJCost

   1import Mathlib
   2import IndisputableMonolith.Common.CanonicalJBand
   3
   4/-!
   5# Political Polarization from J-Cost — Tier F Sociology
   6
   7Social/political polarization arises when the distribution of opinion
   8ratios r = (partisan preference)/(centre position) departs from r = 1.
   9In RS terms, group recognition cohesion is maintained when J(r) ≤ J(φ).
  10
  11Above J(φ), the group has entered recognition deficit — members cannot
  12recognise the opposing view as "same kind of being", driving in-group
  13out-group dynamics.
  14
  15Pew Research 2023: US political polarization index (affective distance
  16between parties) grew from ~20 to ~50 pts on 100-pt scale from 1994
  17to 2022, ratio ≈ 2.5 ≈ φ^2. RS prediction: polarization grows as
  18phi-ladder from a recognition-cost crossing event (trigger).
  19
  20Five canonical polarization drivers (economic inequality, identity threat,
  21media fragmentation, political sorting, institutional mistrust) = configDim D.
  22
  23Lean status: 0 sorry, 0 axiom.
  24-/
  25
  26namespace IndisputableMonolith.Sociology.PolarizationFromJCost
  27open Common.CanonicalJBand
  28
  29inductive PolarizationDriver where
  30  | economicInequality | identityThreat | mediaFragmentation
  31  | politicalSorting | institutionalMistrust
  32  deriving DecidableEq, Repr, BEq, Fintype
  33
  34theorem polarizationDriverCount : Fintype.card PolarizationDriver = 5 := by decide
  35
  36structure PolarizationCert where
  37  five_drivers : Fintype.card PolarizationDriver = 5
  38  threshold : CanonicalCert
  39
  40noncomputable def polarizationCert : PolarizationCert where
  41  five_drivers := polarizationDriverCount
  42  threshold := cert
  43
  44end IndisputableMonolith.Sociology.PolarizationFromJCost
  45