phi_neg2_gt
plain-language theorem explainer
This theorem proves that the golden ratio to the power negative two exceeds 0.3818. Researchers deriving quark and neutrino mass intervals in the Recognition framework cite it to anchor the phi-ladder predictions. The tactic proof reduces the claim to the companion upper bound on phi squared by rewriting the negative exponent as a reciprocal and applying the reciprocal inequality for positive reals.
Claim. $0.3818 < phi^{-2}$ where $phi = (1 + sqrt(5))/2$ denotes the golden ratio.
background
The module supplies rigorous numerical bounds on the golden ratio phi = (1 + sqrt(5))/2 derived from algebraic inequalities on sqrt(5). It begins from 2.236 squared less than 5 less than 2.237 squared, which yields 1.618 less than phi less than 1.6185, then tightens the decimals for physics use. The immediate predecessor phi_sq_lt establishes phi squared less than 2.619 by combining the upper bound on phi with the identity phi squared equals phi plus one.
proof idea
The proof invokes phi_sq_lt to obtain phi squared less than 2.619. It asserts positivity of phi squared, rewrites the negative integer power as the reciprocal of phi squared, shows 0.3818 less than 1 over 2.619 by norm_num, applies one_div_lt_one_div_of_lt to reverse the inequality for the positive quantities, and closes with linarith.
why it matters
The bound feeds pmns_theta12_match for the solar mixing angle, nu1_frac_pred_bounds for neutrino mass fractions, and bottom_mass_pred_bounds for the interval (4140, 4155) MeV on the bottom quark. It anchors the phi to the minus two term in the Recognition mass formula yardstick times phi to the rung, consistent with the self-similar fixed point property of phi at T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.