one_one_is_complete_ordered_minimizer
plain-language theorem explainer
Canonical coefficients (1,1) form a complete ordered minimizer for the even charge polynomial: both quadratic and quartic terms are present, the SM family hierarchy holds, and no other complete ordered pair has smaller coefficient sum. Downstream first-principles characterization of the Z-map tuple cites this fact. The proof packages nonnegativity, the ordered-hierarchy check at (1,1), and the lower bound a'+b'≥2.
Claim. The integer pair $(a,b)=(1,1)$ is a complete ordered minimizer: $a\ge 1$, $b\ge 1$, the ordered hierarchy of lepton/up/down band labels holds for $Z=a\tilde{Q}^2+b\tilde{Q}^4$, and every other pair $(a',b')$ with $a'\ge 1$, $b'\ge 1$ that also satisfies the ordered hierarchy obeys $a+b\le a'+b'$.
background
This module derives the charge-to-band map $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without empirical mass anchors. Stage 2 requires a gauge-invariant even polynomial $Z=a\tilde{Q}^2+b\tilde{Q}^4$ with $a\ge 0$, $b>0$, vanishing at neutral charge, and producing distinct band labels for the three SM families (family separation).
A complete ordered minimizer is a pair $(a,b)$ of integers with $a\ge 1$, $b\ge 1$ (both quadratic and quartic terms present), satisfying the ordered hierarchy of lepton/up/down $Z$ values, and minimal among all such pairs in the sum $a+b$. Completeness excludes pure-quadratic or pure-quartic spectra, which fail to match the physical gap structure.
Upstream, canonical_ordered checks that $(1,1)$ itself obeys the hierarchy via direct evaluation of $Z$ on the three SM $\tilde{Q}$ values. unique_minimal_complete states that every complete ordered pair satisfies $a+b\ge 2$, so the sum-two floor is forced once both coefficients are at least one.
proof idea
Term-mode proof by refine into the four conjuncts of the minimizer predicate. The bounds $1\ge 1$ and $1\ge 1$ are discharged by omega. Ordered hierarchy at $(1,1)$ is the upstream lemma canonical_ordered. For the universal minimality clause, introduce any competing complete ordered pair $(a',b')$; apply unique_minimal_complete to obtain $a'+b'\ge 2$, then linarith closes $1+1\le a'+b'$.
why it matters
Stage 2 of the topological Z-map derivation claims that family separation plus completeness uniquely forces the polynomial coefficients to $(a,b)=(1,1)$. This theorem supplies one half of that claim: $(1,1)$ attains the complete-ordered minimum. The immediate parent is zmap_canonical_tuple_satisfies_first_principles, which packages the full canonical tuple $(F,a,b,\mathrm{offset})=(6,1,1,4)$ as satisfying all first-principles conditions (face-count integerization, coefficient minimality, and color offset $2^{D-1}=4$).
In the broader Recognition chain this sits under T8 ($D=3$ spatial dimensions), which fixes both the face count $F=2D=6$ used in Stage 1 and the edge-direction color offset. The companion uniqueness statement (any complete ordered minimizer equals $(1,1)$) sits immediately downstream in the same module and finishes the forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.