ConfigDimUniversalityCert
plain-language theorem explainer
ConfigDimUniversalityCert packages five HasConfigDim5 instances for the listed domain types together with a general triple-product cardinality rule and the explicit five-fold product count. Cross-domain researchers in the Recognition framework cite the resulting certificate when invoking D=5 universality. The declaration is a direct structure definition whose fields are populated by the sibling cardinality lemmas.
Claim. A structure whose fields assert: each of SensoryModality, PrimaryEmotion, BiologicalState, EconomicCycle and LinguisticRole satisfies $Fintype.card = 5$; for any three finite types $A,B,C$ each of cardinality 5 their product has cardinality 125; the five-fold product has cardinality 3125; and $5^5 = 3125$.
background
The module formalises the observation that configDim D=5 occurs across independent domain modules. HasConfigDim5 (T : Type) [Fintype T] is the predicate $Fintype.card T = 5$. The five concrete domains are fresh inductive types, each with 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). MODULE_DOC states the structural claim that D=5 appears with overwhelming frequency and records that the Lean development contains zero sorry or axiom.
proof idea
The declaration is a structure definition; its fields are simply the five HasConfigDim5 instances supplied by the sibling lemmas sensory_hasConfigDim5 etc., the quantified triple-product statement, the five-domain cardinality equation, and the numerical identity $5^5 = 3125$. No tactics or lemmas are applied inside the definition itself.
why it matters
The structure is instantiated by the downstream definition configDimUniversalityCert, which supplies a single witness object for the C13 universality claim. It therefore serves as the canonical carrier for any later theorem that needs to invoke simultaneous D=5 structure across the five listed domains. The construction sits outside the core T0-T8 forcing chain (which fixes spatial dimension D=3) and remains a cross-domain organisational device rather than a derived physical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.