Z_up_with_offset
plain-language theorem explainer
Specializes the quark-sector Z-map to the up-type charge by fixing the integerized charge to Q̃_up = 4. Anyone matching topology-compatible Z values against SM anchor outputs cites this branch. The body is a one-line specialization of the quark-with-offset polynomial at that fixed charge.
Claim. For integer coefficients $c,a,b$, the up-quark band label with color offset is $Z_{\mathrm{up}}(c,a,b) := c + a\,\tilde{Q}_{u}^{2} + b\,\tilde{Q}_{u}^{4}$, where $\tilde{Q}_{u} = 4$ is the face-count integerization $6\cdot(2/3)$ of the up-quark electric charge.
background
This module derives the charge-to-band map $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without empirical mass anchors. Stage 1 integerizes SM charges by the face count $F=2D=6$ at $D=3$, the minimal positive even $k$ with $kQ\in\mathbb{Z}$ for $Q\in{-1,2/3,-1/3}$. Thus $\tilde{Q}_{u}=6\cdot(2/3)=4$.
Stage 2 forces the even non-negative polynomial $Z=a\tilde{Q}^{2}+b\tilde{Q}^{4}$ with family separation pinning $a=b=1$. Stage 3 adds a quark color offset $c=2^{D-1}=4$ from edge channels, so quarks use $Z_{\mathrm{quark}}=c+a\tilde{Q}^{2}+b\tilde{Q}^{4}$ while leptons omit $c$.
Z_quark_with_offset is exactly that quark extension: $c+Z_{\mathrm{poly}}(a,b,Q)$. The present definition plugs in the up charge $\tilde{Q}_{u}=4$.
proof idea
Pure abbreviation: apply the quark-sector map Z_quark_with_offset at the fixed integerized up charge Q_tilde_up ($=4$). No tactics or lemmas; the value is $c+Z_{\mathrm{poly}}(a,b,4)$.
why it matters
Supplies the up-quark leg of the topology-compatible family used to force the canonical triple $(a,b,c)=(1,1,4)$. Downstream, full_anchor_tuple_forces_coefficients_and_offset equates this branch to the anchor output $276$ (with lepton $1332$ and down $24$) and concludes the coefficients. The mass-layer bridge canonical_tuple_forced_from_anchor_outputs does the same against ChargeIndex.Z sector values.
In the RS chain this closes Stage 3 of the Z-map derivation: color offset $c=2^{D-1}=4$ at $D=3$ (T8), sitting on the face-count integerization from Stage 1. Without a named up branch, the three-sector forcing theorems cannot state their hypotheses cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.