phonologicalFeatureCert
plain-language theorem explainer
Definition phonologicalFeatureCert supplies the concrete certificate asserting that the phonological feature space has cardinality five, matching the configDim value of five. Linguists modeling SPE distinctive-feature matrices would cite it to anchor phoneme inventories in the five-axis system of place, manner, voicing, nasality and roundness. The construction is a direct one-line structure instantiation that populates the five_features field with the decidable cardinality theorem.
Claim. Let $P$ denote the type of phonological features. The definition supplies the structure instance satisfying the field condition $|P| = 5$.
background
PhonologicalFeatureCert is the structure whose sole field requires that the cardinality of the phonological feature type equals five. The module sets this cardinality to match configDim D = 5 and enumerates the five canonical axes: place, manner, voicing, nasality, roundness, which together generate the SPE feature matrix for attested phoneme inventories. The upstream theorem phonologicalFeature_count establishes the equality Fintype.card PhonologicalFeature = 5 by a decision procedure.
proof idea
One-line wrapper that constructs the PhonologicalFeatureCert structure by assigning its five_features field the value of the theorem phonologicalFeature_count.
why it matters
The definition closes the linguistics module by furnishing the certified instance of the five-dimensional feature space required by configDim D = 5 in the Recognition Science forcing chain. It supplies the concrete link between the phonological feature count and the dimensional constraints of the framework, though the module records no downstream uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.