IndisputableMonolith.Physics.LeptonGenerations
This module aggregates the T10 results on lepton generations by importing definitions and necessity proofs. It establishes that muon and tau masses are forced from the electron mass and geometric constants, yielding a proven interval bound for the muon mass. Particle physicists modeling lepton hierarchies would cite these results to replace prior axioms with derived inequalities. The module structure isolates definitions to avoid cycles while the necessity submodule supplies the forcing arguments.
claimThe predicted muon mass satisfies $105 < m_μ < 107$ (MeV), with experimental value 105.6583755 MeV and maximum relative error ≈1.3% < 2%.
background
The module organizes T10 lepton generation results in the Physics domain. Its Defs submodule supplies core definitions for lepton mass derivations, isolated to break import cycles. The Necessity submodule proves the muon and tau masses are forced from T9 (electron mass) and geometric constants derived earlier in the forcing chain.
proof idea
This is a module that imports the definitions and necessity submodules; it contains no direct proofs itself but aggregates the results on forced lepton masses.
why it matters in Recognition Science
This module supplies the proven bounds for the second and third generation lepton masses, completing the T10 step in the unified forcing chain. It feeds higher-level mass predictions by replacing two axioms with derived inequalities, as stated in the Necessity documentation. The results connect to the phi-ladder mass formula and phi-residue interval propagation.
scope and limits
- Does not derive the electron mass (handled in T9).
- Does not address quark masses or other sectors.
- Does not claim exact mass equality beyond the stated error bound.
- Does not extend to higher generations or mixing angles.