mass_ratio_structural
plain-language theorem explainer
Structural equality of the proton-electron mass ratio holds whenever the proton mass occupies an integer rung on the phi-ladder. A researcher deriving RS mass hierarchies cites the result to fix the exponent difference once the proton rung is supplied by confinement. The proof is a direct algebraic reduction that substitutes the rung definitions and applies the zpow subtraction identity after clearing the common factor with phi nonzero.
Claim. Let $r_p$ be an integer and let $m_p$ be a positive real satisfying $m_p =$ mass on rung $r_p$. Let $m_e$ denote the electron mass on rung 2. Then $m_p / m_e = phi^{r_p - 2}$.
background
In Recognition Science the electron mass is placed at rung 2 on the phi-ladder, so $m_e :=$ mass_on_rung 2. The proton mass is likewise required to lie on the same ladder at rung $r_p$, with the rung value to be fixed by the confinement argument of C-008. The phi-ladder itself is the discrete scaling generated by the self-similar fixed point of the J-function (T6). Upstream, phi_ne_zero supplies the nonzero property required for exponent rules, while mass_on_rung encodes the yardstick scaling $phi^{rung-8+gap(Z)}$ from the MassHierarchy module.
proof idea
The term proof rewrites both sides by substituting the hypothesis $m_p =$ mass_on_rung $r_p$ together with the definition of $m_e$. It then invokes field_simp using phi_ne_zero to cancel the common mass_on_rung factor, after which the exact application of (zpow_sub₀ phi_ne_zero r_p 2).symm yields the required power difference.
why it matters
The declaration supplies the structural form required by the downstream theorem proton_electron_ratio_from_ladder, which simply forwards the same statement. It completes the C-009 registry item by showing that the ratio collapses to a pure power of phi once C-007 and C-008 place both particles on the ladder. Within the framework it illustrates how the phi fixed point (T6) and eight-tick octave propagate into observable mass ratios, leaving only the determination of $r_p$ open pending the confinement derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.