phi_pow_575_upper
plain-language theorem explainer
The numerical bound φ^{5.75} < 15.9104 supplies the upper cap on the structural mass term for the top quark under the quarter-ladder hypothesis. Researchers deriving quark masses from the phi-ladder cite it when closing the interval on predicted top mass in combination with structural bounds. The proof is a short tactic sequence that invokes norm_num on the approximate value 15.91035 then applies linarith to confirm the strict inequality.
Claim. Let φ denote the golden ratio. Then φ^{5.75} < 15.9104, where the exponent equals the ideal residue 23/4 assigned to the top quark on the phi-ladder.
background
The RRF.Physics.QuarkMasses module implements the quarter-ladder hypothesis: quarks occupy the same structural base mass as leptons but sit at quarter-integer rungs on the phi-ladder. The top quark is placed at rung 5.75, defined by the sibling declaration res_top : ℚ := 23/4. This supplies the exact exponent needed for the mass formula yardstick · φ^{rung-8+gap(Z)} in the Recognition framework.
proof idea
The tactic proof first uses norm_num to establish the auxiliary inequality 15.91035 < 15.9104, then invokes linarith to transfer the bound to φ raised to 5.75 after recording the external numeric approximation in a comment.
why it matters
The theorem supplies the missing upper half of the interval used inside top_mass_pred_bounds, which combines it with phi_pow_575_lower and structural_mass_bounds from ElectronMass.Necessity to produce the concrete top-mass prediction (172722, 172756). It therefore completes the numerical axiom slot for the T12 quark-mass derivation and supports the phi-ladder assignments that feed the eight-tick octave and D = 3 emergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.