mu_pred_lower
plain-language theorem explainer
The theorem proves that the phi-ladder prediction for the proton-electron mass ratio exceeds 1898. Recognition Science mass modelers cite this lower bound when constructing the bracketed interval for the dimensionless ratio against CODATA data. The proof unfolds the ratio definition, applies the positivity lemma for the electron prediction to convert to a product inequality, bounds the product below 969 using the supplied mass intervals, and closes the chain with linarith.
Claim. $1898 < m_p^pred / m_e^pred$, where $m_e^pred = phi^{59}/4194304000000$ MeV lies in $(0.5098, 0.5102)$ and $m_p^pred = phi^{43}/1000000$ MeV lies in $(969, 970.4)$.
background
The module records proved interval bounds on the predicted proton-electron mass ratio in the phi-ladder framework of Recognition Science. The ratio is defined as proton_binding_pred divided by electron_pred, with electron_pred = phi^59 / 4194304000000 and proton_binding_pred = phi^43 / 1000000. Upstream theorems supply the tight intervals electron_mass_bounds and proton_mass_bounds together with the positivity lemma electron_pred_pos.
proof idea
The proof unfolds mu_pred and invokes electron_pred_pos to rewrite the target inequality as 1898 * electron_pred < proton_binding_pred. It applies the upper bound from electron_mass_bounds to obtain 1898 * electron_pred < 1898 * 0.5102, shows the right-hand side is less than 969 by norm_num, and combines with the lower bound from proton_mass_bounds via linarith.
why it matters
This lower bound is paired with mu_pred_upper inside the downstream theorem mu_pred_bracket to produce the full interval (1898, 1904). The module compares the resulting prediction to the CODATA value 1836.15 and notes the 4 percent deviation arising from the proton sitting between phi-ladder rungs 47 and 48. It fills the Phase 0 row P0-MU of the physical derivation plan and supports the mass formula yardstick * phi^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.