ratio_mu_e_RS
plain-language theorem explainer
Defines the Recognition Science prediction for the muon-to-electron mass ratio as φ raised to the difference of the two lepton rung integers. Mass-comparison and PDG-audit work cites it as the pure RS-side ratio before any experimental overlay. The body is a one-line abbreviation of the φ-ladder mass formula with a common yardstick cancelled.
Claim. The RS-predicted muon-to-electron mass ratio is $\varphi^{r(\mu)-r(e)}$, where $r(\ell)$ is the integer rung assigned to lepton $\ell$ on the $\varphi$-ladder and $\varphi$ is the golden ratio fixed by self-similarity.
background
In the quarantined MassComparison module, species masses are written $m = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}}$. For two leptons the sector yardstick and base offset cancel, so the mass ratio collapses to a pure power of $\varphi$ fixed by the rung difference alone.
Rungs $r_{\mathrm{lepton}}$ come from the lepton-generation geometry (cube edge counts and passive-field structure). The constant $\varphi$ is the unique self-similar fixed point of the Recognition forcing chain (T6). Coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ sets the absolute scale but drops out of ratios.
The module imports experimental PDG anchors only for later numerical comparison; this definition itself is purely RS-native and does not mention measured masses.
proof idea
Definitional abbreviation, not a proved theorem. The right-hand side is exactly $\varphi$ raised to the integer $r_{\mathrm{lepton}}(\mathrm{mu''})-r_{\mathrm{lepton}}(\mathrm{e''})$. No tactics or lemmas are invoked; downstream equality theorems unfold this def and simplify the rung integers.
why it matters
Supplies the RS-side ratio that ratio_mu_e_RS_eq immediately rewrites to $\varphi^{11}$. That exponent is identified with the passive edge count of a 3-cube, tying the lepton mass hierarchy to the same cube geometry that forces $D=3$ (T8) and the eight-tick octave (T7). Parent comparison theorems then confront $\varphi^{11}$ with the PDG $m_\mu/m_e$ band inside the quarantined verification surface. The definition therefore sits at the junction of the $\varphi$-ladder mass formula and the geometric origin of rung integers, without itself importing experimental data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.