ConfigDimUniversalityCert
plain-language theorem explainer
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.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.