proton_relative_error
plain-language theorem explainer
The theorem shows that the phi-ladder proton mass prediction, given by phi to the 43rd power divided by one million in MeV units, lies within 3.5 percent relative error of the experimental value 938.272 MeV. Verification authors and Recognition Science mass checks would cite this result to replace placeholder assumptions with concrete bounds. The proof obtains the prediction interval from proton_mass_bounds, rewrites the relative-error inequality via division and absolute-value rules, unfolds the definitions, and closes with linear arithmetic.
Claim. Let $P = 938.272$ denote the experimental proton mass in MeV and let $Q = 969.030$ denote the binding-dominated phi-ladder prediction $Q = 10^{-6} phi^{43}$. Then $|Q - P| / P < 0.035$.
background
In the Masses.Verification module, experimental PDG values are treated as imported constants rather than RS derivations. The proton_binding_pred definition supplies the concrete phi-ladder value $phi^{43}/10^6$ MeV, while m_p_exp fixes the PDG anchor at 938.272 MeV. The upstream theorem proton_mass_bounds establishes the interval (969, 970.4) MeV for this prediction, obtained by direct norm_num evaluation of the power and division. The module doc notes that the integer rung nearest the proton is 48, with the 3.3 percent overshoot attributed to non-perturbative QCD binding between rungs 47 and 48. This verification replaces the surrogate mass_ladder_assumption, which merely asserted that imported measurements satisfy the ladder bound without supplying numbers.
proof idea
The tactic proof first obtains the interval bounds via have hb := proton_mass_bounds. It then proves positivity of m_p_exp by unfolding and norm_num. The target inequality is rewritten by div_lt_iff₀ and abs_lt, after which both definitions are unfolded. The resulting two-sided inequality is discharged by a single nlinarith call on the two bounds from hb.
why it matters
This theorem supplies the direct numerical verification that the phi-ladder mass formula matches the PDG proton value to the stated tolerance, thereby discharging the placeholder mass_ladder_assumption from Assumptions.lean. It sits inside the mass-prediction verification block that follows the phi-ladder construction in NumberTheory.PhiLadderLattice and the spacetime-emergence interval. Within the Recognition framework it instantiates the mass formula yardstick times phi to the (rung minus 8 plus gap) on the phi-ladder, confirming consistency with the self-similar fixed point phi after T6 and the eight-tick octave of T7. No open question is left; the result closes the assumption for the proton sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.