one_one_achieves_minimum
plain-language theorem explainer
In the Z-map coefficient family, the ordered pair (a,b)=(1,1) realizes the minimal budget a+b=2. Anyone citing the Stage-2 uniqueness of Z=Q̃²+Q̃⁴ needs this trivial arithmetic step. The proof is a one-line omega discharge of 1+1=2 on integers.
Claim. As integers, $1+1=2$. In the selection-rule reading: among coefficients $a\ge 1$, $b\ge 1$ for the even polynomial $Z=a\tilde{Q}^2+b\tilde{Q}^4$, the pair $(a,b)=(1,1)$ achieves the minimal coefficient budget $a+b=2$.
background
This module derives the charge-to-band polynomial $Z(\tilde{Q})$ from recognition topology on the 3-cube, without mass anchors. Stage 1 fixes the integerization scale $\tilde{Q}=FQ$ with face count $F=6$ at $D=3$ (T8). Stage 2 requires $Z$ to be charge-conjugation even, non-negative, and zero at neutral charge, so the minimal form is $Z=a\tilde{Q}^2+b\tilde{Q}^4$ with $a\ge 0$, $b>0$.
Family separation (distinct $Z$ on the three SM charge values) plus an ordered hierarchy $a\ge 1$, $b\ge 1$ then forces the coefficient budget. The minimal admissible budget is $a+b=2$. Sibling results in the module classify which positive integers integerize SM charges and which coefficient pairs fail separation; this declaration only records that $(1,1)$ meets the budget floor.
proof idea
Pure integer arithmetic. The goal is (1 : ℤ) + 1 = 2, discharged in one tactic step by omega. No Recognition lemmas are invoked; the upstream depends_on edges are name-resolution noise (shared tokens like canonical), not proof ingredients.
why it matters
Stage 2 of the Z-map derivation claims that family separation forces $a=1$, $b=1$ uniquely for $Z=a\tilde{Q}^2+b\tilde{Q}^4$. Showing that $(1,1)$ achieves the minimal budget $a+b=2$ is the positive half of that selection rule (the negative half is that other small pairs fail). Downstream the module builds $Z_{\mathrm{lepton}}=\tilde{Q}^2+\tilde{Q}^4$ and the quark offset $2^{D-1}=4$, tying the polynomial to the eight-tick / $D=3$ cube geometry (T7–T8). No used_by edges are recorded yet, so this is a local arithmetic pin rather than a widely cited lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.