IndisputableMonolith.Physics.LeptonGenerations
This module assembles the definitions and necessity proofs for lepton generations under Recognition Science. It delivers proven bounds on the muon mass via interval propagation from structural mass and phi-residue, placing the prediction in (105, 107) MeV against the measured 105.658 MeV with relative error below 2 percent. Physicists deriving the lepton spectrum from the phi-ladder cite these results to replace earlier axioms. The module structure imports Defs and Necessity to enforce separation of definitions from forcing arguments.
claimThe module establishes the bounds $105 < m_μ < 107$ (MeV) on the predicted muon mass, obtained by propagating the structural mass formula through the φ-residue on the phi-ladder, with measured value 105.6583755 MeV and maximum relative error ≈1.3 percent.
background
Recognition Science derives lepton masses from the phi-ladder anchored at the electron mass (T9). The imported Defs module supplies the core structural_mass and residue functions that break import cycles. The Necessity module proves the muon and tau masses are forced by the geometric constants and J-uniqueness from T5, replacing two prior axioms with explicit inequalities. The present module serves as the T10 entry point that exposes these results to downstream physics derivations.
proof idea
This is an assembler module with no internal proofs. It imports the definitions from Defs and the forcing theorems from Necessity, exposing the lepton-generation results at the top level while preserving import hygiene.
why it matters in Recognition Science
The module supplies the T10 lepton-generation results that feed higher-level spectrum calculations. It completes the step that replaces the original axioms in LeptonGenerations.lean with proven inequalities derived from the phi-ladder and eight-tick octave (T5-T8). Downstream work on particle masses therefore rests on these bounds rather than ad-hoc inputs.
scope and limits
- Does not derive the electron mass, which enters from T9.
- Does not treat quark masses or baryon generations.
- Does not supply exact closed-form values, only interval bounds.
- Does not perform direct experimental fitting beyond the stated error check.