Z_poly
plain-language theorem explainer
Defines the bare charge-to-band map as the even degree-4 polynomial Z(Q̃)=a Q̃² + b Q̃⁴ with no constant term. Mass and verification work cite it as the gauge-invariant form of the Z-map before color offset. The body is a one-line arithmetic definition.
Claim. For integer coefficients $a,b$ and integerized charge $\tilde{Q}$, set $Z(\tilde{Q}) := a\,\tilde{Q}^{2} + b\,\tilde{Q}^{4}$. This is the general even polynomial of degree at most $4$ with vanishing constant term.
background
The module derives the charge-to-band polynomial from recognition topology on the 3-cube, without empirical mass anchors. Stage 1 integerizes SM charges via the face count $F=2D=6$ at $D=3$, so $\tilde{Q}=FQ$ is integral for $Q\in{-1,2/3,-1/3}$. Stage 2 requires the band label $Z$ to be charge-conjugation even, non-negative, and zero on neutrals: $Z(\tilde{Q})=Z(-\tilde{Q})$, $Z\ge 0$, $Z(0)=0$.
Those constraints force an even polynomial with no constant term. The minimal degree-$\le 4$ form is exactly $Z=a\tilde{Q}^{2}+b\tilde{Q}^{4}$. A parallel definition in the mass baseline uses natural-number coefficients; here coefficients are integers so conjugation and ring identities apply directly. Family separation later pins $a=b=1$; quarks then add the color offset $2^{D-1}=4$.
proof idea
Pure definition: expand as $a\cdot Q^{2}+b\cdot Q^{4}$. No lemmas or tactics. Downstream proofs unfold it and finish by ring, norm_num, or omega.
why it matters
This is the Stage-2 skeleton of the topological Z-map derivation. It feeds charge-conjugation invariance (automatic for even powers), bare lepton/up/down values at $a=b=1$ ($1332$, $272$, $20$), family separation, ordered hierarchy, and the uniqueness theorems that force coefficients from quark bare anchors. The mass baseline reuses the same polynomial and proves strict increase for $a,b\ge 1$ (B-26).
In the broader chain it sits after T8 ($D=3$, face count six) and before the color-offset quark sector $Z=4+\tilde{Q}^{2}+\tilde{Q}^{4}$. The mass formula then places species on the $\varphi$-ladder via these band labels. Without this form, gauge invariance and neutral vanishing would not be built into the map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.