matches_anchor_Z
plain-language theorem explainer
The topologically derived Z-map with unit coefficients and color offset 4 recovers the three canonical band labels used by the mass-anchor tables: 1332 (lepton), 276 (up), and 24 (down). Anyone wiring the first-principles Z-polynomial into Masses/Anchor cites this equality. The proof is a one-line term that reuses the already-computed full_Z_values conjunction.
Claim. With the full charge-to-band map $Z$ (color offset $4$ on quarks, coefficients $a=b=1$) and the face-integerized SM charges $\tilde Q_e=-6$, $\tilde Q_u=4$, $\tilde Q_d=-2$, one has $Z_{\mathrm{lep}}(\tilde Q_e)=1332$, $Z_{\mathrm{up}}(\tilde Q_u)=276$, and $Z_{\mathrm{down}}(\tilde Q_d)=24$.
background
This module builds the charge-to-band polynomial $Z(\tilde Q)$ from recognition boundaries on the 3-cube, without mass data. Stage 1 integerizes SM charges by the face count $F=2D=6$ (the least positive even $k$ with $kQ\in\mathbb{Z}$ for $Q\in{-1,2/3,-1/3}$), giving $\tilde Q_e=-6$, $\tilde Q_u=4$, $\tilde Q_d=-2$. Stage 2 forces the minimal even non-negative form $Z=a\tilde Q^2+b\tilde Q^4$ with $a=b=1$ by family separation. Stage 3 adds the quark color offset $2^{D-1}=4$ (edge directions of the cube).
The full map is $Z_{\mathrm{full}}(\mathrm{is_quark},a,b,\tilde Q)=(\mathrm{offset\ if\ quark})+a\tilde Q^2+b\tilde Q^4$. The upstream theorem full_Z_values already evaluates the three SM points at the canonical coefficients and records the arithmetic $0+36+1296=1332$, $4+16+256=276$, $4+4+16=24$.
proof idea
One-line term proof: the goal is definitionally identical to the statement of full_Z_values, so the proof is just that theorem name. No new simplification or case split occurs here; all simp work (unfolding $Z_{\mathrm{full}}$, the degree-4 polynomial, the three $\tilde Q$ constants, and the edge-direction count at $D=3$) lives upstream.
why it matters
Closes the verification loop between the topological Z-derivation and the mass-anchor tables: the numbers 1332, 276, and 24 that Masses/Anchor treats as given are exactly the values forced by face-count integerization, even-polynomial uniqueness, and the $2^{D-1}$ color offset at $D=3$. That $D=3$ step is the T8 landmark of the forcing chain; the face count $F=6$ is the same six that integerizes all three SM charges. With no downstream dependents yet, this declaration is the export surface for any later mass or $\alpha$ check that needs the anchor Z-labels without re-deriving the cube topology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.