phi_neg2174_lt
plain-language theorem explainer
This theorem proves that the golden ratio raised to -217/4 is strictly less than 4.598e-12. Neutrino mass interval calculations in the Recognition framework cite it to control the fractional rung contribution at -217/4. The proof splits the exponent into -54 and -1/4, multiplies the separate upper bounds on each factor, and closes the chain with transitivity.
Claim. $φ^{-217/4} < 4.598 × 10^{-12}$, where $φ = (1 + √5)/2$.
background
The module supplies certified numerical bounds on real powers of the golden ratio by starting from rational approximations to √5 and propagating through algebraic identities. Key upstream results are phi_neg54_lt, which asserts φ^{-54} < 5.185e-12, and phi_neg_quarter_bounds, which gives φ^{-1/4} < 1/φ_quarter_lo with the certified lower bound φ_quarter_lo = 1.12783847. These anchors certify the phi-ladder mass assignments required by the Recognition framework.
proof idea
The tactic proof rewrites the exponent -217/4 as -54 - 1/4 via norm_num, expresses the power as a product, and applies phi_neg54_lt to the first factor after integer casting. It bounds the second factor above by the right conjunct of phi_neg_quarter_bounds, then uses two mul_lt_mul_of_pos_* steps to obtain a product upper bound. The final comparison to 4.598e-12 is performed by simp and norm_num, with lt_trans closing the chain.
why it matters
The bound is invoked inside nu3_frac_pred_bounds to establish the interval (0.04985, 0.04993) for the third neutrino's predicted mass in eV. It supplies a verified numerical link between the abstract phi-ladder rung formula and concrete scales, supporting the self-similar fixed point (T6) and eight-tick octave (T7) of the Recognition framework. No scaffolding remains for this exponent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.