Z_quark_with_offset
plain-language theorem explainer
Defines the quark-sector band label as a constant color offset plus the even charge polynomial aQ̃² + bQ̃⁴. Anyone deriving SM mass anchors or the topological Z-map cites it to separate quark from lepton sectors. The body is a one-line sum of the offset and the bare polynomial.
Claim. For integers $c,a,b$ and integerized charge $\tilde{Q}$, the quark-sector band map is $Z_{\mathrm{quark}}(c,a,b;\tilde{Q}) := c + a\tilde{Q}^{2} + b\tilde{Q}^{4}$.
background
This module derives the charge-to-band map $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without empirical mass anchors. Stage 1 fixes the integerization scale $\tilde{Q}=FQ$ with face count $F=6$ at $D=3$ (T8). Stage 2 forces an even non-negative polynomial vanishing at zero: the minimal form is $Z=a\tilde{Q}^{2}+b\tilde{Q}^{4}$.
The sibling bare polynomial is exactly that form: $Z_{\mathrm{poly}}(a,b;\tilde{Q})=a\tilde{Q}^{2}+b\tilde{Q}^{4}$. Stage 3 adds a sector-dependent constant for color. Quarks couple to $2^{D-1}$ extra edge channels on the cube, so the quark map is offset by a constant $c$ while leptons keep the bare polynomial. The intended physical value is $c=2^{D-1}=4$.
proof idea
Pure definitional abbreviation: return the sum of the integer offset $c$ and the already-defined even polynomial $aQ^{2}+bQ^{4}$. No lemmas or tactics.
why it matters
Stage 3 of the topological Z-map derivation: color offset separates quark and lepton bands while preserving charge-conjugation evenness of the polynomial part. Downstream, the up and down branches specialize this map at the integerized up/down charges, and the full-anchor theorem uses those branches to force $(a,b,c)=(1,1,4)$ from the tuple $(1332,276,24)$. That pins the RS mass-ladder band labels for quarks against the cube geometry ($D=3$, edge count $2^{D-1}=4$) rather than fit parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.