phi_neg54_lt
plain-language theorem explainer
The inequality φ^{-54} < 5.185 × 10^{-12} supplies a concrete numerical ceiling on the inverse power used in the phi-ladder mass formula. Neutrino-sector calculations cite it to bound the predicted m3 mass near 0.056 eV. The proof inverts the companion lower bound φ^{54} > 192894126000 via strict monotonicity of inversion on the positives followed by a direct numerical comparison.
Claim. Let φ denote the golden ratio. Then φ^{-54} < 5.185 × 10^{-12}.
background
The module supplies rigorous algebraic bounds on φ = (1 + √5)/2 by establishing tight inequalities on √5 and propagating them through powers. The companion result phi_pow54_gt proves the lower bound 192894126000 < φ^{54} by reducing to the already-established φ^{51} > 45536856942 and φ^3 > 4.236. These bounds sit inside the Recognition numerics layer that converts the abstract phi-ladder into concrete mass predictions.
proof idea
The tactic proof begins by invoking phi_pow54_gt. It rewrites the negative exponent as the reciprocal of φ^{54} using zpow_neg_coe_of_pos, applies inv_strictAnti₀ to obtain the reciprocal inequality, replaces the right-hand side by its numerical upper bound via norm_num, and closes with linarith.
why it matters
This bound feeds directly into nu3_pred_bounds, which combines it with the structural-mass interval (10856, 10858) to certify that the predicted neutrino mass lies in (0.055, 0.058) eV. It therefore closes one link in the phi-ladder mass formula yardstick · φ^{rung-8+gap(Z)} for the neutrino rung. The result belongs to the chain of numerical controls that convert the self-similar fixed point φ into observable particle masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.