module module high

`IndisputableMonolith.Foundation.CKMHierarchyFromPhiLadder`

This module defines the canonical six-quark structure of three generations with two isospin partners each, realized as rung assignments on the phi-ladder. Particle physicists modeling quark masses and CKM mixing would cite these assignments when connecting Recognition Science to the standard model flavor sector. The module consists of successive definitions and ordering lemmas that fix the rung values and derive the geometric mass progression.

claimThe module introduces the six quarks $u,d,s,c,b,t$ as a canonical structure with three generations and two isospin partners, each assigned a rung $r$ on the $\phi$-ladder satisfying the mass formula $m = ext{yardstick} imes \phi^{r-8+ ext{gap}(Z)}$.

background

Recognition Science places all masses on a discrete phi-ladder whose steps are fixed by the J-cost function $J(x) = (x + x^{-1})/2 - 1$ and the Recognition Composition Law. The module imports the fundamental time quantum $ au_0 = 1$ tick from Constants and the cost machinery from Cost. It then enumerates the six quarks via the listed sibling definitions, each tying a flavor to a specific rung while enforcing the strict ordering required by the three-generation pattern.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the rung assignments that feed the CKM hierarchy construction from the phi-ladder. It realizes the canonical six-quark structure required for the three-generation model, linking directly to the phi-ladder mass formula and the eight-tick octave structure of the framework.

scope and limits

Does not compute numerical CKM matrix elements.
Does not derive the underlying mass formula or J-cost.
Does not address lepton masses or mixing.
Does not include explicit gap(Z) values for each quark.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (20)

def quark_count L93
theorem quark_count_eq L95
def up_rung L98
def down_rung L101
def strange_rung L104
def charm_rung L107
def bottom_rung L110
def top_rung L114
theorem quark_rungs_strict_ordering L119
def mass_at_rung L135
theorem mass_at_rung_pos L137
theorem mass_geometric L143
theorem mass_strict_increasing L150
def mass_ratio_top_up L161
theorem mass_ratio_top_up_pos L163
theorem mass_ratio_top_up_above_30000 L170
theorem mass_ratio_top_up_pos_band L196
structure CKMHierarchyFromPhiLadderCert L218
def ckmHierarchyFromPhiLadderCert L237
theorem ckm_hierarchy_one_statement L257