Directional Tableau — Position-Vector EVAL

@cite{eisner-2000} @cite{eisner-2002} @cite{lamont-2022b}

Sibling to Core/Constraint/OT/Basic.lean's parallel Tableau. Where parallel OT compares candidates by count of violations (NamedConstraint.eval : C → Nat), directional OT compares by position vector (DirectionalConstraint.eval : C → List Nat, indicator-coded with positions in left-to-right order). The actual comparison procedure is governed by an EvalMode.

Why a sibling, not an extension

Per @cite{lamont-2022b}: directional EVAL is theoretically incompatible with weighted aggregation (Harmonic Grammar, MaxEnt). A parallel constraint's count can be multiplied by a weight; a position vector cannot. The existing NamedConstraint/Weighted/MaxEnt stack is committed to scalar violations and cannot host directional constraints. So they live in parallel type hierarchies, with EvalMode.le_singleton providing the structural bridge for the degenerate (singleton-vector) case where the two coincide.

Scope

This module ships:

• DirectionalConstraint C — the constraint type (analog of NamedConstraint C)
• DirectionalTableau C — the tableau type (analog of Tableau C n)
• DirectionalTableau.optimal — optimal-set extraction via per-entry EvalMode.le, lex-aggregated across constraints in ranking order

It deliberately does NOT yet ship:

• A WeightedDirectional analog (theoretically incoherent per above)
• A Stratal × Directional composition
• An n-step iteration combinator (handled by Iteration.iterateGen once HSDerivation dispatches on evalMode; deferred to follow-up)

structure Core.Constraint.OT.DirectionalConstraint (C : Type u_1) : Type u_1

A directional OT constraint. eval c returns the indicator vector for candidate c: positions in left-to-right order, with each entry recording the violation status at that position (binary {0, 1} for the typical case, but Nat for gradient).

The constraint itself is direction-neutral; the direction of evaluation is supplied by EvalMode at the tableau level (per @cite{lamont-2022b}'s reframing).

Distinct from NamedConstraint C which has eval : C → Nat (count). These cannot interconvert without losing position information; see EvalMode.le_singleton for the degenerate-case bridge.

• name : String
• family : ConstraintFamily
• eval : C → List ℕ

def Core.Constraint.OT.LexLEByMode (m : EvalMode) : List (List ℕ) → List (List ℕ) → Prop

Lex-compare two profiles (each a List of indicator vectors, one per constraint in ranking order) under an EvalMode. At the first constraint position where the two profiles strictly differ under EvalMode.le m, the better candidate wins. Equal throughout = equal-harmony.

Convention matches the parallel Tableau lex order: LexLEByMode m a b iff a is at-least-as-harmonic as b.

Equations

• Core.Constraint.OT.LexLEByMode m [] x✝ = True
• Core.Constraint.OT.LexLEByMode m (head :: tail) [] = False
• Core.Constraint.OT.LexLEByMode m (a :: as) (b :: bs) = (m.le a b ∧ ¬m.le b a ∨ m.le a b ∧ m.le b a ∧ Core.Constraint.OT.LexLEByMode m as bs)

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableLexLEByMode (m : EvalMode) (a b : List (List ℕ)) : Decidable (LexLEByMode m a b)

Equations

• Core.Constraint.OT.instDecidableLexLEByMode m [] x✝ = isTrue trivial
• Core.Constraint.OT.instDecidableLexLEByMode m (head :: tail) [] = isFalse ⋯
• Core.Constraint.OT.instDecidableLexLEByMode m (a :: as) (b :: bs) = Core.Constraint.OT.instDecidableLexLEByMode._aux_1 m a as b bs (Core.Constraint.OT.instDecidableLexLEByMode m as bs)

structure Core.Constraint.OT.DirectionalTableau (C : Type u_1) [DecidableEq C] : Type u_1

A tableau where all constraints are DirectionalConstraint and evaluated under a single EvalMode. The mode governs the within-constraint comparison; LexLEByMode lifts that to the across-constraints lex order in ranking position.

Single-mode (one evalMode for all constraints) is the simplest case. Mixed-mode rankings — where parallel and directional constraints coexist in one ranking — are a future extension and require a sum-typed constraint or per-constraint mode field.

• candidates : Finset C
• ranking : List (DirectionalConstraint C)
• evalMode : EvalMode
• nonempty : self.candidates.Nonempty

def Core.Constraint.OT.DirectionalTableau.profile {C : Type u_1} [DecidableEq C] (t : DirectionalTableau C) (c : C) : List (List ℕ)

The violation profile of candidate c: one indicator vector per constraint in ranking, in ranking order.

Equations

• t.profile c = List.map (fun (con : Core.Constraint.OT.DirectionalConstraint C) => con.eval c) t.ranking

def Core.Constraint.OT.DirectionalTableau.IsOptimal {C : Type u_1} [DecidableEq C] (t : DirectionalTableau C) (c : C) : Prop

A candidate is optimal iff its profile is at-least-as-harmonic (under LexLEByMode t.evalMode) as every other candidate's.

Equations

• t.IsOptimal c = (c ∈ t.candidates ∧ ∀ c' ∈ t.candidates, Core.Constraint.OT.LexLEByMode t.evalMode (t.profile c) (t.profile c'))

