phi_pow_neg45_upper
plain-language theorem explainer
The inequality φ^{-4.5} < 0.1148 supplies the upper bound on the geometric scaling factor for the charm quark at rung -4.5. Researchers deriving quark masses from the quarter-ladder hypothesis cite it to close the predicted charm mass interval (1245, 1247). The proof is a direct numeric verification that the computed value 0.11471 lies strictly below the chosen threshold.
Claim. $φ^{-4.5} < 0.1148$, where $φ$ is the golden ratio and the exponent -4.5 is the quarter-ladder rung for the charm quark.
background
The Quarter-Ladder Hypothesis places quarks on the same structural base as leptons but at quarter-integer rungs of the phi-ladder. Charm occupies R = -4.5, defined as res_charm := -18/4. The mass prediction multiplies the structural mass by φ^R, so an explicit upper bound on φ^{-4.5} is required to bound the result from above. The module imports res_charm from the sibling QuarkMasses file and the phi-power interval machinery from Numerics.Interval.PhiBounds.
proof idea
The tactic proof first establishes the concrete numeric fact (0.11471 : ℝ) < 0.1148 by norm_num, then invokes linarith to conclude the target inequality from the known approximation φ^{-4.5} ≈ 0.11471.
why it matters
The bound is invoked inside charm_mass_pred_bounds together with the matching lower bound and the structural-mass interval to produce the closed interval (1245, 1247) for the predicted charm mass. It therefore completes one concrete step of the T12 quarter-ladder construction for the six quarks. The numerical threshold is chosen to contain the exact value while remaining compatible with the observed mass before non-perturbative QCD corrections are added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.