neutral_vanishes
plain-language theorem explainer
For any integer coefficients a and b, the even charge-to-band polynomial Z(Q̃)=a Q̃²+b Q̃⁴ evaluates to zero at Q̃=0. Anyone checking Stage 2 of the topological Z-map derivation cites this as the neutral-boundary constraint. The proof is a one-line simplification of the polynomial definition.
Claim. For all integers $a,b$, the even degree-$\leq 4$ polynomial $Z_{a,b}(\tilde{Q})=a\tilde{Q}^2+b\tilde{Q}^4$ satisfies $Z_{a,b}(0)=0$.
background
This module derives the Standard Model charge-to-band map $Z(\tilde{Q})$ from recognition topology on the 3-cube, without mass anchors. Stage 1 fixes the integerization scale $\tilde{Q}=FQ$ with face count $F=6$ at $D=3$. Stage 2 constrains the band label by three structural requirements: charge-conjugation invariance (evenness in $\tilde{Q}$), non-negativity, and vanishing on neutral boundaries.
The general candidate is the even polynomial with no constant term $Z_{\mathrm{poly}}(a,b;Q)=a Q^2+b Q^4$. Neutrality means $\tilde{Q}=0$: a recognition boundary carrying no electric charge should induce no band shift, so the constant term is forbidden and the polynomial must evaluate to zero at the origin. That is exactly the content of this lemma.
Downstream, Stage 3 adds the color offset $2^{D-1}=4$ for quarks, yielding the familiar lepton and quark formulas $Z=\tilde{Q}^2+\tilde{Q}^4$ and $Z=4+\tilde{Q}^2+\tilde{Q}^4$.
proof idea
One-line tactic proof: unfold Z_poly and simplify. Substituting $Q=0$ into $a Q^2+b Q^4$ yields $0$ immediately in $\mathbb{Z}$. No external lemmas are required.
why it matters
This discharges gauge constraint (G3) in Stage 2 of the Z-map topological derivation: neutral boundaries produce no band shift. The parent structure derivation_complete wires it in as the neutral_zero field of ZMapDerivation, alongside face-count integerization ($F=6$), charge-conjugation invariance, and family separation (which uniquely forces $a=b=1$).
In the broader Recognition framework the result sits under T8 ($D=3$ spatial dimensions): the 3-cube face count and edge channels that fix integerization and the color offset presuppose three dimensions. Without $Z(0)=0$, the minimal even polynomial would admit a free constant and family separation would no longer pin $(a,b)$ uniquely.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.