ConventionA_Rungs
plain-language theorem explainer
Canonical integer rung bundle for the six quarks under Convention A: up-type (u,c,t)=(4,15,21) and down-type (d,s,b)=(4,15,21). Cited by anyone auditing the dual-coordinate quark mass pipeline or comparing core rungs to the quarter-ladder hypothesis. Plain structure with default field values; no proof content.
Claim. Convention A fixes integer rungs $u=4$, $c=15$, $t=21$ (up-type) and $d=4$, $s=15$, $b=21$ (down-type). The heavier rungs decompose as generation torsion offsets above the light base: $15=4+11$ and $21=4+17$.
background
The Quark Sector Audit module formalizes a dual-coordinate blocker: two coexisting quark rung conventions that are not mathematically equivalent and have not been merged into one forward, parameter-free pipeline.
Convention A is the canonical integer-rung model (from the mass-anchor layer). Masses obey $m=\mathrm{yardstick}(\mathrm{Sector})\times\varphi^{r-8+\mathrm{gap}(Z)}$, with up-type and down-type sharing the rung triple ${4,15,21}$ but different sector yardsticks. Inline comments mark $15=4+11$ and $21=4+17$ as gen-2 and gen-3 torsion offsets.
Convention B (quarter-ladder residues anchored to PDG targets) coexists and is explicitly not claimed equivalent. This structure freezes the Convention A integers as the audit reference.
proof idea
Definition only: a structure with six $\mathbb{Z}$ fields and default values $u=d=4$, $c=s=15$, $t=b=21$. No tactics, no lemmas. Instantiation yields those defaults; comments record the torsion split of the heavier rungs.
why it matters
Audit-side snapshot of the core-model rungs used by the $\varphi$-ladder mass law. The module states Convention A is canonical and parameter-free (cube geometry), while Convention B is hypothesis-level and PDG-tied; the two are "NOT meant to be mathematically equivalent." Sibling audit objects (reconciliation proof status, accuracy checks) need a fixed Convention A reference. Until one forward coordinate system replaces the dual setup, end-to-end "correct for all fermions" is not defensible. Ties directly to the RS mass formula $m=\mathrm{yardstick}\times\varphi^{r-8+\mathrm{gap}(Z)}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.