canonical_separates
plain-language theorem explainer
The canonical coefficients a=1, b=1 of the even charge polynomial Z=aQ̃²+bQ̃⁴ yield three pairwise distinct band labels for the lepton, up, and down families. Anyone citing the first-principles Z-map derivation needs this separation fact. The proof unfolds the three closed-form Z values and discharges the inequalities by linear arithmetic.
Claim. For the even polynomial $Z(\tilde{Q})=a\tilde{Q}^2+b\tilde{Q}^4$ at coefficients $a=1$, $b=1$, the three Standard Model family band labels are pairwise distinct: $Z_{\mathrm{lepton}}\neq Z_{\mathrm{up}}$, $Z_{\mathrm{up}}\neq Z_{\mathrm{down}}$, and $Z_{\mathrm{lepton}}\neq Z_{\mathrm{down}}$.
background
This module derives the charge-to-band map Z from recognition topology on the 3-cube, without anchors or empirical masses. Stage 1 integerizes SM charges Q∈{−1,2/3,−1/3} by the face count F=2D=6, producing the scaled charges Q̃ (lepton Q̃=−6, up Q̃=4, down Q̃=−2). Stage 2 requires a gauge-invariant band label: even in Q̃, nonnegative, and vanishing at zero. The minimal such polynomial is Z_poly(a,b;q)=a q²+b q⁴ with a≥0, b>0.
Family separation is the Prop that the three evaluated Z values are pairwise unequal. Explicitly, with a=b=1 one obtains Z_lepton=1332, Z_up=272, Z_down=20 (pure quartic-plus-quadratic; color offset is Stage 3). The companion comment notes that pure quadratic (b=0) also separates but with weaker ratios; the quartic term improves separation markedly.
proof idea
Term-mode proof by simplification and arithmetic. Unfold families_separated together with the three family Z wrappers (Z_lepton, Z_up, Z_down), the polynomial Z_poly, and the three fixed Q̃ values. After unfolding, the goal is three concrete integer inequalities among 1332, 272, and 20, which omega discharges.
why it matters
This is the constructive half of Stage 2 in the module derivation: the canonical choice a=1, b=1 separates all three SM families. It is wired directly into derivation_complete as the separation field of the ZMapDerivation record, alongside face-count integerization (F=6), gauge invariance, and neutral vanishing.
The surrounding narrative claims that separation plus the structural constraints forces a=b=1 uniquely; this theorem supplies the positive witness. Framework link: Stage 1 rests on T8 (D=3 spatial dimensions), which fixes F=2D=6 as the minimal positive even integerizer of the SM charges. Without separation, the band labels would collide and the mass ladder could not assign distinct rungs to the three families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.