Tableaux as Constraint Systems

The OT-specific predict view: a Tableau is an argminDecoder over a ViolationProfile-valued score, i.e. a Core.Optimization.ConstraintSystem. This is the OT counterpart of the Harmonic-Grammar ConstraintSystem (a softmaxDecoder over harmonyScore con w, built inline in HG study files), kept on the OT layer so the neutral Core.Optimization machinery stays independent of the Tableau API.

A study file can keep its Tableau/optimal formulation and additionally expose the unified ConstraintSystem.predict distribution via tableauSystem.

Main definitions

• tableauSystem — an OT tableau viewed as a generic ConstraintSystem.

Main results

• tableauSystem_predict_eq — predict is uniform over Tableau.optimal.
• tableauSystem_predict_unique_winner / tableauSystem_predict_loser — the deterministic (single-winner) specialisations used in study files.

noncomputable def OptimalityTheory.tableauSystem {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) : Core.Optimization.ConstraintSystem C (Core.Optimization.LexProfile ℕ n)

An OT tableau viewed as a generic ConstraintSystem. The score type LexProfile Nat n is definitionally ViolationProfile n, so the argminDecoder's LinearOrder requirement is satisfied by the standard Pi.Lex instance.

Equations

• OptimalityTheory.tableauSystem t = { candidates := t.candidates, score := t.profile, decoder := Core.Optimization.argminDecoder }

theorem OptimalityTheory.tableauSystem_predict_eq {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) (c : C) : (tableauSystem t).predict c = if c ∈ t.optimal then (↑t.optimal.card)⁻¹ else 0

The unifying identity: tableauSystem's prediction is uniform over Tableau.optimal. Since Tableau.optimal IS the argmin filter set by definition, the argminDecoder reduces to the standard "uniform over winners" formula. All other bridge results follow.

theorem OptimalityTheory.tableauSystem_predict_pos_iff_optimal {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) (c : C) : 0 < (tableauSystem t).predict c ↔ c ∈ t.optimal

A candidate is in the support of the tableauSystem distribution iff it is in the tableau's optimal set.

theorem OptimalityTheory.tableauSystem_predict_unique_winner {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) (winner : C) (h : t.optimal = {winner}) : (tableauSystem t).predict winner = 1

When Tableau.optimal = {winner} (the typical deterministic-OT pattern used in study files via by decide), the unified predict view assigns probability 1 to the winner.

theorem OptimalityTheory.tableauSystem_predict_loser {C : Type u_1} [DecidableEq C] {n : ℕ} (t : Tableau C n) (winner loser : C) (hne : loser ≠ winner) (h : t.optimal = {winner}) : (tableauSystem t).predict loser = 0

And losers in a unique-winner tableau receive probability 0.