w8_from_eight_tick

formal source

  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