three_weak_hierarchy
plain-language theorem explainer
With integerization scale k=3 the rescaled SM charges are (−3, 2, −1), and the band polynomial Z=Q̃²+Q̃⁴ evaluates to 90, 20, and 2 on those three values. Anyone comparing candidate integerizers to the face-count scale k=6 cites this as the weak-hierarchy baseline. The proof unfolds the polynomial definition and closes by integer arithmetic.
Claim. For the even quartic $Z(\tilde{Q})=\tilde{Q}^{2}+\tilde{Q}^{4}$, one has $Z(-3)=90$, $Z(2)=20$, and $Z(-1)=2$.
background
This module derives the charge-to-band map $Z(\tilde{Q})$ from recognition boundaries on the 3-cube, without anchor masses. Stage 1 integerizes SM charges $Q\in{-1,2/3,-1/3}$ by a positive even scale $k$ so that $\tilde{Q}:=kQ\in\mathbb{Z}$. The face count $F=2D=6$ at $D=3$ is the minimal such $k$; smaller candidates are checked for contrast.
Z_poly a b Q is the general even degree-$\le 4$ polynomial with no constant term: $Z=a\tilde{Q}^{2}+b\tilde{Q}^{4}$. Gauge constraints (charge-conjugation invariance, non-negativity, $Z(0)=0$) force this shape; family separation later pins $a=b=1$.
For $k=3$ the integerized charges are exactly $(-3,2,-1)$. This theorem records the three resulting $Z$ values under $a=b=1$, labeled a weak hierarchy in the module doc.
proof idea
One-line tactic proof. simp only [Z_poly] expands each conjunct to $a Q^{2}+b Q^{4}$ at $(a,b)=(1,1)$ and the three $Q$ values, yielding the integer equations $9+81=90$, $4+16=20$, and $1+1=2$. omega discharges the arithmetic. No external lemmas are required.
why it matters
In the Stage-1 integerization survey, $k=3$ is the smallest odd scale that integerizes all three SM charges, but it is not even and is not the face count. The computed triple $(Z_{\ell},Z_{u},Z_{d})=(90,20,2)$ is the weak hierarchy against which the canonical $k=6$ values are compared (siblings such as six_integerizes and six_smallest_positive_even_integerizer).
The module’s Stage-2 uniqueness theorem then forces $a=b=1$ from distinct family bands, and Stage 3 adds the color offset $2^{D-1}=4$ for quarks. This lemma is pure arithmetic bookkeeping inside that chain; it does not itself invoke T8 or the RCL, but it sits under the $D=3$ face-count story that T8 supplies. No downstream theorems currently depend on it (used_by is empty); it is a local verification fact for the $k=3$ branch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.