Sagey (1986) [Sag86]

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

[Sag86] 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 (Phonology/Segmental/Geometry.lean). The geometry predicts which multiply-articulated (complex) segments are possible in human language (Phonology/Segmental/Geometry.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.

Interval-overlap semantics for association lines

[Sag86] §5.3 derives the ban on crossing association lines from temporal precedence rather than stipulating it as a well-formedness condition.

The key move is choosing the right temporal relation for association lines. Simultaneity (identity of time points) is too strong — it predicts that contour segments and geminates are impossible, since two distinct elements cannot both be identical to the same time point (§5.2.2). Overlap is the correct relation: it is reflexive and symmetric but crucially NOT transitive (NonemptyInterval.overlaps_not_transitive), which is what allows the NCC proof to go through via a contradiction chain (§5.2.2, fn. 6).

The derivation (§5.3, p.294): if timing₁ ≺ timing₂ on the timing tier but melody₂ ≺ melody₁ on the melody tier, the overlap requirements on valid associations produce a chain melody₂.finish < melody₁.start ≤ timing₁.finish < timing₂.start ≤ melody₂.finish — a contradiction. Crossing is therefore logically impossible for valid associations.

This section formalizes the derivation using NonemptyInterval for temporal intervals and its precedes/overlaps relations.

structure Autosegmental.TierPosition (T : Type u_2) [LinearOrder T] : Type u_2

A position on an autosegmental tier, occupying a temporal interval.

• interval : NonemptyInterval T

structure Autosegmental.Association (T : Type u_2) [LinearOrder T] : Type u_2

An association between a timing-tier position and a melody-tier position. An association line represents temporal overlap: the melody element is realized during the timing position's interval.

• timing : TierPosition T
• melody : TierPosition T

def Autosegmental.validAssociation {T : Type u_1} [LinearOrder T] (a : Association T) : Prop

Association validity: the timing and melody intervals must overlap. This is the phonetic grounding — an association line means the melodic content is realized during the timing slot.

Equations

• Autosegmental.validAssociation a = a.timing.interval.overlaps a.melody.interval

theorem Autosegmental.simultaneity_no_contours {T : Type u_2} (t m₁ m₂ : T) (h₁ : t = m₁) (h₂ : t = m₂) : m₁ = m₂

Simultaneity contradicts contours ([Sag86] §5.2.2): if association required temporal identity (simultaneity), contour segments — two distinct melody elements F ≠ G associated to the same timing position x — would be impossible, since F = x and G = x imply F = G by transitivity. This is Sagey's negative argument for why association must be overlap, not identity.

def Autosegmental.crosses {T : Type u_1} [LinearOrder T] (a₁ a₂ : Association T) : Prop

Two associations cross iff their timing positions are ordered one way but their melody positions are ordered the other way. Crossing(a₁, a₂) ≡ timing₁ ≺ timing₂ ∧ melody₂ ≺ melody₁.

Equations

• Autosegmental.crosses a₁ a₂ = (a₁.timing.interval.precedes a₂.timing.interval ∧ a₂.melody.interval.precedes a₁.melody.interval)

theorem Autosegmental.no_crossing {T : Type u_1} [LinearOrder T] (a₁ a₂ : Association T) (h₁ : validAssociation a₁) (h₂ : validAssociation a₂) : ¬crosses a₁ a₂

No-Crossing Constraint ([Sag86] §5.3, [Gol76]): Two valid associations cannot cross.

If timing₁ ≺ timing₂, then timing₁.finish < timing₂.start. Validity requires timing₁ overlaps melody₁ and timing₂ overlaps melody₂. If melodies also cross (melody₂ ≺ melody₁), then melody₂.finish < melody₁.start.

From timing₁ overlaps melody₁: melody₁.start ≤ timing₁.finish. From timing₂ overlaps melody₂: timing₂.start ≤ melody₂.finish.

Chaining: melody₂.finish < melody₁.start ≤ timing₁.finish < timing₂.start ≤ melody₂.finish. This gives melody₂.finish < melody₂.finish — a contradiction.

theorem Autosegmental.no_crossing_symm {T : Type u_1} [LinearOrder T] (a₁ a₂ : Association T) (h₁ : validAssociation a₁) (h₂ : validAssociation a₂) : ¬crosses a₂ a₁

Crossing is also impossible in the symmetric direction: if timing₂ ≺ timing₁ and melody₁ ≺ melody₂, the same contradiction arises.

Set-level No-Crossing Constraint

def Autosegmental.Association.IsNoCrossing {T : Type u_1} [LinearOrder T] (associations : Set (Association T)) : Prop

A set of associations satisfies the No-Crossing Constraint iff no two associations in the set cross. Expressed via mathlib's Set.Pairwise.

Equations

• Autosegmental.Association.IsNoCrossing associations = associations.Pairwise fun (a₁ a₂ : Autosegmental.Association T) => ¬Autosegmental.crosses a₁ a₂

theorem Autosegmental.Association.IsNoCrossing.of_all_valid {T : Type u_1} [LinearOrder T] {associations : Set (Association T)} (hValid : ∀ a ∈ associations, validAssociation a) : IsNoCrossing associations

Set-level lift of no_crossing: any set of valid associations automatically satisfies the No-Crossing Constraint.

theorem Autosegmental.Association.IsNoCrossing.subset {T : Type u_1} [LinearOrder T] {s t : Set (Association T)} (hst : s ⊆ t) (h : IsNoCrossing t) : IsNoCrossing s

A subset of a no-crossing association set is no-crossing. Inherited from Set.Pairwise.mono.

Grounding the combinatorial No-Crossing Constraint

[Gol76]'s index-level NCC (IsNonCrossing over Finset (ℕ × ℕ) in Autosegmental/NonCrossing.lean) is stipulated as the filter on autosegmental GEN. [Sag86] §5.4 argues it should instead be derived from the temporal-overlap semantics of association lines (§5.3). This section makes the derivation load-bearing: an order-respecting assignment of time intervals to tier positions turns an index-level crossing into a Sagey crosses, which no_crossing rules out. The combinatorial filter is thus the discrete shadow of the temporal derivation, not an independent axiom.

structure Autosegmental.TierRealization (T : Type u_2) [LinearOrder T] : Type u_2

An interval realization of the two tiers: time intervals for lower-tier (timing) positions and upper-tier (melody) positions, each respecting tier index order as temporal precedence.

• tim : ℕ → NonemptyInterval T
• mel : ℕ → NonemptyInterval T
• tim_mono {i j : ℕ} : i < j → (self.tim i).precedes (self.tim j)
• mel_mono {k l : ℕ} : k < l → (self.mel k).precedes (self.mel l)

def Autosegmental.TierRealization.assoc {T : Type u_1} [LinearOrder T] (R : TierRealization T) (k i : ℕ) : Association T

The association realizing the index link (k, i): upper-tier position k linked to lower-tier position i.

Equations

• R.assoc k i = { timing := { interval := R.tim i }, melody := { interval := R.mel k } }

theorem Autosegmental.isNonCrossing_of_validRealization {T : Type u_1} [LinearOrder T] (R : TierRealization T) {links : Finset (ℕ × ℕ)} (hValid : ∀ p ∈ links, validAssociation (R.assoc p.1 p.2)) : IsNonCrossing links

The combinatorial NCC is derived, not stipulated. If every link in a set is realized as a valid (temporally overlapping) association under some order-respecting interval assignment, the set automatically satisfies [Gol76]'s index-level No-Crossing Constraint. The stipulated GEN filter (IsNonCrossing) is exactly the discrete shadow of [Sag86]'s overlap derivation (no_crossing): a crossing pair of links would realize two associations that cross, which cannot both overlap-validly.

def Autosegmental.TierRealization.canonical : TierRealization ℤ

Witness that the grounding hypothesis is non-vacuous: over ℤ, tier position n occupies the unit interval [2n, 2n+1], so index order is realized as temporal precedence (consecutive positions are disjoint and ordered).

Equations

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

theorem Autosegmental.canonical_diagonal_valid (n : ℕ) : validAssociation (TierRealization.canonical.assoc n n)

Under the canonical realization every diagonal link (n, n) is valid — a position overlaps itself — so the grounding theorem's hypothesis is satisfiable (any diagonal link set is IsNonCrossing through it), not vacuously true.

Concrete demonstrations

def Autosegmental.geminate {T : Type u_1} [LinearOrder T] (t1s t1f t2s t2f ms mf : T) (h1 : t1s ≤ t1f) (h2 : t2s ≤ t2f) (hm : ms ≤ mf) : Association T × Association T

A geminate consonant: two adjacent timing positions associated to a single melodic element. The melodic element's interval spans both timing slots.

Example: /t/ linked to two C-slots in [atta].

C-tier:    C₁    C₂
            \  /
melody:     t

Equations

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

def Autosegmental.contourTone {T : Type u_1} [LinearOrder T] (ts tf m1s m1f m2s m2f : T) (ht : ts ≤ tf) (hm1 : m1s ≤ m1f) (hm2 : m2s ≤ m2f) : Association T × Association T

A contour tone: one timing position associated to two tonal elements sequenced within it. The two tonal elements occupy sub-intervals.

Example: falling tone HL on a single syllable.

timing:     σ
           / \
tone:     H   L

Equations

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

structure Sagey1986.MajorMinor : Type

When a complex segment's two articulations differ in degree of closure, one articulator is major — it receives the segment's lexical degree-of-closure specification — and the other minor, its degree of closure predictable ([Sag86] §3.3, p.217). Majorness is lexically marked, not reducible to anterior/posterior order. This distinction is Sagey-specific — modern phonology does not uniformly adopt it.

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

def Sagey1986.margi_ps_articulation : MajorMinor

Margi labiocoronal /ps/: the coronal articulation is major, the labial minor — even though coronal is the more posterior of the two ([Sag86] §3.4, p.258, where Sagey contrasts it with Kinyarwanda [skw], also coronal-major). The point is that majorness cannot be read off articulator order; it must be lexically marked.

Nupe /k͡p/ is deliberately not the example here: Sagey shows that in /k͡p/ both labial and dorsal are major — they share a degree of closure (both stops) — so it is symmetric, not an asymmetric major/minor segment ([Sag86] §3.3, p.217).

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 ⋯

@[implicit_reducible]

instance Sagey1986.instReprDegreeOfClosure : Repr DegreeOfClosure

Equations

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

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

Equations

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

structure Sagey1986.ArticulatorSpec : Type

An articulator paired with its degree of closure: degree of closure is a property of an articulator node, not the whole segment. In a !Xõ click both the coronal (anterior) and dorsal (velar) closures are stops, but only the major one — the velar — carries the segment's lexical degree-of-closure specification; the anterior closure's is predictable ([Sag86] §3.4, p.258).

• node : Phonology.FeatureGeometry.Node
• 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.Node.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.Node.dorsal, closure := Sagey1986.DegreeOfClosure.stop, node_is_articulator := Sagey1986.click_posterior._proof_1 }

