proton_relative_error
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the experimental proton mass from the Recognition functional equation.
- Does not extend the 3.5 percent bound to other hadrons or leptons.
- Does not claim the prediction is exact or free of QCD corrections.
- Does not replace the full mass-ladder construction, only the proton verification step.
formal statement (Lean)
308theorem proton_relative_error :
309 |proton_binding_pred - m_p_exp| / m_p_exp < 0.035 := by
proof body
Tactic-mode proof.
310 have hb := proton_mass_bounds
311 have hexp_pos : (0 : ℝ) < m_p_exp := by unfold m_p_exp; norm_num
312 rw [div_lt_iff₀ hexp_pos, abs_lt]
313 unfold m_p_exp
314 constructor <;> nlinarith [hb.1, hb.2]
315
316/-! ## Verification Supersedes mass_ladder_assumption
317
318The concrete interval-arithmetic bounds above replace the placeholder
319`mass_ladder_assumption` from `Assumptions.lean`. The following theorem
320provides the direct replacement: the phi-ladder model with geometry-derived
321parameters matches PDG masses without any external assumption. -/
322
323/-- Direct verification that the phi-ladder model matches PDG to stated tolerances.
324 This supersedes `Masses.mass_ladder_assumption`. -/