different_rung_types
plain-language theorem explainer
Not every rational equals an integer: the quarter-integer 23/4 is a concrete counterexample. Quark-sector auditors cite this to separate Convention A (integer rungs only) from Convention B (quarter-ladder residues such as top = 23/4). The proof is a short push-negation with witness 23/4 and an omega contradiction on 4n = 23.
Claim. It is false that every rational $r \in \mathbb{Q}$ equals some integer $n \in \mathbb{Z}$. In particular, the quarter-integer $23/4$ (the Convention B top residue) is not an integer, so the two quark rung conventions use genuinely different rung types.
background
The Quark Sector Audit module records the dual-coordinate blocker: two coexisting quark rung conventions that are not mathematically equivalent and have not been reconciled into one forward pipeline.
Convention A (canonical core) uses integer rungs from cube geometry, with mass $m = \mathrm{yardstick}(\mathrm{Sector}) \times \varphi^{r-8+\mathrm{gap}(Z)}$ and up/down-type rungs in ${4,15,21}$. Convention B (hypothesis module) uses a quarter-ladder $R \in \tfrac14\mathbb{Z}$ with residues such as top $= 23/4$, bottom $= -8/4$, charm $= -18/4$, and fits PDG targets rather than a parameter-free derivation.
The module doc states the conventions are "NOT meant to be mathematically equivalent." This lemma isolates one elementary mismatch: B's residues are not all integers, while A's rungs are.
proof idea
Push the universal quantifier to an existential: it suffices to exhibit one rational with no integer equal. Take the witness $r = 23/4$ (Convention B's top residue). Assume $23/4 = n$ for some $n \in \mathbb{Z}$. Clear the denominator by linarith to get $4n = 23$ over $\mathbb{Q}$, cast to $\mathbb{Z}$, and finish with omega (4 does not divide 23). No external RS lemmas are required; the argument is pure arithmetic.
why it matters
This is a small but explicit audit fact in the dual-coordinate problem: until quark masses sit on one coordinate system with one forward pipeline, "correct for all fermions" is not defensible on the same footing as the lepton chain. The doc-comment pins the point: Convention B needs quarter-integers; Convention A uses only integers. Sibling audit lemmas (different references, generation spacing differs, no reconciliation yet) build the same case. Downstream use is currently empty; the lemma stands as a named non-equivalence brick rather than a mass-formula input. It does not touch T5–T8 or the RCL; it only polices the quark coordinate split that blocks end-to-end fermion claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.