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

IndisputableMonolith.Masses.QuarkVerification

show as:
view Lean formalization →

QuarkVerification defines experimental quark mass values and up/down sector parameters in RS-native units for the Masses domain. Researchers comparing phi-ladder predictions to PDG data cite these constants. The module holds only definitions and positive assertions with no theorems.

claimExperimental masses $m_u^{exp}$, $m_d^{exp}$, $m_s^{exp}$, $m_c^{exp}$, $m_b^{exp}$, $m_t^{exp}$ and sector parameters $r_{up}$, $r_{down}$ with positivity assertions.

background

The module resides in the Masses domain and imports the RS time quantum τ₀ = 1 tick from Constants. Anchor supplies the canonical mass constants derived from first principles via its derivation chain. Verification frames the PDG comparison while quarantining experimental inputs as imported constants outside the certified RS surface.

proof idea

This is a definition module, no proofs. It aggregates value definitions for the six quark masses and the two sector parameter sets together with positivity statements.

why it matters in Recognition Science

QuarkVerification supplies the experimental anchors required for quark-sector verification in the mass manuscripts. It feeds the broader mass-prediction pipeline that applies the phi-ladder formula and the eight-tick octave structure.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)