cube_face_cubed
plain-language theorem explainer
The theorem shows that the Cartesian product of three finite sets, each with exactly six elements, has cardinality 216. Researchers mapping structural analogies across Recognition Science domains cite it when combining counts such as quarks, leptons, and cortical layers. The proof reduces the statement by unfolding the cube-face count predicate and simplifying the product cardinality rule.
Claim. If $A$, $B$, and $C$ are finite sets each satisfying $|A| = |B| = |C| = 6$, then $|A × B × C| = 216$.
background
Module C15 states that the 3-cube has six faces, so the count 6 appears uniformly as the face-level enumeration for spatial dimension D=3. HasCubeFaceCount is the predicate asserting that a finite type T satisfies Fintype.card T = 6. The module lists concrete instances: six quarks, six leptons, six cortical layers, six Braak stages, and six robotic degrees of freedom. The upstream definition of HasCubeFaceCount supplies the exact cardinality hypothesis required by the theorem.
proof idea
The proof unfolds HasCubeFaceCount at each hypothesis to replace the predicates with the equalities Fintype.card A = 6, Fintype.card B = 6, and Fintype.card C = 6. It then applies simp using the Fintype.card_prod lemma to obtain the product 6 × 6 × 6 = 216.
why it matters
The result fills the algebraic step inside the cube-face universality claim of C15, confirming that any three domains carrying the count 6 multiply to 216. It anchors the structural pattern 6 = 2 · 3 that links the forcing-chain result D = 3 to the listed cross-domain instances. No downstream theorems are recorded, yet the identity supports enumeration arguments that appear in the eight-tick octave and the alpha-band constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.