PhonologicalFeature
plain-language theorem explainer
The inductive type enumerates the five phonological feature axes place, manner, voicing, nasality and roundness that arise for configDim equal to 5. Researchers applying Recognition Science to language acquisition cite this enumeration to fix the SPE feature matrix for phoneme inventories. The declaration is a direct inductive definition that derives decidable equality and finite type structure.
Claim. Let $F$ be the finite set of phonological features $F = $ {place, manner, voicing, nasality, roundness}, equipped with decidable equality and Fintype structure, with cardinality 5.
background
In the Recognition Science linguistics module, configDim is the dimension of the configuration space; here it is specialized to D = 5 to generate the canonical phonological axes. The module states that these five axes (place of articulation, manner of articulation, voicing, nasality, roundness) span the SPE (Chomsky-Halle) feature matrix that produces every attested phoneme inventory. Lean status is zero sorry and zero axiom.
proof idea
The declaration is an inductive definition that introduces exactly five constructors, one for each feature axis. It automatically derives the instances DecidableEq, Repr, BEq and Fintype, which together establish that the type is finite with cardinality five.
why it matters
This definition supplies the concrete feature set used by PhonologicalFeatureCert and the theorem phonologicalFeature_count, both of which assert Fintype.card = 5. It feeds LanguageAcquisitionCert in the sibling module, where feature_count equals 5 and critical_period_threshold is a CanonicalCert. The enumeration aligns with the configDim = 5 specialization and supports the claim that language acquisition thresholds derive from J-cost; it touches the open question of how configDim = 5 emerges from the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.