up_generation_spacing
plain-language theorem explainer
The declaration records that rung integers for up-type quarks differ by 11 between charm and up, and by 17 between top and up. Mass modelers cite these fixed spacings when locating quarks on the phi-ladder inside the scorecard. The proof reduces to a single decide tactic that evaluates the concrete integer definitions from the Anchor module.
Claim. Let $r$ be the rung function on up-type quarks with $r(u)=4$, $r(c)=15$, $r(t)=21$. Then $r(c)-r(u)=11$ and $r(t)-r(u)=17$.
background
The Quark Score Card module consolidates proved facts about quark rungs without introducing new physics. The rung function $r_up$ is defined in the Anchor module by the assignments $r_up(u)=4$, $r_up(c)=4+tau(1)$, $r_up(t)=4+tau(2)$, where the tau increments are taken from the integer sequence in Anchor. These values produce the exact differences 11 and 17 that appear in the theorem statement. The upstream Anchor definition supplies the explicit mapping, while the QuarkVerification sibling re-derives the same spacing via simp and omega.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the decidable equality on the concrete rung integers.
why it matters
This spacing populates the rung_spacing_up field inside the QuarkVerificationCert constructed in the sibling QuarkVerification module. It supports the scorecard claim that charm/up equals phi to the 11 and top/charm equals phi to the 6. The differences align with the phi-ladder steps used for mass predictions in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.