configDimUniversalityCert
plain-language theorem explainer
This definition assembles a single certificate that five distinct domains each satisfy the HasConfigDim5 predicate, meaning each has finite cardinality exactly 5. Cross-domain researchers in Recognition Science cite it to invoke D=5 universality and the associated product cardinalities without repeating the per-domain proofs. The construction is a direct structure literal that wires together five decide-based cardinality theorems, a triple-product lemma, and the five-fold product identity.
Claim. Let $C$ be the certificate of D=5 universality. Then $C$ contains: $|$SensoryModality$|=5$, $|$PrimaryEmotion$|=5$, $|$BiologicalState$|=5$, $|$EconomicCycle$|=5$, $|$LinguisticRole$|=5$; for any three types $A,B,C$ each of cardinality 5, $|A×B×C|=125$; and $|$SensoryModality × PrimaryEmotion × BiologicalState × EconomicCycle × LinguisticRole$|=3125$, together with the numerical identity $5^5=3125$.
background
The module establishes cross-domain equicardinality at D=5. HasConfigDim5 T is the predicate that the finite type T has cardinality exactly 5. The five domains are SensoryModality, PrimaryEmotion, BiologicalState, EconomicCycle and LinguisticRole. Upstream theorems prove each instance by unfolding the predicate and deciding the cardinality. The five_domain_product theorem then shows that the Cartesian product of all five types has cardinality 3125, while fivePowFive records the elementary arithmetic fact $5^5=3125$.
proof idea
The definition is a structure literal that directly assigns the five domain-specific cardinality theorems (each proved by unfold HasConfigDim5; decide) to the corresponding fields of ConfigDimUniversalityCert. It further wires the pre-proved triple-product lemma into the triple_125 field and the five-domain product theorem into the five_domain_3125 field.
why it matters
The certificate packages the D=5 facts required by the C13 universality claim in the Recognition Science framework. It supplies a single reference object that any later cross-domain argument can use to obtain all five instances and the 125- and 3125-cardinality identities at once. The construction supports the structural observation that configuration dimension 5 appears with high frequency across domain modules, consistent with the framework's emphasis on discrete invariants such as the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.