IndisputableMonolith.Masses.AlphaGScoreCard

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Numerics.Interval.PhiBounds
   4import IndisputableMonolith.Physics.ElectronMass
   5
   6/-!
   7# Gravitational Coupling (Dimensionless) Score Card
   8
   9Phase 0 row **P0-AG** in `planning/PHYSICAL_DERIVATION_PLAN.md`.
  10
  11## Predicted (RS-native, coherence-mass units)
  12
  13\[
  14\alpha_G^{\text{RS}} \;:=\; \frac{G\,m_e^2}{\hbar\,c}
  15\]
  16
  17using the in-framework definitions `Constants.G`, `Constants.hbar`, `Constants.c`, and
  18`Physics.ElectronMass.electron_structural_mass` for `m_e`.
  19
  20In these units, this simplifies to a closed \(\varphi\)-form (Theorem `alphaG_pred_eq`).
  21
  22## Measurement target (CODATA, dimensionless, SI)
  23
  24CODATA: \(\alpha_G \approx 1.7518 \times 10^{-45}\) (electron scale).
  25
  26**Epistemic tag:** this row is a **HYPOTHESIS** bridge alert, not a match claim:
  27the raw RS-native value is \(O(10^9)\) while the SI dimensionless number is
  28\(O(10^{-45})\). The missing piece is the same dimensional bridge that converts
  29coherence-mass reports to kilograms. See
  30`IndisputableMonolith/Foundation/DimensionalBridgeStructural.lean`.
  31
  32Falsifier: if the SI `α_G` and the RS-native `α_G^RS` are identified without an explicit
  33`ExternalCalibration` mass map, the comparison is numerically false.
  34
  35## Lean status: 0 sorry, 0 axiom
  36-/
  37
  38namespace IndisputableMonolith.Masses.AlphaGScoreCard
  39
  40open Constants
  41open Physics.ElectronMass
  42open Physics.ElectronMass.Necessity
  43open IndisputableMonolith.Numerics
  44
  45noncomputable section
  46
  47/-! ## Re-exported row aliases -/
  48
  49noncomputable def row_alphaG_pred : ℝ := G * electron_structural_mass ^ 2 / (hbar * c)
  50
  51theorem row_alphaG_pred_eq : row_alphaG_pred = G * electron_structural_mass ^ 2 / (hbar * c) := rfl
  52
  53/-! ## Helper algebra (native units) -/
  54
  55private theorem c_eq_one' : c = 1 := rfl
  56
  57private theorem hbar_c_eq_hbar : hbar * c = hbar := by
  58  rw [c_eq_one', mul_one]
  59
  60private theorem G_div_hbar : G / hbar = phi ^ (10 : ℝ) / Real.pi := by
  61  have hG : G = 1 / (Real.pi * hbar) := by
  62    unfold G lambda_rec ell0 c
  63    simp
  64  have hh0 : hbar ≠ 0 := ne_of_gt hbar_pos
  65  have h1 : G / hbar = 1 / (Real.pi * hbar ^ 2) := by
  66    rw [hG]
  67    field_simp [Real.pi_ne_zero, hh0]
  68  have h2 : hbar ^ 2 = phi ^ (-(10 : ℝ)) := by
  69    rw [hbar_eq_phi_inv_fifth, pow_two]
  70    have hs : (-(5 : ℝ)) + (-(5 : ℝ)) = -(10 : ℝ) := by ring
  71    rw [← Real.rpow_add phi_pos, hs]
  72  -- `G/ħ = 1/(π·ħ²) = 1/(π·φ^{-10}) = φ^{10}/π`.
  73  rw [h1, h2]
  74  have hphiInv10 : 0 < phi ^ (-(10 : ℝ)) := Real.rpow_pos_of_pos phi_pos (-(10 : ℝ))
  75  have hden : (Real.pi : ℝ) * phi ^ (-(10 : ℝ)) ≠ 0 := by
  76    nlinarith [Real.pi_pos, hphiInv10]
  77  -- `1 = φ^{10} · φ^{-10}`.
  78  have h1over : (1 : ℝ) = phi ^ (10 : ℝ) * phi ^ (-(10 : ℝ)) := by
  79    have h10 : (10 : ℝ) + (-(10 : ℝ)) = 0 := by ring
  80    calc
  81      (1 : ℝ) = phi ^ (0 : ℝ) := (Real.rpow_zero phi).symm
  82      _ = phi ^ ((10 : ℝ) + (-(10 : ℝ))) := by rw [h10]
  83      _ = phi ^ (10 : ℝ) * phi ^ (-(10 : ℝ)) := (Real.rpow_add phi_pos (10 : ℝ) (-(10 : ℝ)))
  84  have hA : (1 : ℝ) / (Real.pi * phi ^ (-(10 : ℝ))) = phi ^ (10 : ℝ) / Real.pi := by
  85    have hπ : Real.pi ≠ 0 := Real.pi_ne_zero
  86    have hφn : phi ^ (-(10 : ℝ)) ≠ 0 := hphiInv10.ne'
  87    field_simp [hden, hπ, hφn, Real.rpow_pos_of_pos phi_pos (10 : ℝ)]
  88    simpa [h1over, mul_assoc, mul_comm, mul_left_comm]
  89  rw [hA]
  90
  91theorem alphaG_pred_eq :
  92    row_alphaG_pred = electron_structural_mass ^ 2 * phi ^ (10 : ℝ) / Real.pi := by
  93  have hc : hbar * c = hbar := hbar_c_eq_hbar
  94  rw [row_alphaG_pred, hc]
  95  have h1 : G * electron_structural_mass ^ 2 / hbar
  96        = (G / hbar) * electron_structural_mass ^ 2 := by
  97    have hh : hbar ≠ 0 := ne_of_gt hbar_pos
  98    field_simp [hh]
  99  rw [h1, G_div_hbar]
 100  ring
 101
 102theorem alphaG_pred_closed :
 103    row_alphaG_pred = ((2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ)) / Real.pi := by
 104  have hme : electron_structural_mass = (2 : ℝ) ^ (-(22 : ℤ)) * phi ^ (51 : ℤ) := electron_structural_mass_forced
 105  have h2n : (2 : ℝ) ≠ 0 := by norm_num
 106  have hA2 : ((2 : ℝ) ^ (-(22 : ℤ))) ^ 2 = (2 : ℝ) ^ (-(44 : ℤ)) := by
 107    rw [pow_two, ← zpow_add₀ h2n]
 108    norm_num
 109  have h0 : (phi : ℝ) ≠ 0 := phi_ne_zero
 110  have hBz : (phi : ℝ) ^ (51 : ℤ) * (phi : ℝ) ^ (51 : ℤ) = (phi : ℝ) ^ (102 : ℤ) := by
 111    rw [← zpow_add₀ h0]
 112    norm_num
 113  have hφsq : ((phi : ℝ) ^ (51 : ℤ)) ^ 2 = (phi : ℝ) ^ (102 : ℤ) := by
 114    rw [pow_two]
 115    exact hBz
 116  have hsq : (electron_structural_mass) ^ 2 = (2 : ℝ) ^ (-(44 : ℤ)) * (phi : ℝ) ^ (102 : ℝ) := by
 117    rw [hme, pow_two]
 118    have hre :
 119        ((2 : ℝ) ^ (-(22 : ℤ)) * phi ^ (51 : ℤ)) * ((2 : ℝ) ^ (-(22 : ℤ)) * phi ^ (51 : ℤ))
 120          = ((2 : ℝ) ^ (-(22 : ℤ))) ^ 2 * ((phi : ℝ) ^ (51 : ℤ)) ^ 2 := by
 121      ring
 122    rw [hre, hA2, hφsq]
 123    have hΦ : (phi : ℝ) ^ (102 : ℤ) = (phi : ℝ) ^ (102 : ℝ) := by
 124      -- integer `zpow` and real `rpow` with an `Int` exponent agree on `ℝ`.
 125      simp [zpow_ofNat, phi]
 126    rw [hΦ]
 127  have h112 : (102 : ℝ) + (10 : ℝ) = (112 : ℝ) := by norm_cast
 128  have hφ112 : (phi : ℝ) ^ (102 : ℝ) * (phi : ℝ) ^ (10 : ℝ) = (phi : ℝ) ^ (112 : ℝ) := by
 129    rw [← Real.rpow_add phi_pos, h112]
 130  have hc : hbar * c = hbar := hbar_c_eq_hbar
 131  have h2pos : (0 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) := by
 132    simpa [zpow_pos (by norm_num : (0 : ℝ) < (2 : ℝ))]
 133  rw [row_alphaG_pred, hc, hsq]
 134  have hsplit :
 135      G * ((2 : ℝ) ^ (-(44 : ℤ)) * (phi : ℝ) ^ (102 : ℝ)) / hbar
 136        = (G / hbar) * ((2 : ℝ) ^ (-(44 : ℤ)) * (phi : ℝ) ^ (102 : ℝ)) := by
 137    have hh : hbar ≠ 0 := ne_of_gt hbar_pos
 138    field_simp [hh]
 139  rw [hsplit, G_div_hbar]
 140  have hmerge : phi ^ (10 : ℝ) * phi ^ (102 : ℝ) = phi ^ (112 : ℝ) := by
 141    simpa [mul_comm] using hφ112
 142  field_simp [Real.pi_ne_zero, h0, Real.rpow_pos_of_pos phi_pos, h2pos, Real.rpow_pos_of_pos phi_pos (102 : ℝ),
 143    Real.rpow_pos_of_pos phi_pos (10 : ℝ), Real.rpow_pos_of_pos phi_pos (112 : ℝ)]
 144  -- After clearing `π`, identify `φ^{10}·φ^{102} = φ^{112}`.
 145  exact hmerge
 146
 147/-! ## Bracket: single-φ function (avoids a fake independence assumption) -/
 148
 149theorem alphaG_pred_lower : (4.5e9 : ℝ) < row_alphaG_pred := by
 150  have hφ : (1.618 : ℝ) < phi := by
 151    simpa [show phi = (Real.goldenRatio : ℝ) from rfl] using phi_gt_1618
 152  have hpiUB : (Real.pi : ℝ) < 3.142 := by
 153    linarith [Real.pi_lt_d6, Real.pi_pos]
 154  have hN :
 155      (2 : ℝ) ^ (-(44 : ℤ)) * (1.618 : ℝ) ^ (112 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) := by
 156    have hr112 : (1.618 : ℝ) ^ (112 : ℝ) < phi ^ (112 : ℝ) := by
 157      exact Real.rpow_lt_rpow (by norm_num) hφ (by nlinarith)
 158    nlinarith [hr112, zpow_pos (by norm_num : (0 : ℝ) < (2 : ℝ))]
 159  have h0 : (4.5e9 : ℝ) * (3.142 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * (1.618 : ℝ) ^ (112 : ℝ) := by
 160    -- conservative numeric bound (independent of the model)
 161    nlinarith
 162  have hltNum : (4.5e9 : ℝ) * Real.pi < (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) := by
 163    nlinarith [h0, hN, hpiUB, Real.pi_pos]
 164  have h1 : (4.5e9 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) / Real.pi := by
 165    rw [lt_div_iff₀ Real.pi_pos]
 166    simpa [mul_assoc, mul_left_comm, mul_comm] using hltNum
 167  simpa [alphaG_pred_closed] using h1
 168
 169theorem alphaG_pred_upper : row_alphaG_pred < (4.85e9 : ℝ) := by
 170  have hφ : phi < (1.6185 : ℝ) := by
 171    simpa [show phi = (Real.goldenRatio : ℝ) from rfl] using phi_lt_16185
 172  have hpiLB : (3.1415 : ℝ) < (Real.pi : ℝ) := by
 173    linarith [Real.pi_gt_d6, Real.pi_pos]
 174  have hN : (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) < (2 : ℝ) ^ (-(44 : ℤ)) * (1.6185 : ℝ) ^ (112 : ℝ) := by
 175    have hr112 : (phi : ℝ) ^ (112 : ℝ) < (1.6185 : ℝ) ^ (112 : ℝ) := by
 176      exact Real.rpow_lt_rpow (by nlinarith [phi_pos, hφ]) hφ (by nlinarith)
 177    nlinarith [hr112, zpow_pos (by norm_num : (0 : ℝ) < (2 : ℝ))]
 178  have h0 :
 179      (2 : ℝ) ^ (-(44 : ℤ)) * (1.6185 : ℝ) ^ (112 : ℝ) < (4.85e9 : ℝ) * (3.1415 : ℝ) := by
 180    nlinarith
 181  have h1 : (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) / Real.pi < (4.85e9 : ℝ) := by
 182    have hltNum : (2 : ℝ) ^ (-(44 : ℤ)) * phi ^ (112 : ℝ) < (4.85e9 : ℝ) * Real.pi := by
 183      nlinarith [h0, hN, hpiLB, Real.pi_pos]
 184    rw [div_lt_iff₀ Real.pi_pos]
 185    simpa [mul_assoc, mul_left_comm, mul_comm] using hltNum
 186  simpa [alphaG_pred_closed] using h1
 187
 188theorem alphaG_pred_bracket : (4.5e9 : ℝ) < row_alphaG_pred ∧ row_alphaG_pred < (4.85e9 : ℝ) :=
 189  ⟨alphaG_pred_lower, alphaG_pred_upper⟩
 190
 191/-! ## CODATA reference (SI units, dimensionless) -/
 192
 193def alphaG_codata : ℝ := 1.7518e-45
 194
 195theorem codata_very_small : alphaG_codata < 1e-40 := by
 196  unfold alphaG_codata; norm_num
 197
 198theorem native_very_not_codata : alphaG_codata < row_alphaG_pred := by
 199  have h1 := alphaG_pred_lower
 200  have h0 : alphaG_codata < (1e9 : ℝ) := by
 201    unfold alphaG_codata; norm_num
 202  linarith [h0, h1]
 203
 204/-!
 205## Falsifier (one line)
 206
 207A CODATA-consistent dimensionless `α_G` in SI and the RS-native
 208`G m_e^2 / (ℏ c)` written with `electron_structural_mass` cannot be the same
 209real number: matching experiment requires the explicit SI mass bridge, not
 210identification of the raw coherence-mass value with the kilogram number.
 211-/
 212
 213structure AlphaGScoreCardCert where
 214  native_bracket : (4.5e9 : ℝ) < row_alphaG_pred ∧ row_alphaG_pred < (4.85e9 : ℝ)
 215  not_codata : alphaG_codata < row_alphaG_pred
 216
 217def cert : AlphaGScoreCardCert where
 218  native_bracket := alphaG_pred_bracket
 219  not_codata := native_very_not_codata
 220
 221theorem cert_inhabited : Nonempty AlphaGScoreCardCert := ⟨cert⟩
 222
 223end
 224
 225end IndisputableMonolith.Masses.AlphaGScoreCard
 226