Cavirani & Vanden Wyngaerd (2026): Czech palatalisation

[CVW26]

Czech has three palatalisation patterns triggered by different suffixes. The trigger is not the suffix's front vowel but a set of floating elements the suffix carries; the triggers (PAL₁ ⊏ PAL₂ ⊏ PAL₃, "small/medium/big") stand in a containment relation — PAL₁ adds |I|, PAL₂ adds |H| + |I|, PAL₃ adds |H| + headed |I̲| — which is exactly the substrate's Segment.Refines order (palataliser_chain).

Floating elements dock onto a base; the substance-free interpret : Segment → CzechPhone reproduces the paper's tables (velar_derivations, coronal_derivations), is non-injective (interpret_not_injective), and reads the |I|-vs-|I̲| contrast differently on velars vs /s/. Labial output-invisibility and lateral resistance follow from the |U|⊕|I| antagonism (labial_output_invisible, lateral_resists).

Scope

Representational output only — which elements end up in which node. The strict-CV skeleton and government/licensing driving the slot-by-slot derivations ([Low96], [Sch04a]), the glide-vs-invisible labial split, and the /m/ → [mɲ] nasal spreading are not modelled. (Studies/FaustLampitelli2026.lean inlines a StrictCV substrate; this is its second consumer — a shared graduation is the natural next step.)

Plain consonants (Tables 9, 11, 13; voiceless members only)

The dot convention is manner node . place node. /r/ has |A| in the manner node whereas /s/ has |A| in the place node — the contrast the geometry is for.

def CaviraniVandenWyngaerd2026.k : ElementTheory.Segment

/k/ = |ʔ| — a placeless velar stop.

Equations

• CaviraniVandenWyngaerd2026.k = { manner := ElementTheory.MR.simplex ElementTheory.Element.glottal, place := ElementTheory.MR.empty, laryngeal := ElementTheory.MR.empty }

def CaviraniVandenWyngaerd2026.x : ElementTheory.Segment

/x/ = |H| — a placeless velar fricative.

Equations

• CaviraniVandenWyngaerd2026.x = { manner := ElementTheory.MR.simplex ElementTheory.Element.H, place := ElementTheory.MR.empty, laryngeal := ElementTheory.MR.empty }

def CaviraniVandenWyngaerd2026.t : ElementTheory.Segment

/t/ = |ʔ.A| — coronal stop (|ʔ| manner, |A| place).

Equations

• One or more equations did not get rendered due to their size.

def CaviraniVandenWyngaerd2026.s : ElementTheory.Segment

/s/ = |H.AI| — coronal fricative (|H| manner, |A I| place).

Equations

• One or more equations did not get rendered due to their size.

def CaviraniVandenWyngaerd2026.n : ElementTheory.Segment

/n/ = |L.A| — coronal nasal (|L| manner, |A| place).

Equations

• CaviraniVandenWyngaerd2026.n = { manner := ElementTheory.MR.simplex ElementTheory.Element.L, place := ElementTheory.MR.simplex ElementTheory.Element.A, laryngeal := ElementTheory.MR.empty }

def CaviraniVandenWyngaerd2026.r : ElementTheory.Segment

/r/ = |A| — a rhotic, |A| in the manner node.

Equations

• CaviraniVandenWyngaerd2026.r = { manner := ElementTheory.MR.simplex ElementTheory.Element.A, place := ElementTheory.MR.empty, laryngeal := ElementTheory.MR.empty }

def CaviraniVandenWyngaerd2026.p : ElementTheory.Segment

/p/ = |ʔ.U| — labial stop (|ʔ| manner, |U| place).

Equations

• One or more equations did not get rendered due to their size.

def CaviraniVandenWyngaerd2026.f : ElementTheory.Segment

/f/ = |H.U| — labial fricative.

Equations

• CaviraniVandenWyngaerd2026.f = { manner := ElementTheory.MR.simplex ElementTheory.Element.H, place := ElementTheory.MR.simplex ElementTheory.Element.U, laryngeal := ElementTheory.MR.empty }

def CaviraniVandenWyngaerd2026.m : ElementTheory.Segment

/m/ = |L.U| — labial nasal.

Equations

• CaviraniVandenWyngaerd2026.m = { manner := ElementTheory.MR.simplex ElementTheory.Element.L, place := ElementTheory.MR.simplex ElementTheory.Element.U, laryngeal := ElementTheory.MR.empty }

