phi_neg58_gt
plain-language theorem explainer
Neutrino mass calculations cite this result to bound φ^{-58} from below by 7.55 × 10^{-13}. It supplies the lower half of the interval required for the predicted m2 mass in the Recognition framework. The tactic proof inverts the companion upper bound on φ^{58} using reciprocal inequalities and linarith.
Claim. $7.55 × 10^{-13} < φ^{-58}$, where $φ = (1 + √5)/2$ denotes the golden ratio.
background
The module Numerics.Interval.PhiBounds develops rigorous numerical bounds on the golden ratio φ by chaining algebraic inequalities from rational approximations to √5. It begins with 2.236² < 5 < 2.237² to obtain 1.618 < φ < 1.6185 and refines these for higher powers. The upstream lemma phi_pow58_lt asserts φ^{58} < 1.324 × 10^{12}, obtained by multiplying bounds on φ^{54} and φ^4.
proof idea
The proof invokes phi_pow58_lt to obtain φ^{58} < 1.324e12. It establishes positivity of φ^{58}, rewrites the negative power as the reciprocal via zpow_neg_coe_of_pos, shows 7.55e-13 < 1/1.324e12 by norm_num, applies one_div_lt_one_div_of_lt to compare reciprocals, and concludes with linarith.
why it matters
This bound supports the neutrino sector analysis in nu2_pred_bounds, where it combines with structural mass bounds to verify that the predicted mass for rung_nu2 falls within 0.0081 to 0.0083 eV. It contributes to the phi-ladder mass formula by providing precise numerical anchors for negative exponents. The result also enables the extension to phi_neg2314_gt for fractional exponents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.