phonologicalFeature_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the feature set from the Recognition Composition Law or forcing chain.
- Does not apply to phonological systems outside the SPE framework.
- Does not prove that five is the minimal number of features needed for all languages.
formal statement (Lean)
26theorem phonologicalFeature_count : Fintype.card PhonologicalFeature = 5 := by decide
proof body
27