Documentation

Linglib.Theories.Phonology.SibilantTier

Sibilant-tier substrate #

A small alphabet shared across linglib's sibilant-harmony formalisations (Athabaskan, Berber, Chumash, …): three classes — anterior (alveolar sibilants [s, z, ts, dz, …]), posterior (postalveolar [ʃ, ʒ, tʃ, dʒ, …]), and neutral (everything else, off the harmony tier). Plus the canonical on-tier predicate, the symmetric harmony grammar (Navajo, Berber Tashlhiyt — both directions of disagreement forbidden), and the asymmetric harmony grammars (Tsuut'ina — only one direction forbidden).

The audit chronology: Lambert (2026) §4.2 (Tsuut'ina) and Hansson (2010) §2.4.1 (Navajo) independently stipulated their own three- and four-case inductive types for the same primitive. The four-case Navajo alphabet (NSeg) preserves a neutralC vs vowel distinction that no theorem uses but that documents word-list examples; it is left in place as the educational alphabet. The three-case substrate here is what Tsuut'ina (and any future asymmetric-harmony paper) consumes directly.

Main definitions #

References #

source
inductive Theories.Phonology.SibilantTier.SibilantTierSeg :
Type

Three-class sibilant-tier alphabet: anterior (s-class), posterior (ʃ-class), and neutral (off the harmony tier). The minimal alphabet sufficient for sibilant-harmony formalisations; finer-grained alphabets (e.g. Hansson 2010's NSeg distinguishing non-sibilant consonants from vowels) are paper-specific elaborations that don't change the harmony constraint.

Instances For
    source
    @[implicit_reducible]
    instance Theories.Phonology.SibilantTier.instDecidableEqSibilantTierSeg :
    DecidableEq SibilantTierSeg
    Equations
    source
    def Theories.Phonology.SibilantTier.instReprSibilantTierSeg.repr :
    SibilantTierSeg → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Theories.Phonology.SibilantTier.instReprSibilantTierSeg :
      Repr SibilantTierSeg
      Equations
      source
      @[reducible]
      def Theories.Phonology.SibilantTier.SibilantTierSeg.onTier :
      SibilantTierSeg → Prop

      The harmony-tier predicate: only sibilants project onto the tier; neutral material is transparent.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Theories.Phonology.SibilantTier.instDecidablePredSibilantTierSegOnTier :
        DecidablePred SibilantTierSeg.onTier
        Equations
        source
        def Theories.Phonology.SibilantTier.symmetricHarmony :
        Core.Computability.Subregular.TSLGrammar 2 SibilantTierSeg

        The symmetric sibilant-harmony TSL_2 grammar: any disagreement between adjacent (on-tier) sibilants is forbidden. Identity-relation- inverse specialisation of TSLGrammar.agree to the three-case alphabet. Matches the @cite{sapir-hoijer-1967} / @cite{hansson-2010} Navajo analysis and other Athabaskan symmetric-harmony languages.

        Equations
        Instances For
          source
          def Theories.Phonology.SibilantTier.antPostForbidden :
          SibilantTierSeg → SibilantTierSeg → Prop

          Forbidden-pair relation for "anterior preceding posterior is forbidden on the tier" — the @cite{cook-1978} Tsuut'ina pattern.

          Equations
          Instances For
            source
            @[implicit_reducible]
            instance Theories.Phonology.SibilantTier.instDecidableRelSibilantTierSegAntPostForbidden :
            DecidableRel antPostForbidden
            Equations
            source
            def Theories.Phonology.SibilantTier.asymmetricHarmonyAntFirst :
            Core.Computability.Subregular.TSLGrammar 2 SibilantTierSeg

            The asymmetric sibilant-harmony TSL_2 grammar with anterior-first prohibition: an anterior sibilant immediately preceding a posterior sibilant on the tier is forbidden, but the reverse adjacency [posterior, anterior] is permitted. The @cite{cook-1978} @cite{lambert-2026} §4.2 Tsuut'ina pattern.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Theories.Phonology.SibilantTier.postAntForbidden :
              SibilantTierSeg → SibilantTierSeg → Prop

              Dual: posterior preceding anterior is forbidden. The reverse direction of asymmetricHarmonyAntFirst; provided for completeness so either asymmetric direction can be selected by name.

              Equations
              Instances For
                source
                @[implicit_reducible]
                instance Theories.Phonology.SibilantTier.instDecidableRelSibilantTierSegPostAntForbidden :
                DecidableRel postAntForbidden
                Equations
                source
                def Theories.Phonology.SibilantTier.asymmetricHarmonyPostFirst :
                Core.Computability.Subregular.TSLGrammar 2 SibilantTierSeg

                Posterior-first asymmetric sibilant-harmony TSL_2 grammar.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Theories.Phonology.SibilantTier.symmetricHarmony_lang_subset_asymAntFirst :
                  symmetricHarmony.lang ≤ asymmetricHarmonyAntFirst.lang

                  The symmetric harmony language is contained in each asymmetric harmony language: anything ruled out by the asymmetric constraint (which forbids only one direction) is also ruled out by the symmetric one (which forbids both). Application of lang_antitone_R: forbidding more pairs (antPostForbidden ⊆ (· ≠ ·)) shrinks the language.

                  source
                  theorem Theories.Phonology.SibilantTier.symmetricHarmony_lang_subset_asymPostFirst :
                  symmetricHarmony.lang ≤ asymmetricHarmonyPostFirst.lang

                  Dual inclusion.