generation_spacing_differs
plain-language theorem explainer
Generation spacings on the quark ladder disagree between the two coexisting coordinate conventions: integer-rung Convention A uses universal steps 11 then 6, while quarter-ladder Convention B uses 7.75, 2.5, and 5.5 along the heavy chain. Quark-sector auditors cite this as a concrete non-equivalence witness. The proof is the trivial inhabitant of True, recording the discrepancy as an audited fact rather than deriving the numbers.
Claim. The generation spacings of the two quark coordinate conventions are not the same. Under the integer-rung convention, $\Delta(\mathrm{gen}_1\to\mathrm{gen}_2)=11$ and $\Delta(\mathrm{gen}_2\to\mathrm{gen}_3)=6$ universally. Under the quarter-ladder convention the successive steps are $\mathrm{top}\to\mathrm{bottom}=7.75$, $\mathrm{bottom}\to\mathrm{charm}=2.5$, $\mathrm{charm}\to\mathrm{strange}=5.5$. These numerical sequences are disjoint.
background
The Quark Sector Audit module records the main blocker to an end-to-end fermion mass claim: two coexisting quark coordinate systems that are not mathematically equivalent and have not been folded into one forward pipeline.
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 in ${4,15,21}$ and sector yardsticks from the counting layer. Convention B (quarter-ladder) is a hypothesis layer: $m=m_e^{\mathrm{struct}}\times\varphi^R$ with $R\in\tfrac14\mathbb{Z}$ and residues such as top $=23/4$, bottom $=-8/4$, charm $=-18/4$.
The inductive Convention type in QuarkCoordinateReconciliation names the two systems (IntegerRung vs QuarterLadder). The reconciliation module states explicitly that the conventions are not meant to be equivalent. Generation spacing is one of the concrete numerical mismatches that make that non-equivalence visible.
proof idea
Term-mode proof of True by trivial. No arithmetic is performed and no upstream lemma about rung differences is invoked. The declaration is a documented audit marker: the doc-comment carries the numerical claim (A: steps 11 and 6; B: 7.75, 2.5, 5.5), while the Lean body only asserts that the discrepancy statement is recorded as a proved placeholder in the audit module.
why it matters
Inside the dual-coordinate problem, this item is one of the specific discrepancy witnesses (alongside different references and different rung types) that justify refusing a single unified, parameter-free quark mass derivation on the same footing as the lepton chain.
The mass formula on the $\varphi$-ladder is the framework landmark at stake: until one coordinate system and one forward pipeline replace the pair of conventions, "correct for all fermions" is not defensible. Convention B matches to PDG targets are explicitly outside the clean core prediction pipeline. No downstream theorem currently consumes this declaration; it feeds the audit narrative and the open reconciliation question rather than a parent proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.