IndisputableMonolith.RRF.Physics.LeptonGenerations
This module supplies proven bounds on the predicted muon mass in the Recognition Science framework, placing it in (105, 107) MeV with relative error at most 1.3 percent. Physicists deriving lepton masses from the phi-ladder cite these results to replace earlier axioms with derived inequalities. The bounds follow from interval propagation applied to structural_mass and phi-residue terms.
claimThe predicted muon mass satisfies $105 < m_μ^{pred} < 107$ (MeV units), with maximum relative deviation from the experimental value 105.6583755 MeV of approximately 1.3 percent.
background
The module aggregates results from two upstream modules. IndisputableMonolith.Physics.LeptonGenerations.Defs isolates the core structural definitions for lepton mass derivations to break import cycles. IndisputableMonolith.Physics.LeptonGenerations.Necessity proves that muon and tau masses are forced from T9 (electron mass) and the geometric constants derived in earlier theorems, with the explicit goal to replace the two axioms in LeptonGenerations.lean with proven inequalities. The setting uses the phi-ladder, structural_mass, and phi-residue from the Recognition Science forcing chain.
proof idea
This module imports the Defs and Necessity submodules and exposes the muon mass bounds. The bounds are obtained by interval propagation from structural_mass and phi-residue; the module itself contains no independent proofs and serves as the aggregation point for the T10 results.
why it matters in Recognition Science
The module advances T10 lepton generations by delivering the proven muon mass interval, directly fulfilling the Necessity module goal of replacing axioms with theorems. It supplies the concrete bounds (105, 107) with error below 2 percent that higher-level RRF derivations rely upon.
scope and limits
- Does not derive the exact experimental mass value.
- Does not address tau lepton mass predictions.
- Does not include the electron mass derivation (taken from T9).
- Does not extend to non-lepton particles.