mu_pred_pos
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 in Recognition Science
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.
scope and limits
- Does not establish the numerical bounds 1898 < mu_pred < 1904.
- Does not compare the prediction to the CODATA experimental value.
- Does not incorporate binding-energy corrections beyond the current rung placement.
- Does not extend to other particle mass ratios such as muon-electron.
formal statement (Lean)
59theorem mu_pred_pos : 0 < mu_pred :=
proof body
Tactic-mode proof.
60 div_pos proton_pred_pos electron_pred_pos
61
62/-! ## Predicted ratio bracket
63
64We prove `1898 < μ_pred < 1904`. The proof strategy: multiply through
65by `electron_pred` (positive) to convert ratio bounds into
66multiplicative bounds, then apply the two mass-bound theorems plus
67arithmetic.
68-/
69