IndisputableMonolith.Constants.GapWeight

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace Constants
   6
   7/-!
   8# Gap weight `w₈` — 8-tick projection weight (parameter-free, closed form)
   9
  10In the α pipeline we use a single gap term:
  11
  12`f_gap = w₈ · ln(φ)`.
  13
  14Historically the repository carried `w₈` as a *numeric certificate*.
  15This is no longer acceptable for the “no free parameters” claim: `w₈` must be
  16defined from first principles.
  17
  18We therefore expose `w8_from_eight_tick` as a **parameter-free closed form**
  19that is (numerically) the normalized DFT-8 “neutral spectral deficit” weight of
  20the canonical φ-pattern.
  21
  22Notes:
  23- A DFT-based *raw* energy sum exists as `Constants.GapWeight.w8_dft_candidate`
  24  in `Constants/GapWeight/Formula.lean`.
  25- That raw sum is **not** equal to `w8_from_eight_tick` (see
  26  `Verification/GapWeightCandidateMismatchCert.lean`); the missing piece is a
  27  normalization/projection step.
  28- The closed form below is the current canonical projection weight on the
  29  8-tick basis.
  30-/
  31
  32/-- The canonical gap weight `w₈` (parameter‑free, closed form).
  33
  34This is the normalized projection weight of the gap onto the fundamental
  358-tick basis. Numerically it is approximately `2.49056927545…`. -/
  36@[simp] noncomputable def w8_from_eight_tick : ℝ :=
  37  (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * phi) / 7
  38
  39/-- Derived w₈ is positive. -/
  40theorem w8_pos : 0 < w8_from_eight_tick := by
  41  -- A coarse but self-contained positivity proof using rational upper bounds.
  42  -- We show the numerator is positive under worst-case substitution (largest φ and √2).
  43  have hs2_hi : Real.sqrt 2 < (71 / 50 : ℝ) := by
  44    have hx : (0 : ℝ) ≤ 2 := by norm_num
  45    have hy : (0 : ℝ) ≤ (71 / 50 : ℝ) := by norm_num
  46    have hsq : (2 : ℝ) < (71 / 50 : ℝ) ^ 2 := by norm_num
  47    exact (Real.sqrt_lt hx hy).2 hsq
  48  have hs5_hi : Real.sqrt 5 < (56 / 25 : ℝ) := by
  49    have hx : (0 : ℝ) ≤ 5 := by norm_num
  50    have hy : (0 : ℝ) ≤ (56 / 25 : ℝ) := by norm_num
  51    have hsq : (5 : ℝ) < (56 / 25 : ℝ) ^ 2 := by norm_num
  52    exact (Real.sqrt_lt hx hy).2 hsq
  53  have hphi_hi : phi < (81 / 50 : ℝ) := by
  54    -- φ = (1 + √5)/2 < (1 + 56/25)/2 = 81/50
  55    have : (phi : ℝ) = (1 + Real.sqrt 5) / 2 := by rfl
  56    rw [this]
  57    have h2pos : (0 : ℝ) < (2 : ℝ) := by norm_num
  58    have hnum : (1 + Real.sqrt 5) < (1 + (56 / 25 : ℝ)) := by linarith [hs5_hi]
  59    have hdiv : (1 + Real.sqrt 5) / 2 < (1 + (56 / 25 : ℝ)) / 2 :=
  60      div_lt_div_of_pos_right hnum h2pos
  61    have hR : (1 + (56 / 25 : ℝ)) / 2 = (81 / 50 : ℝ) := by norm_num
  62    simpa [hR] using hdiv
  63  have hphi_lo : (21 / 13 : ℝ) < phi := by
  64    -- √5 > 2.231, so φ = (1+√5)/2 > (1+2.231)/2 = 1.6155 > 21/13.
  65    have hs5_lo : (2231 / 1000 : ℝ) < Real.sqrt 5 := by
  66      have hx : (0 : ℝ) ≤ (2231 / 1000 : ℝ) := by norm_num
  67      have hsq : (2231 / 1000 : ℝ) ^ 2 < (5 : ℝ) := by norm_num
  68      exact (Real.lt_sqrt hx).2 hsq
  69    have : (phi : ℝ) = (1 + Real.sqrt 5) / 2 := by rfl
  70    rw [this]
  71    have h2pos : (0 : ℝ) < (2 : ℝ) := by norm_num
  72    have hnum : (1 + (2231 / 1000 : ℝ)) < (1 + Real.sqrt 5) := by linarith [hs5_lo]
  73    have hdiv : (1 + (2231 / 1000 : ℝ)) / 2 < (1 + Real.sqrt 5) / 2 :=
  74      div_lt_div_of_pos_right hnum h2pos
  75    have hconst : (21 / 13 : ℝ) < (1 + (2231 / 1000 : ℝ)) / 2 := by norm_num
  76    exact lt_trans hconst (by simpa using hdiv)
  77  have hcoeff_nonpos : (210 : ℝ) - 130 * phi ≤ 0 := by
  78    -- from 21/13 < φ, we get 210 ≤ 130φ
  79    have hφ : (21 / 13 : ℝ) ≤ phi := le_of_lt hphi_lo
  80    have : (210 : ℝ) ≤ 130 * phi := by
  81      have : (130 : ℝ) * (21 / 13 : ℝ) ≤ 130 * phi := by nlinarith [hφ]
  82      simpa using (le_trans (by norm_num : (210 : ℝ) ≤ (130 : ℝ) * (21 / 13 : ℝ)) this)
  83    linarith
  84  -- Numerator positivity by worst-case substitution (largest φ and √2).
  85  have hφ : phi ≤ (81 / 50 : ℝ) := le_of_lt hphi_hi
  86  have hs2 : Real.sqrt 2 ≤ (71 / 50 : ℝ) := le_of_lt hs2_hi
  87  have hconst :
  88      (0 : ℝ) <
  89        (348 : ℝ) - 204 * (81 / 50 : ℝ) + (71 / 50 : ℝ) * ((210 : ℝ) - 130 * (81 / 50 : ℝ)) := by
  90    norm_num
  91  have hbase :
  92      (348 : ℝ) - 204 * phi + (71 / 50 : ℝ) * ((210 : ℝ) - 130 * phi)
  93        ≥ (348 : ℝ) - 204 * (81 / 50 : ℝ) + (71 / 50 : ℝ) * ((210 : ℝ) - 130 * (81 / 50 : ℝ)) := by
  94    nlinarith [hφ]
  95  have hnum_pos :
  96      0 < (348 : ℝ) - 204 * phi + (71 / 50 : ℝ) * ((210 : ℝ) - 130 * phi) :=
  97    lt_of_lt_of_le hconst hbase
  98  have hterm :
  99      (Real.sqrt 2) * ((210 : ℝ) - 130 * phi) ≥ (71 / 50 : ℝ) * ((210 : ℝ) - 130 * phi) := by
 100    exact mul_le_mul_of_nonpos_right hs2 hcoeff_nonpos
 101  have hnum :
 102      0 < (348 : ℝ) - 204 * phi + (Real.sqrt 2) * ((210 : ℝ) - 130 * phi) := by
 103    linarith
 104  have hrewrite :
 105      (348 : ℝ) - 204 * phi + (Real.sqrt 2) * ((210 : ℝ) - 130 * phi)
 106        = (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * phi) := by
 107    ring
 108  have hnum' : 0 < (348 + 210 * Real.sqrt 2 - (204 + 130 * Real.sqrt 2) * phi) := by
 109    simpa [hrewrite] using hnum
 110  have h7 : (0 : ℝ) < (7 : ℝ) := by norm_num
 111  unfold w8_from_eight_tick
 112  simpa using (div_pos hnum' h7)
 113
 114noncomputable def f_gap : ℝ := w8_from_eight_tick * Real.log phi
 115
 116def fGapLowerBound : ℚ := 2993443258792019287026689 / 2500000000000000000000000
 117def fGapUpperBound : ℚ := 5986887286510633232418913 / 5000000000000000000000000
 118
 119/-- Hypothesis for the certified numerical bounds for the gap weight. -/
 120def f_gap_bounds_hypothesis : Prop :=
 121  ((fGapLowerBound : ℚ) : ℝ) < f_gap ∧ f_gap < ((fGapUpperBound : ℚ) : ℝ)
 122
 123end Constants
 124end IndisputableMonolith
 125