QuarkConvention
plain-language theorem explainer
Enumerates the two coexisting quark mass coordinate systems in Recognition Science: integer rungs (canonical, parameter-free, cube-geometry derived) versus quarter-ladder residues (hypothesis layer that fits PDG targets). Anyone auditing fermion-mass completeness or the dual-coordinate blocker cites this tag. It is a two-constructor inductive definition, not a proved equivalence.
Claim. There are exactly two named quark coordinate conventions: (A) the integer-rung system, in which masses follow $m = \mathrm{yardstick}(\mathrm{sector})\,\varphi^{r-8+\mathrm{gap}(Z)}$ with integer rungs; and (B) the quarter-ladder system, in which masses follow $m = m_e^{\mathrm{struct}}\,\varphi^{R}$ with $R\in\tfrac14\mathbb{Z}$. The type is the discrete choice between these two labels.
background
The Quark Sector Audit module records the main obstacle to an end-to-end fermion mass claim: two quark coordinate conventions coexist and are explicitly not treated as mathematically equivalent.
Convention A (integer rungs) is the core model from the mass-anchor and mass-law layer. Rungs for up-type and down-type are ${4,15,21}$; the formula is the standard RS yardstick times $\varphi^{r-8+\mathrm{gap}(Z)}$, with sector yardsticks from the counting layer. It is parameter-free and tied to cube geometry.
Convention B (quarter-ladder) lives in the hypothesis quark-masses module. Residues sit in $\tfrac14\mathbb{Z}$ (e.g. top $23/4$, up $-71/4$) and the formula is electron structural mass times $\varphi^R$. Assignments use PDG mass targets, so B is outside the clean core prediction pipeline. The mass formula landmark (yardstick $\times\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) is the A-side reference; B is a separate fitting coordinate.
proof idea
No proof body: this is an inductive type with two nullary constructors, IntegerRung and QuarterLadder, deriving Repr and DecidableEq. The constructors are labels only; mathematical content of each convention is documented in the module header and in the sibling structures that consume the tag.
why it matters
This tag is the coordinate field of UnifiedQuarkSector, the structure that states what a reconciled quark sector must provide: a single convention, a forward pipeline with no PDG in the loop, and no PDG targets in rung or residue assignment.
It exists because the audit treats the dual-coordinate problem as the principal blocker to "correct for all fermions." Downstream, choosing one constructor forces the rest of the audit to track whether the sector is still split (A core vs B hypothesis) or has been collapsed. Until reconciliation, claims that sit on the same footing as the lepton chain remain out of scope. The declaration does not itself close T5–T8 or the RCL; it only names which mass-ladder coordinate is in force when those landmarks are applied to quarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.