IndisputableMonolith.Constants.AlphaGenesis.MeasurementVerdict

   1import Mathlib
   2import IndisputableMonolith.Constants.AlphaGenesis.LoopCertificate
   3import IndisputableMonolith.Constants.AlphaGenesis.ResidualTarget
   4import IndisputableMonolith.Constants.ExternalAnchors
   5import IndisputableMonolith.Numerics.Interval.AlphaBounds
   6import IndisputableMonolith.Numerics.Interval.W8Bounds
   7
   8/-!
   9# Alpha Genesis M7: Measurement Verdict (quarantine module)
  10
  11This module formalizes Anil Thapa's strongest measurement-side objection.
  12It is quarantined: it imports CODATA through `ExternalAnchors`, and nothing in
  13the forward Alpha Genesis construction imports this module.
  14
  15The theorem proved here is intentionally coarse but decisive:
  16
  17`alphaInvGenesis > alpha_inv_CODATA + 0.0007`.
  18
  19Since CODATA's one-sigma uncertainty for `α⁻¹` is `2.1e-8`, this also implies
  20the first-order Alpha Genesis value is more than `30000σ` high. The exact
  21reported residual is about `7.67e-4`; the certified margin here is the stronger
  22honest fact needed for the reply: the current first-order value is excluded by
  23measurement before any seam correction is derived.
  24
  25STATUS: THEOREM for the comparison; QUARANTINE because it imports CODATA.
  26-/
  27
  28namespace IndisputableMonolith
  29namespace Constants
  30namespace AlphaGenesis
  31namespace MeasurementVerdict
  32
  33noncomputable section
  34
  35open Constants.ExternalAnchors
  36
  37/-! ## Tight local interval inputs -/
  38
  39private def exp_taylor_12_at_048122 : ℚ :=
  40  let x : ℚ := (48122 : ℚ) / 100000
  41  1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040
  42    + x^8/40320 + x^9/362880 + x^10/3628800 + x^11/39916800
  43
  44private def exp_error_12_at_048122 : ℚ :=
  45  let x : ℚ := (48122 : ℚ) / 100000
  46  x^12 * 13 / (Nat.factorial 12 * 12)
  47
  48private lemma exp_048122_taylor_floor :
  49    (80902 / 50000 : ℚ) < exp_taylor_12_at_048122 - exp_error_12_at_048122 := by
  50  native_decide
  51
  52/-- `exp(0.48122) > 1.61804`, enough to prove `log φ < 0.48122`. -/
  53private lemma exp_048122_gt : (1.61804 : ℝ) < Real.exp (0.48122 : ℝ) := by
  54  have hx_abs : |(0.48122 : ℝ)| ≤ 1 := by norm_num
  55  have h_bound := Real.exp_bound hx_abs (n := 12) (by norm_num : 0 < 12)
  56  have h_abs := abs_sub_le_iff.mp h_bound
  57  have h_taylor_eq :
  58      (∑ m ∈ Finset.range 12, (0.48122 : ℝ)^m / m.factorial) =
  59        (exp_taylor_12_at_048122 : ℝ) := by
  60    simp only [exp_taylor_12_at_048122, Finset.sum_range_succ, Finset.sum_range_zero,
  61      Nat.factorial]
  62    norm_num
  63  have h_err_eq :
  64      |(0.48122 : ℝ)|^12 * ((Nat.succ 12 : ℕ) / ((Nat.factorial 12 : ℕ) * 12)) =
  65        (exp_error_12_at_048122 : ℝ) := by
  66    simp only [exp_error_12_at_048122, Nat.factorial, Nat.succ_eq_add_one]
  67    norm_num
  68  have h_lower_raw :
  69      (exp_taylor_12_at_048122 : ℝ) ≤
  70        |(0.48122 : ℝ)|^12 * ((Nat.succ 12 : ℕ) / ((Nat.factorial 12 : ℕ) * 12)) +
  71          Real.exp (0.48122 : ℝ) := by
  72    simpa [h_taylor_eq, add_comm, add_left_comm, add_assoc] using h_abs.2
  73  have h_lower :
  74      (exp_taylor_12_at_048122 : ℝ) - (exp_error_12_at_048122 : ℝ) ≤
  75        Real.exp (0.48122 : ℝ) := by
  76    have h_lower' :
  77        (exp_taylor_12_at_048122 : ℝ) ≤
  78          (exp_error_12_at_048122 : ℝ) + Real.exp (0.48122 : ℝ) := by
  79      calc
  80        (exp_taylor_12_at_048122 : ℝ)
  81            ≤ |(0.48122 : ℝ)|^12 *
  82                ((Nat.succ 12 : ℕ) / ((Nat.factorial 12 : ℕ) * 12)) +
  83                  Real.exp (0.48122 : ℝ) := h_lower_raw
  84        _ = (exp_error_12_at_048122 : ℝ) + Real.exp (0.48122 : ℝ) := by
  85              rw [h_err_eq]
  86    linarith
  87  have h_num :
  88      (1.61804 : ℝ) <
  89        (exp_taylor_12_at_048122 : ℝ) - (exp_error_12_at_048122 : ℝ) := by
  90    have h' : (((80902 / 50000 : ℚ) : ℝ)) <
  91        (exp_taylor_12_at_048122 : ℝ) - (exp_error_12_at_048122 : ℝ) := by
  92      exact_mod_cast exp_048122_taylor_floor
  93    norm_num at h' ⊢
  94    exact h'
  95  exact lt_of_lt_of_le h_num h_lower
  96
  97/-- Tight enough upper bound on `log φ` for the measurement verdict. -/
  98theorem log_phi_lt_048122 : Real.log Constants.phi < (0.48122 : ℝ) := by
  99  rw [Real.log_lt_iff_lt_exp Constants.phi_pos]
 100  have hphi_hi : Constants.phi < (1.6180340 : ℝ) :=
 101    Numerics.W8Bounds.phi_lt_16180340
 102  exact lt_trans hphi_hi (by linarith [exp_048122_gt])
 103
 104private def exp_taylor_12_at_neg_0086705 : ℚ :=
 105  let x : ℚ := -(86705 : ℚ) / 10000000
 106  1 + x + x^2/2 + x^3/6 + x^4/24 + x^5/120 + x^6/720 + x^7/5040
 107    + x^8/40320 + x^9/362880 + x^10/3628800 + x^11/39916800
 108
 109private def exp_error_12_at_neg_0086705 : ℚ :=
 110  let x : ℚ := (86705 : ℚ) / 10000000
 111  x^12 * 13 / (Nat.factorial 12 * 12)
 112
 113private lemma exp_neg_0086705_taylor_floor :
 114    (49568347 / 50000000 : ℚ) <
 115      exp_taylor_12_at_neg_0086705 - exp_error_12_at_neg_0086705 := by
 116  native_decide
 117
 118/-- `exp(-0.0086705) > 0.99136694`. -/
 119private lemma exp_neg_0086705_gt : (0.99136694 : ℝ) < Real.exp (-0.0086705 : ℝ) := by
 120  have hx_abs : |(-0.0086705 : ℝ)| ≤ 1 := by norm_num
 121  have h_bound := Real.exp_bound hx_abs (n := 12) (by norm_num : 0 < 12)
 122  have h_abs := abs_sub_le_iff.mp h_bound
 123  have h_taylor_eq :
 124      (∑ m ∈ Finset.range 12, (-0.0086705 : ℝ)^m / m.factorial) =
 125        (exp_taylor_12_at_neg_0086705 : ℝ) := by
 126    simp only [exp_taylor_12_at_neg_0086705, Finset.sum_range_succ, Finset.sum_range_zero,
 127      Nat.factorial]
 128    norm_num
 129  have h_err_eq :
 130      |(-0.0086705 : ℝ)|^12 * ((Nat.succ 12 : ℕ) / ((Nat.factorial 12 : ℕ) * 12)) =
 131        (exp_error_12_at_neg_0086705 : ℝ) := by
 132    simp only [exp_error_12_at_neg_0086705, Nat.factorial, Nat.succ_eq_add_one]
 133    norm_num
 134  have h_lower_raw :
 135      (exp_taylor_12_at_neg_0086705 : ℝ) ≤
 136        |(-0.0086705 : ℝ)|^12 * ((Nat.succ 12 : ℕ) / ((Nat.factorial 12 : ℕ) * 12)) +
 137          Real.exp (-0.0086705 : ℝ) := by
 138    simpa [h_taylor_eq, add_comm, add_left_comm, add_assoc] using h_abs.2
 139  have h_lower :
 140      (exp_taylor_12_at_neg_0086705 : ℝ) - (exp_error_12_at_neg_0086705 : ℝ) ≤
 141        Real.exp (-0.0086705 : ℝ) := by
 142    have h_lower' :
 143        (exp_taylor_12_at_neg_0086705 : ℝ) ≤
 144          (exp_error_12_at_neg_0086705 : ℝ) + Real.exp (-0.0086705 : ℝ) := by
 145      calc
 146        (exp_taylor_12_at_neg_0086705 : ℝ)
 147            ≤ |(-0.0086705 : ℝ)|^12 *
 148                ((Nat.succ 12 : ℕ) / ((Nat.factorial 12 : ℕ) * 12)) +
 149                  Real.exp (-0.0086705 : ℝ) := h_lower_raw
 150        _ = (exp_error_12_at_neg_0086705 : ℝ) + Real.exp (-0.0086705 : ℝ) := by
 151              rw [h_err_eq]
 152    linarith
 153  have h_num :
 154      (0.99136694 : ℝ) <
 155        (exp_taylor_12_at_neg_0086705 : ℝ) - (exp_error_12_at_neg_0086705 : ℝ) := by
 156    have h' : (((49568347 / 50000000 : ℚ) : ℝ)) <
 157        (exp_taylor_12_at_neg_0086705 : ℝ) - (exp_error_12_at_neg_0086705 : ℝ) := by
 158      exact_mod_cast exp_neg_0086705_taylor_floor
 159    norm_num at h' ⊢
 160    exact h'
 161  exact lt_of_lt_of_le h_num h_lower
 162
 163/-! ## Certified first-order exclusion -/
 164
 165/-- Tight upper bound on the natural exponential load `f_gap / alpha_seed`. -/
 166theorem exponentialLoad_lt_0086705 :
 167    Constants.f_gap / Constants.alpha_seed < (0.0086705 : ℝ) := by
 168  have hfg_hi : Constants.f_gap < (1.198514 : ℝ) := by
 169    unfold Constants.f_gap
 170    have hw_hi := Numerics.W8Bounds.w8_computed_lt
 171    have hlog_hi := log_phi_lt_048122
 172    have hw_pos : 0 < Constants.w8_from_eight_tick := Constants.w8_pos
 173    have hlog_pos : 0 < Real.log Constants.phi := by
 174      exact Real.log_pos Constants.one_lt_phi
 175    calc
 176      Constants.w8_from_eight_tick * Real.log Constants.phi
 177          < Constants.w8_from_eight_tick * (0.48122 : ℝ) :=
 178            mul_lt_mul_of_pos_left hlog_hi hw_pos
 179      _ < (2.490572090 : ℝ) * (0.48122 : ℝ) :=
 180            mul_lt_mul_of_pos_right hw_hi (by norm_num)
 181      _ < (1.198514 : ℝ) := by norm_num
 182  have hseed_lo : (138.230048 : ℝ) < Constants.alpha_seed := Numerics.alpha_seed_gt
 183  have hseed_pos : 0 < Constants.alpha_seed := lt_trans (by norm_num) hseed_lo
 184  rw [div_lt_iff₀ hseed_pos]
 185  calc
 186    Constants.f_gap < (1.198514 : ℝ) := hfg_hi
 187    _ < (0.0086705 : ℝ) * Constants.alpha_seed := by nlinarith [hseed_lo]
 188
 189/-- The first-order Alpha Genesis value is above CODATA by at least `0.0007`.
 190This is the formal version of Anil's measurement objection, stated coarsely
 191but with a fully certified margin. -/
 192theorem alphaInvGenesis_exceeds_CODATA_by_0007 :
 193    alpha_inv_CODATA + (0.0007 : ℝ) < alphaInvGenesis := by
 194  rw [alphaInvGenesis_eq_alphaInv]
 195  unfold Constants.alphaInv
 196  have hseed_lo : (138.230048 : ℝ) < Constants.alpha_seed := Numerics.alpha_seed_gt
 197  have hseed_pos : 0 < Constants.alpha_seed := lt_trans (by norm_num) hseed_lo
 198  have hload_hi : Constants.f_gap / Constants.alpha_seed < (0.0086705 : ℝ) :=
 199    exponentialLoad_lt_0086705
 200  have hexp_mono : Real.exp (-0.0086705 : ℝ) < Real.exp (-(Constants.f_gap / Constants.alpha_seed)) := by
 201    exact Real.exp_lt_exp.mpr (by linarith)
 202  have hexp_lo : (0.99136694 : ℝ) < Real.exp (-(Constants.f_gap / Constants.alpha_seed)) :=
 203    lt_trans exp_neg_0086705_gt hexp_mono
 204  have hmul :
 205      (138.230048 : ℝ) * (0.99136694 : ℝ) <
 206        Constants.alpha_seed * Real.exp (-(Constants.f_gap / Constants.alpha_seed)) := by
 207    have h1 :
 208        (138.230048 : ℝ) * (0.99136694 : ℝ) <
 209          Constants.alpha_seed * (0.99136694 : ℝ) :=
 210      mul_lt_mul_of_pos_right hseed_lo (by norm_num)
 211    have h2 :
 212        Constants.alpha_seed * (0.99136694 : ℝ) <
 213          Constants.alpha_seed * Real.exp (-(Constants.f_gap / Constants.alpha_seed)) :=
 214      mul_lt_mul_of_pos_left hexp_lo hseed_pos
 215    exact lt_trans h1 h2
 216  have htarget :
 217      alpha_inv_CODATA + (0.0007 : ℝ) <
 218        (138.230048 : ℝ) * (0.99136694 : ℝ) := by
 219    norm_num [alpha_inv_CODATA]
 220  exact lt_trans htarget hmul
 221
 222/-- CODATA uncertainty is exactly the stored one-sigma value. -/
 223theorem alpha_inv_uncertainty_eq : alpha_inv_CODATA_uncertainty = (0.000000021 : ℝ) := rfl
 224
 225/-- The certified `0.0007` overshoot is more than `30000` one-sigma
 226uncertainties. -/
 227theorem margin_0007_gt_30000_sigma :
 228    (30000 : ℝ) * alpha_inv_CODATA_uncertainty < (0.0007 : ℝ) := by
 229  norm_num [alpha_inv_CODATA_uncertainty]
 230
 231/-- Measurement verdict certificate: the first-order genesis value is excluded
 232by a CODATA comparison with a margin greater than `30000σ`. -/
 233structure MeasurementVerdictCert where
 234  exceeds_by_margin : alpha_inv_CODATA + (0.0007 : ℝ) < alphaInvGenesis
 235  margin_many_sigma : (30000 : ℝ) * alpha_inv_CODATA_uncertainty < (0.0007 : ℝ)
 236  quarantine : True
 237
 238def measurementVerdictCert : MeasurementVerdictCert where
 239  exceeds_by_margin := alphaInvGenesis_exceeds_CODATA_by_0007
 240  margin_many_sigma := margin_0007_gt_30000_sigma
 241  quarantine := trivial
 242
 243end
 244
 245end MeasurementVerdict
 246end AlphaGenesis
 247end Constants
 248end IndisputableMonolith
 249