Complex and Contour Segments @cite{sagey-1986}

Segments with multiple simultaneous or sequential articulations.

Complex segments have one root node with multiple place articulator nodes active simultaneously (e.g., labiovelars [k͡p], [g͡b]; corono-velar clicks). They occupy a single timing slot and their articulations are unordered. The soft palate is an articulator in the vocal tract but sits outside the place node, so nasal + place combinations (e.g., [ŋ]) are simple segments, not complex ones.

Contour segments have two root nodes linked to a single timing slot, with articulations in sequence (e.g., affricates [ts], [tʃ]; prenasalized stops [ⁿd], [ᵐb]).

The distinction was established by @cite{sagey-1986} and is now standard in phonological theory. The feature geometry predicts exactly which complex segments are possible: only those combining distinct articulator nodes. Palatal–velar stops are impossible because both use the dorsal articulator; labio-velars are possible because labial and dorsal are independent.

def Phonology.FeatureGeometry.GeomNode.IsArticulator : GeomNode → Prop

Is this a place articulator node? The three place articulators — labial (lips), coronal (tongue blade/tip), dorsal (tongue body) — are the independent articulators whose combinations give rise to complex segments (@cite{sagey-1986} Ch. 2). The soft palate is an articulator in the vocal tract but sits outside the place node (as a sibling under supralaryngeal), so it does not participate in complex segment formation: a velar nasal [ŋ] is simple despite activating both dorsal and soft palate.

Equations

• Phonology.FeatureGeometry.GeomNode.labial.IsArticulator = True
• Phonology.FeatureGeometry.GeomNode.coronal.IsArticulator = True
• Phonology.FeatureGeometry.GeomNode.dorsal.IsArticulator = True
• x✝.IsArticulator = False

@[implicit_reducible]

instance Phonology.FeatureGeometry.instDecidablePredGeomNodeIsArticulator : DecidablePred GeomNode.IsArticulator

Equations

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

def Phonology.ComplexSegments.articulatorNodes : List FeatureGeometry.GeomNode

The articulator nodes in the geometry.

Equations

• Phonology.ComplexSegments.articulatorNodes = List.filter (fun (n : Phonology.FeatureGeometry.GeomNode) => decide n.IsArticulator) Phonology.FeatureGeometry.GeomNode.allNodes

theorem Phonology.ComplexSegments.articulatorNodes_count : articulatorNodes.length = 3

def Phonology.ComplexSegments.activeArticulators (s : Segment) : List FeatureGeometry.GeomNode

Which articulator nodes have at least one specified feature in segment s?

Equations

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

def Phonology.ComplexSegments.articulatorCount (s : Segment) : Nat

Number of active articulator nodes in a segment.

Equations

• Phonology.ComplexSegments.articulatorCount s = (Phonology.ComplexSegments.activeArticulators s).length

def Phonology.ComplexSegments.IsComplex (s : Segment) : Prop

A complex segment has two or more simultaneously active articulator nodes — e.g., labiovelars [k͡p] (labial + dorsal).

Equations

• Phonology.ComplexSegments.IsComplex s = (Phonology.ComplexSegments.articulatorCount s ≥ 2)

@[implicit_reducible]

instance Phonology.ComplexSegments.instDecidablePredSegmentIsComplex : DecidablePred IsComplex

Equations

• Phonology.ComplexSegments.instDecidablePredSegmentIsComplex x✝ = Phonology.ComplexSegments.instDecidablePredSegmentIsComplex._aux_1 x✝

def Phonology.ComplexSegments.ComplexWF (s : Segment) : Prop

Complex segment well-formedness: active articulators must be distinct nodes. This is trivially satisfied by activeArticulators (which returns a duplicate-free sublist of articulatorNodes), but we state it explicitly as the standard WFC.

Equations

• Phonology.ComplexSegments.ComplexWF s = ((Phonology.ComplexSegments.activeArticulators s).length = (Phonology.ComplexSegments.activeArticulators s).eraseDups.length)

@[implicit_reducible]

instance Phonology.ComplexSegments.instDecidablePredSegmentComplexWF : DecidablePred ComplexWF

Equations

• Phonology.ComplexSegments.instDecidablePredSegmentComplexWF x✝ = Phonology.ComplexSegments.instDecidablePredSegmentComplexWF._aux_1 x✝

theorem Phonology.ComplexSegments.articulators_are_leaves (n : FeatureGeometry.GeomNode) : n ∈ articulatorNodes → n.children = []

Articulators are exactly the leaf-level nodes (no children).

theorem Phonology.ComplexSegments.articulators_under_root (n : FeatureGeometry.GeomNode) : n ∈ articulatorNodes → FeatureGeometry.GeomNode.root.Dominates n

Every articulator is dominated by root.

theorem Phonology.ComplexSegments.labial_ne_dorsal : FeatureGeometry.GeomNode.labial ≠ FeatureGeometry.GeomNode.dorsal

Labial and dorsal are distinct (required for labiovelars).

theorem Phonology.ComplexSegments.softPalate_not_under_place : ¬FeatureGeometry.GeomNode.place.Dominates FeatureGeometry.GeomNode.softPalate

Soft palate is not a place node — it is a sibling of Place under Supralaryngeal, not a child. This means nasal assimilation (spreading soft palate) is independent of place assimilation (spreading place).

theorem Phonology.ComplexSegments.softPalate_not_articulator : ¬FeatureGeometry.GeomNode.softPalate.IsArticulator

Soft palate is not a place articulator — nasals are simple segments even though they involve velum lowering plus an oral place of articulation. This follows from softPalate being a sibling of place under supralaryngeal, not a child of place.

theorem Phonology.ComplexSegments.place_articulators_distinct : FeatureGeometry.GeomNode.labial ≠ FeatureGeometry.GeomNode.coronal ∧ FeatureGeometry.GeomNode.labial ≠ FeatureGeometry.GeomNode.dorsal ∧ FeatureGeometry.GeomNode.coronal ≠ FeatureGeometry.GeomNode.dorsal

The three place articulators are all distinct from each other — this gives rise to three possible complex segment types: labio-coronal, labio-dorsal, corono-dorsal.

theorem Phonology.ComplexSegments.articulators_under_place (n : FeatureGeometry.GeomNode) : n ∈ articulatorNodes → FeatureGeometry.GeomNode.place.Dominates n

Every place articulator is under the place node.