pith. sign in
module module moderate

IndisputableMonolith.Masses.ChargedLeptonMassScoreCard

show as:
view Lean formalization →

The ChargedLeptonMassScoreCard module consolidates theorem-grade and residual facts for electron, muon, and tau masses under the Recognition Science phi-ladder. It mirrors the QuarkScoreCard structure by recording relative masses and ratios without new derivations. Mass-prediction researchers cite it to check lepton-sector status against the unified forcing chain. The module consists of row definitions plus a top-level certification.

claimThe scorecard certifies rows for electron relative mass, muon-electron ratio, tau-electron ratio, and the overall ChargedLeptonMassScoreCardCert under the RS mass formula $m = y_0 · ϕ^{r-8+gap(Z)}$.

background

The module sits in the Masses domain and imports the RS time quantum τ₀ = 1 tick from Constants. It follows the QuarkScoreCard pattern, which consolidates existing proofs for the quark sector and tags residuals honestly without introducing new physics. The Verification import supplies the machine-verified PDG comparison, explicitly quarantining experimental values as imported constants rather than RS derivations. Sibling rows define relative lepton masses and ratios on the phi-ladder.

proof idea

This is a definition module, no proofs. It assembles row definitions for the three charged leptons and their ratios, then packages them under a single certification object.

why it matters in Recognition Science

The module supplies the charged-lepton counterpart to the QuarkScoreCard, completing the lepton sector of the mass scorecard that feeds the Verification comparison. It fills the Phase-0 lepton rows of the PHYSICAL_DERIVATION_PLAN.md without advancing new chain steps T5-T8 or the Recognition Composition Law.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (7)