minimal_nonzero_coefficients
plain-language theorem explainer
Any nonnegative integers a,b that are not both zero and obey the ordered-hierarchy constraint on Z-map coefficients satisfy a+b ≥ 1. This is the first rung of the minimality argument that later singles out (1,1) among complete even polynomials Z = a Q̃² + b Q̃⁴. The proof is a two-case omega split on which coefficient is nonzero; the hierarchy hypothesis is unused.
Claim. For all integers $a,b \geq 0$, if $(a,b) \neq (0,0)$ and $(a,b)$ satisfies the ordered-hierarchy condition on Z-map coefficients, then $a+b \geq 1$.
background
The ambient module derives the charge-to-band map $Z(\tilde Q)$ from recognition topology on the 3-cube, without mass anchors. Stage 2 requires $Z$ to be charge-conjugation even, nonnegative, and zero at neutral charge, so the minimal polynomial form is $Z = a\tilde Q^2 + b\tilde Q^4$ with $a \geq 0$ and $b \geq 0$.
Face-count integerization (Stage 1) fixes the scale $\tilde Q = FQ$ with $F = 6$ at $D=3$, the least positive even integer sending all SM charges ${-1,2/3,-1/3}$ into $\mathbb{Z}$. The ordered-hierarchy predicate on coefficient pairs $(a,b)$ is the local filter that keeps only candidates compatible with that ledger structure and with family separation.
Sibling facts record that $(1,0)$ and $(0,1)$ already achieve sum 1, while complete polynomials (both quadratic and quartic present) start at sum 2, with $(1,1)$ uniquely minimal among them.
proof idea
Term-mode proof by introduction of $a,b$ and the four hypotheses. Case-split the disjunction $a \neq 0 \lor b \neq 0$. In each branch omega discharges $a+b \geq 1$ from nonnegativity plus the nonzero literal. The ordered-hierarchy hypothesis is introduced but never consulted; the claim is pure integer arithmetic.
why it matters
Inside the Z-map derivation this is the base minimality step: nonzero coefficient pairs cannot have vanishing total degree. The module doc's Stage-2 uniqueness theorem (family separation forces $a=1,b=1$) builds on the stronger observation that among complete polynomials ($a \geq 1$, $b \geq 1$) the pair $(1,1)$ is uniquely minimal, while incomplete pairs $(1,0)$ and $(0,1)$ fail to match the physical gap structure.
No downstream consumers are recorded yet; the lemma sits as local scaffolding for the coefficient-selection chain that yields $Z_{\mathrm{lepton}} = \tilde Q^2 + \tilde Q^4$ and $Z_{\mathrm{quark}} = 4 + \tilde Q^2 + \tilde Q^4$ (with color offset $2^{D-1}=4$). It touches the T8 forcing of $D=3$ only indirectly, via the face-count $F=2D=6$ that defines $\tilde Q$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.