def CaviraniVandenWyngaerd2026.l : ElementTheory.Segment

/l/ = |A.U| — the lateral; its |U| place makes it pattern with the labials [CVW26].

Equations

• CaviraniVandenWyngaerd2026.l = { manner := ElementTheory.MR.simplex ElementTheory.Element.A, place := ElementTheory.MR.simplex ElementTheory.Element.U, laryngeal := ElementTheory.MR.empty }

The three palatalisers (Table 8) and their suffixes

def CaviraniVandenWyngaerd2026.PAL₁ : ElementTheory.Segment

PAL₁ ("small"): a floating |I| in the place node.

Equations

• CaviraniVandenWyngaerd2026.PAL₁ = { manner := ElementTheory.MR.empty, place := ElementTheory.MR.simplex ElementTheory.Element.I, laryngeal := ElementTheory.MR.empty }

def CaviraniVandenWyngaerd2026.PAL₂ : ElementTheory.Segment

PAL₂ ("medium"): floating |H| (manner) + |I| (place).

Equations

• CaviraniVandenWyngaerd2026.PAL₂ = { manner := ElementTheory.MR.simplex ElementTheory.Element.H, place := ElementTheory.MR.simplex ElementTheory.Element.I, laryngeal := ElementTheory.MR.empty }

def CaviraniVandenWyngaerd2026.PAL₃ : ElementTheory.Segment

PAL₃ ("big"): floating |H| (manner) + headed |I̲| (place).

Equations

• One or more equations did not get rendered due to their size.

inductive CaviraniVandenWyngaerd2026.Suffix : Type

The palatalising suffixes; look-alikes split by their floating element, not their vowel (-ý/-í are both [iː] but only -í palatalises).

• locDatFSg : Suffix

  -ě LOC/DAT.F.SG, e.g. louka 'meadow' ~ louce.

• comparative : Suffix

  -ěj comparative, e.g. divoký 'wild' ~ divočejší.

• causative : Suffix

  -i causative, e.g. trpký 'bitter' ~ ztrpčil.

• passPtcp : Suffix

  -ěn passive participle, e.g. nutit 'force' ~ nucen.

@[implicit_reducible]

instance CaviraniVandenWyngaerd2026.instDecidableEqSuffix : DecidableEq Suffix

Equations

• CaviraniVandenWyngaerd2026.instDecidableEqSuffix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance CaviraniVandenWyngaerd2026.instReprSuffix : Repr Suffix

Equations

• CaviraniVandenWyngaerd2026.instReprSuffix = { reprPrec := CaviraniVandenWyngaerd2026.instReprSuffix.repr }

def CaviraniVandenWyngaerd2026.instReprSuffix.repr : Suffix → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def CaviraniVandenWyngaerd2026.Suffix.palataliser : Suffix → ElementTheory.Segment

The palataliser each suffix carries (§4.2 / Table 8).

Equations

• CaviraniVandenWyngaerd2026.Suffix.locDatFSg.palataliser = CaviraniVandenWyngaerd2026.PAL₁
• CaviraniVandenWyngaerd2026.Suffix.comparative.palataliser = CaviraniVandenWyngaerd2026.PAL₂
• CaviraniVandenWyngaerd2026.Suffix.causative.palataliser = CaviraniVandenWyngaerd2026.PAL₂
• CaviraniVandenWyngaerd2026.Suffix.passPtcp.palataliser = CaviraniVandenWyngaerd2026.PAL₃

Palatalisation

def CaviraniVandenWyngaerd2026.palatalise (base pal : ElementTheory.Segment) : ElementTheory.Segment

Palatalisation: the floating palataliser docks onto the base node-by-node ([CVW26] §4.3, convention (13)).

Equations

• CaviraniVandenWyngaerd2026.palatalise base pal = base.dock pal

The palataliser containment chain

theorem CaviraniVandenWyngaerd2026.palataliser_chain : PAL₁ ≤ PAL₂ ∧ PAL₂ ≤ PAL₃

PAL₁ ⊏ PAL₂ ⊏ PAL₃ in the refinement order [CVW26]: PAL₁ ⊏ PAL₂ adds |H|; PAL₂ ⊏ PAL₃ heads |I|.

theorem CaviraniVandenWyngaerd2026.palatalisers_distinct : PAL₁ ≠ PAL₂ ∧ PAL₂ ≠ PAL₃ ∧ PAL₁ ≠ PAL₃

The three palatalisers are distinct.

