PhonologicalFeatureCert
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not derive the specific choice of five features from the J-uniqueness or phi fixed point.
- Does not connect the features to mass formulas or physical constants.
- Does not address how the features interact with the Recognition Composition Law.
- Does not provide a proof that these features generate all phonemes.
formal statement (Lean)
28structure PhonologicalFeatureCert where
29 five_features : Fintype.card PhonologicalFeature = 5
30