predicted_residue_tau_bounds
plain-language theorem explainer
The lemma establishes that the predicted tau residue on the phi-ladder lies strictly between -3.77 and -3.75. Researchers deriving lepton masses from the Recognition Science forcing chain would cite it to anchor the tau prediction after the muon residue is fixed. The proof unfolds the residue definition, pulls in the muon bounds and mu-tau step bounds, then splits the goal and finishes with linear arithmetic.
Claim. $-3.77 < r_τ < -3.75$, where $r_τ$ is the predicted residue for the tau lepton obtained by adding the predicted muon residue to the mu-tau step function derived from cube geometry and the fine-structure constant.
background
The module proves T10 necessity: the lepton ladder is forced from the electron mass (T9) together with geometric constants. The tau residue equals the muon residue plus the mu-tau step; steps combine passive cube edges (11), cube faces (6), wallpaper groups (17), alpha, and pi, all already fixed by the eight-tick structure and D = 3. Upstream results supply the spectral-emergence structure that forces exactly three generations from face-pair count and the phi-forcing structure that supplies the underlying J-cost.
proof idea
Term proof. It simplifies the tau-residue definition, invokes the muon-residue bounds and the mu-tau-step bounds, splits the conjunction, and closes both sides by linear arithmetic.
why it matters
The lemma supplies the interval needed for the lower and upper bounds on phi to the power of the tau residue, which in turn fix the predicted tau mass on the phi-ladder. It fills the T10 slot in the lepton-generations necessity proof, using the eight-tick octave and three spatial dimensions from the forcing chain (T7, T8). It closes one scaffolding gap between the electron-mass theorem and the full three-generation mass predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.