  67/-! ### φ power bounds -/
  68
  69/-- Key identity: φ² = φ + 1 (from the defining equation x² - x - 1 = 0). -/
  70lemma phi_sq_eq : phi^2 = phi + 1 := by
  71  simp only [phi]
  72  have h5_pos : (0 : ℝ) ≤ 5 := by norm_num
  73  have hsq : (Real.sqrt 5)^2 = 5 := Real.sq_sqrt h5_pos
  74  ring_nf
  75  linear_combination (1/4) * hsq
  76
  77/-- Tighter lower bound: φ > 1.5 (since √5 > 2, so (1 + √5)/2 > 1.5). -/
  78lemma phi_gt_onePointFive : (1.5 : ℝ) < phi := by
  79  simp only [phi]
  80  have h5 : (2 : ℝ) < Real.sqrt 5 := by
  81    have h : (2 : ℝ)^2 < 5 := by norm_num
  82    rw [← Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
  83    exact Real.sqrt_lt_sqrt (by norm_num) h
  84  linarith
  85
  86/-- Tighter upper bound: φ < 1.62 (since √5 < 2.24). -/
  87lemma phi_lt_onePointSixTwo : phi < (1.62 : ℝ) := by
  88  simp only [phi]
  89  have h5 : Real.sqrt 5 < (2.24 : ℝ) := by
  90    have h : (5 : ℝ) < (2.24 : ℝ)^2 := by norm_num
  91    have h24_pos : (0 : ℝ) ≤ 2.24 := by norm_num
  92    rw [← Real.sqrt_sq h24_pos]
  93    exact Real.sqrt_lt_sqrt (by norm_num) h
  94  linarith
  95
  96/-- Even tighter lower bound: φ > 1.61. -/
  97lemma phi_gt_onePointSixOne : (1.61 : ℝ) < phi := by
  98  simp only [phi]
  99  have h5 : (2.22 : ℝ) < Real.sqrt 5 := by
 100    have h : (2.22 : ℝ)^2 < 5 := by norm_num

papers checked against this theorem (showing 5 of 5)

Pulse ordering shapes pair-creation spectra but not total yield
unclear · 2605.02515

"quasiperiodic (Fibonacci-ordered) structure, where the amplitudes follow a deterministic but aperiodic sequence generated by the Fibonacci substitution rule"
Strong locality forms a tetrahedron in reduced Bell space
unclear · 2605.03104

"V_SL/V_NS = 1/3, V_Q/V_NS = π²/16 ≈ 0.62"
Multi-head attention energy rises monotonically along gradient flows
echoes · 2605.04279

"Condition 8 simplifies to (H−1)ρ ≤ 1−ρ², i.e., ρ² + (H−1)ρ − 1 ≤ 0. The positive root is c*(H) = (√((H−1)²+4) − (H−1))/2."
All fermion masses and α from one equation and the cube
matches · 2506.12859

"T6 (φ as hierarchy base): additive scale closure forces r² = r + 1; the unique positive real is φ = (1+√5)/2. Lean: Constants/phi_sq_eq, phi_irrational, PhiNecessityCert."
One golden-ratio curve organizes four periodic-table trends at once
echoes · 2605.00028

"Two golden-ratio identities, IE_1(G_p)/IE_1(G_{p+1}) ≈ φ^{1/4} on three heavy noble-gas pairs and IE_1(halogen)/IE_1(alkali) ≈ φ^2 on four within-period pairs"