pith. sign in
module module high

IndisputableMonolith.Masses.MuRatioScoreCard

show as:
view Lean formalization →

The MuRatioScoreCard module supplies the CODATA 2022 proton-electron mass ratio data together with model predictions and a holding certificate inside the Recognition Science mass framework. Researchers verifying phi-ladder mass predictions against experiment would reference its bracket and relative-error definitions. The module is purely definitional and imports its supporting constants and verification machinery without proofs.

claimThe certificate asserts that the model prediction for the proton-electron mass ratio lies inside the bracket formed by the CODATA 2022 value and the positive/lower/upper bounds derived from the Recognition Science mass ladder.

background

The Anchor module centralizes canonical mass constants derived from first principles along the Recognition Science derivation chain. The Verification module supplies machine-verified comparison machinery while treating experimental values as imported constants rather than RS-derived quantities. Constants supplies the base RS time quantum τ₀ = 1 tick. This module applies those tools to the specific proton-electron mass ratio using CODATA 2022 data.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the concrete scorecard and certificate for the proton-electron mass ratio comparison. It supports the broader mass-prediction verification workflow described in the Verification module and the derivation chain in Anchor. No downstream theorems are recorded as users.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (11)