proton_binding_pred
plain-language theorem explainer
The Recognition Science framework predicts the proton binding energy as φ^43 divided by 10^6 in MeV units. Researchers constructing mass ratio scorecards against PDG data cite this value to anchor proton bounds and muon-electron comparisons. The declaration is a direct noncomputable assignment drawn from the phi constant in the CPM bundle.
Claim. The predicted proton binding energy is given by $p = φ^{43}/10^6$ in MeV, where $φ$ is the golden ratio constant from the CPM constants bundle.
background
The Verification module compares RS mass predictions to PDG 2024 data while keeping experimental values as imported constants. Proton predictions use a dedicated rung on the phi-ladder, separate from the lepton formula $φ^{57+r}/(2^{22}×10^6)$. The constant φ originates in the Constants structure of the Law of Existence module, an abstract bundle of CPM parameters that includes Knet together with its nonnegativity hypothesis.
proof idea
This is a one-line definition that directly assigns Constants.phi raised to the 43rd power and divided by 1000000.
why it matters
The definition supplies the proton term for mu_pred in the MuRatioScoreCard module and for the MuRatioScoreCardCert structure that certifies the ratio interval (1898, 1904) with less than 4% deviation from codata. It also feeds the proton_mass_bounds theorem establishing the (969, 970.4) MeV interval. In the framework it realizes the mass formula at the proton rung, consistent with the phi fixed point of T6 and the phi-ladder scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.