pith. sign in
module module moderate

IndisputableMonolith.Masses.QuarkVerification

show as:
view Lean formalization →

QuarkVerification assembles the experimental mass values for the six quarks along with up and down sector parameters for use in Recognition Science mass comparisons. Researchers auditing RS phi-ladder predictions against PDG data cite these constants when checking the quark sector. The module is entirely definitional, importing from Anchor and Verification with no theorems or proofs present.

claimThe module defines the experimental quark masses $m_u^exp$, $m_d^exp$, $m_s^exp$, $m_c^exp$, $m_b^exp$, $m_t^exp$ and the sector parameters $r_{up}$, $r_{down}$ together with positivity and spacing statements for the quark mass ladder.

background

The module sits in the Masses domain and imports the RS time quantum τ₀ = 1 tick from Constants. Anchor supplies the canonical, parameter-free mass constants derived from first principles via the phi-ladder and the mass formula yardstick · ϕ^(rung − 8 + gap(Z)). Verification provides the comparison framework while explicitly quarantining experimental values as imported constants rather than RS derivations.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the quark-specific experimental anchors required for the mass verification pipeline. It feeds the broader Recognition Science mass predictions by providing the up and down generation spacing and positivity statements that allow direct comparison of RS-derived values against PDG data in the quark sector.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (17)