first_principles_zmap_tuple
plain-language theorem explainer
Bundles the first-principles constraints that force the Z-map parameters (k,a,b,c): minimal positive even integerizer of SM charges, complete ordered minimizer for the even quartic, and color offset equal to the edge-direction count. Mass and verification lanes cite it as the single Prop whose solutions are exactly the canonical tuple (6,1,1,4). It is a pure conjunction of already-defined predicates, not a proved uniqueness statement.
Claim. A 4-tuple $(k,a,b,c)$ satisfies the first-principles Z-map characterization when $k>0$ is even, $k$ integerizes every Standard Model charge $Q\in\{-1,2/3,-1/3\}$, $k$ is the least such positive even integer, $(a,b)$ is a complete ordered minimizer of the even quartic band polynomial (so $a\ge 1$, $b\ge 1$, ordered hierarchy, and minimal $a+b$), and $c$ equals the edge-direction count $2^{D-1}$.
background
This module derives the charge-to-band map $Z(\tilde Q)$ from recognition boundaries on the 3-cube, without anchors or empirical masses. Stage 1 fixes the integerization scale: a boundary of charge $Q$ couples to the $F=2D$ faces, and the ledger demands integer entries, so one seeks the least positive even $k$ with $kQ\in\mathbb{Z}$ for all SM charges. That predicate is integerizes_all; at $D=3$ the minimizer is $k=6$.
Stage 2 requires $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$. Family separation plus an ordered-hierarchy rule select a unique complete ordered minimizer $(a,b)$. Stage 3 adds a sector offset equal to the number of edges along one spatial direction, edge_direction_count $:=2^{D-1}$ (equal to 4 when $D=3$), which is the color channel count for quarks.
The present definition packages those three stages into one Prop on $(k,a,b,c)$, so downstream forcing theorems can treat the whole first-principles package as a single hypothesis.
proof idea
Definitional abbreviation only: the body is the six-way conjunction of positivity and evenness of $k$, integerizes_all k, minimality of $k$ among positive even integerizers, complete_ordered_minimizer a b, and equality of $c$ with edge_direction_count cast to $\mathbb{Z}$. No tactics or lemmas are invoked; meaning is inherited entirely from those named predicates.
why it matters
Gives the single interface Prop that the Z-map forcing lane equates with canonicity. The local theorem canonical_tuple_iff_first_principles (and its upstream in Masses.ZMapForcing) states that this Prop holds iff $(k,a,b,c)=(6,1,1,4)$. That closes the three-stage topological derivation: face-count integerization at $D=3$ (T8), unique even quartic $(a,b)=(1,1)$, and color offset $c=2^{D-1}=4$. Downstream mass formulas that write $Z_{\mathrm{lepton}}=\tilde Q^2+\tilde Q^4$ and $Z_{\mathrm{quark}}=4+\tilde Q^2+\tilde Q^4$ therefore rest on a first-principles package rather than an ad hoc choice of coefficients.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.