SensoryModality
plain-language theorem explainer
SensoryModality enumerates five perceptual channels as an inductive type whose cardinality is exactly 5. Cross-domain universality arguments in Recognition Science cite it as one of the five canonical D=5 instances. The declaration is a direct inductive construction that derives Fintype, from which the cardinality follows immediately.
Claim. Let SensoryModality be the finite set consisting of the five elements sight, hearing, touch, smell, taste. Then the cardinality of SensoryModality equals 5.
background
The module formalizes the structural claim that configuration dimension D=5 appears across five domains in the Recognition Science framework. HasConfigDim5 is the predicate on a finite type T asserting that Fintype.card T equals 5. SensoryModality supplies one of the five self-contained inductive instances; the others are PrimaryEmotion, BiologicalState, EconomicCycle, and LinguisticRole.
proof idea
This is a direct inductive definition with five constructors that derives DecidableEq, Repr, BEq, and Fintype. The derived Fintype instance immediately yields cardinality 5, which is then unfolded into HasConfigDim5 and discharged by decide in the companion theorem sensory_hasConfigDim5.
why it matters
The definition supplies the sensory_5 field of the ConfigDimUniversalityCert structure that collects all five D=5 domains. It is invoked by five_domain_product to obtain the 5^5 = 3125 cardinality of the full product and by three_domain_product for the 125 cardinality of the sensory-emotion-biological triple. This contributes to the documented universality of D=5 structures across the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.