tau_mass_pred_bounds_proven
plain-language theorem explainer
The result shows that the tau mass predicted from the electron structural mass scaled by phi to the tau residue lies strictly between 1768 and 1792. Lepton mass derivations in the Recognition Science program cite it to replace an axiom inside the T10 necessity argument. The proof is a term that directly pairs the already-proven lower and upper bound lemmas on the product.
Claim. $1768 < m_τ^{pred} < 1792$, where $m_τ^{pred} = m_e^{struct} ⋅ ϕ^r$ and $r$ is the predicted residue for the tau generation on the phi-ladder.
background
The T10 module proves the lepton ladder is forced from the T9 electron mass together with cube-derived constants: passive edges E_passive = 11, faces = 6, wallpaper groups W = 17, and the fine-structure constant alpha. The predicted tau mass is the electron structural mass multiplied by phi raised to the power of the tau residue. Upstream results define the generation torsion tau with value 17 for the second generation and supply separate lower and upper bound theorems that propagate intervals from the structural mass bounds and the corresponding phi-power bounds.
proof idea
Term-mode proof that returns the ordered pair of the lower-bound theorem and the upper-bound theorem. Each bound lemma applies the structural mass interval from ElectronMass.Necessity together with the phi-power interval specific to the tau residue.
why it matters
Supplies the proven bounds that replace the original axiom for the tau mass prediction. It is invoked by the public tau_mass_pred_bounds theorem and by the main lepton_ladder_forced_from_T9 result, which states that the e-to-mu and mu-to-tau steps are fixed by E_passive, faces, W, and alpha. This closes the T10 necessity claim that the full lepton spectrum follows from T9 and the geometric constants of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.