phi_neg2314_lt
plain-language theorem explainer
This result supplies a certified upper bound φ^{-231/4} < 8.538 × 10^{-13} obtained by splitting the exponent as -58 + 1/4. Neutrino-sector mass calculations cite it to close the high-side estimate on predicted electron-volt fractions for the first and second mass eigenstates. The proof rewrites the power via rpow_add, invokes the prior bound on φ^{-58}, multiplies through by the quarter-root upper bound, and chains the inequalities with lt_trans.
Claim. $φ^{-231/4} < 8.538 × 10^{-13}$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The module Numerics.Interval.PhiBounds develops rigorous numerical bounds on powers of the golden ratio φ using its algebraic definition and properties of real exponentiation. It begins from tight rational bounds on √5 (2.236 < √5 < 2.237) that yield interval bounds on φ itself, then extends these to fractional powers such as φ^{1/4} via the consolidated statement phi_quarter_bounds. The present theorem relies on the upstream result phi_neg58_lt asserting φ^{-58} < 7.57 × 10^{-13}, the definition phi_quarter_hi := 1.12783849, and the basic transitivity lemma lt_trans from ArithmeticFromLogic.
proof idea
The proof first rewrites the exponent -231/4 as -58 + 1/4 by norm_num. It factors the power via Real.rpow_add, reduces the integer-power term with rpow_intCast, invokes phi_neg58_lt for the -58 factor, and extracts the upper bound phi_quarter_hi from phi_quarter_bounds. Two applications of mul_lt_mul_of_pos_right and mul_lt_mul_of_pos_left produce an intermediate product bound, which is compared to the target constant by norm_num and chained via lt_trans.
why it matters
This bound closes the upper estimate required by the phi-ladder mass formula when the rung corresponds to the neutrino sector. It is invoked directly in nu1_frac_pred_bounds and nu2_frac_pred_bounds to certify that the predicted mass fractions lie inside the intervals (0.00352, 0.00355) and (0.00924, 0.00928). Within the Recognition Science framework the result supports the T6 self-similar fixed-point property of φ by furnishing concrete numerical control on high negative powers that appear in the mass-yardstick construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.