phi17_lt
The lemma proves that the golden ratio to the 17th power is strictly less than 3574. Workers checking lepton mass predictions against PDG data cite it when bounding the tau-to-electron ratio error. The tactic proof rewrites phi to the golden ratio, invokes pre-established bounds on phi^8 and phi, decomposes the exponent by ring normalization, multiplies the inequalities, and closes with linear arithmetic.
claim$phi^{17} < 3574$ where $phi$ is the golden ratio satisfying $phi = (1 + sqrt(5))/2$.
background
The Masses.Verification module compares RS lepton mass predictions to PDG 2024 values. The formula used is m(Lepton, r) = phi^{57+r} / (2^{22} * 10^6) in MeV for B_pow = -22 and r0 = 62. Upstream results include phi_eq_goldenRatio equating Constants.phi to Real.goldenRatio, phi_lt_16185 giving phi < 1.6185, and phi_pow8_lt supplying the bound on phi^8.
proof idea
Rewrite via phi_eq_goldenRatio. Obtain h8_hi from phi_pow8_lt and hφ_hi from phi_lt_16185. Establish positivity of the terms. Decompose the 17th power as phi^8 * phi^8 * phi by ring_nf. Apply mul_lt_mul twice to reach the product bound 46.99^2 * 1.6185. Finish with linarith showing the product is less than 3574.
why it matters in Recognition Science
The bound is invoked inside tau_electron_ratio_error to establish that the relative error between the predicted and experimental tau-to-electron ratio stays below 0.03. It supplies a concrete numerical check for the phi-ladder rung at exponent 17 in the lepton sector. The result aligns with the self-similar fixed point and eight-tick octave from the forcing chain while remaining quarantined from the certified derivation of the mass formula itself.
scope and limits
- Does not supply a matching lower bound on phi^17.
- Does not derive the mass formula or any rung prediction.
- Applies only to the specific numerical threshold 3574.
- Remains silent on connections to spatial dimension D=3 or the alpha band.
Lean usage
nlinarith [phi17_lt]formal statement (Lean)
214private lemma phi17_lt : Constants.phi ^ (17 : ℕ) < (3574 : ℝ) := by
proof body
Tactic-mode proof.
215 rw [phi_eq_goldenRatio]
216 have h8_hi := Numerics.phi_pow8_lt
217 have hφ_hi := Numerics.phi_lt_16185
218 have hpos8 : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
219 have hφ_pos : (0 : ℝ) < Real.goldenRatio := by simpa using Real.goldenRatio_pos
220 have heq : Real.goldenRatio ^ 17 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio := by ring_nf
221 rw [heq]
222 have h16_hi : Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 < (46.99 : ℝ) * (46.99 : ℝ) :=
223 mul_lt_mul h8_hi (le_of_lt h8_hi) hpos8 (by norm_num)
224 have h17_hi : Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio <
225 (46.99 : ℝ) * (46.99 : ℝ) * (1.6185 : ℝ) :=
226 mul_lt_mul h16_hi (le_of_lt hφ_hi) hφ_pos (by norm_num)
227 linarith [show (46.99 : ℝ) * (46.99 : ℝ) * (1.6185 : ℝ) < (3574 : ℝ) from by norm_num]
228