cube_face_identity
plain-language theorem explainer
The cube face identity states that the three-cube possesses exactly six faces, recovered as the product of binary face states and spatial dimension three. Recognition Science researchers cite the result when unifying six-element enumerations such as quarks, leptons, cortical layers, and Braak stages. The proof is a direct decision procedure on natural numbers.
Claim. In the three-dimensional cube the face count satisfies $6 = 2 × 3$, where the factor 2 enumerates binary states per face and the factor 3 is the spatial dimension.
background
The module C15 treats the three-cube Q₃ whose Euler characteristic is V − E + F = 2. Upstream definitions supply V(D) = 2^D for vertices and E(D) = D × 2^(D−1) for edges; for D = 3 these yield V = 8 and E = 12, fixing F = 6. The same face count reappears across domains as the product of binary face enumeration and spatial dimension.
proof idea
The proof is a one-line decision procedure that verifies the arithmetic equality 6 = 2 * 3 directly on natural numbers.
why it matters
The identity supplies the common factor 6 = 2 × 3 that cubeFaceUniversalityCert aggregates into the six-fold lists for quarks, leptons, cortical layers, Braak stages, and robotic degrees of freedom. It realizes the structural claim of C15 that the cube-face count equals D_cube × D_spatial with D = 3 taken from the forcing chain T8. The result closes the enumeration step for cross-domain universality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.