IndisputableMonolith.Foundation.DeltaSpine.MassRatioBindingReal

   1import Mathlib
   2import IndisputableMonolith.Foundation.DeltaSpine.MassRatioBinding
   3import IndisputableMonolith.Foundation.DeltaSpine.GoldenIntReal
   4import IndisputableMonolith.RSBridge.Anchor
   5
   6/-!
   7# Mass Ratio Binding: σ1 Real Display (muon/electron ↔ rung 11)
   8
   9**Forcing tier: σ1 (CHOICE).** This module is the *display layer* for
  10`MassRatioBinding.lean` (the σ0 kernel-decided facts). Everything here is a
  11real-number reading of certificates the kernel already verified by `decide`
  12on ℤ[φ]; the only new mathematical content is:
  13
  14* the interpretation map `toReal : ℤ[φ] → ℝ` (noncomputable, σ1), and
  15* the RS model linkage via `RSBridge.anchor_ratio`.
  16
  17## What is proved
  18
  19Let `R` be any real number in the CODATA-2022 ±10σ window for the
  20muon/electron mass ratio (`muEWindow R`, i.e. `R ∈ [206.7682367, 206.7683287]`).
  21Then, writing `φ` for the golden ratio and `L := log_φ R`:
  22
  231. `muE_window_between_rungs`: `φ^11 < R < φ^12` — the measured ratio sits
  24   strictly between two adjacent φ-rungs.
  252. `muE_logb_window`: `11 < L < 12`.
  263. `muE_logb_halfstep`: `21/2 < L < 23/2` — `R²` lies between `φ^21` and
  27   `φ^23`, so `L` is within a half-step of 11.
  284. `muE_nearest_rung_unique`: rung 11 is the **unique nearest integer rung**:
  29   for every integer `n ≠ 11`, `|L - 11| < |L - n|`.
  305. `muE_epsilon_bracket`: the deviation `ε := L - 11` satisfies
  31   `5/63 < ε < 7/88` (i.e. `0.0794 < ε < 0.0795…`), a kernel-certified
  32   two-sided bracket ~0.2% wide.
  336. `epsilon_upper_lt_inv_four_pi`: `7/88 < 1/(4π)`, hence
  34   `muE_deviation_refutes_inv4pi`: `ε < 1/(4π)` — the measured deviation is
  35   strictly below the `1/(4π)` curvature-scale candidate, refuting
  36   `ε = 1/(4π)` (≈ 0.0796) as an exact identification.
  377. `muE_anchor_prediction`: the RS anchor model itself predicts
  38   `m_μ/m_e = φ^11` at the anchor scale: electron and muon share
  39   `Z = 1332`, so `anchor_ratio` collapses to the pure rung gap
  40   `rung μ − rung e = 13 − 2 = 11`.
  418. `muE_rung_gap_certified`: the capstone bundle — the model's φ^11
  42   prediction and the measured window's bracket `(φ^11, φ^12)`, nearest-rung
  43   uniqueness, and the ε bracket, all in one statement.
  44
  45## Honest status
  46
  47* The six inequalities on `R` are THEOREMs conditional only on the MEASURED
  48  hypothesis `muEWindow R` (CODATA 2022, ±10σ). The kernel arithmetic behind
  49  them is σ0 (`MassRatioBinding.lean`).
  50* `muE_anchor_prediction` is a THEOREM about the RS **model** `massAtAnchor`
  51  (rung assignments are definitional inputs; see `RSBridge/Anchor.lean`).
  52* The *identification* of the measured ratio with the model's anchor ratio
  53  (i.e. that physical masses at the anchor scale realize `massAtAnchor`) is
  54  the standing RS phenomenology claim, NOT proved here. What IS proved: the
  55  model says φ^11 exactly, the measurement says φ^11 · φ^ε with
  56  ε ∈ (5/63, 7/88), and ε < 1/(4π). The residual ε is the open QED-dressing
  57  seam, stated honestly as a bracket.
  58-/
  59
  60namespace IndisputableMonolith
  61namespace Foundation
  62namespace DeltaSpine
  63
  64open GoldenInt
  65
  66/-- The CODATA-2022 ±10σ window for the muon/electron mass ratio, as a
  67    predicate on a real number `R`. Numerically `[206.7682367, 206.7683287]`
  68    (central value 206.7682827, σ = 4.6e-6). MEASURED hypothesis. -/
  69def muEWindow (R : ℝ) : Prop :=
  70  (muE_lo : ℝ) / (muE_scale : ℝ) ≤ R ∧ R ≤ (muE_hi : ℝ) / (muE_scale : ℝ)
  71
  72private lemma muE_scale_pos : (0 : ℤ) < muE_scale := by norm_num [muE_scale]
  73
  74private lemma muE_lo_div_pos : (0 : ℝ) < (muE_lo : ℝ) / (muE_scale : ℝ) := by
  75  norm_num [muE_lo, muE_scale]
  76
  77/-- Any ratio in the window is positive. -/
  78theorem muEWindow_pos {R : ℝ} (hR : muEWindow R) : 0 < R :=
  79  lt_of_lt_of_le muE_lo_div_pos hR.1
  80
  81/-! ## Level 1: the window sits strictly between rungs 11 and 12 -/
  82
  83/-- σ1 reading of the σ0 window certificates: `φ^11 < R < φ^12`. -/
  84theorem muE_window_between_rungs {R : ℝ} (hR : muEWindow R) :
  85    PhiForcing.φ ^ (11 : ℕ) < R ∧ R < PhiForcing.φ ^ (12 : ℕ) := by
  86  obtain ⟨hlo, hhi⟩ := hR
  87  have h1 := ratGt_toReal muE_scale_pos muE_window_lower
  88  have h2 := ratLt_toReal muE_scale_pos muE_window_upper
  89  rw [toReal_phiPow] at h1 h2
  90  exact ⟨lt_of_lt_of_le h1 hlo, lt_of_le_of_lt hhi h2⟩
  91
  92/-! ## Level 2: half-step bracket via `R²` -/
  93
  94/-- σ1 reading of the σ0 square certificates: `φ^21 < R² < φ^23`. -/
  95theorem muE_sq_between {R : ℝ} (hR : muEWindow R) :
  96    PhiForcing.φ ^ (21 : ℕ) < R ^ 2 ∧ R ^ 2 < PhiForcing.φ ^ (23 : ℕ) := by
  97  obtain ⟨hlo, hhi⟩ := hR
  98  have hRpos := muEWindow_pos ⟨hlo, hhi⟩
  99  constructor
 100  · have h1 := ratGt_toReal (pow_pos muE_scale_pos 2) muE_nearest_rung_lower
 101    rw [toReal_phiPow] at h1
 102    push_cast at h1
 103    have hsq : ((muE_lo : ℝ) / (muE_scale : ℝ)) ^ 2 ≤ R ^ 2 :=
 104      pow_le_pow_left₀ (le_of_lt muE_lo_div_pos) hlo 2
 105    rw [div_pow] at hsq
 106    exact lt_of_lt_of_le h1 hsq
 107  · have h2 := ratLt_toReal (pow_pos muE_scale_pos 2) muE_nearest_rung_upper
 108    rw [toReal_phiPow] at h2
 109    push_cast at h2
 110    have hsq : R ^ 2 ≤ ((muE_hi : ℝ) / (muE_scale : ℝ)) ^ 2 :=
 111      pow_le_pow_left₀ (le_of_lt hRpos) hhi 2
 112    rw [div_pow] at hsq
 113    exact lt_of_le_of_lt hsq h2
 114
 115/-! ## Level 3: tight deviation bracket via `R^63` and `R^88` -/
 116
 117/-- σ1 reading of the σ0 deviation certificates: `φ^698 < R^63`. -/
 118theorem muE_pow63_gt {R : ℝ} (hR : muEWindow R) :
 119    PhiForcing.φ ^ (698 : ℕ) < R ^ 63 := by
 120  obtain ⟨hlo, _⟩ := hR
 121  have h1 := ratGt_toReal (pow_pos muE_scale_pos 63) muE_deviation_lower
 122  rw [toReal_phiPow] at h1
 123  push_cast at h1
 124  have hp : ((muE_lo : ℝ) / (muE_scale : ℝ)) ^ 63 ≤ R ^ 63 :=
 125    pow_le_pow_left₀ (le_of_lt muE_lo_div_pos) hlo 63
 126  rw [div_pow] at hp
 127  exact lt_of_lt_of_le h1 hp
 128
 129/-- σ1 reading of the σ0 deviation certificates: `R^88 < φ^975`. -/
 130theorem muE_pow88_lt {R : ℝ} (hR : muEWindow R) :
 131    R ^ 88 < PhiForcing.φ ^ (975 : ℕ) := by
 132  have hRpos := muEWindow_pos hR
 133  obtain ⟨_, hhi⟩ := hR
 134  have h2 := ratLt_toReal (pow_pos muE_scale_pos 88) muE_deviation_upper
 135  rw [toReal_phiPow] at h2
 136  push_cast at h2
 137  have hp : R ^ 88 ≤ ((muE_hi : ℝ) / (muE_scale : ℝ)) ^ 88 :=
 138    pow_le_pow_left₀ (le_of_lt hRpos) hhi 88
 139  rw [div_pow] at hp
 140  exact lt_of_le_of_lt hp h2
 141
 142/-! ## Logarithmic display: `L = log_φ R` -/
 143
 144private lemma logb_lift_lower {R : ℝ} {a k : ℕ}
 145    (h : PhiForcing.φ ^ a < R ^ k) :
 146    (a : ℝ) < (k : ℝ) * Real.logb PhiForcing.φ R := by
 147  have hb : (1 : ℝ) < PhiForcing.φ := PhiForcing.phi_gt_one
 148  have hx : (0 : ℝ) < PhiForcing.φ ^ a := pow_pos PhiForcing.phi_pos a
 149  have hlt := Real.logb_lt_logb hb hx h
 150  rw [Real.logb_pow, Real.logb_pow, Real.logb_self_eq_one hb, mul_one] at hlt
 151  exact hlt
 152
 153private lemma logb_lift_upper {R : ℝ} (hR : 0 < R) {a k : ℕ}
 154    (h : R ^ k < PhiForcing.φ ^ a) :
 155    (k : ℝ) * Real.logb PhiForcing.φ R < (a : ℝ) := by
 156  have hb : (1 : ℝ) < PhiForcing.φ := PhiForcing.phi_gt_one
 157  have hx : (0 : ℝ) < R ^ k := pow_pos hR k
 158  have hlt := Real.logb_lt_logb hb hx h
 159  rw [Real.logb_pow, Real.logb_pow, Real.logb_self_eq_one hb, mul_one] at hlt
 160  exact hlt
 161
 162/-- `11 < log_φ R < 12`: the measured ratio's φ-logarithm sits strictly
 163    between the adjacent integer rungs. -/
 164theorem muE_logb_window {R : ℝ} (hR : muEWindow R) :
 165    (11 : ℝ) < Real.logb PhiForcing.φ R ∧ Real.logb PhiForcing.φ R < 12 := by
 166  have hRpos := muEWindow_pos hR
 167  obtain ⟨h1, h2⟩ := muE_window_between_rungs hR
 168  have hl : (11 : ℝ) < 1 * Real.logb PhiForcing.φ R := by
 169    exact_mod_cast logb_lift_lower (k := 1) (by simpa using h1)
 170  have hu : (1 : ℝ) * Real.logb PhiForcing.φ R < 12 := by
 171    exact_mod_cast logb_lift_upper hRpos (k := 1) (by simpa using h2)
 172  constructor <;> linarith
 173
 174/-- `21/2 < log_φ R < 23/2`: the φ-logarithm is within a half-step of 11,
 175    so 11 is a nearest integer rung. -/
 176theorem muE_logb_halfstep {R : ℝ} (hR : muEWindow R) :
 177    (21 : ℝ) / 2 < Real.logb PhiForcing.φ R ∧
 178    Real.logb PhiForcing.φ R < (23 : ℝ) / 2 := by
 179  have hRpos := muEWindow_pos hR
 180  obtain ⟨h1, h2⟩ := muE_sq_between hR
 181  have hl : (21 : ℝ) < 2 * Real.logb PhiForcing.φ R := by
 182    exact_mod_cast logb_lift_lower (k := 2) h1
 183  have hu : (2 : ℝ) * Real.logb PhiForcing.φ R < 23 := by
 184    exact_mod_cast logb_lift_upper hRpos (k := 2) h2
 185  constructor <;> linarith
 186
 187/-- Rung 11 is the **unique nearest integer rung** to `log_φ R`:
 188    every other integer is strictly farther away. -/
 189theorem muE_nearest_rung_unique {R : ℝ} (hR : muEWindow R) :
 190    ∀ n : ℤ, n ≠ 11 →
 191      |Real.logb PhiForcing.φ R - 11| < |Real.logb PhiForcing.φ R - (n : ℝ)| := by
 192  intro n hn
 193  set L := Real.logb PhiForcing.φ R with hLdef
 194  obtain ⟨h1, h2⟩ := muE_logb_halfstep hR
 195  have habs : |L - 11| < 1 / 2 := by
 196    rw [abs_lt]; constructor <;> linarith
 197  have hn1 : (1 : ℝ) ≤ |(n : ℝ) - 11| := by
 198    have h : (1 : ℤ) ≤ |n - 11| := Int.one_le_abs (sub_ne_zero.mpr hn)
 199    exact_mod_cast h
 200  have htri : |(n : ℝ) - 11| ≤ |(n : ℝ) - L| + |L - 11| := abs_sub_le _ L _
 201  have hcomm : |L - (n : ℝ)| = |(n : ℝ) - L| := abs_sub_comm L _
 202  rw [hcomm]
 203  linarith
 204
 205/-- The kernel-certified two-sided deviation bracket:
 206    `5/63 < log_φ R − 11 < 7/88` (≈ `0.07937 < ε < 0.07955`). -/
 207theorem muE_epsilon_bracket {R : ℝ} (hR : muEWindow R) :
 208    (5 : ℝ) / 63 < Real.logb PhiForcing.φ R - 11 ∧
 209    Real.logb PhiForcing.φ R - 11 < (7 : ℝ) / 88 := by
 210  have hRpos := muEWindow_pos hR
 211  have hl : (698 : ℝ) < 63 * Real.logb PhiForcing.φ R := by
 212    exact_mod_cast logb_lift_lower (k := 63) (muE_pow63_gt hR)
 213  have hu : (88 : ℝ) * Real.logb PhiForcing.φ R < 975 := by
 214    exact_mod_cast logb_lift_upper hRpos (k := 88) (muE_pow88_lt hR)
 215  constructor
 216  · linarith
 217  · linarith
 218
 219/-! ## Refuting ε = 1/(4π) -/
 220
 221/-- `7/88 < 1/(4π)`: the certified upper bound on the deviation is strictly
 222    below the `1/(4π)` candidate (uses `π < 3.1416`, Mathlib `pi_lt_d4`). -/
 223theorem epsilon_upper_lt_inv_four_pi : (7 : ℝ) / 88 < 1 / (4 * Real.pi) := by
 224  have hpi : Real.pi < 3.1416 := Real.pi_lt_d4
 225  have hpipos : (0 : ℝ) < Real.pi := Real.pi_pos
 226  rw [div_lt_div_iff₀ (by norm_num) (by positivity)]
 227  nlinarith
 228
 229/-- The measured deviation is strictly below `1/(4π)`: the exact
 230    identification `ε = 1/(4π)` is refuted by the CODATA window. -/
 231theorem muE_deviation_refutes_inv4pi {R : ℝ} (hR : muEWindow R) :
 232    Real.logb PhiForcing.φ R - 11 < 1 / (4 * Real.pi) :=
 233  lt_trans (muE_epsilon_bracket hR).2 epsilon_upper_lt_inv_four_pi
 234
 235/-! ## RS model linkage: the anchor model predicts exactly φ^11 -/
 236
 237/-- Electron and muon carry the same charge-index `Z = 1332`. -/
 238theorem muE_equal_Z : RSBridge.ZOf RSBridge.Fermion.mu = RSBridge.ZOf RSBridge.Fermion.e := rfl
 239
 240/-- The RS anchor model's prediction: `m_μ/m_e = φ^11` exactly at the anchor
 241    scale. Same-Z species cancel the gap term, leaving the pure rung gap
 242    `rung μ − rung e = 13 − 2 = 11`. -/
 243theorem muE_anchor_prediction :
 244    RSBridge.massAtAnchor RSBridge.Fermion.mu / RSBridge.massAtAnchor RSBridge.Fermion.e
 245      = PhiForcing.φ ^ (11 : ℕ) := by
 246  rw [RSBridge.anchor_ratio _ _ muE_equal_Z]
 247  have hrung : ((RSBridge.rung RSBridge.Fermion.mu : ℝ) - (RSBridge.rung RSBridge.Fermion.e : ℝ))
 248      = ((11 : ℕ) : ℝ) := by
 249    norm_num [RSBridge.rung]
 250  rw [hrung, Real.exp_nat_mul,
 251      show Constants.phi = PhiForcing.φ from rfl,
 252      Real.exp_log PhiForcing.phi_pos]
 253
 254/-! ## Capstone -/
 255
 256/-- **Capstone (σ1 display).** For any `R` in the CODATA ±10σ window for
 257    `m_μ/m_e`:
 258
 259    * the RS anchor model predicts the ratio is exactly `φ^11`;
 260    * the measured window sits strictly inside `(φ^11, φ^12)`;
 261    * 11 is the unique nearest integer rung to `log_φ R`;
 262    * the deviation `ε = log_φ R − 11` is bracketed in `(5/63, 7/88)`;
 263    * `ε < 1/(4π)` (the curvature-candidate identification is refuted).
 264
 265    Kernel content is σ0 (`MassRatioBinding.lean`); this statement is its
 266    σ1 real-number reading plus the model linkage. -/
 267theorem muE_rung_gap_certified {R : ℝ} (hR : muEWindow R) :
 268    (RSBridge.massAtAnchor RSBridge.Fermion.mu / RSBridge.massAtAnchor RSBridge.Fermion.e
 269        = PhiForcing.φ ^ (11 : ℕ))
 270    ∧ (PhiForcing.φ ^ (11 : ℕ) < R ∧ R < PhiForcing.φ ^ (12 : ℕ))
 271    ∧ (∀ n : ℤ, n ≠ 11 →
 272        |Real.logb PhiForcing.φ R - 11| < |Real.logb PhiForcing.φ R - (n : ℝ)|)
 273    ∧ ((5 : ℝ) / 63 < Real.logb PhiForcing.φ R - 11 ∧
 274        Real.logb PhiForcing.φ R - 11 < (7 : ℝ) / 88)
 275    ∧ Real.logb PhiForcing.φ R - 11 < 1 / (4 * Real.pi) :=
 276  ⟨muE_anchor_prediction,
 277   muE_window_between_rungs hR,
 278   muE_nearest_rung_unique hR,
 279   muE_epsilon_bracket hR,
 280   muE_deviation_refutes_inv4pi hR⟩
 281
 282end DeltaSpine
 283end Foundation
 284end IndisputableMonolith
 285