proton_mass_bounds
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the experimental PDG value from the forcing chain.
- Does not incorporate explicit QCD binding corrections beyond the rung gap.
- Does not extend the interval claim to other hadrons or leptons.
- Does not assert exact numerical equality with measured proton mass.
Lean usage
have hb := proton_mass_boundsformal statement (Lean)
291theorem proton_mass_bounds :
292 (969 : ℝ) < proton_binding_pred ∧ proton_binding_pred < (970.4 : ℝ) := by
proof body
Tactic-mode proof.
293 unfold proton_binding_pred
294 constructor
295 · rw [lt_div_iff₀ (by norm_num : (0 : ℝ) < 1000000)]
296 calc (969 : ℝ) * 1000000 < (969030000 : ℝ) := by norm_num
297 _ < Constants.phi ^ 43 := phi43_gt
298 · rw [div_lt_iff₀ (by norm_num : (0 : ℝ) < 1000000)]
299 calc Constants.phi ^ 43 < (970320000 : ℝ) := phi43_lt
300 _ < (970400000 : ℝ) := by norm_num
301 _ = (970.4 : ℝ) * 1000000 := by norm_num
302
303/-- The proton prediction (binding-dominated) is within 3.5% of the PDG value.
304
305Note: the integer rung 48 is the closest to the proton mass. The ~3.3%
306overshoot reflects the non-perturbative QCD binding that sits between
307rungs 47 and 48 on the phi-ladder. -/