mu_pred
plain-language theorem explainer
The definition supplies the predicted proton-electron mass ratio as the quotient of the phi-ladder proton binding prediction and the electron mass prediction. Researchers comparing Recognition Science mass ladders to experimental data would reference this value when assessing the interval against CODATA. It is a direct algebraic quotient of two upstream constant expressions derived from the phi ladder.
Claim. $μ_{pred} := (φ^{43}/10^6) / (φ^{59}/4194304000000)$, where $φ$ is the golden-ratio fixed point satisfying the Recognition Composition Law.
background
In the Recognition Science framework the proton-electron mass ratio is obtained from the phi-ladder mass formula. The upstream definition electron_pred equals $φ^{59}/4194304000000$, corresponding to the lepton sector at rung 2. The upstream definition proton_binding_pred equals $φ^{43}/10^6$, reflecting the binding-energy-dominated proton.
proof idea
The definition is a one-line wrapper that divides proton_binding_pred by electron_pred. No lemmas are invoked inside the definition itself; the resulting expression is unfolded directly in the downstream theorems mu_pred_pos, mu_pred_lower and mu_pred_upper.
why it matters
This definition is the input to mu_pred_bracket, which proves the interval (1898, 1904), and to the structure MuRatioScoreCardCert that records the 4 percent relative error to CODATA. It implements phase 0 row P0-MU of the physical derivation plan by supplying the explicit ratio from the phi-ladder; the documented deviation indicates that the proton sits between rungs 47 and 48 and requires a later refinement pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.