predicted_mass_tau_upper_v2
plain-language theorem explainer
predicted_mass_tau_upper_v2 establishes that the RS-predicted tau mass lies strictly below 1779. Researchers closing the lepton mass ladder from geometric forcing cite it to complete the tau interval. The proof rewrites the mass definition, pulls in structural mass bounds and the phi-residue upper bound, then applies nlinarith followed by norm_num to confirm the product inequality.
Claim. Let $m_τ$ be the predicted tau mass defined by $m_τ = m_{struct} ⋅ φ^{r_τ}$, where $m_{struct}$ is the electron structural mass and $r_τ$ is the predicted tau residue. Then $m_τ < 1779$.
background
Module T10 proves the lepton ladder is forced from the electron mass (T9) and geometric constants from cube geometry and the eight-tick octave. The muon and tau masses arise from the structural mass scale multiplied by phi-powered residues that encode the step functions E_passive = 11, faces = 6, W = 17, α, and π.
proof idea
The tactic proof first simplifies the definition of predicted_mass_tau. It obtains the structural mass bounds (10856 < electron_structural_mass < 10858) and the phi-power upper bound (phi ^ predicted_residue_tau < 0.16381) as hypotheses. A calc block then bounds the product below 10858 ⋅ 0.16381 via nlinarith on the two upper estimates, after which norm_num confirms the result is below 1779.
why it matters
This supplies the upper half of tau_mass_pred_bounds_v2, which states 1774 < predicted_mass_tau < 1779 with relative error below 0.2 percent. It completes the forcing of the tau mass from the electron structural mass and the phi-ladder steps, building directly on T9 and the geometric derivations of α and π in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.