phonologicalFeature_count
plain-language theorem explainer
The declaration fixes the number of phonological features at five. Linguists applying Recognition Science to phonology cite it to anchor the dimension of the distinctive feature space. The proof is a direct decision procedure on the enumerated inductive type.
Claim. The set of phonological features has cardinality five, with the features being place, manner, voicing, nasality, and roundness: $5 = |$ {place, manner, voicing, nasality, roundness} $|$.
background
The module defines five canonical phonological distinctive-feature axes equal to configDim D = 5: place, manner, voicing, nasality, roundness. These axes generate the SPE feature matrix for all attested phoneme inventories. The inductive type lists precisely these five constructors and derives the Fintype instance required for cardinality statements.
proof idea
The proof applies the decide tactic in a single step to compute the cardinality of the finite type by enumerating its constructors.
why it matters
This theorem provides the cardinality value consumed by the downstream phonological feature certificate, which records five_features equal to this count. It implements the configDim D = 5 landmark for the linguistics extension of the Recognition framework, aligning with the five axes of the SPE matrix. The result closes the count for this feature set without addressing further derivations from the J-cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.