pair_product_25
plain-language theorem explainer
Any two finite types each of cardinality 5 have Cartesian product of size 25. Cross-domain modelers cite the result when composing independent D=5 structures such as sensory and emotional domains. The proof is a one-line term that unfolds the cardinality predicate and simplifies the product rule.
Claim. Let $A$ and $B$ be finite types each satisfying $Fintype.card A = 5$ and $Fintype.card B = 5$. Then $Fintype.card (A × B) = 25$.
background
The module formalizes C13 universality of configuration dimension D=5 across Recognition Science domains. HasConfigDim5 is the predicate that a finite type T satisfies exactly when its cardinality is 5. The setting supplies five canonical domain instances and cross-product theorems for pairs and triples of such types.
proof idea
The term proof unfolds HasConfigDim5 at both hypotheses then applies simp with Fintype.card_prod and the resulting equalities to reduce the product cardinality directly to 25.
why it matters
The declaration supplies the equicardinality step inside the D=5 universality claim. It supports composition of the five listed domains and aligns with the framework's use of fixed cardinalities for configuration spaces. It prepares the ground for the sibling triple-product result of size 125.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.