phi_neg58_lt
plain-language theorem explainer
φ^{-58} < 7.57 × 10^{-13} follows from inverting the companion lower bound φ^{58} > 1.3219 × 10^{12}. Neutrino-sector mass predictions cite this interval to constrain the rung -58 prediction on the phi-ladder. The tactic proof rewrites the negative power as a reciprocal, applies strict inverse monotonicity, and closes the comparison with norm_num and linarith.
Claim. $φ^{-58} < 7.57 × 10^{-13}$ where $φ = (1 + √5)/2$ is the golden ratio.
background
The Numerics.Interval.PhiBounds module supplies rigorous algebraic bounds on integer powers of the golden ratio without external numeric axioms. It begins from the elementary inequalities 2.236 < √5 < 2.237 that yield 1.618 < φ < 1.6185 and then tightens them via higher-precision comparisons. This lemma depends on the upstream result phi_pow58_gt, which supplies the key lower bound φ^{58} > 1.3219 × 10^{12}.
proof idea
The tactic proof first invokes phi_pow58_gt to obtain φ^{58} > 1.3219e12. It establishes positivity of the bound via norm_num, rewrites goldenRatio ^ (-58) as the reciprocal of φ^{58} using zpow_neg_coe_of_pos, applies inv_strictAnti₀ to reverse the inequality, verifies the reciprocal comparison to 7.57e-13 by norm_num, and concludes with linarith.
why it matters
This bound is invoked by phi_neg2314_lt to obtain the quarter-step extension φ^{-231/4} < 8.538e-13 and by nu2_pred_bounds to verify that the predicted neutrino mass at rung -58 lies in (0.0081, 0.0083) eV. It supplies the concrete numeric interval required by the phi-ladder mass formula yardstick · φ^{rung-8+gap(Z)} and supports the eight-tick octave structure in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.