HasConfigDim5
A predicate on finite types asserting exact cardinality five. Cross-domain researchers cite it to certify that sensory modalities, primary emotions, biological states, economic cycles, and linguistic roles each realize a five-element configuration space. The definition is a direct abbreviation of the Fintype.card equality with no additional lemmas required.
claimA finite type $T$ has configuration dimension 5 when $|T|=5$.
background
Module C13 establishes configDim universality for D=5, stating that cardinality-five structures recur across roughly 90 percent of domain modules. The predicate HasConfigDim5 holds exactly when a type equipped with Fintype satisfies Fintype.card T = 5. This supplies the common interface for the five canonical domains listed in the module: SensoryModality, PrimaryEmotion, BiologicalState, EconomicCycle, and LinguisticRole.
proof idea
The declaration is a direct definition that sets the predicate equal to the cardinality condition Fintype.card T = 5. No lemmas from the upstream list are invoked; the body is a one-line abbreviation.
why it matters in Recognition Science
HasConfigDim5 anchors the ConfigDimUniversalityCert structure that collects the five domain instances and feeds the equicardinality and triple-product theorems. It realizes the structural claim of C13 that D=5 appears with high frequency, consistent with the eight-tick octave and self-similar fixed-point constructions of the Recognition framework. The definition closes the interface layer before the decide-based instance proofs.
scope and limits
- Does not prove that any concrete domain has cardinality five.
- Does not establish bijections or equinumerosity between distinct D=5 types.
- Does not link to the spatial dimension D=3 of the forcing chain T8.
- Does not derive the product size 125; that follows from separate theorems.
formal statement (Lean)
22def HasConfigDim5 (T : Type) [Fintype T] : Prop := Fintype.card T = 5
proof body
Definition body.
23
24/-! ## Five canonical D=5 domains (fresh local inductives, self-contained). -/
25