ZMapDerivation
plain-language theorem explainer
A structure that packages the three-stage first-principles derivation of the charge-to-band map Z from 3-cube recognition topology: face-count integerization at F=6, the unique even quartic Z=Q̃²+Q̃⁴ forced by family separation, and color offset 4. Anyone citing the topological origin of the SM Z-values (1332, 276, 24) points here. Pure data structure; fields are discharged by sibling lemmas, not proved inside the type.
Claim. A complete Z-map derivation is a record of: (i) face count of the $D$-cube equals $6$ at $D=3$; (ii) among $k\in\{1,\ldots,6\}$, only $k=3$ and $k=6$ send all SM charges $\{-1,2/3,-1/3\}$ into $\mathbb{Z}$, with $k=6$ preferred; (iii) $Z=a\tilde{Q}^2+b\tilde{Q}^4$ is charge-conjugation invariant and vanishes at $\tilde{Q}=0$; (iv) $a=b=1$ separates the three families; (v) color offset equals $2^{D-1}=4$; (vi) resulting values $Z_\ell=1332$, $Z_u=276$, $Z_d=24$.
background
This module derives the charge-to-band polynomial $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without anchor constraints or empirical masses. Stage 1 uses the face count $F=2D$ of the $D$-cube as the integerization scale $\tilde{Q}=FQ$: the ledger demands integer entries (T8: $\delta$-units $\simeq\mathbb{Z}$), and SM charges ${-1,2/3,-1/3}$ must all land in $\mathbb{Z}$. At the forced dimension $D=3$ one has $F=6$.
Stage 2 requires $Z$ to be charge-conjugation even, non-negative, and zero on neutrals. The minimal even polynomial of degree $\le 4$ with no constant term is $Z=a\tilde{Q}^2+b\tilde{Q}^4$. Family separation then forces the canonical coefficients $a=b=1$. Stage 3 adds a quark-only color offset equal to the number of edge directions along one spatial axis, $2^{D-1}=4$.
Referenced maps: $Z_{\mathrm{poly}}(a,b,Q)=aQ^2+bQ^4$; $Z_{\mathrm{full}}$ adds the color offset on the quark sector. Integerized charges are $\tilde{Q}_\ell=-6$, $\tilde{Q}_u=4$, $\tilde{Q}_d=-2$.
proof idea
No proof body: this is a structure (record type) whose seven fields are propositions. Instantiation is deferred to derivation_complete, which fills each field by a named sibling lemma: face count via face_count_eq_six, the six-way integerization table via integerization_results, conjugation invariance and neutral vanishing via the corresponding poly identities, family separation via canonical_separates, and the numerical Z-values by direct evaluation of $Z_{\mathrm{full}}$ at the integerized charges with $a=b=1$.
why it matters
This is the certificate type for the claim that the SM band labels arise from 3-cube topology alone. Downstream, derivation_complete inhabits the structure, closing the module's verification goal. It sits on the forcing chain at T8 ($D=3$ spatial dimensions) and the eight-tick cube geometry: face count $F=2D=6$ and edge-direction count $2^{D-1}=4$ are pure combinatorial consequences of that dimension. The resulting anchors $Z_\ell=1332$, $Z_u=276$, $Z_d=24$ feed the phi-ladder mass formula (yardstick $\times\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) without importing empirical masses into the derivation of $Z$ itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.