PhonologicalFeatureCert
plain-language theorem explainer
A structure is introduced to certify that the phonological feature set has exactly five members. Linguists applying distinctive feature theory in the Recognition Science context would cite it to fix the dimensionality of the feature space. The definition is a straightforward record whose single field encodes the finite cardinality condition.
Claim. A certificate structure asserting that the set of phonological features has cardinality five, where the features are place, manner, voicing, nasality, and roundness.
background
The module defines five canonical phonological distinctive-feature axes that correspond to the configDim parameter set to five: place, manner, voicing, nasality, roundness. These axes span the SPE feature matrix generating attested phoneme inventories. An upstream result in LanguageAcquisitionFromJCost provides a separate inductive definition of phonological features consisting of vowel, consonant, tone, stress, and prosody, while this module specializes the feature set to the five axes for the dimensionality constraint.
proof idea
The declaration is a direct structure definition containing a single field that asserts the cardinality of the feature set equals five. No additional lemmas or tactics are invoked.
why it matters
This structure serves as the type for the phonological feature certificate constructor in the same module, which instantiates it with the feature count. It establishes the linguistic depth of the framework by fixing the number of distinctive features at five, aligning with the configDim dimension. The definition supports the embedding of phonological theory into the Recognition Science model without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.