IndisputableMonolith.Foundation.DeltaSpine.MassRatioBinding

   1import IndisputableMonolith.Foundation.DeltaSpine.LadderRatioBounds
   2
   3/-!
   4# MassRatioBinding: the muon/electron mass ratio pinned to the φ-ladder (sigma0)
   5
   6**The first empirical bite of the forced-ratio thread: a measured particle-mass
   7ratio bound against φ-ladder rungs by choice-free integer arithmetic alone.**
   8
   9CODATA 2022 gives the muon-electron mass ratio as
  10
  11  `m_μ / m_e = 206.768 2827 (46)`.
  12
  13We take the deliberately generous ±10σ window
  14
  15  `R ∈ [206.7682367, 206.7683287]`,
  16
  17encoded exactly as the integer interval `[muE_lo, muE_hi] / muE_scale` with
  18`muE_scale = 10^7`. Everything proved here is a sigma0 arithmetic fact about
  19those integer endpoints against `phiPow` on ℤ[φ]; the (MEASURED) claim that the
  20physical ratio lies in the window is CODATA's, quoted in
  21`MassRatioBindingReal` (sigma1) as an explicit hypothesis, never as a theorem.
  22
  23Three levels of binding, each a pair of kernel-`decide` facts:
  24
  251. **Window** (`muE_window_*`): `φ¹¹ < R_lo` and `R_hi < φ¹²`. The whole
  26   measured window lies strictly between consecutive ladder rungs 11 and 12.
  27   The RS mass law (`RSBridge.Anchor`) assigns the muon and electron equal
  28   charge index `Z = 1332` and rungs 13 and 2, predicting the pure φ-power
  29   ratio `φ^(13−2) = φ¹¹` — the rung gap this window brackets.
  30
  312. **Nearest rung** (`muE_nearest_rung_*`): `φ²¹ < R_lo²` and `R_hi² < φ²³`,
  32   i.e. `10.5 < log_φ R < 11.5`. Among ALL integers, 11 is the unique nearest
  33   rung gap to the measured ratio: the RS assignment is not merely consistent
  34   with the window, it is forced as the closest ladder point.
  35
  363. **Deviation bracket** (`muE_deviation_*`): with `ε := log_φ R − 11` the
  37   deviation of the measured ratio from the exact rung,
  38   `φ⁶⁹⁸ < R_lo⁶³` and `R_hi⁸⁸ < φ⁹⁷⁵` give the tight rational bracket
  39
  40     `5/63 < ε < 7/88`   (`0.0793651 < ε < 0.0795455`; ε ≈ 0.0795256).
  41
  42   Since `7/88 < 1/(4π)` (equivalent to `π < 22/7`; proved at sigma1), the
  43   bracket REFUTES the naive identification `ε = 1/(4π)` at ≥10σ: the measured
  44   deviation sits strictly below `1/(4π) ≈ 0.0795775`. Any finer closed form
  45   for ε is OPEN; this module claims only the bracket.
  46
  47The mechanism is the sigma0 sign machinery of `DeltaSpine.GoldenInt`
  48(`IsPos`/`RatLt`/`RatGt`): `p/q < φⁿ` reduces to the sign of an element of
  49ℤ[φ], decided by comparing `s²` with `5t²` (√5-irrationality,
  50`int_sq_eq_five_sq`). Integer powers like `muE_lo⁶³` (a 587-digit numerator)
  51reduce in the kernel via GMP-backed `Int` arithmetic. No `Real`, no `Float`,
  52no `native_decide`.
  53
  54**Verdict target: sigma0 DELTA_FORCED** — every theorem here closes within
  55`{propext, Quot.sound}`. Audit with `scripts/sigma_audit.py`.
  56
  57Real-side reading and the link to the RS mass law: `MassRatioBindingReal`
  58(sigma1 CHOICE). Numeric pre-verification:
  59`scripts/_probe_mass_ratio_binding.py`.
  60
  61Delta Forcing Spectrum program: `Delta_Forcing_Spectrum_20260626.tex`.
  62-/
  63
  64namespace IndisputableMonolith
  65namespace Foundation
  66namespace DeltaSpine
  67namespace GoldenInt
  68
  69/- `phiPow 975` unfolds through 975 nested applications; the kernel needs the
  70   recursion-depth headroom (measured: the default 512 fails, 100000 passes
  71   with a wide margin). -/
  72set_option maxRecDepth 100000
  73
  74/-! ## The CODATA 2022 window (exact integer encoding)
  75
  76`m_μ/m_e = 206.7682827(46)`; window = central value ± 10σ, over `10^7`. -/
  77
  78/-- Lower endpoint of the CODATA 2022 ±10σ window: `206.7682367 · 10⁷`. -/
  79def muE_lo : ℤ := 2067682367
  80
  81/-- Upper endpoint of the CODATA 2022 ±10σ window: `206.7683287 · 10⁷`. -/
  82def muE_hi : ℤ := 2067683287
  83
  84/-- Common denominator of the window endpoints: `10⁷`. -/
  85def muE_scale : ℤ := 10000000
  86
  87/-! ## Level 1: the window lies strictly between rungs 11 and 12 -/
  88
  89/-- **Window, lower**: `φ¹¹ < R_lo` — the eleventh rung lies strictly below
  90    the entire measured window (`φ¹¹ ≈ 199.005`). -/
  91theorem muE_window_lower : RatGt muE_lo muE_scale (phiPow 11) := by decide
  92
  93/-- **Window, upper**: `R_hi < φ¹²` — the twelfth rung lies strictly above
  94    the entire measured window (`φ¹² ≈ 321.997`). -/
  95theorem muE_window_upper : RatLt muE_hi muE_scale (phiPow 12) := by decide
  96
  97/-! ## Level 2: 11 is the unique nearest rung (`10.5 < log_φ R < 11.5`) -/
  98
  99/-- **Nearest rung, lower**: `φ²¹ < R_lo²`, i.e. `φ^10.5 < R_lo`. -/
 100theorem muE_nearest_rung_lower :
 101    RatGt (muE_lo ^ 2) (muE_scale ^ 2) (phiPow 21) := by decide
 102
 103/-- **Nearest rung, upper**: `R_hi² < φ²³`, i.e. `R_hi < φ^11.5`. -/
 104theorem muE_nearest_rung_upper :
 105    RatLt (muE_hi ^ 2) (muE_scale ^ 2) (phiPow 23) := by decide
 106
 107/-! ## Level 3: the deviation bracket `5/63 < ε < 7/88`
 108
 109`ε := log_φ R − 11`. The exponents encode `11 + 5/63 = 698/63` and
 110`11 + 7/88 = 975/88`. -/
 111
 112/-- **Deviation, lower**: `φ⁶⁹⁸ < R_lo⁶³`, i.e. `φ^(11 + 5/63) < R_lo`,
 113    hence `ε > 5/63` across the window. -/
 114theorem muE_deviation_lower :
 115    RatGt (muE_lo ^ 63) (muE_scale ^ 63) (phiPow 698) := by decide
 116
 117/-- **Deviation, upper**: `R_hi⁸⁸ < φ⁹⁷⁵`, i.e. `R_hi < φ^(11 + 7/88)`,
 118    hence `ε < 7/88` across the window. -/
 119theorem muE_deviation_upper :
 120    RatLt (muE_hi ^ 88) (muE_scale ^ 88) (phiPow 975) := by decide
 121
 122/-- **Mass-ratio binding, delta-forced (sigma0)**: the full bundle. The CODATA
 123    2022 ±10σ window for `m_μ/m_e` lies strictly inside `(φ¹¹, φ¹²)`, has 11 as
 124    its unique nearest rung gap (`φ²¹ < R² < φ²³`), and its deviation exponent
 125    from the exact rung is bracketed by `5/63 < ε < 7/88`. Every conjunct is a
 126    choice-free integer computation on ℤ[φ], closed by kernel `decide` inside
 127    `{propext, Quot.sound}`. -/
 128theorem mass_ratio_binding :
 129    (RatGt muE_lo muE_scale (phiPow 11) ∧ RatLt muE_hi muE_scale (phiPow 12)) ∧
 130    (RatGt (muE_lo ^ 2) (muE_scale ^ 2) (phiPow 21) ∧
 131     RatLt (muE_hi ^ 2) (muE_scale ^ 2) (phiPow 23)) ∧
 132    (RatGt (muE_lo ^ 63) (muE_scale ^ 63) (phiPow 698) ∧
 133     RatLt (muE_hi ^ 88) (muE_scale ^ 88) (phiPow 975)) :=
 134  ⟨⟨muE_window_lower, muE_window_upper⟩,
 135   ⟨muE_nearest_rung_lower, muE_nearest_rung_upper⟩,
 136   ⟨muE_deviation_lower, muE_deviation_upper⟩⟩
 137
 138/-! ## Runtime certificates (`#eval`)
 139
 140The same decidable predicates evaluated through the compiler, so each bound is
 141confirmed by two independent engines (kernel + runtime). -/
 142
 143/-- info: true -/
 144#guard_msgs in
 145#eval decide (RatGt muE_lo muE_scale (phiPow 11))
 146
 147/-- info: true -/
 148#guard_msgs in
 149#eval decide (RatLt muE_hi muE_scale (phiPow 12))
 150
 151/-- info: true -/
 152#guard_msgs in
 153#eval decide (RatGt (muE_lo ^ 2) (muE_scale ^ 2) (phiPow 21))
 154
 155/-- info: true -/
 156#guard_msgs in
 157#eval decide (RatLt (muE_hi ^ 2) (muE_scale ^ 2) (phiPow 23))
 158
 159/-- info: true -/
 160#guard_msgs in
 161#eval decide (RatGt (muE_lo ^ 63) (muE_scale ^ 63) (phiPow 698))
 162
 163/-- info: true -/
 164#guard_msgs in
 165#eval decide (RatLt (muE_hi ^ 88) (muE_scale ^ 88) (phiPow 975))
 166
 167end GoldenInt
 168end DeltaSpine
 169end Foundation
 170end IndisputableMonolith
 171