Sagey (1986) @cite{sagey-1986}

The Representation of Features and Relations in Non-Linear Phonology. PhD dissertation, Massachusetts Institute of Technology.

@cite{sagey-1986} proposes a hierarchical feature geometry organized by vocal tract articulator, establishing the labial, coronal, dorsal, and soft palate nodes that are now standard in phonological theory (Theories/Phonology/FeatureGeometry.lean). The geometry predicts which multiply-articulated (complex) segments are possible in human language (Theories/Phonology/ComplexSegments.lean).

This study file formalizes Sagey-specific contributions that go beyond the consensus geometry:

Formalized contributions

1. Major/minor articulator distinction (Ch. 3): in complex segments, one articulator is major (determines degree of closure) and one is minor.

2. Degree of closure as articulator-level property (Ch. 3): [continuant] and [consonantal] describe the root-to-articulator relationship, not the segment as a whole. This allows different degrees of closure at different articulators within one segment (e.g., clicks).

3. Soft palate independence (Ch. 2): nasal assimilation (spreading the soft palate node) is structurally simpler than place assimilation (spreading the place node), explaining its cross-linguistic frequency.

4. Empirical arguments: Nupe labiovelars [k͡p]/[g͡b] as labio-dorsal complex segments with dorsal as major articulator.

structure Sagey1986.MajorMinor : Type

In a complex segment, one articulator is designated as major (determines the primary degree of closure seen by syllable structure) and the other as minor. This distinction is Sagey-specific — modern phonology does not uniformly adopt it.

• major : Phonology.FeatureGeometry.GeomNode
• minor : Phonology.FeatureGeometry.GeomNode
• major_is_articulator : self.major.IsArticulator
• minor_is_articulator : self.minor.IsArticulator
• distinct : self.major ≠ self.minor

def Sagey1986.nupe_kp_articulation : MajorMinor

Nupe labiovelar /k͡p/: dorsal is major (stop closure), labial is minor. Sagey argues this based on nasalization patterns: labiovelars in Nupe nasalize to [ŋ͡m], with the velar nasal first, showing dorsal is the major articulator.

Equations

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

inductive Sagey1986.DegreeOfClosure : Type

Sagey's degree of closure: a property of an articulator node, not a terminal feature. This is the Sagey-specific treatment; the modern geometry encodes closure as [±continuant] at the supralaryngeal node.

• stop : DegreeOfClosure
• fricative : DegreeOfClosure
• approximant : DegreeOfClosure

@[implicit_reducible]

instance Sagey1986.instDecidableEqDegreeOfClosure : DecidableEq DegreeOfClosure

Equations

• Sagey1986.instDecidableEqDegreeOfClosure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Sagey1986.instReprDegreeOfClosure.repr : DegreeOfClosure → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Sagey1986.instReprDegreeOfClosure : Repr DegreeOfClosure

Equations

• Sagey1986.instReprDegreeOfClosure = { reprPrec := Sagey1986.instReprDegreeOfClosure.repr }

structure Sagey1986.ArticulatorSpec : Type

An articulator paired with its degree of closure. In Sagey's framework, a click can be [−cont] at coronal and [−cont] at dorsal independently.

• node : Phonology.FeatureGeometry.GeomNode
• closure : DegreeOfClosure
• node_is_articulator : self.node.IsArticulator = (true = true)

def Sagey1986.click_anterior : ArticulatorSpec

A click's anterior closure (coronal, full stop).

Equations

• Sagey1986.click_anterior = { node := Phonology.FeatureGeometry.GeomNode.coronal, closure := Sagey1986.DegreeOfClosure.stop, node_is_articulator := Sagey1986.click_anterior._proof_1 }

def Sagey1986.click_posterior : ArticulatorSpec

A click's posterior closure (dorsal, full stop).

Equations

• Sagey1986.click_posterior = { node := Phonology.FeatureGeometry.GeomNode.dorsal, closure := Sagey1986.DegreeOfClosure.stop, node_is_articulator := Sagey1986.click_posterior._proof_1 }

theorem Sagey1986.nasal_assimilation_scope : Phonology.FeatureGeometry.GeomNode.softPalate.features.length < Phonology.FeatureGeometry.GeomNode.place.features.length

Nasal assimilation spreads the soft palate node (1 feature), while place assimilation spreads the place node (14 features). The soft palate's independence from place explains why nasal assimilation is cross-linguistically simpler and more common than place assimilation: it involves spreading a smaller constituent.

theorem Sagey1986.nasal_not_under_place : ¬Phonology.Feature.nasal.DominatedBy Phonology.FeatureGeometry.GeomNode.place

Nasality is NOT under the place node — spreading place does not spread nasality. This is Sagey's core structural argument for the soft palate node as a separate constituent.

