phi_pow_residue_tau_bounds
plain-language theorem explainer
Bounds 0.1629 < φ^{predicted_residue_tau} < 0.165 close the phi-power factor in the tau mass formula. Researchers replacing lepton-generation axioms with forced inequalities cite this result inside the T10 necessity argument. The proof is a one-line wrapper that pairs the separately established lower and upper bound lemmas.
Claim. Let $r_τ$ be the predicted tau residue. Then $0.1629 < φ^{r_τ} < 0.165$.
background
Module T10 proves the lepton ladder is forced from the electron structural mass (T9) and geometric constants: E_passive = 11, six cube faces, W = 17, together with the golden ratio φ fixed point (T4) and the eight-tick octave. predicted_residue_tau is defined in LeptonGenerations.Defs as predicted_residue_mu + step_mu_tau, the cumulative geometric increment on the phi-ladder. The lemma depends on structural_mass_bounds (10856 < electron_structural_mass < 10858) and the dedicated lower/upper phi-power lemmas for the tau residue.
proof idea
The proof is a one-line wrapper that applies phi_pow_residue_tau_lower and phi_pow_residue_tau_upper by constructing the ordered pair of inequalities.
why it matters
The lemma supplies the tau phi-power interval required to prove corrected mass bounds that replace the original axioms in the lepton necessity module. It feeds the downstream RRF results muon_mass_pred_bounds_proven and the mirrored phi_pow_residue_tau_bounds. It advances the forcing chain by confirming that the phi fixed point and cube-derived steps determine the lepton generations without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.