proton_electron_ratio_from_ladder
plain-language theorem explainer
When the proton mass is placed on the phi-ladder at rung r_p, the ratio to the electron mass equals phi to the power r_p minus 2. Researchers deriving the observed proton-electron mass ratio near 1836.15 within Recognition Science cite this to fix the effective rung once both particles obey the same ladder. The proof is a direct one-line application of the structural mass-ratio lemma after substituting the rung definitions.
Claim. Assume the proton mass satisfies $m_p = E_0 phi^{r_p}$ with $m_p > 0$, where $E_0$ is the coherence energy. Then $m_p / m_e = phi^{r_p - 2}$, with the electron mass fixed at rung 2 by $m_e = E_0 phi^2$.
background
Recognition Science places particle masses on an exponential phi-ladder whose general term is mass_on_rung r = E_coh * phi^r. The electron is fixed at rung 2, so m_e is defined as mass_on_rung 2. The present theorem assumes the proton likewise lies on the ladder at some integer rung r_p and derives the resulting ratio. Module C-009 assembles this relation after C-007 (electron mass) and C-008 (proton mass from confinement) have supplied the individual placements.
proof idea
The proof is a one-line wrapper that applies mass_ratio_structural to the supplied hypotheses. That lemma rewrites the ratio using the definitions of m_p and m_e, then cancels the common E_coh factor via field_simp to leave the pure power of phi.
why it matters
The declaration supplies the final algebraic step of C-009, showing the ratio is completely determined by the rung difference once both masses obey the phi-ladder. It sits downstream of the electron-mass result (r_e = 2) and the proton-mass placement, both of which trace to the forcing chain T5-T6. The measured ratio 1836.15 then constrains the effective r_p, consistent with the Berry threshold and Z_cf = phi^5. The result remains open pending the confinement derivation for the proton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.