cube_face_cubed
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not derive the number 6 from the forcing chain T0-T8.
- Does not apply to non-finite or infinite types.
- Does not prove that every listed domain must carry exactly six elements.
- Does not address why the count 6 recurs across the listed domains.
formal statement (Lean)
86theorem cube_face_cubed
87 {A B C : Type} [Fintype A] [Fintype B] [Fintype C]
88 (hA : HasCubeFaceCount A) (hB : HasCubeFaceCount B) (hC : HasCubeFaceCount C) :
89 Fintype.card (A × B × C) = 216 := by
proof body
Term-mode proof.
90 unfold HasCubeFaceCount at hA hB hC
91 simp [Fintype.card_prod, hA, hB, hC]
92
93/-- 216 = 6³. -/