Z_down_with_offset
plain-language theorem explainer
Specializes the quark-sector Z-map at the integerized down charge Q̃ = −2, keeping a symbolic color offset c and even-polynomial coefficients a, b. Anyone matching topology-compatible Z-values to anchor outputs (or to the full anchor tuple 1332/276/24) cites this branch. The body is a one-line abbreviation of the general quark-with-offset formula.
Claim. For integers $c,a,b$, the down-quark band label is $Z_{\mathrm{down}}(c,a,b) := c + a\tilde{Q}_d^2 + b\tilde{Q}_d^4$, where $\tilde{Q}_d = -2$ is the face-count integerization $6\cdot(-1/3)$ of the down-quark charge.
background
This module derives the charge-to-band polynomial $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without anchor or mass data. Stage 1 integerizes SM charges by the face count $F=2D=6$ at $D=3$, so $\tilde{Q}=6Q\in\mathbb{Z}$. For the down quark $Q=-1/3$ one gets $\tilde{Q}_d=-2$.
Stage 2 forces the minimal even non-negative form $Z=a\tilde{Q}^2+b\tilde{Q}^4$ (charge-conjugation invariant, $Z(0)=0$). Stage 3 adds a quark color offset $c$ from $2^{D-1}$ edge channels: $Z_{\mathrm{quark}}=c+a\tilde{Q}^2+b\tilde{Q}^4$. The sibling Z_quark_with_offset is exactly that extension of the bare even polynomial; the present definition plugs in $\tilde{Q}_d$.
The mass-layer anchor map uses the same shape for the down sector: $4+(Q_6)^2+(Q_6)^4$ with $Q_6=6Q$, i.e. the specialized case $c=4$, $a=b=1$.
proof idea
Definitional one-liner: apply the quark-sector formula (color offset $c$ plus even degree-$\le 4$ polynomial in $\tilde{Q}$) at the fixed integer $\tilde{Q}_d=-2$. No tactics, no lemmas.
why it matters
Closes the down-quark slot of the topology-compatible family used to force the canonical coefficients. Downstream, full_anchor_tuple_forces_coefficients_and_offset assumes $Z_{\mathrm{down}}(c,a,b)=24$ together with lepton $1332$ and up $276$, and concludes $(a,b,c)=(1,1,4)$. The mass-layer bridge canonical_tuple_forced_from_anchor_outputs does the same against the Paper-1 anchor outputs for lepton/up/down sectors.
In the RS chain this is Stage 3 of the Z-map derivation: color offset $c=2^{D-1}=4$ at $D=3$ (T8), sitting on the face-count integerization $F=6$ and the unique even polynomial $a=b=1$ from family separation. Without a named down branch, the three-sector forcing theorems cannot state their hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.