phi_neg2314_gt
plain-language theorem explainer
The declaration supplies a certified lower bound 8.514e-13 < phi^(-231/4) for the golden ratio power. Neutrino mass calculations in the Recognition Science model invoke this when bounding fractional predictions for the first two neutrino species. The proof splits the exponent as -58 + 1/4, imports the prior lower bound on phi^(-58), multiplies through by the certified lower bound on phi^(1/4), and chains the resulting inequalities via transitivity.
Claim. $8.514 times 10^{-13} < phi^{-231/4}$, where $phi = (1 + sqrt{5})/2$ denotes the golden ratio.
background
The module Numerics.Interval.PhiBounds develops rigorous numerical bounds on powers of the golden ratio phi by refining rational approximations to sqrt(5), starting from 2.236 < sqrt(5) < 2.237 and tightening to more decimal places. Key supporting definitions include phi_quarter_lo, the certified lower rational bound 1.12783847 for phi^{1/4}, together with the lemma phi_neg58_gt that establishes phi^{-58} > 7.55e-13. The upstream result phi_quarter_bounds consolidates the full interval for phi^{1/4} as phi_quarter_lo < phi^{1/4} < phi_quarter_hi, while qlo_pos confirms positivity of the lower endpoint.
proof idea
The proof rewrites the exponent (-231/4) as -58 + 1/4 via norm_num, then splits the power into the product phi^{-58} * phi^{1/4} using Real.rpow_add. It imports the lower bound on phi^{-58} from phi_neg58_gt after integer casting, extracts the lower bound on phi^{1/4} from phi_quarter_bounds, and applies mul_lt_mul_of_pos_right followed by mul_lt_mul_of_pos_left to obtain two strict inequalities. The final step chains these with the initial numerical comparison via lt_trans.
why it matters
This bound feeds directly into the neutrino-sector lemmas nu1_frac_pred_bounds and nu2_frac_pred_bounds that compute predicted mass fractions for the first two neutrinos, and supports rung_gap_is_seven_halves by supplying the interval arithmetic needed for phi-powered mass ratios. Within the Recognition framework it closes numerical gaps in the T5 J-uniqueness and T6 phi fixed-point steps, ensuring the mass formula yardstick * phi^{rung - 8 + gap(Z)} remains rigorously bounded for comparison with experimental data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.