pith. sign in
module module high

IndisputableMonolith.Masses.TopQuarkMassScoreCard

show as:
view Lean formalization →

The TopQuarkMassScoreCard module consolidates the top quark mass scorecard, recording theorem-grade facts and open residuals for the heaviest quark in the Recognition Science framework. Researchers verifying mass predictions against PDG data cite it to check sector consistency. It follows the QuarkScoreCard pattern by importing verification tools and defining specific rows for PDG values and band checks without new derivations.

claimThe top quark mass scorecard certification asserts that the predicted top quark mass lies within the PDG experimental band, with auxiliary rows recording the PDG value in MeV, positivity, ordering relative to charm, and in-band status.

background

This module sits in the masses domain and imports QuarkScoreCard, which consolidates phase 0 quark-sector facts from the physical derivation plan and tags residuals honestly without introducing new physics. It also imports Verification, which compares RS mass predictions to PDG values while treating experimental numbers as imported constants rather than derived quantities. The module defines concrete rows for the top quark (PDG mass in MeV, positive value, order, and in-band scorecard) plus the certification object TopQuarkMassScoreCardCert.

proof idea

This is a definition module, no proofs. It assembles rows for PDG top mass in MeV, positivity, charm comparison, ordering, in-band scorecard status, and certifies the overall scorecard via a direct declaration that the certification holds.

why it matters in Recognition Science

The module supplies the top-quark specialization required by the parent QuarkScoreCard, which consolidates all quark-sector facts for the Recognition Science mass ladder. It supports verification of the phi-ladder mass formula against the heaviest quark without adding new derivations or closing open residuals.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)