tau_mass_pred_bounds_proven
plain-language theorem explainer
The theorem establishes that the predicted tau lepton mass lies strictly between 1769 and 1792 in RS-native units. Researchers deriving lepton masses from the unified forcing chain cite this to confirm the third generation follows deterministically from the electron mass and cube-derived constants. The proof is a direct term that pairs the lower and upper bound lemmas obtained by interval propagation through the residue and step functions.
Claim. $1769 < m_τ^pred < 1792$, where $m_τ^pred$ is the tau mass obtained from the electron structural mass via the face-symmetry step $step_μτ = 6 - (2·17 + 3)/2 · α$ together with the golden-ratio residue on the phi-ladder.
background
The module proves T10 necessity: once the electron mass is fixed by T9, the muon and tau masses are forced by the geometric constants E_passive = 11, cube faces F = 6, wallpaper groups W = 17, the fine-structure constant α from T6, and φ from T4. The Anchor.tau definition supplies the generation torsions τ(0) = 0, τ(1) = 11, τ(2) = 17 that enter the step functions. Predicted mass is computed by applying the mass formula yardstick · φ^(rung − 8 + gap) to the cumulative steps, with interval arithmetic tracking the propagated uncertainty.
proof idea
The proof is a one-line term wrapper that applies the pair of lemmas predicted_mass_tau_lower and predicted_mass_tau_upper. These lemmas are obtained by interval propagation through the definitions of step_mu_tau_bounds and predicted_residue_tau_bounds, using the already-proven bounds on α and the structural mass.
why it matters
This declaration supplies the tau bounds required by the downstream tau_mass_pred_bounds theorems and by lepton_ladder_forced_from_T9, thereby completing the proof that the lepton ladder is forced from T9. It realizes the T10 step of the forcing chain (T0–T8) using cube-face universality and the eight-tick octave. The result replaces an earlier axiom with a proven interval whose width is set by current input precision; tighter bounds on α or the structural mass would narrow the prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.