theorem CaviraniVandenWyngaerd2026.palataliser_chain_strict : PAL₁ < PAL₂ ∧ PAL₂ < PAL₃

The chain is therefore strict: PAL₁ ⊏ PAL₂ ⊏ PAL₃.

Phonetic interpretation and derivation tables (Tables 11, 13)

inductive CaviraniVandenWyngaerd2026.CzechPhone : Type

The voiceless Czech phones; ASCII for IPA: tsh=[t͡ʃ], sh=[ʃ], nj=[ɲ], rj=[r̝].

• k : CzechPhone
• x : CzechPhone
• t : CzechPhone
• s : CzechPhone
• n : CzechPhone
• r : CzechPhone
• ts : CzechPhone
• tsh : CzechPhone
• c : CzechPhone
• sh : CzechPhone
• nj : CzechPhone
• rj : CzechPhone

@[implicit_reducible]

instance CaviraniVandenWyngaerd2026.instDecidableEqCzechPhone : DecidableEq CzechPhone

Equations

• CaviraniVandenWyngaerd2026.instDecidableEqCzechPhone x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CaviraniVandenWyngaerd2026.instReprCzechPhone.repr : CzechPhone → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance CaviraniVandenWyngaerd2026.instReprCzechPhone : Repr CzechPhone

Equations

• CaviraniVandenWyngaerd2026.instReprCzechPhone = { reprPrec := CaviraniVandenWyngaerd2026.instReprCzechPhone.repr }

def CaviraniVandenWyngaerd2026.interpret (seg : ElementTheory.Segment) : CzechPhone

Substance-free phonetic interpretation (lexical access, [Bac11]-style; [CVW26] §4.1); domain is the non-labial inventory.

Equations

• One or more equations did not get rendered due to their size.

theorem CaviraniVandenWyngaerd2026.plain_interpretation : interpret k = CzechPhone.k ∧ interpret x = CzechPhone.x ∧ interpret t = CzechPhone.t ∧ interpret s = CzechPhone.s ∧ interpret n = CzechPhone.n ∧ interpret r = CzechPhone.r

The plain consonants interpret as themselves.

theorem CaviraniVandenWyngaerd2026.velar_derivations : interpret (palatalise k PAL₁) = CzechPhone.ts ∧ interpret (palatalise k PAL₂) = CzechPhone.tsh ∧ interpret (palatalise k PAL₃) = CzechPhone.tsh ∧ interpret (palatalise x PAL₁) = CzechPhone.sh ∧ interpret (palatalise x PAL₂) = CzechPhone.sh ∧ interpret (palatalise x PAL₃) = CzechPhone.sh

Velar derivations (Table 11): /k/ ts tʃ tʃ; /x/ neutralises to [ʃ].

theorem CaviraniVandenWyngaerd2026.coronal_derivations : interpret (palatalise t PAL₁) = CzechPhone.c ∧ interpret (palatalise t PAL₂) = CzechPhone.c ∧ interpret (palatalise t PAL₃) = CzechPhone.ts ∧ interpret (palatalise s PAL₁) = CzechPhone.s ∧ interpret (palatalise s PAL₂) = CzechPhone.s ∧ interpret (palatalise s PAL₃) = CzechPhone.sh ∧ interpret (palatalise n PAL₁) = CzechPhone.nj ∧ interpret (palatalise n PAL₂) = CzechPhone.nj ∧ interpret (palatalise n PAL₃) = CzechPhone.nj ∧ interpret (palatalise r PAL₁) = CzechPhone.rj ∧ interpret (palatalise r PAL₂) = CzechPhone.rj ∧ interpret (palatalise r PAL₃) = CzechPhone.rj

Coronal derivations (Table 13): /t/ c c ts; /s/ s s ʃ; /n/, /r/ uniform [ɲ], [r̝].

Small / medium / big (Table 4b)

def CaviraniVandenWyngaerd2026.applySuffix (base : ElementTheory.Segment) (suf : Suffix) : CzechPhone

Surface phone of a suffix's palataliser applied to a base.

Equations

• CaviraniVandenWyngaerd2026.applySuffix base suf = CaviraniVandenWyngaerd2026.interpret (CaviraniVandenWyngaerd2026.palatalise base suf.palataliser)

theorem CaviraniVandenWyngaerd2026.suffix_outcomes_on_k : applySuffix k Suffix.locDatFSg = CzechPhone.ts ∧ applySuffix k Suffix.comparative = CzechPhone.tsh ∧ applySuffix k Suffix.causative = CzechPhone.tsh ∧ applySuffix k Suffix.passPtcp = CzechPhone.tsh

