bare_Z_values
plain-language theorem explainer
For unit coefficients a=b=1, the bare charge-to-band polynomial evaluates to 1332 (leptons), 272 (up-type), and 20 (down-type) on the three face-integerized SM charges. Anchor and mass verifiers cite these as the color-free Z baselines before the 2^{D-1} offset. The proof unfolds the polynomial definition and evaluates the integers.
Claim. For coefficients $a=1$ and $b=1$, the bare Z-map $Z(\tilde{Q})=a\tilde{Q}^2+b\tilde{Q}^4$ satisfies $Z(\tilde{Q}_\ell)=1332$, $Z(\tilde{Q}_u)=272$, and $Z(\tilde{Q}_d)=20$, where $\tilde{Q}_\ell$, $\tilde{Q}_u$, $\tilde{Q}_d$ are the face-count integerized Standard Model charges of the lepton, up-quark, and down-quark sectors (without color offset).
background
This module derives the charge-to-band map from recognition topology on the 3-cube, without empirical mass anchors. Stage 1 integerizes SM charges $Q\in{-1,2/3,-1/3}$ by the face count $F=6$ (the minimal positive even integerizer at $D=3$), yielding $\tilde{Q}_\ell=-6$, $\tilde{Q}_u=4$, $\tilde{Q}_d=-2$.
Stage 2 requires $Z$ even in $\tilde{Q}$, non-negative, and vanishing at neutrality. The minimal form is $Z=a\tilde{Q}^2+b\tilde{Q}^4$. Family separation forces $a=b=1$. Bare values omit the Stage 3 color offset $2^{D-1}=4$ that quarks receive.
The polynomial is $Z_{\mathrm{poly}}(a,b,q)=aq^2+bq^4$. Sector wrappers evaluate it on the three $\tilde{Q}$ values. Upstream anchor facts record the full (offset-inclusive) targets $Z_u=276$ and $Z_d=24$, and the lepton map $q\tilde{}=-6\mapsto 1332$.
proof idea
One-shot definitional computation. Unfold the three sector wrappers and the polynomial $aq^2+bq^4$, substitute the three fixed $\tilde{Q}$ values, then close by numeric normalization. Explicitly: $\tilde{Q}_\ell=-6$ gives $36+1296=1332$; $\tilde{Q}_u=4$ gives $16+256=272$; $\tilde{Q}_d=-2$ gives $4+16=20$. No intermediate lemmas are required.
why it matters
These bare numbers are the topological baseline for the RS Z-map before color channels. They match the lepton anchor 1332 and the quark bare anchors 272 and 20 that, after adding the offset 4, recover the empirical $Z_u=276$ and $Z_d=24$ used in AnchorPolicy. The module notes that the quark bare anchors force the polynomial coefficients uniquely ($a=b=1$).
In the forcing chain this sits after T8 ($D=3$), which fixes both $F=6$ and the color offset $2^{D-1}=4$. No downstream dependents are recorded yet; the theorem is a verification checkpoint that the first-principles Stage-2 polynomial lands on the known bare integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.