predicted_mass_tau_upper
plain-language theorem explainer
The upper bound on the predicted tau mass states that the geometrically forced value lies strictly below 1792 in RS units. Physicists closing the lepton mass spectrum from the Recognition Science forcing chain cite this to confirm the tau rung follows from the electron structural mass and phi-powered residue. The tactic proof unfolds the mass definition then chains the structural mass interval with the phi-residue upper bound via nlinarith and norm_num.
Claim. The predicted tau mass, defined as the electron structural mass multiplied by $phi$ raised to the predicted tau residue, satisfies $predicted_mass_tau < 1792$.
background
Module T10 proves the lepton ladder forced from T9 electron mass and geometric constants. The electron structural mass equals the lepton yardstick times $phi$ to the power of (electron rung minus 8), with upstream theorem structural_mass_bounds establishing the tight interval 10856 < electron_structural_mass < 10858. Predicted tau mass is this structural mass times $phi$ to the predicted residue tau, where the residue accumulates step functions from cube edges, faces, wallpaper groups, and alpha. Upstream phi_pow_residue_tau_upper supplies the companion bound $phi^{predicted_residue_tau} < 0.165$.
proof idea
The proof unfolds predicted_mass_tau via simp. It pulls the structural mass bounds from ElectronMass.Necessity.structural_mass_bounds and the phi power bound from phi_pow_residue_tau_upper. A calc block then shows the product is less than 10858 times 0.165 by nlinarith, after which norm_num confirms the result is below 1792.
why it matters
This supplies the upper half of tau_mass_pred_bounds_proven, which replaces the original axiom for tau mass bounds. It advances the T10 necessity claim that muon and tau masses are forced by the Recognition Science chain, using the phi-ladder mass formula and eight-tick octave. The bound sits inside the alpha-derived interval and closes one link in the lepton generation forcing sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.