quark_rungs_strict_ordering
plain-language theorem explainer
Quark rungs on the phi-ladder obey the strict chain 8 < 9 < 14 < 17 < 22 < 30. Model builders in Recognition Science cite this to anchor the CKM mass hierarchy. The proof reduces each inequality to numerical comparison after unfolding the rung constants.
Claim. $8 < 9 land 9 < 14 land 14 < 17 land 17 < 22 land 22 < 30$, where the integers label the up, down, strange, charm, bottom and top quark rungs respectively.
background
The module assigns the six quarks to fixed rungs on the phi-ladder: up at 8, down at 9, strange at 14, charm at 17, bottom at 22, top at 30. These integers arise from the SU(3) times SU(2) times U(1) gauge structure on the third generation, as stated in the module documentation. The Mass type is an abbreviation for real numbers imported from RSNativeUnits, while rung itself is a basic natural-number definition from Compat.Constants.
proof idea
A term-mode proof that refines the five-fold conjunction into separate goals. Each goal is discharged by unfolding the pair of relevant rung definitions followed by norm_num to confirm the concrete integer inequality.
why it matters
It supplies the strict-ordering clause inside the CKMHierarchyFromPhiLadderCert structure. That certificate is built in ckmHierarchyFromPhiLadderCert and invoked by ckm_hierarchy_one_statement to obtain the single-statement hierarchy theorem. The result confirms monotonicity of the phi-ladder mass formula, which supports the phi^22 top-to-up ratio and aligns with the phi fixed point and eight-tick octave from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.