pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Masses.ChargedLeptonMassScoreCard

show as:
view Lean formalization →

The ChargedLeptonMassScoreCard module records theorem-grade status for electron, muon, and tau mass relations in Recognition Science units. It defines relative rows and ratio facts then aggregates them under a single certificate. Researchers verifying lepton mass hierarchies against the phi-ladder cite it to separate proved claims from residuals. The module consists of row definitions plus a top-level certificate declaration with no internal proofs.

claimThe scorecard certifies the verified status of charged-lepton mass rows $m_e$, $m_μ$, $m_τ$ and their ratios, each expressed on the phi-ladder with J-cost adjustments, together with the aggregate proposition ChargedLeptonMassScoreCardCert.

background

Recognition Science places fermion masses on the phi-ladder using rung and gap(Z) offsets applied to the base yardstick. The J-cost function J(x) = (x + x^{-1})/2 - 1 supplies the defect measure, while Constants supplies the fundamental time quantum τ₀ = 1 tick. This module mirrors the structure of QuarkScoreCard, which consolidates quark-sector facts without introducing new physics, and draws comparison machinery from Verification while keeping PDG values quarantined as external constants.

proof idea

This is a definition module, no proofs. It introduces the sibling row definitions row_electron_rel, row_muon_rel, row_tau_rel together with the ratio facts and the aggregate certificate ChargedLeptonMassScoreCardCert, whose holding is declared separately.

why it matters in Recognition Science

The module supplies the lepton-sector ledger that completes the fermion scorecard alongside QuarkScoreCard. It feeds the mass verification pipeline and records which relations reach theorem grade versus which remain open, directly supporting the T5-T8 forcing chain mass formula. It touches the residual question of full spectrum closure from the eight-tick octave and D = 3.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (7)