down_generation_spacing
plain-language theorem explainer
The rung function for down-type quarks satisfies s minus d equals 11 and b minus d equals 17. Quark mass modelers cite this to lock the phi-ladder assignments for the down sector in the scorecard. The proof is a single decide tactic that evaluates the explicit integer cases in the rung definition.
Claim. The rung differences for down-type quarks satisfy $r(s) - r(d) = 11$ and $r(b) - r(d) = 17$, where $r$ maps the labels d, s, b to the integers 4, 15, 21 on the phi-ladder.
background
The Quark Score Card module consolidates theorem-grade facts for the quark sector without new physics. It records rung integers via the r_down definition from Masses.Anchor: d at rung 4, s at 4 plus tau(1) equals 15, and b at 4 plus tau(2) equals 21. This draws directly from the phi-forcing structures and the anchor policy for mass ladders.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the explicit case analysis in the r_down definition, reducing the two integer subtractions to decidable arithmetic.
why it matters
This supplies the rung spacings consumed by down_generation_spacing and quark_verification_cert_exists in QuarkVerification. It fills the P0-Q row of the physical derivation plan by confirming rung differences from the tau function. In the Recognition framework it supports the phi-ladder consistent with T6 and the eight-tick octave, while the open question of absolute mass match including the gap(ZOf) correction remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.