ConfigDimUniversalityCert
ConfigDimUniversalityCert packages five HasConfigDim5 instances for the sensory, emotional, biological, economic and linguistic domains together with a general triple-product lemma and the identity 5^5=3125. Cross-domain researchers cite it to certify uniform cardinality 5 across these categories in the Recognition Science framework. The declaration is a plain structure definition whose fields are filled by decidable cardinality facts from sibling lemmas.
claimLet HasConfigDim5(T) denote that a finite type T has cardinality exactly 5. The certificate asserts HasConfigDim5(SensoryModality), HasConfigDim5(PrimaryEmotion), HasConfigDim5(BiologicalState), HasConfigDim5(EconomicCycle) and HasConfigDim5(LinguisticRole), that any three such types A, B, C satisfy |A × B × C| = 125, that the five-fold product has cardinality 3125, and that 5^5 = 3125.
background
The module states that configDim D=5 appears across the framework with high frequency. HasConfigDim5(T) is the predicate that holds precisely when T is finite and Fintype.card T = 5. Five self-contained inductive types each carry exactly five constructors: SensoryModality (sight, hearing, touch, smell, taste), PrimaryEmotion (joy, sadness, fear, anger, disgust), BiologicalState (embryonic, developmental, mature, aging, senescent), EconomicCycle (recession, recovery, expansion, peak, contraction) and LinguisticRole (subject, verb, object, modifier, complement).
proof idea
The declaration is a structure definition. Its fields are populated directly by the sibling decidable instances sensory_hasConfigDim5, emotion_hasConfigDim5 and their analogues, together with the explicit Nat.pow and Fintype.card equalities that Lean reduces by decide.
why it matters in Recognition Science
The structure supplies the data for the downstream definition configDimUniversalityCert. It realizes the C13 structural claim that D=5 appears uniformly across domains, extending the self-similar five-state motif beyond the spatial D=3 of the T0-T8 chain. It does not yet link the domains to the J-cost or phi-ladder.
scope and limits
- Does not prove that configDim must equal 5 in every domain.
- Does not derive the listed domain partitions from the forcing chain or RCL.
- Does not supply explicit bijections between domains, only equicardinality.
- Does not address whether other cardinalities admit analogous cross-domain theorems.
Lean usage
def cert : ConfigDimUniversalityCert := configDimUniversalityCertformal statement (Lean)
101structure ConfigDimUniversalityCert where
102 sensory_5 : HasConfigDim5 SensoryModality
103 emotion_5 : HasConfigDim5 PrimaryEmotion
104 biological_5 : HasConfigDim5 BiologicalState
105 economic_5 : HasConfigDim5 EconomicCycle
106 linguistic_5 : HasConfigDim5 LinguisticRole
107 triple_125 : ∀ (A B C : Type) [Fintype A] [Fintype B] [Fintype C],
108 HasConfigDim5 A → HasConfigDim5 B → HasConfigDim5 C →
109 Fintype.card (A × B × C) = 125
110 five_domain_3125 :
111 Fintype.card (SensoryModality × PrimaryEmotion × BiologicalState ×
112 EconomicCycle × LinguisticRole) = 3125
113 five_pow_five : (5 : ℕ)^5 = 3125
114