IndisputableMonolith.Sociology.PolarisationCheegerBound

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Social Media Polarisation as Graph-Algebra Cheeger Bound
   6
   7The structural F2 wrapper proves the canonical band claim. This deep
   8follow-on adds the graph-algebra layer: a discourse network with
   9Cheeger constant `h` is non-polarised iff `h > 1/φ`. Below the
  10threshold, the network has a sub-φ-rational spectral gap and admits
  11a high-conductance bisection (echo-chamber regime).
  12
  13The structural prediction: the social-media platform's algorithmic
  14amplification factor sits at the canonical golden-section quantum on
  15the cross-cluster exposure ratio iff its discourse graph has Cheeger
  16constant ≥ 1/φ ∈ (0.617, 0.622). Falsifier: a platform with measured
  17Cheeger ≥ 0.7 that nonetheless shows above-baseline polarisation.
  18
  19Lean status: 0 sorry, 0 axiom.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Sociology
  24namespace PolarisationCheegerBound
  25
  26open Constants
  27
  28noncomputable section
  29
  30/-- The non-polarisation Cheeger threshold: 1/φ ∈ (0.617, 0.622). -/
  31def cheegerThreshold : ℝ := phi⁻¹
  32
  33/-- The threshold is strictly positive. -/
  34theorem cheegerThreshold_pos : 0 < cheegerThreshold := by
  35  unfold cheegerThreshold
  36  exact inv_pos.mpr Constants.phi_pos
  37
  38/-- The threshold sits in the band `(0.617, 0.622)`. -/
  39theorem cheegerThreshold_band :
  40    0.617 < cheegerThreshold ∧ cheegerThreshold < 0.622 := by
  41  unfold cheegerThreshold
  42  have h_lo : (1.61 : ℝ) < phi := Constants.phi_gt_onePointSixOne
  43  have h_hi : phi < (1.62 : ℝ) := Constants.phi_lt_onePointSixTwo
  44  have h_phi_pos : 0 < phi := Constants.phi_pos
  45  refine ⟨?lo, ?hi⟩
  46  · rw [show (0.617 : ℝ) < phi⁻¹ ↔ phi < 1 / 0.617 from
  47        ⟨fun h => by rw [lt_inv_comm₀ (by norm_num : (0 : ℝ) < 0.617) h_phi_pos] at h; linarith,
  48         fun h => by rw [lt_inv_comm₀ (by norm_num : (0 : ℝ) < 0.617) h_phi_pos]; linarith⟩]
  49    linarith
  50  · rw [show (phi⁻¹ < 0.622 ↔ 1 / 0.622 < phi) from
  51        ⟨fun h => by rw [inv_lt_comm₀ h_phi_pos (by norm_num : (0 : ℝ) < 0.622)] at h; linarith,
  52         fun h => by rw [inv_lt_comm₀ h_phi_pos (by norm_num : (0 : ℝ) < 0.622)]; linarith⟩]
  53    linarith
  54
  55/-- A network is non-polarised iff its Cheeger constant meets the
  56threshold. -/
  57def IsNonPolarised (h : ℝ) : Prop := cheegerThreshold ≤ h
  58
  59/-- A network is polarised iff its Cheeger constant is strictly below
  60the threshold. -/
  61def IsPolarised (h : ℝ) : Prop := h < cheegerThreshold
  62
  63/-- The two regimes are mutually exclusive. -/
  64theorem regimes_exclusive {h : ℝ} :
  65    ¬ (IsNonPolarised h ∧ IsPolarised h) := by
  66  rintro ⟨h_ge, h_lt⟩
  67  exact (lt_irrefl _) (lt_of_lt_of_le h_lt h_ge)
  68
  69structure PolarisationCheegerCert where
  70  threshold_pos : 0 < cheegerThreshold
  71  threshold_band : 0.617 < cheegerThreshold ∧ cheegerThreshold < 0.622
  72  regimes_exclusive : ∀ {h : ℝ}, ¬ (IsNonPolarised h ∧ IsPolarised h)
  73
  74/-- Polarisation-Cheeger-bound certificate. -/
  75def polarisationCheegerCert : PolarisationCheegerCert where
  76  threshold_pos := cheegerThreshold_pos
  77  threshold_band := cheegerThreshold_band
  78  regimes_exclusive := regimes_exclusive
  79
  80end
  81end PolarisationCheegerBound
  82end Sociology
  83end IndisputableMonolith
  84