theorem Sagey1986.nasal_assimilation_scope : Phonology.FeatureGeometry.Node.softPalate.features.length < Phonology.FeatureGeometry.Node.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.Node.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.Node.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 : nupe_kp_segment.IsComplex

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

theorem Sagey1986.nupe_kp_wf : nupe_kp_segment.activeArticulators.Nodup

The Nupe /k͡p/ is well-formed: its active articulators (labial, dorsal) are distinct — an instance of the by-construction guarantee.

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 : ¬simple_p.IsComplex

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 : ¬velar_nasal.IsComplex

theorem Sagey1986.velar_nasal_wf : velar_nasal.activeArticulators.Nodup

The velar nasal is well-formed (only one place articulator: dorsal), its active articulators trivially distinct.

def Sagey1986.alveolar_t : Phonology.Segment

A coronal-only segment (alveolar /t/, [+cor, +ant]) is NOT complex: multiple coronal features fall under the single coronal articulator. This formalizes Sagey's key prediction (§2.2): complex segments are possible only for combinations of two different articulators, so no combination of features under a single articulator yields a complex segment. The same-articulator bar is exactly why alveolars and alveopalatals — both coronal — cannot form a doubly-articulated stop ([Sag86] §2.2, p.64).

Equations

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

theorem Sagey1986.alveolar_not_complex : ¬alveolar_t.IsComplex

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 ([Sag86] §2.2).

Equations

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

theorem Sagey1986.alveopalatal_not_complex : ¬alveopalatal.IsComplex

Temporal derivation of the No-Crossing Constraint

[Sag86] 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 : Autosegmental.Association ℤ × 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 : Autosegmental.validAssociation geminate_tt.1 ∧ Autosegmental.validAssociation geminate_tt.2

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

def Sagey1986.contour_HL : Autosegmental.Association ℤ × 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 : Autosegmental.validAssociation contour_HL.1 ∧ 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 ⋯ ⋯; Autosegmental.crosses a₁ a₂ ∧ ¬Autosegmental.validAssociation a₁

Crossing forces invalidity ([Sag86] §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.