module module high

`IndisputableMonolith.Masses.QuarkScoreCard`

The QuarkScoreCard module organizes the P0-Q structural rows for up and down quarks on the phi-ladder, including the proved ratio m_c / m_u = φ^11. Researchers deriving fermion masses from the recognition framework would cite it when building absolute bridge scorecards. The module supplies ZOf mappings, generation spacing lemmas, and equal-Z relations as definitions that downstream modules import directly.

claimThe P0-Q structural row states that the charm-to-up quark mass ratio satisfies $m_c / m_u = φ^{11}$, with analogous relations for top-up, strange-down, and bottom-down pairs obtained from the gap function $F(Z) = ln(1 + Z/φ)/ln(φ)$ on the phi-ladder.

background

This module belongs to the Masses domain and imports the RS time quantum τ₀ = 1 tick from Constants together with the canonical mass constants from Anchor. The RSBridge.Anchor supplies the core bridge: Fermion species, the charge-indexed Z_i = q̃² + q̃⁴ (+4 for quarks), the gap function F(Z), and massAtAnchor at the reference scale μ⋆. Verification supplies the machine-verified comparison layer but quarantines all PDG values as imported constants, not RS derivations.

proof idea

This is a definition module, no proofs. It assembles the P0-Q rows through a collection of sibling definitions (ZOf_up_quarks, ZOf_down_quarks, up_generation_spacing, down_generation_spacing, row_charm_up_ratio, row_top_charm_ratio, row_top_quark_in_band) that encode the equal-Z and generation-spacing relations required by the phi-ladder mass formula.

why it matters in Recognition Science

The module supplies the quark-side foundations for QuarkAbsoluteBridgeScoreCard (which deepens the P0-Q01..P0-Q06 rows from the physical derivation plan) and is imported by ChargedLeptonMassScoreCard and TopQuarkMassScoreCard. It thereby links the J-uniqueness fixed point and eight-tick octave structure to concrete quark ratios such as the proved m_c / m_u = φ^11.

scope and limits

Does not claim numerical agreement with measured quark masses.
Does not derive absolute mass values, only structural ratios on the phi-ladder.
Does not address neutrino or charged-lepton mass rows.
Does not import or use experimental PDG data inside its definitions.

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Masses.ChargedLeptonMassScoreCard module_import
IndisputableMonolith.Masses.QuarkAbsoluteBridgeScoreCard module_import
IndisputableMonolith.Masses.TopQuarkMassScoreCard module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Masses.Anchor module_import
IndisputableMonolith.Masses.RSBridge.Anchor module_import
IndisputableMonolith.Masses.Verification module_import

declarations in this module (21)

theorem ZOf_up_quarks L47
theorem ZOf_down_quarks L50
theorem ZOf_charged_leptons L53
theorem charm_up_equal_Z L58
theorem top_up_equal_Z L62
theorem strange_down_equal_Z L66
theorem bottom_down_equal_Z L70
theorem up_generation_spacing L77
theorem down_generation_spacing L82
theorem row_charm_up_ratio L93
theorem row_top_charm_ratio L99
theorem row_top_quark_in_band L105
theorem row_quark_preds_pos L111
theorem row_electron_pct L125
theorem row_muon_pct L131
theorem row_tau_pct L137
theorem row_muon_electron_ratio_pct L143
theorem row_tau_electron_ratio_pct L149
def QuarkAbsoluteMassResidual L172
structure QuarkScoreCardCert L184
theorem quarkScoreCardCert_holds L208