phi_neg54_gt
plain-language theorem explainer
This theorem proves φ^{-54} exceeds 5.181 × 10^{-12} where φ is the golden ratio. Neutrino mass calculations in the Recognition Science framework cite it to bound the predicted m3 mass near 0.056 eV. The proof inverts the upstream upper bound φ^{54} < 192983018016, rewrites the negative exponent as a reciprocal, and chains reciprocal inequalities with numerical verification.
Claim. $5.181 × 10^{-12} < φ^{-54}$ where φ denotes the golden ratio.
background
The module supplies rigorous interval bounds on φ = (1 + √5)/2 by refining integer-square estimates on √5, starting from 2.236 < √5 < 2.237 and tightening for higher powers. Upstream result phi_pow54_lt establishes φ^{54} < 192983018016 by factoring into φ^{51} and φ^3 bounds. This numerical scaffolding supports the phi-ladder mass formula yardstick · φ^{rung-8+gap(Z)} used for particle predictions.
proof idea
The tactic proof invokes the upstream lemma phi_pow54_lt to obtain φ^{54} < 192983018016. It establishes positivity of φ^{54}, rewrites the negative power via zpow_neg_coe_of_pos, verifies the numerical reciprocal inequality by norm_num, applies one_div_lt_one_div_of_lt, and closes with linarith.
why it matters
The bound is invoked by nu3_pred_bounds to place the predicted m3 mass in (0.055, 0.058) eV and by sibling results phi_neg2174_gt and phi_neg58_lt for refined negative exponents. It supplies concrete constants for the Recognition Science mass ladder at rung -54, closing numerical gaps in the T5 J-uniqueness and phi fixed-point steps without touching the forcing chain T0-T8 directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.