sensory_hasConfigDim5
plain-language theorem explainer
The theorem asserts that the SensoryModality type has cardinality exactly five. Cross-domain universality proofs in the Recognition Science framework cite this result to establish the D=5 structure for sensory inputs. The proof proceeds as a one-line wrapper that unfolds the HasConfigDim5 predicate and invokes the decide tactic to confirm the finite cardinality.
Claim. Let SensoryModality be the finite type with five elements (sight, hearing, touch, smell, taste). Then Fintype.card SensoryModality = 5.
background
The module establishes the structural claim that configuration dimension D=5 appears across the framework with high frequency. HasConfigDim5 is the predicate on a type T (with Fintype instance) that holds precisely when Fintype.card T equals 5. SensoryModality is the inductive type whose five constructors are sight, hearing, touch, smell, and taste, deriving the necessary Fintype instance.
proof idea
The proof is a one-line wrapper. It unfolds HasConfigDim5 to expose the cardinality equality and applies the decide tactic, which succeeds on the computed Fintype.card value of 5.
why it matters
This instance populates the ConfigDimUniversalityCert record and supplies the sensory factor for three_domain_product (product cardinality 125) and five_domain_product (product cardinality 3125). It instantiates the module's universality claim for D=5 types and aligns with the framework's cross-domain product constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.