The suffixes' outcomes on the diagnostic velar /k/: -ě [ts]; -ěj/-i [tʃ]; -ěn [tʃ] — look-alikes splitting by floating element, not vowel.

theorem CaviraniVandenWyngaerd2026.k_small_vs_medium : interpret (palatalise k PAL₁) ≠ interpret (palatalise k PAL₂)

/k/ diagnoses small vs medium: PAL₁ [ts] ≠ PAL₂ [tʃ].

theorem CaviraniVandenWyngaerd2026.t_medium_vs_big : interpret (palatalise t PAL₂) ≠ interpret (palatalise t PAL₃)

/t/ diagnoses medium vs big: PAL₂ [c] ≠ PAL₃ [ts].

theorem CaviraniVandenWyngaerd2026.three_distinct_patterns : (∃ (base : ElementTheory.Segment), interpret (palatalise base PAL₁) ≠ interpret (palatalise base PAL₂)) ∧ ∃ (base : ElementTheory.Segment), interpret (palatalise base PAL₂) ≠ interpret (palatalise base PAL₃)

The three patterns are genuinely three (separated by /k/ and /t/).

The substance-free payoff

theorem CaviraniVandenWyngaerd2026.interpret_not_injective : interpret (palatalise x PAL₁) = CzechPhone.sh ∧ interpret (palatalise s PAL₃) = CzechPhone.sh ∧ (palatalise x PAL₁).place.elements ≠ (palatalise s PAL₃).place.elements

interpret is non-injective (Table 12): palatalised /x/ (|H.I|) and big-palatalised /s/ (|H.A I̲|) are different structures, both [ʃ].

theorem CaviraniVandenWyngaerd2026.headedness_invisible_on_velars : interpret (palatalise k PAL₂) = interpret (palatalise k PAL₃) ∧ (palatalise k PAL₂).place.head ≠ (palatalise k PAL₃).place.head

Headedness of |I| is invisible on velars: PAL₂ and PAL₃ differ in the place head but both surface as [tʃ].

theorem CaviraniVandenWyngaerd2026.headedness_visible_on_coronal_s : interpret (palatalise s PAL₂) ≠ interpret (palatalise s PAL₃)

…yet the same |I|-vs-|I̲| difference is visible on /s/: [s] vs [ʃ].

Labial output-invisibility and lateral resistance (the |U|⊕|I| clash)

def CaviraniVandenWyngaerd2026.PlaceColourClash (seg : ElementTheory.Segment) : Prop

A colour clash: |U| and |I| (antagonistic) both in the place node — which Czech forbids ([CVW26] §4.3.3, after [Jan22]).

Equations

• CaviraniVandenWyngaerd2026.PlaceColourClash seg = ¬seg.place.AntagonismFree

@[implicit_reducible]

instance CaviraniVandenWyngaerd2026.instDecidablePlaceColourClash (seg : ElementTheory.Segment) : Decidable (PlaceColourClash seg)

Equations

• CaviraniVandenWyngaerd2026.instDecidablePlaceColourClash seg = id inferInstance

theorem CaviraniVandenWyngaerd2026.labial_output_invisible : PlaceColourClash (palatalise p PAL₁)

Labial output-invisibility: docking |I| onto a labial (place |U|) would forge the forbidden |U I| place — so labials never fully palatalise.

theorem CaviraniVandenWyngaerd2026.all_labials_clash : PlaceColourClash (palatalise f PAL₁) ∧ PlaceColourClash (palatalise m PAL₁)

/f/ and /m/ clash too — all labials carry |U| in place.

theorem CaviraniVandenWyngaerd2026.lateral_resists : PlaceColourClash (palatalise l PAL₁)

Lateral resistance: /l/ carries |U| in place, so it clashes like the labials — why /l/ never palatalises ([CVW26] §4.3.4).

theorem CaviraniVandenWyngaerd2026.velar_no_clash : (palatalise k PAL₁).place.AntagonismFree

A velar (placeless) keeps an antagonism-free place node — so velars palatalise freely.

theorem CaviraniVandenWyngaerd2026.coronal_no_clash : (palatalise t PAL₁).place.AntagonismFree ∧ (palatalise s PAL₁).place.AntagonismFree

The clash is colour-specific: coronals (place |A I|) stay antagonism-free.