Canonical comparison on the SO₀ alphabet

A carrier-free family of strict-total comparisons on the lexical alphabet (Cat, SimpleLI, LexicalItem, LIToken) and on lists thereof. Each cmp* satisfies two laws:

• cmp*_swap: cmp a b = (cmp b a).swap (antisymmetry)
• cmp*_eq: cmp a b = .eq → a = b (distinct values compare unequal)

These make the comparison usable as a commutative tie-break: the SO-carrier externalization ([MCB25] §1.12.1 / Lemma 1.13.5) orders exocentric nodes — off Dom(h), where c-selection does not pick a head — by cmpList cmpTok (SyntacticObject/Externalization.lean's exoYield), keeping the section computable with no Quot.out.

The leaf comparators reuse mathlib's compare (and its Std.OrientedOrd.eq_swap / Std.compare_eq_iff_eq laws) on ℕ/String; Cat is compared via its constructor index.

Category comparison

def Minimalist.cmpCat (c₁ c₂ : Cat) : Ordering

Comparison on syntactic categories via the constructor index.

Equations

• Minimalist.cmpCat c₁ c₂ = compare c₁.ctorIdx c₂.ctorIdx

theorem Minimalist.cmpCat_swap (c₁ c₂ : Cat) : cmpCat c₁ c₂ = (cmpCat c₂ c₁).swap

theorem Minimalist.cmpCat_eq {c₁ c₂ : Cat} (h : cmpCat c₁ c₂ = Ordering.eq) : c₁ = c₂

Lexicographic list comparison

def Minimalist.cmpList {β : Type u_1} (cmp : β → β → Ordering) : List β → List β → Ordering

Lexicographic comparison on lists, given an element comparison.

Equations

• Minimalist.cmpList cmp [] [] = Ordering.eq
• Minimalist.cmpList cmp [] (head :: tail) = Ordering.lt
• Minimalist.cmpList cmp (head :: tail) [] = Ordering.gt
• Minimalist.cmpList cmp (x_2 :: xs) (y :: ys) = (cmp x_2 y).then (Minimalist.cmpList cmp xs ys)

theorem Minimalist.cmpList_swap {β : Type u_1} {cmp : β → β → Ordering} (hsw : ∀ (a b : β), cmp a b = (cmp b a).swap) (xs ys : List β) : cmpList cmp xs ys = (cmpList cmp ys xs).swap

theorem Minimalist.cmpList_eq {β : Type u_1} {cmp : β → β → Ordering} (heq : ∀ (a b : β), cmp a b = Ordering.eq → a = b) (xs ys : List β) : cmpList cmp xs ys = Ordering.eq → xs = ys

Lexical item / token comparison

def Minimalist.cmpSimpleLI (s₁ s₂ : SimpleLI) : Ordering

Comparison on simple lexical items: category, then selectional stack, then phonological form.

Equations

• Minimalist.cmpSimpleLI s₁ s₂ = (Minimalist.cmpCat s₁.cat s₂.cat).then ((Minimalist.cmpList Minimalist.cmpCat s₁.sel s₂.sel).then (compare s₁.phonForm s₂.phonForm))

theorem Minimalist.cmpSimpleLI_swap (s₁ s₂ : SimpleLI) : cmpSimpleLI s₁ s₂ = (cmpSimpleLI s₂ s₁).swap

theorem Minimalist.cmpSimpleLI_eq {s₁ s₂ : SimpleLI} (h : cmpSimpleLI s₁ s₂ = Ordering.eq) : s₁ = s₂

def Minimalist.cmpLexItem (l₁ l₂ : LexicalItem) : Ordering

Comparison on lexical items: lexicographic on their feature lists (the nonempty proof is irrelevant).

Equations

• Minimalist.cmpLexItem l₁ l₂ = Minimalist.cmpList Minimalist.cmpSimpleLI l₁.features l₂.features

theorem Minimalist.cmpLexItem_swap (l₁ l₂ : LexicalItem) : cmpLexItem l₁ l₂ = (cmpLexItem l₂ l₁).swap

theorem Minimalist.cmpLexItem_eq {l₁ l₂ : LexicalItem} (h : cmpLexItem l₁ l₂ = Ordering.eq) : l₁ = l₂

def Minimalist.cmpTok (t₁ t₂ : LIToken) : Ordering

Comparison on tokens: by id, then by lexical item.

Equations

• Minimalist.cmpTok t₁ t₂ = (compare t₁.id t₂.id).then (Minimalist.cmpLexItem t₁.item t₂.item)

theorem Minimalist.cmpTok_swap (t₁ t₂ : LIToken) : cmpTok t₁ t₂ = (cmpTok t₂ t₁).swap

theorem Minimalist.cmpTok_eq {t₁ t₂ : LIToken} (h : cmpTok t₁ t₂ = Ordering.eq) : t₁ = t₂