Z_down
plain-language theorem explainer
The bare down-quark band label is the even degree-4 polynomial Z = a Q̃² + b Q̃⁴ at the integerized down charge Q̃ = −2 (six times −1/3). Anyone proving family separation, coefficient uniqueness, or the completed Z-map derivation cites this specialization. It is a one-line application of the general polynomial to that fixed charge.
Claim. For $a,b \in \mathbb{Z}$, the bare down-quark band index is $Z_{\mathrm{down}}(a,b) := a\,\tilde{Q}_d^{2} + b\,\tilde{Q}_d^{4}$, where $\tilde{Q}_d = -2$ is the face-integerized down charge $6 \times (-1/3)$.
background
This module derives the charge-to-band map Z from recognition topology on the 3-cube, without empirical mass anchors. Stage 1 integerizes SM charges by the face count F = 2D = 6 (forced at D = 3 by T8), so the ledger entries live in ℤ. The down quark has electric charge −1/3, hence Q̃_d = 6 · (−1/3) = −2.
Stage 2 requires Z to be charge-conjugation even, non-negative, and zero at neutral charge. The minimal such polynomial is Z_poly(a,b;Q) = a Q² + b Q⁴. The present definition is that polynomial evaluated at the down integerized charge.
Color offset (Stage 3: +2^{D−1} = +4 for quarks) is not folded in here; bare values are used first to force (a,b), then the offset is restored when matching physical anchors such as Z(d) = 24.
proof idea
One-line definition: apply the general even polynomial Z_poly(a,b;·) = a Q² + b Q⁴ to the constant Q̃_down = −2. No tactics or lemmas; pure abbreviation of that specialization.
why it matters
Feeds the Stage-2 uniqueness and separation chain. bare_Z_values records Z_down(1,1) = 20; coefficients_forced_from_quark_bare_anchors uses the pair (Z_up = 272, Z_down = 20) to force a = 1 ∧ b = 1 uniquely. canonical_separates and canonical_ordered unfold this definition to prove family hierarchy under the canonical coefficients. derivation_complete packages those facts into the finished ZMapDerivation record.
Downstream, Physics.AnchorPolicy.Z_down states the physical anchor ZOf(d) = 24, which is the bare value 20 plus the color offset 4 = 2^{D−1}. Thus the definition sits between topological forcing (face integerization at D = 3, even polynomial form) and the mass-ladder anchors used elsewhere in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.