predicted_residue_tau_bounds_v2
plain-language theorem explainer
The predicted residue for the tau lepton on the Recognition Science phi-ladder satisfies the strict numerical interval from -3.7619 to -3.7603. Physicists deriving forced lepton masses from the electron structural mass and geometric steps would cite this bound to close the tau prediction. The argument is a one-line wrapper that simplifies the residue definition, invokes the muon residue bounds together with the mu-to-tau step bounds, and closes both sides via linear arithmetic.
Claim. $-3.7619 < r_τ < -3.7603$, where $r_τ$ is the predicted residue for the tau lepton obtained by adding the muon residue to the mu-to-tau step function derived from cube geometry and the fine-structure constant.
background
Under T10 the lepton ladder is forced from the electron mass (T9), step functions built from passive cube edges, faces, wallpaper groups, α, and π, together with the golden ratio φ fixed by T4-T6. The residue is the fractional correction in the exponent of the mass formula yardstick · φ^(rung + residue). The predicted tau residue is computed from the corresponding muon residue plus the fixed mu-to-tau step interval.
proof idea
The term proof first simplifies the definition of the predicted tau residue. It obtains the already-proved muon residue bounds and the mu-to-tau step bounds. The constructor splits the target conjunction and linarith combines the two input intervals to verify both sides of the stated numerical bound.
why it matters
The lemma supplies one of the two numerical anchors required to replace the original lepton axioms with theorems in T10. It is invoked directly by the lower and upper bounds on φ raised to the tau residue, which in turn support the tau mass interval. The result therefore contributes to showing that all three lepton generations are forced by the eight-tick octave and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.