phi_pow_6_bounds

formal source

  45
  46/-- φ⁶ ∈ (17, 18): the generation mass ratio m_b/m_s or m_τ/m_μ × corrections.
  47    Uses φ⁶ = 8φ + 5 (Fibonacci identity). -/
  48theorem phi_pow_6_bounds : (17 : ℝ) < phi ^ 6 ∧ phi ^ 6 < (18 : ℝ) := by
  49  have h6 : phi ^ 6 = 8 * phi + 5 := phi_sixth_eq
  50  constructor
  51  · rw [h6]; linarith [phi_gt_onePointFive]
  52  · rw [h6]; linarith [phi_lt_onePointSixTwo]
  53
  54/-- φ⁷ ∈ (28, 30): the neutrino squared-mass ratio m₃²/m₂² = φ⁷.
  55    This is the sharpest seam-free prediction of the framework.
  56    Uses φ⁷ = φ·φ⁶ = φ(8φ+5) = 8φ²+5φ = 8(φ+1)+5φ = 13φ+8. -/
  57private lemma phi_pow_7_eq : phi ^ 7 = 13 * phi + 8 := by
  58  have h6 := phi_sixth_eq
  59  have hsq := phi_sq_eq
  60  calc phi ^ 7 = phi * phi ^ 6 := by ring
  61    _ = phi * (8 * phi + 5) := by rw [h6]
  62    _ = 8 * phi ^ 2 + 5 * phi := by ring
  63    _ = 8 * (phi + 1) + 5 * phi := by rw [hsq]
  64    _ = 13 * phi + 8 := by ring
  65
  66theorem phi_pow_7_gt_28 : (28 : ℝ) < phi ^ 7 := by
  67  rw [phi_pow_7_eq]; linarith [phi_gt_onePointSixOne]
  68
  69theorem phi_pow_7_lt_30 : phi ^ 7 < (30 : ℝ) := by
  70  rw [phi_pow_7_eq]; linarith [phi_lt_onePointSixTwo]
  71
  72theorem phi_pow_7_bounds : (28 : ℝ) < phi ^ 7 ∧ phi ^ 7 < (30 : ℝ) :=
  73  ⟨phi_pow_7_gt_28, phi_pow_7_lt_30⟩
  74
  75/-- φ⁷ > 29: tighter lower bound for the neutrino prediction.
  76    Uses phi > 1.618 (from PhiBounds) since 13 × 1.618 + 8 = 29.034 > 29. -/
  77theorem phi_pow_7_gt_29 : (29 : ℝ) < phi ^ 7 := by
  78  rw [phi_pow_7_eq]