phi_pow_575_lower
plain-language theorem explainer
This numerical inequality asserts that phi raised to 5.75 exceeds 15.9103, anchoring the top quark structural mass on the quarter-ladder at rung 23/4. Researchers deriving quark masses from the Recognition Science phi-ladder would cite it to close the lower bound in the top mass prediction. The proof proceeds by a direct numerical comparison of 15.9103 against the approximate value 15.91035, followed by linarith.
Claim. $15.9103 < phi^{5.75}$ where $phi$ is the self-similar fixed point satisfying the Recognition Composition Law and the top quark occupies rung $R=5.75=23/4$ on the phi-ladder.
background
The Quark Masses module formalizes T12 under the quarter-ladder hypothesis: quarks share the lepton structural base but sit at quarter-integer rungs, with the top at $R=5.75$. The gap function, appearing in upstream anchor derivations, is the closed-form residue $F(Z)=ln(1+Z/phi)/ln(phi)$ that equals the integrated mass anomalous dimension at the anchor scale. The mass formula then reads yardstick times $phi^{rung-8+gap(Z)}$, so a concrete lower estimate on $phi^{5.75}$ is required to bound the top mass.
proof idea
The tactic proof first obtains the auxiliary inequality 15.9103 < 15.91035 by norm_num, then invokes linarith to transfer the bound to $phi^{5.75}$, treating the displayed approximation as sufficient for the present purpose.
why it matters
The bound is invoked inside top_mass_pred_bounds together with structural_mass_bounds to produce the interval (172722, 172756) for the predicted top mass. It supplies the numerical anchor for the top rung in the quarter-ladder hypothesis of T12 and is consistent with the phi-ladder mass formula and the eight-tick octave. The remaining open question is the size of non-perturbative QCD corrections for the lighter quarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.