cube_faces
plain-language theorem explainer
The ordinary 3-cube has exactly six faces, realized as pairs (axis, side). Anyone assembling alpha ingredients, solid-angle normalizations, or holographic face counts from D=3 cube geometry cites this fact. The proof is a one-line finite-type decision: |Fin 3 × Bool| = 6.
Claim. The finite set of pairs $(i,s)$ with spatial axis $i\in\{0,1,2\}$ and side $s\in\{\mathrm{true},\mathrm{false}\}$ has cardinality $6$. Equivalently, a $3$-cube has six faces.
background
PixelLocal works on the forced D=3, eight-tick substrate: the cube $2^3$ with eight vertices and six faces. A boundary recognition pixel is one cube face (a square plaquette). The module enumerates admissible boundary sectors under ledger closure and the face stabilizer $D_4$, aiming at the integer coefficient $4$ in the recognition-pixel area split $a_{\mathrm{pix}}=4\cdot H\cdot\ell_P^2$.
Faces are coded as an axis together with a Boolean side, i.e. elements of $\mathrm{Fin},3\times\mathrm{Bool}$. Upstream constants modules write the same count as the hypercube formula $F=2D$ (so $F=6$ at $D=3$), or as a case match that hard-codes six faces for the $3$-cube. This theorem is the fintype-card form of that geometric fact inside the holography panel.
proof idea
One-line tactic proof: decide evaluates the fintype cardinality of the product Fin 3 × Bool and checks equality with $6$. No lemmas are invoked; the finite type is small enough for kernel decision.
why it matters
This is the substrate-native face count for the forced $D=3$ cube (T8). Downstream alpha work uses it heavily: faces_at_D3 and the def cube_faces in AlphaDerivation; solid-angle identities (per_face_solid_angle, per_face_solid_angle_eq, face_solid_angle_sum) that reconstruct $6\times(2\pi/3)=4\pi$; seam numerator/denominator assembly; and alpha_ingredients_from_D3_cube, whose doc states that all magic numbers come from D=3 cube geometry. U(1) normalization also routes gauge degrees of freedom through faces (gauge_dof_via_faces).
In PixelLocal the six faces are the ambient geometry on which the four admissible recognition sectors live. The module is explicit that counting faces (or sectors) does not by itself identify the area coefficient in $a_{\mathrm{pix}}$; that link remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.