three_domain_product
plain-language theorem explainer
The theorem shows that the Cartesian product of three five-element sets, one each from sensory modalities, primary emotions, and biological states, has exactly 125 elements. Cross-domain researchers in Recognition Science cite it to confirm the repeated D=5 pattern. The proof is a direct one-line application of the general triple-product lemma to the three decidable cardinality facts for these domains.
Claim. Let $S$, $E$, and $B$ be the sets of sensory modalities, primary emotions, and biological states, each of cardinality 5. Then $|S × E × B| = 125$.
background
The module formalizes configDim universality for D=5 across domains. HasConfigDim5(T) is the predicate that a finite type T satisfies Fintype.card T = 5. Three self-contained inductive types are introduced: SensoryModality with five cases (sight, hearing, touch, smell, taste), PrimaryEmotion with five cases (joy, sadness, fear, anger, disgust), and BiologicalState with five cases (embryonic, developmental, mature, aging, senescent). Each satisfies HasConfigDim5 by a decide tactic after unfolding the predicate. The upstream results are precisely these three cardinality theorems together with the inductive definitions of the types.
proof idea
The proof is a term-mode one-liner that feeds the three domain-specific HasConfigDim5 theorems into the general triple_product_125 lemma. No further tactics or reductions are required once the three decidable facts are supplied.
why it matters
This supplies a concrete cross-domain instance inside the C13 universality claim that D=5 appears in roughly 90 percent of domain modules. It directly illustrates the module's third point: any three D=5 types produce a product of size 125. The result sits inside the broader Recognition Science pattern of five-fold structures without yet connecting to the forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.