predicted_mass_tau_lower_v2
plain-language theorem explainer
The predicted tau mass in RS units exceeds 1774. Physicists deriving lepton hierarchies from the golden ratio and cube geometry would cite this to anchor the tau scale above the experimental threshold. The short tactic proof unfolds the mass definition then chains the electron structural mass lower bound with a separate phi-power residue inequality via calc and nlinarith.
Claim. $1774 < m_τ^pred$ where $m_τ^pred := m_struct^e ⋅ φ^{r_τ}$, $m_struct^e$ is the electron structural mass $Y ⋅ φ^{r_e-8}$, and $r_τ$ is the predicted tau residue obtained by adding the muon-to-tau step to the muon residue.
background
In the T10 lepton ladder module the tau prediction is built from the electron structural mass (defined as lepton_yardstick times phi to the power electron_rung minus 8) scaled by phi to the power of the tau residue. The residue itself is the sum of the muon residue and the geometric step_mu_tau that encodes cube faces, E_passive edges, wallpaper groups, and alpha. The module replaces earlier axioms with proven inequalities once the electron mass is fixed by T9 and the eight-tick octave supplies phi.
proof idea
The proof unfolds predicted_mass_tau by simp, then obtains the structural mass bounds (10856 < electron_structural_mass) and the phi-power lower bound (0.1635 < phi^predicted_residue_tau). A calc tactic first verifies the numerical seed 1774 < 10856 * 0.1635 by norm_num, then applies nlinarith to lift the product inequality to the full expression.
why it matters
This supplies the lower half of tau_mass_pred_bounds_v2, the main v2 result that the entire lepton ladder (muon and tau) lies within 0.2 percent relative error of experiment. It completes the T10 necessity step that forces the tau from the electron structural mass, phi, and the cube-derived steps, confirming the framework landmarks T5 (J-uniqueness), T6 (phi fixed point), and T7 (eight-tick octave).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.