predicted_residue_mu
plain-language theorem explainer
predicted_residue_mu assembles the muon residue on the phi-ladder as gap(1332) minus the refined topology shift plus the electron-muon transition step. Researchers deriving second-generation lepton masses from the Recognition Science anchor residue and mass formula would cite this expression. It is a direct one-line algebraic combination of three upstream components.
Claim. $r_μ := ℱ(1332) - Δ_refined + s_{eμ}$, where $ℱ(Z) = ln(1 + Z/φ)/ln φ$ is the gap function at the anchor, $Δ_refined$ is the complete predicted shift, and $s_{eμ}$ is the electron-to-muon step driven by passive edges and spherical geometry.
background
The T10 Lepton Generations module isolates core definitions for lepton mass derivations to break import cycles. The gap function ℱ(Z) is the closed-form residue at the anchor scale μ⋆, given by the logarithm ratio that matches the integrated mass anomalous dimension. refined_shift is the sum of base topology shift and radiative correction. step_e_mu adds the passive-edge term (11) and spherical factor (1/4π) minus α².
proof idea
One-line definition that subtracts refined_shift from gap at 1332 and adds step_e_mu.
why it matters
This residue supplies the exponent for the predicted muon mass and enables the phi-power bounds lemmas in the Necessity module. It realizes the mass formula (yardstick × φ^(rung-8+gap(Z))) for the muon generation, linking to the phi-ladder and T8 D=3 structure. It touches the open question of exact numerical closure to observed masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.