proton_mass_bounds
plain-language theorem explainer
The theorem establishes that the Recognition Science phi-ladder prediction for proton binding energy lies strictly between 969 and 970.4 MeV. Particle physicists verifying mass predictions against PDG data would cite this interval when assessing the model's accuracy for hadrons. The proof is a direct tactic calculation that unfolds the prediction and chains norm_num inequalities with pre-established bounds on phi to the 43rd power.
Claim. Let $p$ be the predicted proton binding energy in MeV units. Then $969 < p < 970.4$.
background
Recognition Science places physical masses on the phi-ladder, with the yardstick scaled by integer powers of the golden ratio phi (the self-similar fixed point from T6). The proton binding prediction takes the form phi^43 divided by 10^6, reflecting the closest integer rung near 48 after accounting for the gap to the experimental scale. This module quarantines experimental PDG values as imported constants and focuses on machine-verified interval checks rather than derivation from the forcing chain. Upstream results include the nuclear density structure from NucleosynthesisTiers.of and rung definitions from Compat.Constants.rung, which calibrate the discrete phi-tiers for nuclear quantities.
proof idea
The proof unfolds the definition of the proton binding prediction. It applies constructor to split the conjunction into lower and upper bounds. The lower bound rewrites via lt_div_iff and reduces 969 times 10^6 less than phi^43 using phi43_gt together with norm_num. The upper bound rewrites via div_lt_iff, chains phi^43 less than 970.32 times 10^6 via phi43_lt, then applies norm_num to reach 970.4 times 10^6.
why it matters
This bound is used directly by mu_pred_lower, mu_pred_upper, muRatioScoreCardCert_holds, proton_pred_pos, and proton_relative_error in the MuRatioScoreCard and Verification modules. It supplies the concrete interval needed to certify the proton mass formula on the phi-ladder, consistent with the mass formula yardstick times phi^(rung-8+gap(Z)) and the eight-tick octave from T7. The accompanying doc comment notes the 3.3 percent overshoot as a signature of non-perturbative QCD binding between rungs 47 and 48, closing one verification step in the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.