Z_up
plain-language theorem explainer
Bare up-quark band label: evaluate the even degree-4 polynomial a Q̃² + b Q̃⁴ at the face-integerized up charge Q̃ = 4. Cited by anyone proving family separation, ordered hierarchy, or uniqueness of (a,b) from quark anchors. One-line specialization of the general Z-polynomial at 6×(2/3).
Claim. For integer coefficients $a,b$, the bare up-quark band label is $Z_{\mathrm{up}}(a,b)=a\cdot 4^{2}+b\cdot 4^{4}=16a+256b$, where the integerized charge $\tilde{Q}_{\mathrm{up}}=6\times(2/3)=4$ is the face-count scaling of the up electric charge on the 3-cube.
background
This module derives the charge-to-band map Z from recognition boundaries on the 3-cube, without empirical mass anchors. Stage 1 fixes the integerization scale: a boundary of charge Q couples to the F=2D faces of the cube; at D=3 one has F=6, the minimal positive even integer sending all SM charges {−1, 2/3, −1/3} into ℤ. Thus the up charge becomes $\tilde{Q}_{\mathrm{up}}=6\times(2/3)=4$.
Stage 2 requires Z to be charge-conjugation even, non-negative, and zero at neutral charge. The minimal such polynomial is $Z=a\tilde{Q}^{2}+b\tilde{Q}^{4}$. The local helper Z_poly is exactly that form; the present definition is its evaluation at the up integerized charge (still bare: no color offset).
Color offset $2^{D-1}=4$ is added only later for the full quark sector; bare values are what force the coefficients.
proof idea
Pure definitional abbreviation: substitute the constant $\tilde{Q}{\mathrm{up}}=4$ into $Z{\mathrm{poly}}(a,b,Q)=aQ^{2}+bQ^{4}$. No tactics, no lemmas. Downstream proofs unfold it and reduce $16a+256b$ by norm_num or omega.
why it matters
Supplies the bare up anchor used throughout Stage 2–3 of the topological Z-map derivation. bare_Z_values records $Z_{\mathrm{up}}(1,1)=272$; coefficients_forced_from_quark_bare_anchors shows that the pair of bare anchors (272, 20) forces $a=1\wedge b=1$ uniquely. The same specialization appears in canonical_separates, canonical_ordered, families_separated, and the packaged witness derivation_complete.
Framework link: face count F=6 is the T8 consequence D=3; the even quartic is the minimal gauge-invariant cost on integerized charge. Downstream AnchorPolicy equates the full (color-offset) up Z to 276, matching the bare 272 plus offset 4. Without this abbreviation the coefficient-forcing and separation theorems cannot even be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.