derivation_complete
plain-language theorem explainer
Packages the full first-principles derivation of the charge-to-band map Z(Q̃) as a single record: face-count integerization at F=6, even quartic form with unique coefficients, color offset 4, and the three SM family values. Anyone citing the topological origin of Z without anchors uses this bundle. The body is a pure structure constructor wiring seven already-proved fields.
Claim. There exists a complete first-principles $Z$-map derivation: the face count of the $3$-cube equals $6$ and is the preferred even integerizer of SM charges $\{-1,2/3,-1/3\}$; the band polynomial is charge-conjugation even, vanishes at neutrality, and family separation forces the unique form $Z=\tilde Q^2+\tilde Q^4$ (leptons) or $Z=4+\tilde Q^2+\tilde Q^4$ (quarks); the color offset equals $2^{D-1}=4$; and the resulting integer band labels match the canonical SM values.
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 integerizes SM charges $Q\in{-1,2/3,-1/3}$ by the face count $F=2D$. At $D=3$ one has $F=6$, the minimal positive even $k$ with $kQ\in\mathbb{Z}$ for all three charges (odd $k=3$ also integerizes but separates families worse).
Stage 2 requires $Z$ even under charge conjugation, nonnegative, and $Z(0)=0$. The minimal even polynomial is $Z=a\tilde Q^2+b\tilde Q^4$; distinct family values force $a=b=1$. Stage 3 adds a quark color offset $2^{D-1}=4$ from edge channels along one spatial direction, so $Z_{\mathrm{lepton}}=\tilde Q^2+\tilde Q^4$ and $Z_{\mathrm{quark}}=4+\tilde Q^2+\tilde Q^4$.
Upstream, the forcing chain fixes $D=3$ (and the eight-tick period). Sibling lemmas supply face count, integerization success/failure for $k=1..6$, conjugation invariance, neutral vanishing, canonical separation, edge-direction offset, and the final $Z$ values.
proof idea
Pure structure assembly: each field of ZMapDerivation is filled by a named in-module result. Face integerization is face_count_eq_six. The six-way integerization dichotomy is integerization_results. Gauge invariance is charge_conjugation_invariant. Neutral vanishing is neutral_vanishes. Family separation (forcing $a=b=1$) is canonical_separates. Color offset is edge_direction_eq_four. Final SM band labels are full_Z_values. No extra tactics; the definition is the record of those seven proofs.
why it matters
Closes the verification claim that the SM band map $Z$ is forced by $3$-cube recognition topology alone (module Stages 1–3), rather than fitted to masses. Lands the T8 spatial dimension $D=3$ in the charge sector: face count $F=2D=6$ and color offset $2^{D-1}=4$ are geometric, not free parameters. Aligns with the mass ladder’s sector-dependent offsets and with fixed lepton/up/down band integers used elsewhere (e.g. $Z_{\mathrm{lepton}}=1332$, $Z_u=276$, $Z_d=24$). No downstream consumers are wired yet; the record is the export surface for any later uniqueness or minimality argument that needs the whole derivation as one hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.