pith. sign in
module module high

IndisputableMonolith.Masses.MuRatioScoreCard

show as:
view Lean formalization →

The MuRatioScoreCard module supplies CODATA 2022 data and RS model predictions for the muon mass ratio together with comparison predicates and a certification object. Researchers checking mass spectra consistency in Recognition Science reference these definitions. The module consists entirely of definitions with no proof content.

claimDefines the CODATA 2022 muon mass ratio $\mu_{\rm codata}$, the RS prediction $\mu_{\rm pred}$, positive and bracketed variants, the relative error, and the certificate asserting the prediction lies inside the CODATA interval.

background

The module sits in the Masses domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants. Anchor centralises the parameter-free constants described in the mass manuscripts; everything lives in the Model layer and no proofs claim experimental agreement. Verification supplies the comparison protocol while stating that experimental values are imported constants, not derived from RS: "QUARANTINED from the certified surface: experimental values are imported constants, not derived from RS."

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module feeds the mass prediction verification layer by supplying the muon ratio scorecard. It supports the Anchor goal of centralising parameter-free constants and the Verification module's machine-verified comparison without entering the certified surface.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (11)