leptonGen23Residual
plain-language theorem explainer
Signed residual (in φ-ladder rungs) of the PDG τ/μ pole-mass ratio against φ⁶. Anyone closing the lepton .neg sector of Item 8 cites it as the gen-23 data coordinate. It is a one-line definition: apply rungResidual to pdg_tau/pdg_muon at step 6.
Claim. Define the generation-2–3 lepton residual $R_{23}^{\ell}\in\mathbb{R}$ by $R_{23}^{\ell}:=\mathrm{rungResidual}(m_\tau^{\mathrm{PDG}}/m_\mu^{\mathrm{PDG}},\,6)$, the signed distance in $\varphi$-ladder rungs between the observed tau-to-muon mass ratio and $\varphi^6$.
background
Item 8 of the Recognition verification stack asks for a unified sub-leading mass formula: residuals of PDG mass ratios against pure $\varphi$-ladder steps, then a refined two-coefficient family that absorbs the structural inconsistency of the bare sign-split family. Residuals live in rung units; a residual of zero means the observed ratio sits exactly on $\varphi^{k}$ for the assigned step $k$.
For charged leptons the natural steps are 11 (μ/e) and 6 (τ/μ). Pole masses are used, so there is no RG-scheme ambiguity. The companion gen-12 residual is positive and small (~0.08 rungs); this gen-23 residual is expected negative (~−0.13 rungs) because $m_\tau/m_\mu$ lies below $\varphi^6$. Together they form the observed residual pair that feeds the closed-form η extractor and the constructive ∃! closure for the .neg sector.
proof idea
Pure definition, not a proof. The body is the single application rungResidual (pdg_tau / pdg_muon) 6: take the PDG tau and muon pole masses, form their ratio, and measure the signed rung residual against the sixth power of φ. No lemmas are invoked at the definition site; downstream theorems unfold this abbreviation and reason about the resulting real.
why it matters
This is the gen-23 coordinate of the cleanest Item 8 test case. It is packaged into leptonObserved, drives leptonEta via etaFromData (reported ≈ +0.065), and supplies the negative factor in the cross-difference $R_{12}^{\ell}\cdot 11 - R_{23}^{\ell}\cdot 6$ whose positivity (leptonCrossDiff_pos) and non-vanishing unlock unique solvability of the refined .neg family at the candidate electromagnetic coupling $κ_{\mathrm{lep}}=1/(4\pi\cdot 11)$. The sign theorem leptonGen23Residual_neg and the full leptonSectorClosure both depend on it. In the broader RS picture it is a concrete φ-ladder mass-ratio residual (mass formula / rung arithmetic), not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.