predicted_mass_tau_lower
plain-language theorem explainer
The theorem establishes that the predicted tau lepton mass exceeds 1769 in Recognition Science units. Physicists deriving generational masses from the phi-ladder and electron structural scale would cite it to confirm the forced tau prediction. The proof is a short tactic sequence that rewrites the mass definition then combines the structural mass interval with the phi-residue lower bound via norm_num and nlinarith.
Claim. $1769 < m_ {struct} · ϕ^{r_τ}$ where $m_{struct}$ is the electron structural mass (bounded in (10856, 10858)) and $r_τ$ is the predicted tau residue (with ϕ^{r_τ} > 0.163).
background
In the Recognition Science setting the lepton ladder is constructed from the electron structural mass and successive phi-powers. The structural mass is defined as lepton_yardstick · ϕ^(electron_rung - octave_period) and equals 2^{-22} · ϕ^{51}; the structural_mass_bounds theorem supplies the tight interval (10856, 10858). The predicted tau mass is then the structural mass multiplied by ϕ raised to the predicted tau residue, where the residue is the cumulative step from muon to tau obtained from cube geometry (E_passive, faces, W) and the fine-structure constant.
proof idea
The proof rewrites predicted_mass_tau to its definition, obtains the structural mass bounds and the phi-residue lower bound, then executes a calc block: the numerical step 1769 < 10856 · 0.163 is discharged by norm_num, after which nlinarith [structural_mass_bounds.1, phi_pow_residue_tau_lower] closes the inequality.
why it matters
This lower bound is used inside tau_mass_pred_bounds_proven to replace the original axiom for the tau mass interval (1769, 1792). It contributes to the T10 necessity result that the lepton ladder is forced from T9 (electron structural mass) and the phi fixed point of T4, together with the eight-tick octave and cube-derived steps. The interval remains wider than the observed 1776.86 MeV because of conservative propagation through the phi-powers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.