Element Theory

Standard Element Theory ([Bac11], [Bre13]): segments built from six privative elements |A I U ʔ H L|, each a Fundamental × Polarity pairing [Bac11]. A melodic representation (MR) is a Finset Element with an optional head (the Single Optional Headedness Condition); a Segment carries one MR per subsegmental node (manner / place / laryngeal), so one element may dock at different nodes in different segments [CVW26].

Main definitions

• Element, Fundamental, Polarity — the six elements as a 3×2 grid; Element.AntagonismFree — at most one element per fundamental.
• MR — a melodic representation, with dock/compose/decompose and the refinement order Refines.
• Segment — a node-structured MR, with Refines, NoAntagonisticHeads (Backley's at-most-one-head-per-fundamental), and node-hosting WellFormed.

Implementation notes

Headedness is positional (the head field), following Breit's SOHC rather than the multiple-heads variant of [Bac17]. The inventory is Standard ET's, not Conservative or Progressive ET ([Bac12]): elements are shared — |L| for nasality/voicing/low tone, |U| for labials/velars, |H| for frication/voicelessness/high tone.

The six elements

inductive ElementTheory.Fundamental : Type

The three fundamentals of spoken language.

• colour : Fundamental

  Colour: |U| (dark) vs |I| (light).

• resonance : Fundamental

  Resonance: |A| (dark) vs |ʔ| (light).

• frequency : Fundamental

  Frequency: |L| (dark) vs |H| (light).

@[implicit_reducible]

instance ElementTheory.instDecidableEqFundamental : DecidableEq Fundamental

Equations

• ElementTheory.instDecidableEqFundamental x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ElementTheory.instReprFundamental.repr : Fundamental → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ElementTheory.instReprFundamental : Repr Fundamental

Equations

• ElementTheory.instReprFundamental = { reprPrec := ElementTheory.instReprFundamental.repr }

inductive ElementTheory.Polarity : Type

The two polar values of a fundamental.

• dark : Polarity
• light : Polarity

@[implicit_reducible]

instance ElementTheory.instDecidableEqPolarity : DecidableEq Polarity

Equations

• ElementTheory.instDecidableEqPolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ElementTheory.instReprPolarity : Repr Polarity

Equations

• ElementTheory.instReprPolarity = { reprPrec := ElementTheory.instReprPolarity.repr }

def ElementTheory.instReprPolarity.repr : Polarity → ℕ → Std.Format

Equations

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

inductive ElementTheory.Element : Type

The six privative elements |A I U ʔ H L|.

• A : Element

  |A| — resonance, dark. Aperture; high F1.

• I : Element

  |I| — colour, light. Palatality; high F2.

• U : Element

  |U| — colour, dark. Labiality / velarity; lowering of all formants.

• glottal : Element

  |ʔ| — resonance, light. Occlusion; abrupt, sustained amplitude drop.

• H : Element

  |H| — frequency, light. Noise / frication / voicelessness / high tone.

• L : Element

  |L| — frequency, dark. Nasality / voicing / low tone.

@[implicit_reducible]

instance ElementTheory.instDecidableEqElement : DecidableEq Element

Equations

• ElementTheory.instDecidableEqElement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ElementTheory.instReprElement : Repr Element

Equations

• ElementTheory.instReprElement = { reprPrec := ElementTheory.instReprElement.repr }

def ElementTheory.instReprElement.repr : Element → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• ElementTheory.instReprElement.repr ElementTheory.Element.A prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Element.A")).group prec✝
• ElementTheory.instReprElement.repr ElementTheory.Element.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Element.I")).group prec✝
• ElementTheory.instReprElement.repr ElementTheory.Element.U prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Element.U")).group prec✝
• ElementTheory.instReprElement.repr ElementTheory.Element.H prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Element.H")).group prec✝
• ElementTheory.instReprElement.repr ElementTheory.Element.L prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Element.L")).group prec✝

The 3×2 grid

def ElementTheory.Element.gridEquiv : Element ≃ Fundamental × Polarity

The six elements are the 3×2 grid Fundamental × Polarity: each is its (fundamental, polarity) pair, and every pair is realized.

Equations

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

def ElementTheory.Element.fundamental (e : Element) : Fundamental

The fundamental an element belongs to.

Equations

• e.fundamental = (ElementTheory.Element.gridEquiv e).1

def ElementTheory.Element.polarity (e : Element) : Polarity

The polar value of an element.

Equations

• e.polarity = (ElementTheory.Element.gridEquiv e).2

def ElementTheory.Element.IsDark (e : Element) : Prop

e is a dark element: |U|, |A|, or |L|.

Equations

• e.IsDark = (e.polarity = ElementTheory.Polarity.dark)

@[implicit_reducible]

instance ElementTheory.Element.instDecidablePredIsDark : DecidablePred IsDark

Equations

• e.instDecidablePredIsDark = ElementTheory.Element.instDecidablePredIsDark._aux_1 e

Antagonism

def ElementTheory.Element.AntagonismFree (s : Finset Element) : Prop

A finset of elements is antagonism-free when no two distinct members share a fundamental — i.e. fundamental is injective on it (at most one per fundamental).

Equations

• ElementTheory.Element.AntagonismFree s = Set.InjOn ElementTheory.Element.fundamental ↑s

@[implicit_reducible]

instance ElementTheory.Element.instDecidableAntagonismFree (s : Finset Element) : Decidable (AntagonismFree s)

Equations

• ElementTheory.Element.instDecidableAntagonismFree s = ElementTheory.Element.instDecidableAntagonismFree._aux_1 s

Melodic representations

structure ElementTheory.MR : Type

A melodic representation: a numeration with an optional head (SOHC).

• elements : Finset Element

  The numeration — Breit's complement-position C: every element present.

• head : Option Element

  The optional head (SOHC: at most one).

• head_mem (e : Element) : e ∈ self.head → e ∈ self.elements

  The head, if any, is among the elements (Breit: H ⊆ C).

theorem ElementTheory.MR.ext {x y : MR} (elements : x.elements = y.elements) (head : x.head = y.head) : x = y

theorem ElementTheory.MR.ext_iff {x y : MR} : x = y ↔ x.elements = y.elements ∧ x.head = y.head

def ElementTheory.instDecidableEqMR.decEq (x✝ x✝¹ : MR) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ElementTheory.instDecidableEqMR : DecidableEq MR

Equations

• ElementTheory.instDecidableEqMR = ElementTheory.instDecidableEqMR.decEq

Set-merge constructors

def ElementTheory.MR.empty : MR

The empty MR | |: the empty representation (usually [ə]).

Equations

• ElementTheory.MR.empty = { elements := ∅, head := none, head_mem := ElementTheory.MR.empty._proof_1 }

def ElementTheory.MR.simplex (e : Element) : MR

The unheaded simplex |e|: a single bare element.

Equations

• ElementTheory.MR.simplex e = { elements := {e}, head := none, head_mem := ⋯ }

def ElementTheory.MR.headedSimplex (e : Element) : MR

The headed simplex |e̲|: a single element that is also its own head.

Equations

• ElementTheory.MR.headedSimplex e = { elements := {e}, head := some e, head_mem := ⋯ }

def ElementTheory.MR.headPlusOp (h op : Element) : MR

|h̲ op|: a head h with one operator op.

Equations

• ElementTheory.MR.headPlusOp h op = { elements := {h, op}, head := some h, head_mem := ⋯ }

def ElementTheory.MR.numeration (es : Finset Element) : MR

An unheaded numeration: a bare set of elements with no head.

Equations

• ElementTheory.MR.numeration es = { elements := es, head := none, head_mem := ⋯ }

Head, complement, operators

def ElementTheory.MR.HasElement (m : MR) (e : Element) : Prop

e is present in the MR (head or operator): Breit's complement membership.

Equations

• m.HasElement e = (e ∈ m.elements)

@[implicit_reducible]

instance ElementTheory.MR.instDecidableHasElement (m : MR) (e : Element) : Decidable (m.HasElement e)

Equations

• m.instDecidableHasElement e = ElementTheory.MR.instDecidableHasElement._aux_1 m e

def ElementTheory.MR.IsHead (m : MR) (e : Element) : Prop

e is the head of the MR.

Equations

• m.IsHead e = (m.head = some e)

@[implicit_reducible]

instance ElementTheory.MR.instDecidableIsHead (m : MR) (e : Element) : Decidable (m.IsHead e)

Equations

• m.instDecidableIsHead e = ElementTheory.MR.instDecidableIsHead._aux_1 m e

def ElementTheory.MR.IsHeaded (m : MR) : Prop

The MR has a head.

Equations

• m.IsHeaded = (m.head ≠ none)

def ElementTheory.MR.ops (m : MR) : Finset Element

The operators (dependents): all but the head ([KLV85]).

Equations

• m.ops = match m.head with | none => m.elements | some h => m.elements.erase h

Antagonism

def ElementTheory.MR.AntagonismFree (m : MR) : Prop

No two co-present elements share a fundamental.

Equations

• m.AntagonismFree = ElementTheory.Element.AntagonismFree m.elements

@[implicit_reducible]

instance ElementTheory.MR.instDecidableAntagonismFree (m : MR) : Decidable m.AntagonismFree

Equations

• m.instDecidableAntagonismFree = ElementTheory.MR.instDecidableAntagonismFree._aux_1 m

Basic theorems

@[simp]

theorem ElementTheory.MR.headedSimplex_isHead (e : Element) : (headedSimplex e).IsHead e

@[simp]

theorem ElementTheory.MR.simplex_hasElement (e : Element) : (simplex e).HasElement e

theorem ElementTheory.MR.simplex_not_headed (e : Element) : ¬(simplex e).IsHeaded

theorem ElementTheory.MR.empty_not_headed : ¬empty.IsHeaded

theorem ElementTheory.MR.exists_headedSimplex (e : Element) : ∃ (m : MR), m.IsHead e

Every element has a headed simplex |e̲|.

Compose and decompose

def ElementTheory.MR.compose (m : MR) (e : Element) : MR

Add element e as an operator (complement-composition).

Equations

• m.compose e = { elements := insert e m.elements, head := m.head, head_mem := ⋯ }

def ElementTheory.MR.decompose (m : MR) (e : Element) : MR

Remove element e, demoting it from head if present (complement-decomposition).

Equations

• m.decompose e = { elements := m.elements.erase e, head := if m.head = some e then none else m.head, head_mem := ⋯ }

def ElementTheory.MR.headCompose (m : MR) (e : Element) : MR

Promote e to head, adding it if absent (head-composition).

Equations

• m.headCompose e = { elements := insert e m.elements, head := some e, head_mem := ⋯ }

def ElementTheory.MR.headDecompose (m : MR) : MR

Remove the head, leaving the elements bare (head-decomposition).

Equations

• m.headDecompose = { elements := m.elements, head := none, head_mem := ⋯ }

def ElementTheory.MR.dock (host floater : MR) : MR

Union host and floater, the floater's head overriding (non-monotone, so not the order-join).

Equations

• host.dock floater = { elements := host.elements ∪ floater.elements, head := match floater.head with | some f => some f | none => host.head, head_mem := ⋯ }

Elemental refinement order

def ElementTheory.MR.Refines (m₁ m₂ : MR) : Prop

Refinement: inclusion on elements, flat order (Option.FlatLE) on the head ([CVW26]).

Equations

• m₁.Refines m₂ = (m₁.elements ⊆ m₂.elements ∧ m₁.head.FlatLE m₂.head)

@[implicit_reducible]

instance ElementTheory.MR.instDecidableRefines (m₁ m₂ : MR) : Decidable (m₁.Refines m₂)

Equations

• m₁.instDecidableRefines m₂ = ElementTheory.MR.instDecidableRefines._aux_1 m₁ m₂

@[implicit_reducible]

instance ElementTheory.MR.instPartialOrder : PartialOrder MR

Equations

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

@[implicit_reducible]

instance ElementTheory.MR.instDecidableLe (m₁ m₂ : MR) : Decidable (m₁ ≤ m₂)

Equations

• m₁.instDecidableLe m₂ = m₁.instDecidableRefines m₂

Nodes: the subsegmental geometry

inductive ElementTheory.Node : Type

The three subsegmental nodes ([Har94]): docking sites, contrastive unlike a Fundamental.

• manner : Node
• place : Node
• laryngeal : Node

@[implicit_reducible]

instance ElementTheory.instDecidableEqNode : DecidableEq Node

Equations

• ElementTheory.instDecidableEqNode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ElementTheory.instReprNode.repr : Node → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• ElementTheory.instReprNode.repr ElementTheory.Node.manner prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Node.manner")).group prec✝
• ElementTheory.instReprNode.repr ElementTheory.Node.place prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ElementTheory.Node.place")).group prec✝

@[implicit_reducible]

instance ElementTheory.instReprNode : Repr Node

Equations

• ElementTheory.instReprNode = { reprPrec := ElementTheory.instReprNode.repr }

Segments: node-structured melodic representations

structure ElementTheory.Segment : Type

A segment: one MR per node (per-node SOHC) — so up to three heads.

• manner : MR
• place : MR
• laryngeal : MR

theorem ElementTheory.Segment.ext {x y : Segment} (manner : x.manner = y.manner) (place : x.place = y.place) (laryngeal : x.laryngeal = y.laryngeal) : x = y

theorem ElementTheory.Segment.ext_iff {x y : Segment} : x = y ↔ x.manner = y.manner ∧ x.place = y.place ∧ x.laryngeal = y.laryngeal

def ElementTheory.instDecidableEqSegment.decEq (x✝ x✝¹ : Segment) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ElementTheory.instDecidableEqSegment : DecidableEq Segment

Equations

• ElementTheory.instDecidableEqSegment = ElementTheory.instDecidableEqSegment.decEq

Projections

def ElementTheory.Segment.atNode (s : Segment) : Node → MR

The MR at a given node.

Equations

• s.atNode ElementTheory.Node.manner = s.manner
• s.atNode ElementTheory.Node.place = s.place
• s.atNode ElementTheory.Node.laryngeal = s.laryngeal

def ElementTheory.Segment.allElements (s : Segment) : Finset Element

All elements across all nodes.

Equations

• s.allElements = s.manner.elements ∪ s.place.elements ∪ s.laryngeal.elements

def ElementTheory.Segment.headCount (s : Segment) : ℕ

The number of headed nodes (0–3).

Equations

• s.headCount = ((if s.manner.head.isSome = true then 1 else 0) + if s.place.head.isSome = true then 1 else 0) + if s.laryngeal.head.isSome = true then 1 else 0

theorem ElementTheory.Segment.headCount_le_three (s : Segment) : s.headCount ≤ 3

At most three heads — one per node.

def ElementTheory.Segment.headFinset (s : Segment) : Finset Element

The heads across all nodes (0–3), deduplicated.

Equations

• s.headFinset = [s.manner.head, s.place.head, s.laryngeal.head].reduceOption.toFinset

Antagonism

def ElementTheory.Segment.NoAntagonisticHeads (s : Segment) : Prop

Backley's headedness constraint: at most one head per fundamental ([Bac17]).

Equations

• s.NoAntagonisticHeads = ElementTheory.Element.AntagonismFree s.headFinset

@[implicit_reducible]

instance ElementTheory.Segment.instDecidableNoAntagonisticHeads (s : Segment) : Decidable s.NoAntagonisticHeads

Equations

• s.instDecidableNoAntagonisticHeads = ElementTheory.Segment.instDecidableNoAntagonisticHeads._aux_1 s

Operations

def ElementTheory.Segment.ofMR (m : MR) : Node → Segment

Embed an MR at a single node (others empty); recovers a flat ET MR.

Equations

• ElementTheory.Segment.ofMR m ElementTheory.Node.manner = { manner := m, place := ElementTheory.MR.empty, laryngeal := ElementTheory.MR.empty }
• ElementTheory.Segment.ofMR m ElementTheory.Node.place = { manner := ElementTheory.MR.empty, place := m, laryngeal := ElementTheory.MR.empty }
• ElementTheory.Segment.ofMR m ElementTheory.Node.laryngeal = { manner := ElementTheory.MR.empty, place := ElementTheory.MR.empty, laryngeal := m }

def ElementTheory.Segment.dock (host floater : Segment) : Segment

MR.dock lifted node-by-node.

Equations

• host.dock floater = { manner := host.manner.dock floater.manner, place := host.place.dock floater.place, laryngeal := host.laryngeal.dock floater.laryngeal }

Well-formedness

def ElementTheory.Segment.WellFormed (s : Segment) : Prop

Node-hosting well-formedness ([Har94]): place |I U A|, laryngeal |L H|, manner |ʔ H L A|.

Equations

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

@[implicit_reducible]

instance ElementTheory.Segment.instDecidableWellFormed (s : Segment) : Decidable s.WellFormed

Equations

• s.instDecidableWellFormed = ElementTheory.Segment.instDecidableWellFormed._aux_1 s

Refinement order

def ElementTheory.Segment.Refines (s₁ s₂ : Segment) : Prop

Pointwise MR-refinement across nodes (the palataliser chain).

Equations

• s₁.Refines s₂ = (s₁.manner ≤ s₂.manner ∧ s₁.place ≤ s₂.place ∧ s₁.laryngeal ≤ s₂.laryngeal)

@[implicit_reducible]

instance ElementTheory.Segment.instDecidableRefines (s₁ s₂ : Segment) : Decidable (s₁.Refines s₂)

Equations

• s₁.instDecidableRefines s₂ = ElementTheory.Segment.instDecidableRefines._aux_1 s₁ s₂

@[implicit_reducible]

instance ElementTheory.Segment.instPartialOrder : PartialOrder Segment

Equations

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

@[implicit_reducible]

instance ElementTheory.Segment.instDecidableLe (s₁ s₂ : Segment) : Decidable (s₁ ≤ s₂)

Equations

• s₁.instDecidableLe s₂ = s₁.instDecidableRefines s₂