proton_pred_pos
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.