cube_face_equicardinal
plain-language theorem explainer
Any two finite types A and B each satisfying the cube-face count property have identical cardinalities. Cross-domain researchers in Recognition Science cite this to unify the recurring count of 6 across quarks, leptons, cortical layers, Braak stages and robotic degrees of freedom. The proof is a one-line term-mode rewrite that substitutes the defining cardinality equations from the two hypotheses.
Claim. Let $A$ and $B$ be finite types. If $A$ satisfies the cube-face count predicate (i.e., $|A|=6$) and $B$ satisfies the cube-face count predicate (i.e., $|B|=6$), then $|A|=|B|$.
background
The module C15 establishes Cube-Face Universality for cross-domain structures in Recognition Science. The count 6 equals the faces of the 3-cube via Euler characteristic $V-E+F=8-12+6=2$ and recurs for spatial dimension $D=3$ in multiple domains. HasCubeFaceCount is the predicate on a finite type $T$ asserting Fintype.card $T=6$. Upstream results supply the Fintype structure from Mathlib together with auxiliary constants $A$ from integration gap, masses and modal actualization modules.
proof idea
The proof is a one-line term-mode wrapper. It rewrites the goal by substituting the defining equations of HasCubeFaceCount from hypotheses hA and hB, each of which equates the respective cardinality to 6.
why it matters
This theorem supports the structural claim of cube-face universality in the Recognition Science framework by showing that any two domains equipped with the count-6 predicate are equicardinal. It connects directly to the forcing chain landmark T8 that fixes $D=3$ spatial dimensions and to the module instances listing six quarks, six leptons and six cortical layers. No downstream theorems are recorded yet; the result closes the equicardinality step within the C15 universality statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.