predicted_mass_tau_upper_tight
plain-language theorem explainer
The declaration proves that the predicted tau mass in the Recognition Science lepton ladder is strictly less than 1791.6. Researchers comparing RS predictions against experimental tau data would cite this bound when tightening the allowed interval. The proof is a short calc that multiplies the structural mass upper bound by the phi-residue upper bound and normalizes the numerical result.
Claim. Let $m_0$ be the electron structural mass and $r_0$ the predicted tau residue. Then $m_0 · φ^{r_0} < 1791.6$.
background
The module proves T10 necessity results that force the muon and tau masses from the electron mass (T9) together with geometric constants. The electron structural mass is the lepton yardstick scaled by φ to the power of the rung offset from the octave period. The predicted tau mass is this structural mass multiplied by φ raised to the tau residue, where the residue accumulates the step from muon to tau. Upstream structural_mass_bounds supplies the interval (10856, 10858) for the structural mass; phi_pow_residue_tau_upper supplies the bound φ to the residue power below 0.165. These rest on the tau anchor definition with generation values 0, 11, 17.
proof idea
The tactic proof begins with simp on the predicted tau mass definition. It obtains structural_mass_bounds and phi_pow_residue_tau_upper. A calc then shows the product is less than 10858 times 0.165 via nlinarith on those two facts, followed by norm_num to confirm the result is below 1791.6.
why it matters
This supplies the upper half of tau_mass_pred_bounds_tight, which tightens the predicted tau interval to roughly 1.3 percent width. It advances the T10 program of forcing the lepton ladder from the electron mass, the φ fixed point (T5-T6), and the eight-tick geometric constants E_passive, W, and cube faces. The bound closes one axiom replacement in the LeptonGenerations module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.