mu_pred_bracket
plain-language theorem explainer
The theorem establishes that the φ-ladder prediction for the proton-electron mass ratio lies strictly between 1898 and 1904. A researcher assembling the Recognition Science scorecard for Phase 0 masses would cite this interval when comparing against CODATA. The proof is the direct conjunction of the separately proved lower and upper bounds on the ratio.
Claim. $1898 < mu_pred < 1904$, where $mu_pred$ denotes the dimensionless ratio of predicted proton binding mass to predicted electron mass obtained from the φ-ladder.
background
The module records proved interval bounds on the predicted proton-to-electron mass ratio in the Recognition Science φ-ladder framework. The ratio is defined by $mu_pred := proton_binding_pred / electron_pred$, with the electron prediction bounded in (0.5098, 0.5102) and the proton prediction in (969, 970.4) from the lepton and binding sectors. Upstream results supply the positivity lemmas for both predictions together with the explicit lower and upper bound theorems that feed this bracket.
proof idea
The proof is a one-line term wrapper that pairs the theorems mu_pred_lower and mu_pred_upper. Each of those unfolds the definition of mu_pred, invokes the electron mass bounds, and applies the appropriate division inequality (lt_div_iff₀ or div_lt_iff₀) to reach the numerical target.
why it matters
This bracket supplies the ratio component of the certificate theorem muRatioScoreCardCert_holds and is used by the relative-error theorem that bounds the residual below 4 percent. It completes the Phase 0 row P0-MU of the derivation plan by confirming the predicted interval (1898, 1904) against the CODATA value 1836.15, consistent with the mass formula on the φ-ladder and the eight-tick octave. The residual deviation remains open for the next pass on proton binding energy between rungs 47 and 48.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.