pith. machine review for the scientific record. sign in
def definition def or abbrev high

proton_binding_pred

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 283noncomputable def proton_binding_pred : ℝ := Constants.phi ^ (43 : ℕ) / 1000000

proof body

Definition body.

 284

used by (7)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.