ratio_tau_e_RS
plain-language theorem explainer
Defines the Recognition Science prediction for the tau-to-electron mass ratio as φ raised to the difference of their lepton rung integers. Mass-comparison and PDG audits cite it as the pure RS-side ratio before experimental confrontation. The body is a one-line power of φ; equality to φ^17 is proved downstream.
Claim. The RS-predicted mass ratio $m_\tau / m_e$ is $\varphi^{r_\tau - r_e}$, where $r_\tau$ and $r_e$ are the integer rungs assigned to the tau and electron on the $\varphi$-ladder.
background
The MassComparison module is quarantined from the certified surface: it mixes RS φ-ladder mass predictions with PDG 2024 experimental anchors. In RS, a species mass is
$m = \mathrm{yardstick}(\mathrm{sector}) \times \varphi^{r_0 + r_{\mathrm{species}}}$,
with coherence energy $E_{\mathrm{coh}} = \varphi^{-5}$ and sector yardsticks fixed by cube geometry. Within one sector the yardstick cancels in ratios, so $m_i/m_j = \varphi^{r_i - r_j}$.
Lepton rungs $r_{\mathrm{lepton}}$ are the integer labels on that ladder for e, μ, τ. The golden ratio φ is the self-similar fixed point forced at T6 of the unified forcing chain. This definition packages only the RS exponent difference for τ versus e; experimental numbers live in sibling constants such as $m_{\tau}^{\mathrm{exp}}$.
proof idea
Definitional abbreviation, not a proof. The right-hand side is literally $\varphi$ raised to the integer $r_{\mathrm{lepton}}(\tau) - r_{\mathrm{lepton}}(e)$. No tactics or lemmas fire here; the numerical identification with exponent 17 is deferred to the companion equality theorem.
why it matters
Feeds ratio_tau_e_RS_eq, which states the ratio equals $\varphi^{17}$ and attributes the exponent 17 to the wallpaper-group count in the alpha-derivation constants. That closed form is the RS-side input for machine-checked comparison against the PDG $m_\tau/m_e$ ratio inside this quarantined verification module.
In the broader framework the mass formula sits on the φ-ladder (T6) with coherence scale $\hbar = \varphi^{-5}$. The definition isolates the pure geometric prediction so experimental confrontation cannot leak into certified cores. It does not itself close any forcing-chain step; it is bookkeeping for the lepton rung difference used in mass audits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.