mu_pred_pos
plain-language theorem explainer
Researchers deriving mass ratios from the φ-ladder cite this result to confirm positivity of the predicted proton-to-electron ratio before establishing numerical bounds. The theorem states that the dimensionless ratio formed by dividing the proton binding prediction by the electron mass prediction is strictly positive. Its proof is a direct one-line invocation of the division-positivity lemma on the two component positivity statements.
Claim. $0 < m_p^{pred} / m_e^{pred}$ where $m_p^{pred}$ is the φ-ladder proton binding prediction and $m_e^{pred}$ is the φ-ladder electron mass prediction.
background
The MuRatioScoreCard module records proved interval bounds on the predicted proton-electron mass ratio μ in the φ-ladder framework of Recognition Science. The electron prediction is defined as φ^59 divided by 4194304000000, while the proton binding prediction is taken from separate mass-bound theorems; their quotient is the noncomputable definition of mu_pred. Positivity of each factor is established independently from the mass bounds via linear arithmetic, as recorded in the sibling lemmas electron_pred_pos and proton_pred_pos.
proof idea
The proof is a one-line wrapper that applies the div_pos lemma directly to the positivity statements proton_pred_pos and electron_pred_pos.
why it matters
This result is a prerequisite for the bracket theorem establishing 1898 < mu_pred < 1904, as stated in the module documentation for Phase 0 row P0-MU of the physical derivation plan. It underpins the hypothesis that the φ-ladder prediction matches the CODATA value 1836.15 within 4 percent, with the deviation attributed to the proton sitting between rungs 47 and 48. The positivity step is required before any further ratio analysis or comparison in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.