quadratic_ordered
plain-language theorem explainer
With only the quadratic term active (coefficients a=1, b=0) in the charge-to-band polynomial, the three SM families still obey the strict ordered hierarchy Z_lepton > Z_up > Z_down > 0. Cited when checking that family separation alone does not yet force the quartic coefficient. Proof unfolds the Z-polynomial and Q-tilde definitions, then closes the three integer inequalities by omega.
Claim. For the charge-to-band polynomial $Z=a\tilde{Q}^2+b\tilde{Q}^4$ at $(a,b)=(1,0)$, the ordered hierarchy holds: $Z_{\mathrm{lepton}}>Z_{\mathrm{up}}>Z_{\mathrm{down}}>0$. (Explicitly $Z_{\mathrm{down}}=4$, which is positive but weak.)
background
This module derives the charge-to-band map $Z(\tilde{Q})$ from recognition topology on the 3-cube, without anchors or empirical masses. Stage 1 integerizes SM charges $Q\in{-1,2/3,-1/3}$ by the face count $F=2D=6$ (forced at $D=3$), giving $\tilde{Q}=FQ\in{-6,4,-2}$. Stage 2 requires $Z$ even, nonnegative, and $Z(0)=0$, so the minimal form is the biquadratic $Z=a\tilde{Q}^2+b\tilde{Q}^4$.
The predicate ordered_hierarchy a b packages the physical demand that the three families be strictly separated and ordered by charge magnitude: $Z_{\mathrm{lepton}}(a,b)>Z_{\mathrm{up}}(a,b)>Z_{\mathrm{down}}(a,b)>0$. Each sector value is the polynomial $Z_{\mathrm{poly}},a,b,\tilde{Q}:=a\tilde{Q}^2+b\tilde{Q}^4$ evaluated at the corresponding $\tilde{Q}$.
Upstream, $Z_{\mathrm{poly}}$ is the shared charge-index polynomial; the local $\tilde{Q}$ constants are the face-scaled SM charges. The canonical target later is $(a,b)=(1,1)$, forced by distinctness plus a non-degenerate hierarchy.
proof idea
One short tactic proof. simp only unfolds ordered_hierarchy into the three strict inequalities, then substitutes the sector maps $Z_{\mathrm{lepton}}$, $Z_{\mathrm{up}}$, $Z_{\mathrm{down}}$, the polynomial $Z_{\mathrm{poly}},a,b,q=a q^2+b q^4$, and the three integer $\tilde{Q}$ values. With $(a,b)=(1,0)$ this reduces to comparing pure squares $36>16>4>0$. omega discharges the resulting linear integer arithmetic.
why it matters
Stage 2 of the topological Z-map derivation aims to force $(a,b)=(1,1)$ uniquely from gauge constraints plus family separation. This lemma records the quadratic-only boundary: hierarchy still holds, but $Z_{\mathrm{down}}=4$ is weak (doc-comment), so the quadratic term alone does not give a physically adequate band gap for the down sector.
Together with the quartic-only companion (a=0,b=1: values 1296, 256, 16), it frames why both coefficients must be present. The ambient chain uses T8 ($D=3$) to fix the face count $F=6$ that produces the integer $\tilde{Q}$ ladder. No used_by edges are recorded yet; the result is local evidence inside the uniqueness argument for the biquadratic coefficients, not a mass-formula input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.