Q3_faces
plain-language theorem explainer
The declaration assigns the integer 6 to the face count of the three-dimensional hypercube Q3. Recognition Science workers cite the value when building the structural certificate for fine-structure corrections and when computing face-wallpaper pairings. The entry is a direct constant definition with no reduction steps or lemmas invoked.
Claim. The three-dimensional hypercube $Q_3$ has six faces: $|F(Q_3)|=6$.
background
The module formalizes combinatorial and spectral properties of the 3-cube $Q_3$, the unit cell of the integer lattice $Z^3$. It records that $Q_3$ possesses eight vertices, twelve edges and six faces, together with the Laplacian spectrum whose eigenvalues are 0 (multiplicity 1), 2 (multiplicity 3), 4 (multiplicity 3) and 6 (multiplicity 1). The automorphism group is $S_4 times Z_2^3$ of order 48. These counts supply the concrete inputs required for critical-exponent corrections inside Recognition Science.
proof idea
The definition is a one-line constant assignment that sets the natural-number value directly to 6. No upstream lemmas are applied and no tactics are executed; the entry simply records the standard combinatorial count of faces on the 3-cube.
why it matters
The definition supplies the face count demanded by the AlphaFrameworkCert structure, by the face-wallpaper-pairs computation, and by the delta-1 negativity argument. It also feeds the numerological summary in SpectralEmergence. Within the Recognition Science forcing chain the entry instantiates the D=3 spatial dimension (T8) and closes the combinatorial data needed for the Euler characteristic of the bounding sphere and for the higher-order alpha corrections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.