IndisputableMonolith.Physics.LeptonGenerations
Aggregator for the T10 lepton-generation story: muon and tau masses are forced from the electron (T9) by the phi-ladder and geometric residues. Experimentalists and RS auditors cite the predicted MeV windows (muon in (105,107), tau analogously). The module re-exports definitions and necessity proofs that replace former mass-step axioms by interval inequalities.
claimPredicted muon and tau masses on the $\varphi$-ladder satisfy $m_\mu^{\mathrm{pred}}\in(105,107)\,\mathrm{MeV}$ and a corresponding tau window, with $m_\mu^{\mathrm{exp}}\approx 105.658\,\mathrm{MeV}$ inside a relative error below $2\%$, forced from the electron mass and structural residues rather than free parameters.
background
Recognition Science places charged-lepton masses on a discrete $\varphi$-ladder whose rungs are fixed once the electron mass (T9) and the geometric constants from the forcing chain are known. The cost functional $J(x)=(x+x^{-1})/2-1$ and the self-similar fixed point $\varphi$ determine admissible mass steps; residues encode the generation offsets.
LeptonGenerations.Defs isolates the core predicates and predicted-mass constructions so import cycles stay broken. LeptonGenerations.Necessity then states the forcing claim: muon and tau are not free fits but consequences of T9 plus those geometric constants.
The module-level note records the concrete muon window obtained by interval propagation through structural mass and $\varphi^{\mathrm{residue}}$: predicted mass in $(105,107),\mathrm{MeV}$ against the PDG value $105.6583755,\mathrm{MeV}$, max relative error about $1.3%$.
proof idea
This is a thin facade module: it imports Mathlib, the Defs layer, and the Necessity layer, then exposes the mass-bound theorems and residual step hypotheses as the public T10 surface. Substantive argument lives in Necessity, which replaces earlier axioms by proven inequalities via interval arithmetic on the phi-ladder expressions. No independent proof body sits at the module root.
why it matters in Recognition Science
T10 is the lepton-generation step after T9 (electron mass) in the RS particle-mass program. Closing muon and tau by forcing, rather than by axiom, removes two free parameters from the generation ladder and ties the observed MeV values to the same $\varphi$-structure that yields the eight-tick octave and $D=3$. Downstream mass and coupling work can cite the predicted windows and the necessity theorems instead of open hypotheses. Sibling surfaces include the muon/tau prediction bounds and the residual step hypotheses that Necessity aims to discharge.
scope and limits
- Does not derive the electron mass; that is T9 input.
- Does not treat quark or neutrino generation ladders.
- Does not claim sub-percent muon precision beyond the stated ~1.3% window.
- Does not itself contain the interval proofs; those live in Necessity.
- Does not fix absolute MeV units without the electron yardstick.