predicted_residue_tau
plain-language theorem explainer
The definition sets the tau lepton residue to the sum of the muon residue and the muon-to-tau transition step. Researchers deriving third-generation lepton masses in the Recognition Science framework cite this when assembling the phi-ladder predictions. It is a direct one-line algebraic sum of two upstream quantities with no further reduction.
Claim. Let $r_τ$ denote the predicted residue for the tau lepton. Then $r_τ = r_μ + Δ_{μτ}$, where $r_μ$ is the muon residue obtained from the gap term at 1332 minus a refined shift plus the electron-to-muon step, and $Δ_{μτ}$ is the transition coefficient $(6 - (2·17 + 3)α/2)$ driven by cube faces and wallpaper symmetry.
background
The module supplies core definitions for lepton mass derivations under the T10 heading, kept separate from theorems to prevent import cycles. Mass is the real numbers in RS-native units. The muon residue is the gap adjustment at 1332 minus refined shift plus the electron-to-muon step. The muon-to-tau step is the cube-faces term minus half the sum of twice the wallpaper groups plus spatial dimension, scaled by the fine-structure constant.
proof idea
One-line definition that adds the precomputed muon residue to the muon-to-tau step coefficient.
why it matters
This supplies the exponent for the phi-power in the predicted tau mass (electron structural mass times phi to the residue). It feeds the bounds lemmas phi_pow_residue_tau_bounds, phi_pow_residue_tau_lower and phi_pow_residue_tau_upper in the Necessity module, confirming the mass hierarchy on the phi-ladder. The construction aligns with the self-similar fixed point and eight-tick octave of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.