lepton_rungs_derived
plain-language theorem explainer
The three charged-lepton rungs on the RS φ-ladder are fixed integers: electron 2, muon 13, tau 19. Anyone writing or checking RS lepton mass predictions against PDG values cites this packing of the generation rungs. The proof is a one-line term that re-exports the already-proved rung table.
Claim. The Recognition Science lepton rung integers satisfy $r(e)=2$, $r(\mu)=13$, and $r(\tau)=19$.
background
This module compares Recognition Science mass predictions to PDG 2024 data. It is quarantined from the certified surface because it imports experimental numbers and uses the anchor/φ-ladder mass system rather than deriving masses from the forcing chain alone.
In RS, a species mass is written $m = \mathrm{yardstick}(\mathrm{sector})\times\varphi^{r_0+r}$, with coherence energy $E_{\mathrm{coh}}=\varphi^{-5}$ and sector integers $B_{\mathrm{pow}}, r_0$ from cube geometry. The species-dependent integer $r$ is the rung on the φ-ladder; for charged leptons those rungs are the content of this theorem.
The local section packages generation-structure outputs so mass-comparison lemmas can quote a single conjunction instead of three separate equalities.
proof idea
One-line term proof: the goal is definitionally the statement of r_lepton_values, so the proof is just that prior result. No new algebra or case split appears here; the derivation of the three integers lives upstream in the lepton-generation rung table.
why it matters
Lepton mass checks in this verification module need fixed rungs before they can form $m_e, m_\mu, m_\tau$ from the yardstick × φ-power formula and compare to PDG. This declaration is the named packing of those three integers (electron 2, muon 13, tau 19) under the "derived from generation structure" label.
It sits on the mass-formula side of the framework (φ-ladder rungs, not the T0–T8 forcing chain itself). Downstream use count is currently empty in the graph, so it is a leaf citation hook for mass-comparison scripts rather than a step inside a larger proved parent. It does not close any sorry; it only freezes the rung triple the comparison layer expects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.