leptonGen12Residual
plain-language theorem explainer
Muon-to-electron mass-ratio residual against eleven φ-ladder rungs: log_φ(m_μ/m_e) − 11. Lepton-sector Item 8 work cites it as the gen-12 data input for η, cross-differences, and the anchored cNeg amplitude. One-line wrapper of the rung residual on fixed PDG pole masses.
Claim. The lepton generation-1–2 residual is $\log_\varphi(m_\mu/m_e)-11$, with $m_\mu=105.658$ and $m_e=0.510999$ the PDG pole masses (MeV).
background
Item 8 Closure Target builds the smallest precise theorem layer that would close the open quark sub-leading mass correction and make the all-sector generalization falsifiable. Residuals live in rung units on the φ-ladder: the integer step is the leading RS prediction, and the leftover is the sub-leading correction the refined family must absorb.
The rung residual is defined by $\mathrm{rungResidual}(r,n)=\log_\varphi r-n$. Here the observed ratio is the PDG muon/electron pole-mass ratio and the integer step is 11 (the lepton gen-12 rung gap). Pole masses make this the cleanest sector: no RG-scheme ambiguity between generations.
Sibling constants fix the numerical anchors (pdg_electron, pdg_muon). Downstream, the same residual feeds the closed-form η formula and the solvability/uniqueness package for the .neg refined family.
proof idea
Pure definitional wrapper. Instantiates rungResidual at ratio pdg_muon / pdg_electron and step 11. No tactics, no lemmas beyond the three inlined constants.
why it matters
Primary gen-12 datum for concrete lepton closure. It is the first argument of leptonEta (η ≈ +0.065 from pole-mass residuals, the cleanest data point) and of leptonAnchoredCNeg, which freezes the active .neg amplitude once η is fixed. Positivity and nonzeroness theorems (leptonGen12Residual_pos, _ne_zero) and the cross-difference facts (leptonCrossDiff_pos, _ne_zero) all quote it, unlocking the constructive ∃! package for the lepton .neg sector at κ_lep = 1/(4π·11).
In the broader RS mass picture this residual is exactly the sub-leading correction on the φ-ladder mass formula (yardstick · φ^(rung−8+gap)). Closing Item 8 for leptons first is the calibration step before the mixed-scheme quark sectors (up/down η) can be trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.