canonical_tuple_iff_first_principles
plain-language theorem explainer
The charge-to-band Z-map parameters are uniquely fixed by first-principles constraints: the integerization scale, quadratic and quartic coefficients, and color offset must be exactly (6,1,1,4). Mass and band-structure derivations cite this as the uniqueness bridge from recognition topology to the canonical Z polynomial. The proof is a two-sided constructor: one direction forces the tuple from the bundled constraints; the other checks that the canonical values satisfy them.
Claim. For natural $k$ and integers $a,b,c$, the bundled first-principles Z-map constraints on $(k,a,b,c)$ hold if and only if $k=6$, $a=1$, $b=1$, and $c=4$. Here $k$ is the charge integerization scale, $a$ and $b$ are the coefficients of the even polynomial $Z=a\tilde{Q}^2+b\tilde{Q}^4$, and $c$ is the color-sector offset.
background
This module derives the charge-to-band map $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without anchor masses. Stage 1: a boundary of charge $Q$ couples to the $F=2D$ faces of the cube; the ledger needs integer entries, so $\tilde{Q}=kQ$ must be integral on the SM charges ${-1,2/3,-1/3}$. At $D=3$ (forced by T8), the minimal positive even such $k$ is $F=6$.
Stage 2: gauge constraints force $Z$ even in $\tilde{Q}$, nonnegative, and $Z(0)=0$, so the minimal form is $Z=a\tilde{Q}^2+b\tilde{Q}^4$ with $a\ge 0$, $b>0$. Distinct family bands then pin $a=b=1$. Stage 3: quarks gain $2^{D-1}=4$ extra edge channels, giving the color offset $c=4$.
The predicate first_principles_zmap_tuple packages positivity and evenness of $k$, integerization of all SM charges, minimality of $k$ and of $(a,b)$, and the color-offset identity. Spatial dimension $D=3$ is the upstream constant used throughout.
proof idea
Biconditional via constructor.
Forward: unpack the six conjuncts of the first-principles bundle (positive $k$, even $k$, full SM integerization, minimal $k$, minimal $(a,b)$, color-offset clause). Feed them to zmap_canonical_tuple_forced_from_first_principles, which returns $k=6\land a=1\land b=1\land c=4$.
Reverse: substitute the four equalities, then rebuild the bundle. Positivity is omega; evenness is the witness $k=2\cdot 3$; the remaining four conjuncts are the four projections of zmap_canonical_tuple_satisfies_first_principles (integerization, minimal $k$, minimal coefficients, color offset).
why it matters
Closes the uniqueness half of the topological Z-map derivation: the only parameters compatible with face-count integerization, even polynomial form, coefficient minimality, and the $2^{D-1}$ color offset are the canonical ones used downstream for mass rungs. The sole consumer is Masses.ZMapForcing.canonical_tuple_iff_first_principles, which re-exports this iff as the forcing interface for the mass sector.
In the module status list this is the capstone of items 1–5 (scale $k=6$, even form, quadratic-plus-quartic necessity, $a=b=1$, color offset $c=4$), with final Z-anchor match already proved separately. Framework landmarks: T8 forces $D=3$, hence $F=2D=6$ and $2^{D-1}=4$. The remaining open question noted in-module is whether coefficient minimality is exactly J-cost minimality (Occam as minimal recognition cost); that link is not required here but would finish the chain to ~100% first-principles status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.