phi_pow_residue_tau_bounds
plain-language theorem explainer
Bounds on the golden ratio raised to the predicted tau residue sit between 0.163 and 0.165. Researchers closing the forced lepton mass ladder in the Recognition framework cite this to confirm the tau interval after the muon step. The proof is a one-line term pairing the dedicated lower and upper bound lemmas.
Claim. $0.163 < phi^{r_τ} < 0.165$, where $r_τ$ is the predicted tau residue formed by adding the muon-to-tau step to the muon residue.
background
The module proves T10 necessity: the lepton ladder is forced from the electron structural mass (T9) together with geometric steps and the golden ratio. The predicted tau residue equals the muon residue plus the mu-tau step, where steps combine cube edges, faces, wallpaper count, and alpha. Upstream structural_mass_bounds supplies the electron scale in (10856, 10858) via $2^{-22} phi^{51}$.
proof idea
The proof is a one-line wrapper that pairs the lower bound lemma for the phi power of the tau residue with its upper bound counterpart.
why it matters
This lemma supports the muon mass prediction bounds theorem that replaces an axiom for the lepton generations. It advances the T10 chain by propagating the phi fixed point (T6) and cube-derived steps through the mass formula. The resulting interval remains wider than the observed tau mass, leaving an open tightening question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.