theorem Sagey1986.nasal_under_supralaryngeal : Phonology.Feature.nasal.DominatedBy Phonology.FeatureGeometry.GeomNode.supralaryngeal

Nasality IS under supralaryngeal (via the soft palate node), so total assimilation (spreading supralaryngeal) does spread nasality.

def Sagey1986.nupe_kp_segment : Phonology.Segment

A Nupe labiovelar stop /k͡p/: specified for both labial and dorsal, voiceless, non-continuant.

Equations

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

theorem Sagey1986.nupe_kp_is_complex : Phonology.ComplexSegments.IsComplex nupe_kp_segment

The Nupe /k͡p/ is a complex segment (two active place articulators).

theorem Sagey1986.nupe_kp_wf : Phonology.ComplexSegments.ComplexWF nupe_kp_segment

The Nupe /k͡p/ is well-formed: labial ≠ dorsal.

def Sagey1986.simple_p : Phonology.Segment

A simple /p/ (labial only) is not complex.

Equations

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

theorem Sagey1986.simple_p_not_complex : ¬Phonology.ComplexSegments.IsComplex simple_p

def Sagey1986.velar_nasal : Phonology.Segment

A velar nasal /ŋ/ is NOT complex despite activating both the dorsal articulator and the soft palate (velum lowering). The soft palate is structurally independent of place, so nasal + place combinations are simple segments — this is Sagey's core argument for the soft palate node's independence.

Equations

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

theorem Sagey1986.velar_nasal_not_complex : ¬Phonology.ComplexSegments.IsComplex velar_nasal

theorem Sagey1986.velar_nasal_wf : Phonology.ComplexSegments.ComplexWF velar_nasal

The velar nasal is well-formed (only one place articulator: dorsal).

def Sagey1986.alveolar_t : Phonology.Segment

A coronal-only segment (alveolar /t/) with multiple coronal features is NOT complex: [+cor, +ant, −dist] all fall under the single coronal articulator. This formalizes Sagey's key prediction: palatal–velar stops are impossible because palatals and velars are both dorsal — no combination of features under a single articulator can produce a complex segment.

Equations

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

theorem Sagey1986.alveolar_not_complex : ¬Phonology.ComplexSegments.IsComplex alveolar_t

def Sagey1986.alveopalatal : Phonology.Segment

An alveopalatal (postalveolar) is [+cor, −ant, +dist] — still just one articulator (coronal), so not complex. An alveolar-alveopalatal doubly-articulated stop is therefore impossible: both articulations use the coronal articulator (@cite{sagey-1986} §2.2).

Equations

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

theorem Sagey1986.alveopalatal_not_complex : ¬Phonology.ComplexSegments.IsComplex alveopalatal

Temporal derivation of the No-Crossing Constraint

@cite{sagey-1986} Ch. 5 derives the ban on crossing association lines from temporal precedence. This section demonstrates the derived constraint with concrete integer-valued time instances.

def Sagey1986.geminate_tt : Phonology.Autosegmental.Association ℤ × Phonology.Autosegmental.Association ℤ

A concrete geminate /t:/ occupying timing slots [0,1] and [2,3], with the melodic element spanning [0,3].

Equations

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

theorem Sagey1986.geminate_tt_valid : Phonology.Autosegmental.validAssociation geminate_tt.1 ∧ Phonology.Autosegmental.validAssociation geminate_tt.2

Both associations in the geminate are valid (timing overlaps melody).

def Sagey1986.contour_HL : Phonology.Autosegmental.Association ℤ × Phonology.Autosegmental.Association ℤ

A concrete falling contour tone: timing [0,4], H tone [0,2], L tone [2,4].

Equations

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

theorem Sagey1986.contour_HL_valid : Phonology.Autosegmental.validAssociation contour_HL.1 ∧ Phonology.Autosegmental.validAssociation contour_HL.2

Both associations in the contour tone are valid.

theorem Sagey1986.crossing_forces_invalidity : have a₁ := Sagey1986.mkAssoc✝ 0 1 4 5 ⋯ ⋯; have a₂ := Sagey1986.mkAssoc✝ 2 3 0 1 ⋯ ⋯; Phonology.Autosegmental.crosses a₁ a₂ ∧ ¬Phonology.Autosegmental.validAssociation a₁

Crossing forces invalidity (@cite{sagey-1986} §5.3): a crossing configuration — timing₁ at [0,1] → melody₁ at [4,5], timing₂ at [2,3] → melody₂ at [0,1] — has its timing positions correctly ordered and melody positions reversed, but the first association is invalid because timing [0,1] does not overlap melody [4,5]. This demonstrates the mechanism: crossing is impossible not because it's stipulated, but because validity (temporal overlap) cannot be satisfied for both associations simultaneously when they cross.