allFaces_length
plain-language theorem explainer
The explicit enumeration of faces of the 3-cube has length exactly 6. Anyone building face windings, generation pairs, or chiral charge on Q₃ cites this as the count check against the geometric 2D face formula. The proof is a one-line native decision on the six-element list.
Claim. The enumerated list of all faces of the 3-cube $Q_3$ has length $6$.
background
The module Face Winding Numbers on $Q_3$ equips Hamiltonian cycles on the 3-cube with signed winding numbers around each face. Those windings are the geometric source of CP violation in Recognition Science: each face pairs with a generation pair, and a nonzero winding distinguishes forward from backward boundary traversal.
A cube face is a pair (fixed axis in ${0,1,2}$, fixed bit). The list allFaces is the six concrete faces $x=0,x=1,y=0,y=1,z=0,z=1$. Independently, the gauge-from-cube count is $\mathrm{cube_face_count}(D)=2D$, hence $6$ when $D=3$ (forced by the T8 step of the forcing chain). This lemma simply records that the explicit list has that length.
proof idea
Term-mode proof by native_decide on the concrete six-element list definition of all faces. No algebraic lemmas are required: Lean evaluates the list length at compile time and closes the equality to $6$.
why it matters
Without a fixed face count of six, the later face-winding and total chiral charge constructions in this module have no well-typed domain. The module’s main line is: enumerate faces, extract boundary edges, sign cycle traversals, form per-face windings, and prove the total chiral charge is nonzero. That nonzero total is the geometric origin of CP violation on the eight-tick octave of $Q_3$ (T7). The sibling count-match against $\mathrm{cube_face_count}(3)=6$ sits next to this fact; together they lock the discrete geometry to the $D=3$ forcing result before any winding arithmetic begins.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.