proton_electron_derived
plain-language theorem explainer
The Recognition Science prediction for the proton-to-electron mass ratio is the fixed dimensionless number 1836.153. Anyone assembling the RS observables pack or checking CODATA compatibility cites this constant. It is a bare numeric definition: the φ-tower composite derivation is asserted in the doc-comment, not expanded in the body.
Claim. The RS-derived proton-to-electron mass ratio equals $1836.153$. It is presented as a prediction from the $\varphi$-tower (proton composite structure with $\varphi$ corrections), not a fit to CODATA.
background
The Observables module separates a cost-first core from an external-anchor seam. The core supplies dimensionless predictions built from the golden ratio $\varphi$ and the recognition cost structure; the seam only compares those numbers to CODATA bounds. Tracked quantities are $\alpha^{-1}$, $m_e/m_\mu$, $m_p/m_e$, and the dimensionless Newton coupling $G m_e^2/(\hbar c)$.
Mass ratios in RS sit on the $\varphi$-ladder (yardstick times $\varphi$ raised to a rung offset by gap terms). The module doc stresses that "derives observables" means concrete numerical output, not a schematic claim. Upstream constants such as the RS-native $G = \lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$ and the scale map $k\mapsto\varphi^k$ fix the same numeric language used here.
proof idea
One-line numeric definition: the real constant is set equal to $1836.153$. No tactic proof, no lemma application, and no expansion of the composite $\varphi$-tower formula appears in the body. The derivation path is only recorded in the doc-comment (proton composite structure times $\varphi$ corrections).
why it matters
This constant is the proton-electron field of rsObservables, the RS prediction pack compared against experiment. The external-anchor theorem rs_within_bounds unfolds it (with the sibling ratio and $\alpha^{-1}$ constants) and discharges the CODATA interval check by norm_num. In the exclusivity story it supplies one of the four dimensionless observables that a competing framework must match. It sits downstream of the forcing chain's $\varphi$ fixed point (T6) and the mass-ladder convention, and is explicitly marked a prediction rather than a calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.