phi_neg2174_gt
plain-language theorem explainer
Physicists modeling neutrino masses via the phi-ladder cite this result to bound the fractional rung contribution to the third neutrino. It asserts that the golden ratio to the power -217/4 exceeds 4.593 times 10 to the minus 12. The proof decomposes the exponent as -54 minus 1/4, reuses the established lower bound on phi to the -54, applies the quarter-power interval, and chains multiplication inequalities to reach the numeric threshold.
Claim. $4.593 times 10^{-12} < phi^{-217/4}$, where $phi = (1 + sqrt{5})/2$ is the golden ratio.
background
The module supplies rigorous numeric bounds on powers of the golden ratio by refining algebraic inequalities on sqrt{5}, starting from 2.236^2 < 5 < 2.237^2 to obtain 1.618 < phi < 1.6185 and then tightening further. Upstream results include the sibling bound phi_neg54_gt on phi^{-54} together with phi_neg_quarter_bounds on the interval for phi^{-1/4}. These support the phi-ladder mass formula in Recognition Science, where masses scale as yardstick times phi to the (rung - 8 + gap(Z)).
proof idea
The proof splits the exponent -217/4 into -54 - 1/4 via norm_num and Real.rpow_add, casts the integer power to zpow for reuse, invokes phi_neg54_gt, pulls the lower quarter bound from phi_neg_quarter_bounds, verifies the numeric product 5.181e-12 * (1/phi_quarter_hi) exceeds 4.593e-12, then applies mul_lt_mul_of_pos_right and mul_lt_mul_of_pos_left to propagate the inequalities before reassembling with lt_trans.
why it matters
This bound feeds directly into nu3_frac_pred_bounds in the NeutrinoSector module, which tightens the predicted mass fraction for the third neutrino, and into rung_gap_is_seven_halves. It closes a required interval for fractional phi-powers in the mass formula yardstick * phi^(rung - 8 + gap(Z)). Within the framework it supports T6 (phi as self-similar fixed point) and the eight-tick octave by supplying concrete arithmetic for negative fractional exponents on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.