predicted_residue_tau_bounds
plain-language theorem explainer
The lemma proves that the tau lepton residue, formed as the muon residue plus the muon-to-tau step, satisfies -3.77 < residue < -3.75. Researchers deriving forced lepton masses from the phi-ladder and cube geometry would cite it to anchor the T10 necessity argument. The proof combines the already-established muon residue bounds with the step bounds through simplification and linear arithmetic.
Claim. Let $r_μ$ be the predicted muon residue and $s_{μτ}$ the muon-to-tau step. Then $-3.77 < r_μ + s_{μτ} < -3.75$.
background
In the Recognition Science setting the lepton ladder is forced from the electron mass (T9) together with geometric steps built from cube edges (E_passive = 11), faces (= 6), wallpaper groups (W = 17), the fine-structure constant α, and π. predicted_residue_tau is the logarithmic offset in the phi-power mass formula, defined explicitly as the sum of predicted_residue_mu (itself bounded in (-9.63, -9.62)) and step_mu_tau (bounded near 5.86). Upstream results on SpectralEmergence establish that the Q₃ structure forces exactly three generations, while PhiForcingDerived supplies the J-cost underlying the residue arithmetic.
proof idea
The proof simplifies the definition of predicted_residue_tau to its sum expression. It then applies the lemmas predicted_residue_mu_bounds and step_mu_tau_bounds. The constructor tactic splits the conjunction into two inequalities, which linarith discharges directly from the numeric component bounds.
why it matters
This lemma supplies the input bounds for phi_pow_residue_tau_lower and phi_pow_residue_tau_upper, which close the tau mass prediction on the phi-ladder. It advances the T10 necessity claim that lepton masses are determined by the golden-ratio fixed point and eight-tick octave rather than free parameters. The result sits inside the chain from T5 J-uniqueness through T6 phi and T8 D = 3, confirming the observed generation structure lies inside the alpha inverse band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.