theorem
proved
phonologicalFeatureCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Linguistics.LanguageAcquisitionFromJCost on GitHub at line 30.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
27 | vowel | consonant | tone | stress | prosody
28 deriving DecidableEq, Repr, BEq, Fintype
29
30theorem phonologicalFeatureCount : Fintype.card PhonologicalFeature = 5 := by decide
31
32structure LanguageAcquisitionCert where
33 feature_count : Fintype.card PhonologicalFeature = 5
34 critical_period_threshold : CanonicalCert
35
36noncomputable def languageAcquisitionCert : LanguageAcquisitionCert where
37 feature_count := phonologicalFeatureCount
38 critical_period_threshold := cert
39
40end IndisputableMonolith.Linguistics.LanguageAcquisitionFromJCost