mu_pred_upper
plain-language theorem explainer
The theorem proves that the φ-ladder prediction for the proton-electron mass ratio lies strictly below 1904. Researchers comparing Recognition Science mass predictions against CODATA data would cite this bound when assembling the full interval for μ_pred. The proof unfolds the ratio definition, applies the division inequality from positivity of the electron prediction, and chains the supplied mass bounds through a multiplication inequality to close the target.
Claim. Let $e_ {pred} := φ^{59}/4194304000000$ and $p_{pred} := φ^{43}/10^6$ be the φ-ladder predictions for the electron and proton binding energies. Define $μ_{pred} := p_{pred}/e_{pred}$. Then $μ_{pred} < 1904$.
background
The MuRatioScoreCard module records proved interval bounds on the predicted proton-electron mass ratio in the φ-ladder framework. The ratio is defined as mu_pred := proton_binding_pred / electron_pred, where electron_pred := Constants.phi ^ 59 / 4194304000000 and proton_binding_pred := Constants.phi ^ 43 / 1000000. Upstream theorems supply the concrete bounds electron_mass_bounds (0.5098 < electron_pred < 0.5102) and proton_mass_bounds (969 < proton_binding_pred < 970.4), together with the positivity fact electron_pred_pos.
proof idea
The tactic proof unfolds mu_pred, invokes electron_pred_pos to obtain 0 < electron_pred, then rewrites the goal via div_lt_iff₀. It extracts the electron lower bound from electron_mass_bounds.1 and the proton upper bound from proton_mass_bounds.2. A norm_num step confirms 970.4 < 1904 * 0.5098; mul_lt_mul_of_pos_left lifts the inequality to 1904 * 0.5098 < 1904 * electron_pred. linarith closes the chain.
why it matters
This upper bound pairs with mu_pred_lower to produce mu_pred_bracket, which asserts the full interval 1898 < mu_pred < 1904. The module documentation states that the predicted value near 1901 deviates from the CODATA ratio 1836.15 by roughly 4 percent, attributing the gap to the binding-energy-dominated proton sitting between φ-ladder rungs 47 and 48. The result supports verification of the mass formula on the phi-ladder and feeds the Phase 0 row P0-MU of the physical derivation plan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.