predicted_residue_tau
plain-language theorem explainer
The definition sets the predicted tau residue as the muon residue plus the muon-to-tau step. Researchers assembling lepton mass hierarchies on the phi-ladder in Recognition Science cite this when chaining generations. It is realized as a direct one-line sum of the two upstream real-valued quantities.
Claim. Let $r_μ$ be the predicted muon residue and $s_{μτ}$ the muon-to-tau step. The predicted tau residue is $r_τ = r_μ + s_{μτ}$.
background
The T10 Lepton Generations module isolates core definitions for lepton mass derivations to break import cycles. Mass is an alias for the reals in RS-native units. The muon residue combines a gap term with the electron-to-muon step. The muon-to-tau step is defined by cube faces minus a wallpaper symmetry term scaled by alpha, per its documentation: Step 2: Muon to Tau. Driven by Faces (6) and Wallpaper Symmetry (17).
proof idea
This is a one-line wrapper that adds the predicted muon residue to the muon-to-tau step.
why it matters
The residue supplies the exponent in the predicted tau mass, formed as electron structural mass times phi to this power. It feeds the bounds lemmas establishing 0.1629 < phi to the residue < 0.165. The construction advances T10 lepton predictions inside the Recognition framework via the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.