face_count_eq_six
plain-language theorem explainer
At spatial dimension D = 3 the hypercube face count F = 2D equals 6. Citation target for Stage 1 of the topological Z-map derivation, where F is the canonical integerization scale for SM charges. The proof is a one-line native decision of the arithmetic 2 · 3 = 6.
Claim. With spatial dimension $D = 3$, the face count of the $D$-cube satisfies $F = 2D = 6$.
background
The module derives the charge-to-band map $Z(\tilde Q)$ from recognition boundaries on the 3-cube, without mass anchors. Stage 1 fixes the integerization scale: a boundary of charge $Q$ couples to the $F$ faces of the cube, and the ledger demands integer entries, so $FQ$ must land in $\mathbb{Z}$ for the SM values $Q \in {-1, 2/3, -1/3}$.
Upstream, cube_faces is defined as $F(d) = 2d$ (number of faces of the $d$-hypercube), and $D$ is the forced spatial dimension $D = 3$ (T8/T9). Parallel modules record the same identity: faces of the 3-cube equal 6, equivalently $\lvert \mathrm{Fin},3 \times \mathrm{Bool}\rvert = 6$.
Thus the present statement is the concrete evaluation $F(D) = 6$ that Stage 1 needs before comparing candidate integerizers $k \in {1,\ldots,6}$.
proof idea
Unfolding gives $2 \cdot D$ with $D = 3$, hence $2 \cdot 3 = 6$. The tactic native_decide discharges the closed natural-number equality; no lemmas beyond the definitions of face count and $D$ are required.
why it matters
Feeds derivation_complete as the face_integerization field of the packaged ZMapDerivation record. That record assembles Stage 1 (face count and the minimality of $k = 6$ among positive even integerizers), Stage 2 (even non-negative polynomial form forced to $Z = \tilde Q^2 + \tilde Q^4$), and Stage 3 (color offset $2^{D-1} = 4$).
In the Recognition chain this sits on T8 ($D = 3$) and the ledger integrality requirement. Sibling results (six_integerizes, one_fails, …, six_smallest_positive_even_integerizer) then show that $F = 6$ is exactly the minimal positive even $k$ that integerizes all three SM charges, locking the scale $\tilde Q = FQ$ used throughout the Z-map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.