IndisputableMonolith.Physics.LeptonGenerations
The LeptonGenerations module supplies proven interval bounds on the predicted muon mass derived from structural mass and phi-residue propagation. Physicists verifying Recognition Science lepton predictions would cite these bounds to confirm the T10 forcing step. The module achieves the result by importing separated definitions and necessity proofs that convert prior axioms into verified inequalities with relative error below 2%.
claimThe principal result states that the predicted muon mass lies in the open interval $(105,107)$ (MeV units), with experimental value $105.6583755$ MeV and maximum relative error approximately $1.3\% < 2\%$.
background
The module occupies the T10 position in the Recognition Science forcing chain. It imports LeptonGenerations.Defs, which isolates core lepton mass definitions to break import cycles, and LeptonGenerations.Necessity, whose doc states: "This module proves that the muon and tau masses are forced from T9 (electron mass) and the geometric constants derived in earlier theorems. Goal: Replace the two axioms in LeptonGenerations.lean with proven inequalities."
Definitions in Defs encode the phi-ladder mass formula and J-cost propagation; Necessity supplies the interval arithmetic that yields the muon bound from the electron mass and residue terms.
proof idea
This module contains no local proofs or signatures. It assembles the imported Defs and Necessity modules so that the muon mass bounds become visible at the top level.
why it matters in Recognition Science
The module closes the T10 lepton ladder by converting two axioms into proven inequalities, completing the step that follows T9 electron mass. It supplies the concrete bounds required by downstream mass-prediction theorems in the Recognition framework.
scope and limits
- Does not derive the electron mass (T9).
- Does not treat quark or boson masses.
- Does not claim exact mass values, only verified intervals.
- Does not address higher-generation mixing angles.