IndisputableMonolith.RRF.Physics.LeptonGenerations
This module assembles definitions and necessity proofs for lepton generations under the Recognition framework. It delivers proven bounds showing the predicted muon mass lies in (105, 107) MeV with relative error below 2 percent, obtained via interval propagation from structural mass and phi-residue. The module imports core definitions and necessity results to replace earlier axioms with derived inequalities, building directly on T9 electron mass.
claimThe module establishes the interval bound $105 < m_μ < 107$ (in MeV) for the predicted muon mass, with $m_μ = 105.6583755$ MeV and maximum relative error approximately 1.3 percent, derived from structural mass and φ-residue propagation.
background
The module imports LeptonGenerations.Defs, which supplies the core definitions for lepton mass derivations separated from theorems to break import cycles. It further imports LeptonGenerations.Necessity, whose goal is to prove that muon and tau masses are forced from T9 (the electron mass) together with geometric constants derived earlier. This places the work inside the T10 step of the Recognition Science chain, where lepton generations follow from the phi-ladder and J-cost structure.
proof idea
The module is an assembler that imports the definitions module and the necessity module. It relies on interval propagation from structural_mass and φ-residue to obtain the stated bounds, with the necessity component discharging the prior axioms by deriving the required inequalities from T9 and the geometric constants.
why it matters in Recognition Science
This module completes the T10 Lepton Generations step by converting two earlier axioms into proven inequalities. It feeds the derived lepton mass bounds into higher-level Recognition Science derivations that use the full phi-ladder and eight-tick structure. The necessity component directly addresses the goal of replacing axioms in LeptonGenerations.lean with forced relations from prior theorems.
scope and limits
- Does not derive the electron mass itself (relies on T9).
- Does not provide explicit numerical predictions for the tau mass.
- Does not address neutrino masses or mixing angles.
- Does not extend the derivation to quark generations.