charge_conjugation_invariant
plain-language theorem explainer
The charge-to-band polynomial Z(Q̃)=a Q̃²+b Q̃⁴ is even: flipping the sign of the integerized charge leaves Z unchanged. Anyone checking Stage-2 gauge invariance of the topological Z-map cites this. The proof unfolds the definition and finishes by ring arithmetic on even powers.
Claim. For all integers $a,b,Q$, the band polynomial $Z(Q)=a Q^{2}+b Q^{4}$ satisfies $Z(Q)=Z(-Q)$.
background
This module derives the charge-to-band map $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without mass anchors. Stage 1 fixes the integerization scale $\tilde{Q}=FQ$ with $F=6$ at $D=3$. Stage 2 constrains the band label by three gauge axioms: (G1) charge-conjugation invariance $Z(\tilde{Q})=Z(-\tilde{Q})$, (G2) non-negativity, (G3) vanishing at neutral charge.
The local object is the general even degree-$\leq 4$ polynomial with no constant term, $Z_{\mathrm{poly}}(a,b;Q)=a Q^{2}+b Q^{4}$. Even powers alone already encode conjugation symmetry; the constant term is forbidden by (G3). A parallel polynomial appears in the mass baseline derivation with the same monomials.
proof idea
Term-mode proof in two steps. Unfold Z_poly to $a Q^{2}+b Q^{4}$, then apply ring. Because every exponent is even, substituting $-Q$ yields identical monomials, so equality is pure polynomial identity. No external lemmas are required.
why it matters
This discharges gauge axiom (G1) in the Stage-2 derivation of the topological Z-map. Downstream, derivation_complete packages it as the gauge_invariance field of the ZMapDerivation certificate, alongside face integerization ($F=6$), neutral vanishing, and family separation that forces $a=b=1$.
In the broader Recognition chain it sits under T8 ($D=3$ spatial dimensions): the 3-cube supplies the face count that integerizes SM charges, and the even polynomial is the minimal conjugation-invariant cost on that integerized charge. Without this identity the lepton/quark band formulas $Z=\tilde{Q}^{2}+\tilde{Q}^{4}$ and $Z=4+\tilde{Q}^{2}+\tilde{Q}^{4}$ would not be C-symmetric.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.