triple_product_125
Any three finite types each of cardinality 5 have Cartesian product of size 125. Cross-domain researchers cite the result when confirming that D=5 structures multiply identically across sensory, emotional, and biological domains. The proof is a direct simplification after unfolding the cardinality predicate for each factor.
claimIf $A$, $B$, and $C$ are finite sets each with cardinality 5, then $|A × B × C| = 125$.
background
HasConfigDim5 holds for a type T precisely when T is finite and Fintype.card T = 5. The module formalizes D=5 universality across domains, stating that any three such types produce a product of size 125 and that every pair is equicardinal. Upstream results supply the HasConfigDim5 definition and place related structures on phi-tiers via NucleosynthesisTiers and PhiForcingDerived.
proof idea
The term proof unfolds HasConfigDim5 at each hypothesis then applies simp with Fintype.card_prod and the resulting equalities, reducing the product cardinality directly to 555.
why it matters in Recognition Science
The theorem supplies the general step used by three_domain_product for the concrete triple SensoryModality × PrimaryEmotion × BiologicalState and by configDimUniversalityCert. It fills the cross-domain product clause in the C13 universality statement. Within the framework it reinforces the observed prevalence of D=5 structures alongside the phi-ladder and eight-tick constructions.
scope and limits
- Does not establish HasConfigDim5 for any concrete domain.
- Does not treat products of two or four or more factors.
- Does not apply to non-finite types.
- Does not derive the cardinality 5 from deeper Recognition Science axioms.
Lean usage
theorem three_domain_product : Fintype.card (SensoryModality × PrimaryEmotion × BiologicalState) = 125 := triple_product_125 sensory_hasConfigDim5 emotion_hasConfigDim5 biological_hasConfigDim5formal statement (Lean)
60theorem triple_product_125
61 {A B C : Type} [Fintype A] [Fintype B] [Fintype C]
62 (hA : HasConfigDim5 A) (hB : HasConfigDim5 B) (hC : HasConfigDim5 C) :
63 Fintype.card (A × B × C) = 125 := by
proof body
Term-mode proof.
64 unfold HasConfigDim5 at hA hB hC
65 simp [Fintype.card_prod, hA, hB, hC]
66
67/-- Any pair of D=5 types has a product of size 25. -/