@[implicit_reducible]

instance Core.Constraint.OT.DirectionalTableau.instDecidableIsOptimal {C : Type u_1} [DecidableEq C] (t : DirectionalTableau C) (c : C) : Decidable (t.IsOptimal c)

Equations

• t.instDecidableIsOptimal c = Core.Constraint.OT.DirectionalTableau.instDecidableIsOptimal._aux_1 t c

def Core.Constraint.OT.DirectionalTableau.optimal {C : Type u_1} [DecidableEq C] (t : DirectionalTableau C) : Finset C

The optimal set: all candidates whose profile is at-least-as-harmonic as every other candidate's. Computable via Finset.filter.

Equations

• t.optimal = {c ∈ t.candidates | ∀ c' ∈ t.candidates, Core.Constraint.OT.LexLEByMode t.evalMode (t.profile c) (t.profile c')}

theorem Core.Constraint.OT.DirectionalTableau.mem_optimal_iff {C : Type u_1} [DecidableEq C] (t : DirectionalTableau C) (c : C) : c ∈ t.optimal ↔ t.IsOptimal c

inductive Core.Constraint.OT.DemoCand : Type

Three candidates representing depth-1 results of deleting one floating H from /H₁ H₂ H₃/ (paper, fig. 3 input). Each candidate's indicator vector records remaining floating Hs at positions 0, 1, 2 (left-to-right).

• deletedAt0 : DemoCand
• deletedAt1 : DemoCand
• deletedAt2 : DemoCand

@[implicit_reducible]

instance Core.Constraint.OT.instDecidableEqDemoCand : DecidableEq DemoCand

Equations

• Core.Constraint.OT.instDecidableEqDemoCand x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Constraint.OT.instReprDemoCand : Repr DemoCand

Equations

• Core.Constraint.OT.instReprDemoCand = { reprPrec := Core.Constraint.OT.instReprDemoCand.repr }

def Core.Constraint.OT.instReprDemoCand.repr : DemoCand → ℕ → Std.Format

Equations

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

def Core.Constraint.OT.demoFloatStar : DirectionalConstraint DemoCand

*FLOAT for the demo: indicator vector of remaining floating H positions.

Equations

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

def Core.Constraint.OT.demoTableauLR : DirectionalTableau DemoCand

DirectionalTableau under *FLOAT^→ (left-to-right). All three candidates have the same total *FLOAT count (2 violations each), so parallel evaluation would tie. Directional EVAL distinguishes them.

Equations

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

def Core.Constraint.OT.demoTableauRL : DirectionalTableau DemoCand

DirectionalTableau under *FLOAT^← (right-to-left). The mirror case.

Equations

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