charm_rung
plain-language theorem explainer
The charm_rung definition fixes the second-generation up-type quark at integer position 17 on the φ-ladder. Modelers of quark masses via geometric progression cite it to place charm between strange (rung 14) and bottom (rung 22) in the six-quark hierarchy. The definition is a direct constant assignment with no computation or lemmas.
Claim. The charm quark occupies rung $k_c = 17$ on the φ-ladder, yielding mass $m_c = m_0 · φ^{17}$ where $m_0 = φ^{-5}/8$ and the full set of rungs is $u:8$, $d:9$, $s:14$, $c:17$, $b:22$, $t:30$.
background
The CKMHierarchyFromPhiLadder module treats quark masses as points on the φ-ladder forced by recognition geometry. Module documentation states that the six quarks sit at rungs u:8 (lightest charged-fermion bond), d:9, s:14 (=8+6), c:17 (=8+9, bond + parity-count), b:22 (=8+14), t:30 (=8+22), with masses given by $m_0 · φ^k$ and $m_0 = E_{coh}/8 = φ^{-5}/8$. Upstream rung maps in RSBridge.Anchor and AnchorPolicy supply the general Fermion-to-integer assignment, but this module specializes the values to close the hierarchy statements.
proof idea
Direct definition: charm_rung is the literal natural number 17. No lemmas or tactics are invoked; the declaration simply names the constant for downstream ordering and ratio proofs.
why it matters
This supplies the charm rung required by CKMHierarchyFromPhiLadderCert and the ckm_hierarchy_one_statement theorem, which assert six-quark structure, strict ordering u < d < s < c < b < t, and per-rung mass ratio exactly φ. It fills Track F7 of the Recognition Science plan, where the φ-ladder (T6 fixed point) generates the observed hierarchy without free parameters. The assignment 17 = 8 + 9 follows the bond + parity-count rule stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.