predicted_residue_mu
plain-language theorem explainer
The definition assembles the predicted muon residue on the phi-ladder as the gap function evaluated at 1332, minus the refined shift, plus the electron-to-muon geometric step. Researchers deriving lepton masses from the Recognition Science ladder cite this when converting the electron structural mass into the muon prediction. It is a direct algebraic combination of the anchor residue, topology shift, and passive-edge correction.
Claim. $r_\mu := \mathcal{F}(1332) - \sigma + \Delta_{e\to\mu}$, where $\mathcal{F}(Z) = \ln(1 + Z/\phi)/\ln(\phi)$ is the anchor residue function, $\sigma$ is the refined shift (base shift plus radiative correction), and $\Delta_{e\to\mu}$ is the electron-to-muon step driven by passive edges and spherical geometry.
background
The module supplies core definitions for T10 lepton generations, separating them from theorems to avoid import cycles. The gap function is the closed-form display F(Z) for the integrated RG residue at the anchor scale, with the claim that the residue equals F(Z) for each fermion species. The refined shift is the complete predicted shift assembled from base shift and radiative correction. The electron-to-muon step is driven by passive edges (11) and spherical geometry (1/4π), expressed as E_passive + 1/(4π) - α².
proof idea
One-line definition that directly combines the gap at 1332, the refined shift from MassTopology, and the electron-to-muon step from the sibling lepton definitions.
why it matters
This supplies the exponent for the predicted muon mass, which is electron structural mass times phi raised to the residue. It supports the T10 lepton ladder forced from T9, where muon and tau masses are fixed by the electron structural mass, passive edges E_p=11, cube faces F=6, wallpaper groups W=17, and the fine-structure constant. Downstream necessity lemmas reuse it for explicit bounds on phi to the residue power.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.