ratio_tau_e_RS_eq
plain-language theorem explainer
The RS-predicted tau-to-electron mass ratio equals φ^17. Lepton-sector and mass-ladder auditors cite this when checking rung arithmetic against PDG ratios. The proof unfolds the ratio to lepton rung data and reduces the integer exponent by the crystallographic constant wallpaper_groups = 17, then closes by numeric normalization.
Claim. The Recognition Science tau-to-electron mass ratio equals $\varphi^{17}$. Equivalently the exponent is $19-2$, with $2$ the electron rung and the shift fixed by the count of distinct 2D wallpaper groups.
background
This module compares RS mass predictions to PDG 2024 values and is quarantined from the certified surface because it mixes derived ladder structure with external experimental anchors. Species masses sit on the $\varphi$-ladder:
$$m(\mathrm{species})=\mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r_{\mathrm{species}}},$$
with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and sector integers from cube geometry. Within one sector the yardstick cancels in ratios, so $m_\tau/m_e$ is a pure power of $\varphi$.
The electron rung is $r_e=2$ (mass-on-rung form used elsewhere for $m_e$). The integer $17$ is the classical count of 2D wallpaper groups (Fedorov 1891), exposed in the constants layer as wallpaper_groups : ℕ := 17 and used as the curvature-fraction denominator (faces × wallpaper groups). The local ratio definition packages lepton rung data (r_lepton, tau) and a witness shell W so the exponent is definitionally that crystallographic integer.
proof idea
Term-style tactic proof, three steps. Unfold the ratio definition together with the lepton rung map, the tau species label, and the witness shell W, exposing an integer expression in the wallpaper count. Simplify with the constants fact that the wallpaper-group count equals 17. Finish by norm_num, which checks the residual integer arithmetic (including the doc-comment form $19-2=17$) and yields equality to $\varphi^{17}$ in $\mathbb{R}$.
why it matters
Closes the pure-RS side of the tau/electron ratio inside the quarantined mass-comparison layer: once the ratio is exactly $\varphi^{17}$, numerical checks against PDG $m_\tau/m_e$ become a comparison of a single closed form to experiment, not an open rung calculation.
The exponent is not fitted; it is the wallpaper-group integer already forced in the alpha/curvature bookkeeping (faces × 17). That ties the lepton mass ladder to the same crystallographic constant that appears in the fine-structure derivation path. Framework landmarks in view: $\varphi$ as the self-similar fixed point (T6) and the mass yardstick formula on the $\varphi$-ladder. No downstream theorems are wired yet (used_by empty); the result is a leaf equality ready for ratio-vs-PDG lemmas beside the experimental m_tau_exp / m_e_exp siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.