Merchant & Prince (2022): tableaux to grammars

[MP22]'s Mother of All Tableaux studies the large-scale structure of an OT typology: the partition of Ord(S.Con) into grammars, the invariant MOAT that every violation tableau yielding the typology instantiates, and its geometry. This file lands the foundational wire — the bridge from the Concrete-OT tableau engine (OptimalityTheory.Tableau, the LexMinProblem the Studies already build) to the abstract Grammar hub (OptimalityTheory.Grammar, [MR16]).

A row w of a tableau, asserted optimal, generates the ERC set of its winner-loser comparisons against the other candidates (rowERCSet); the grammar of that row (rowGrammar) is Grammar.ofERCSet of those conditions. Its legs are exactly the rankings under which w wins (mem_rowGrammar_legs_iff_lex) — this is the semantic anchor connecting the abstract hub back to lexicographic optimality ([PS93]).

This is the first real consumer of the Grammar hub. The MOAT superstructure — Typology as the partition of these row-grammars (one row per grammar, by "One Tableau Suffices"), the border-point pair, the EPO, and the MOAT itself — builds on this bridge and is left to follow-on work.

Main definitions

• rowERCSet — the winner-loser ERCs of a tableau row against the other candidates.
• rowGrammar — the Grammar of a tableau row (the tableau → hub bridge).

Main results

• mem_rowGrammar_legs_iff_lex — a row's grammar collects exactly the rankings under which its profile lexicographically dominates every competitor's.

References

• [MP22]
• [MR16]
• [PS93]

noncomputable def MerchantPrince2022.rowERCSet {C : Type u_1} [DecidableEq C] {n : ℕ} (t : OptimalityTheory.Tableau C n) (w : C) : OptimalityTheory.ERCSet n

The ERC set of a tableau row w: w's winner-loser ERCs against every other candidate. These are the ranking conditions a leg must satisfy for w to be the optimum ([Pri02]). (Noncomputable: it enumerates the competitor Finset via Finset.toList; only the set of conditions matters, and consistency/membership stay decidable.)

Equations

• MerchantPrince2022.rowERCSet t w = List.map (OptimalityTheory.tableauERC t w) (t.candidates.erase w).toList

noncomputable def MerchantPrince2022.rowGrammar {C : Type u_1} [DecidableEq C] {n : ℕ} (t : OptimalityTheory.Tableau C n) (w : C) (h : (rowERCSet t w).Consistent) : OptimalityTheory.Grammar n

The grammar of a tableau row — the bridge from the Concrete-OT tableau engine to the abstract Grammar hub ([MP22]; [MR16]). h is the consistency of the row's conditions, i.e. that w is a genuine, non-harmonically-bounded optimum.

Equations

• MerchantPrince2022.rowGrammar t w h = OptimalityTheory.Grammar.ofERCSet (MerchantPrince2022.rowERCSet t w) h

@[simp]

theorem MerchantPrince2022.mem_rowGrammar_legs {C : Type u_1} [DecidableEq C] {n : ℕ} {t : OptimalityTheory.Tableau C n} {w : C} {h : (rowERCSet t w).Consistent} {r : OptimalityTheory.Ranking n} : r ∈ (rowGrammar t w h).legs ↔ OptimalityTheory.ERCSet.SatisfiedBy r (rowERCSet t w)

theorem MerchantPrince2022.mem_rowGrammar_legs_iff_lex {C : Type u_1} [DecidableEq C] {n : ℕ} {t : OptimalityTheory.Tableau C n} {w : C} {h : (rowERCSet t w).Consistent} {r : OptimalityTheory.Ranking n} : r ∈ (rowGrammar t w h).legs ↔ ∀ l ∈ t.candidates.erase w, (toLex fun (p : Fin n) => t.profile w (r p)) ≤ toLex fun (p : Fin n) => t.profile l (r p)

The semantic anchor. A row's grammar collects exactly the rankings under which w's violation profile, read in the ranking's priority order, lexicographically dominates every competitor's — i.e. the rankings that select w as optimum ([PS93]). This connects the abstract Grammar hub back to the tableau's lexicographic evaluation.