IndisputableMonolith.Linguistics.PhonologicalFeaturesFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Phonological Features from configDim — Linguistics Depth
   6
   7Five canonical phonological distinctive-feature axes (= configDim D = 5):
   8  place, manner, voicing, nasality, roundness.
   9
  10These span the SPE (Chomsky-Halle) feature matrix that generates every
  11attested phoneme inventory.
  12
  13Lean status: 0 sorry, 0 axiom.
  14-/
  15
  16namespace IndisputableMonolith.Linguistics.PhonologicalFeaturesFromConfigDim
  17
  18inductive PhonologicalFeature where
  19  | place
  20  | manner
  21  | voicing
  22  | nasality
  23  | roundness
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem phonologicalFeature_count : Fintype.card PhonologicalFeature = 5 := by decide
  27
  28structure PhonologicalFeatureCert where
  29  five_features : Fintype.card PhonologicalFeature = 5
  30
  31def phonologicalFeatureCert : PhonologicalFeatureCert where
  32  five_features := phonologicalFeature_count
  33
  34end IndisputableMonolith.Linguistics.PhonologicalFeaturesFromConfigDim
  35