edge_direction_eq_four
plain-language theorem explainer
At spatial dimension D = 3 the number of edge directions on the recognition 3-cube is exactly four, i.e. 2^{D-1} = 4. Anyone deriving the quark color offset in the Z-map cites this equality. The proof is a one-line native decision of a closed natural-number expression.
Claim. The edge-direction count of the recognition 3-cube equals $4$. Equivalently, at $D = 3$ one has $2^{D-1} = 4$.
background
The module derives the charge-to-band polynomial $Z(\tilde Q)$ from recognition topology on the 3-cube, without anchor data or empirical masses. Stage 1 fixes the face-count integerization scale $F = 2D = 6$. Stage 2 forces the minimal even polynomial $Z = a\tilde Q^2 + b\tilde Q^4$ with $(a,b) = (1,1)$ by gauge invariance, non-negativity, neutrality, and family separation.
Stage 3 introduces a sector-dependent constant for colored states. Quarks couple to additional recognition channels along the edge directions of the cube. The module defines that count as $2^{D-1}$ and identifies it with the color offset in $Z_{\mathrm{lepton}} = \tilde Q^2 + \tilde Q^4$, $Z_{\mathrm{quark}} = 2^{D-1} + \tilde Q^2 + \tilde Q^4$.
This sits under the forcing chain landmark T8 ($D = 3$ spatial dimensions) and the eight-tick octave structure of the recognition register. The integer map used by the anchor relation already hard-codes the same offset $4$ for up and down quarks; the present result supplies the topological reason.
proof idea
One-line computational proof. The edge-direction count is a closed natural expression (the value of $2^{D-1}$ at $D = 3$), and native_decide evaluates the equality to $4$ in the kernel. No intermediate lemmas are invoked beyond the definition of the count itself.
why it matters
Closes Stage 3 of the first-principles Z-map derivation: the color offset is not an empirical fit but the edge-direction count $2^{D-1} = 4$ on the 3-cube. Downstream, canonical_color_offset is a direct re-export of this equality for the mass-layer forcing module. The joint characterization theorems then pin the full canonical tuple $(k,a,b,c) = (6,1,1,4)$: the forward direction assumes the color offset matches the edge-direction count, and the converse proves $(4:\mathbb{Z})$ equals that count. The derivation-complete certificate packages face integerization, gauge constraints, and this offset into a single ZMapDerivation record. Framework landmark: T8 forces $D = 3$, which forces the numerical value $4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.