complete_ordered_minimizer_forces_unit_coeffs
plain-language theorem explainer
Any complete ordered minimizer pair of integer coefficients for the even charge-to-band polynomial is forced to unit values $(1,1)$. Family-separation and Z-map forcing cite this to pin the Stage-2 polynomial uniquely. The proof sandwiches the coefficient budget $a+b$ at $2$ via uniqueness of the minimal complete pair and optimality against the canonical $(1,1)$, then applies the budget-forcing lemma.
Claim. If integers $a,b$ form a complete ordered minimizer for the even charge-to-band polynomial $Z=a\tilde{Q}^{2}+b\tilde{Q}^{4}$ (nonnegative coefficients, ordered hierarchy, and optimality among such pairs), then $a=1$ and $b=1$.
background
This module derives the charge-to-band map $Z(\tilde{Q})$ from recognition topology on the 3-cube, without anchor masses. Stage 1 fixes the integerization scale $k=F=6$ (face count at $D=3$) as the least positive even integerizer of the SM charges ${-1,2/3,-1/3}$. Stage 2 constrains the band label: charge-conjugation invariance forces an even polynomial; nonnegativity and $Z(0)=0$ cut it to $Z=a\tilde{Q}^{2}+b\tilde{Q}^{4}$ with $a\ge 0$, $b>0$.
A complete ordered minimizer is such a coefficient pair that is nonnegative, respects the ordered hierarchy among SM family $Z$-values, and is optimal (minimal budget) among all pairs meeting those constraints. The module's Stage-2 claim is that family separation plus this minimality uniquely forces unit coefficients. Stage 3 then adds the color offset $c=2^{D-1}=4$ for quarks.
proof idea
Destructure the minimizer hypothesis into nonnegativity of $a,b$, the ordered-hierarchy witness, and the optimality quantifier. From nonnegativity and hierarchy, unique_minimal_complete yields the lower bound $a+b\ge 2$. For the matching upper bound, feed the canonical pair $(1,1)$ (via canonical_ordered) into the optimality clause to obtain $a+b\le 1+1=2$. Linear arithmetic collapses the sandwich to $a+b=2$. The residual lemma complete_ordered_min_budget_forces_unit_coeffs then converts a budget-two complete ordered pair into $a=1\land b=1$.
why it matters
This is the coefficient-selection step of Stage 2 in the first-principles Z-map derivation: once the even quartic form is fixed by gauge constraints (G1)–(G3), minimality plus ordered family separation pins $(a,b)=(1,1)$ and no other pair. Downstream, zmap_canonical_tuple_forced_from_first_principles packages this with the Stage-1 integerizer $k=6$ and the Stage-3 color offset $c=4$ to force the full canonical tuple $(k,a,b,c)=(6,1,1,4)$. The Masses layer re-exports the same statement as the O2' bridge in ZMapForcing, so mass-ladder work can cite unit coefficients without reopening the topology argument. Framework landmarks in play: T8 ($D=3$ face/edge counts) and the ledger integrality that made $k=6$ the integerization scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.