UnifiedQuarkSector
plain-language theorem explainer
Checklist of properties a single, non-circular quark mass sector must meet: one coordinate convention, a forward pipeline with no PDG in the loop, no PDG targeting of rungs or residues, lepton-chain footing, and all six masses from counting integers plus φ and α. Auditors of fermion-mass claims cite it when asking whether quarks match the lepton standard. It is a plain structure packing those five fields; no proof content.
Claim. A unified quark sector is a record consisting of one coordinate convention (either integer rungs or the quarter-ladder) together with four boolean requirements: a forward prediction pipeline from RS inputs to mass with no PDG in the loop; no PDG mass targets used when assigning rungs or residues; the same structural footing as the lepton chain; and all six quark masses predicted from counting-layer integers together with $\varphi$ and $\alpha$.
background
The module audits the dual-coordinate blocker in the quark mass sector. Convention A (integer rungs) is the canonical core model: masses follow $m = \mathrm{yardstick}(\mathrm{Sector}) \times \varphi^{r-8+\mathrm{gap}(Z)}$ with up-type and down-type rungs ${4,15,21}$ and sector yardsticks from the counting layer. Convention B (quarter-ladder) is a hypothesis module writing $m = m_e^{\mathrm{struct}} \times \varphi^R$ for $R \in \tfrac14\mathbb{Z}$ with fixed residues (top $23/4$, bottom $-8/4$, etc.) and explicitly uses PDG mass targets.
The two conventions are stated not to be mathematically equivalent. Until one coordinate system and one forward pipeline exist, "correct for all fermions" is not defensible. The inductive type QuarkConvention names the two options; this structure packages what unification would have to certify.
proof idea
No proof: this is a structure definition. The five fields are data (one convention tag and four booleans). Downstream status objects instantiate or refute the checklist; the declaration itself only names the required properties.
why it matters
This is the acceptance criterion for closing the quark dual-coordinate gap, the module's stated main blocker to an end-to-end mass claim. The lepton chain already sits on a single parameter-free φ-ladder footing; quarks do not yet. The structure makes that gap machine-checkable: a genuine unification must pick one convention, keep PDG out of assignment and prediction, match lepton footing, and predict all six masses from counting integers plus φ and α (RS-native mass formula landmarks). No downstream theorems currently consume it (used_by empty); siblings such as the current-status witness and the no-reconciliation flag are the intended consumers. It does not itself resolve Convention A versus B; it only states what resolution must look like.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.