proton_pred_pos
The lemma establishes positivity of the Recognition Science proton mass prediction phi^43 / 10^6 MeV. Researchers building the predicted proton-electron ratio in the phi-ladder framework cite it when assembling the mu score card. The proof is a one-line wrapper that extracts the lower bound from the mass interval theorem and feeds it to linarith.
claimLet $p = phi^{43}/10^6$ denote the predicted proton mass in MeV. Then $p > 0$.
background
In the Recognition Science framework the proton mass prediction is given by the phi-ladder formula at rung 43 for the binding-energy-dominated proton: proton_binding_pred := phi^43 / 1000000. The MuRatioScoreCard module records interval bounds on this quantity and on the electron prediction to obtain a bracket for the dimensionless ratio mu = m_p / m_e, with CODATA reference value 1836.15267343.
proof idea
The proof is a one-line wrapper. It obtains the mass bounds theorem proton_mass_bounds, extracts its left conjunct (969 < proton_binding_pred), and applies linarith to deduce strict positivity.
why it matters in Recognition Science
This lemma is used by mu_pred_pos to prove 0 < mu_pred via division, which in turn supports the bracket 1898 < mu_pred < 1904. It fills Phase 0 row P0-MU of the physical derivation plan by ensuring the predicted ratio is well-defined before comparison to experiment. The result instantiates the mass formula on the phi-ladder at rung 43, consistent with the eight-tick octave and D = 3. The module notes the open 4 percent deviation from CODATA, attributed to the proton sitting between rungs 47 and 48.
scope and limits
- Does not derive the phi-ladder mass formula or rung assignments.
- Does not establish bounds for the electron mass prediction.
- Does not compare the prediction to CODATA data.
- Does not address higher-order corrections or gap(Z) adjustments.
formal statement (Lean)
55private lemma proton_pred_pos : 0 < proton_binding_pred := by
proof body
Term-mode proof.
56 have hb := proton_mass_bounds
57 linarith [hb.1]
58