Superoptimal: Bidirectional OT via OrderHom.gfp

@cite{blutner-2000} @cite{jaeger-2002}

Mathlib-grounded formulation of @cite{blutner-2000}'s weak Bidirectional OT "superoptimality" (eq. 14). The set of superoptimal form-meaning pairs is the greatest fixed point of the squared blocking operator on Set (F × M), defined via mathlib's OrderHom.gfp on the Set α complete lattice.

Architecture

The blocking operator superoptimalSetStep is anti-monotone (more witnesses ⇒ more blockers ⇒ fewer survivors). Its square is monotone, so mathlib's OrderHom.gfp applies. The substrate definition is:

superoptimalSet pairs profile := (superoptimalSetStepSq pairs profile).gfp

(Renamed from superoptimalSet to superoptimal once the legacy list-based superoptimal in Evaluation.lean is retired.)

Mathlib's GFP API (isGreatest_gfp, le_gfp, gfp_le, map_gfp, Park induction) immediately applies. Per-paper consumers prove superoptimalSet pairs profile = S by exhibiting S as an IsParkWitness (§4 below): a fixed point of the unsquared step that absorbs every non-S pair via blocking. The maximality direction goes through Set.Finite.exists_minimalFor-based minimum-profile descent, anchored in the LexProfile preorder from Evaluation.lean.

def Core.Constraint.Evaluation.Blocks {F : Type u_1} {M : Type u_2} (profile : F × M → List ℕ) (S : Set (F × M)) (p : F × M) : Prop

Blocks profile S p: some witness q ∈ S blocks p — same form or same meaning (not both), strictly better profile under lex order. Set-valued sibling of IsBlocked (will inherit that name once the list-based variant retires).

Equations

• Core.Constraint.Evaluation.Blocks profile S p = ∃ q ∈ S, (q.1 = p.1 ∧ q.2 ≠ p.2 ∨ q.1 ≠ p.1 ∧ q.2 = p.2) ∧ Core.Constraint.Evaluation.LexLT (profile q) (profile p)

theorem Core.Constraint.Evaluation.Blocks.mono {F : Type u_1} {M : Type u_2} {profile : F × M → List ℕ} {S T : Set (F × M)} (hST : S ⊆ T) {p : F × M} : Blocks profile S p → Blocks profile T p

Blocks is monotone in the witness set: more witnesses can only create more blockers.

@[implicit_reducible]

instance Core.Constraint.Evaluation.Blocks.decidableOnFinset {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] (profile : F × M → List ℕ) (S : Finset (F × M)) (p : F × M) : Decidable (Blocks profile (↑S) p)

For Finset-coerced witness sets, Blocks is decidable: the existential over the finite carrier reduces to Finset.decidableBEx. This instance is the load-bearing piece for decide-based per-paper proofs.

Equations

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

def Core.Constraint.Evaluation.superoptimalSetStep {F : Type u_1} {M : Type u_2} (pairs : Set (F × M)) (profile : F × M → List ℕ) (S : Set (F × M)) : Set (F × M)

Single step of the superoptimality computation: keep pairs in pairs that are NOT blocked by any element of S. Anti-monotone in S.

Equations

• Core.Constraint.Evaluation.superoptimalSetStep pairs profile S = {p : F × M | p ∈ pairs ∧ ¬Core.Constraint.Evaluation.Blocks profile S p}

theorem Core.Constraint.Evaluation.superoptimalSetStep_subset {F : Type u_1} {M : Type u_2} (pairs : Set (F × M)) (profile : F × M → List ℕ) (S : Set (F × M)) : superoptimalSetStep pairs profile S ⊆ pairs

@[simp]

theorem Core.Constraint.Evaluation.mem_superoptimalSetStep {F : Type u_1} {M : Type u_2} {pairs : Set (F × M)} {profile : F × M → List ℕ} {S : Set (F × M)} {p : F × M} : p ∈ superoptimalSetStep pairs profile S ↔ p ∈ pairs ∧ ¬Blocks profile S p

theorem Core.Constraint.Evaluation.superoptimalSetStep_antitone {F : Type u_1} {M : Type u_2} (pairs : Set (F × M)) (profile : F × M → List ℕ) : Antitone (superoptimalSetStep pairs profile)

superoptimalSetStep is anti-monotone in the witness set.

def Core.Constraint.Evaluation.superoptimalSetStepSq {F : Type u_1} {M : Type u_2} (pairs : Set (F × M)) (profile : F × M → List ℕ) : Set (F × M) →o Set (F × M)

The squared step. Anti-monotone composed with anti-monotone is monotone, so this is the right object to feed OrderHom.gfp.

Equations

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

@[simp]

theorem Core.Constraint.Evaluation.superoptimalSetStepSq_apply {F : Type u_1} {M : Type u_2} (pairs : Set (F × M)) (profile : F × M → List ℕ) (S : Set (F × M)) : (superoptimalSetStepSq pairs profile) S = superoptimalSetStep pairs profile (superoptimalSetStep pairs profile S)

noncomputable def Core.Constraint.Evaluation.superoptimalSet {F : Type u_1} {M : Type u_2} (pairs : Set (F × M)) (profile : F × M → List ℕ) : Set (F × M)

@cite{blutner-2000}'s superoptimality (eq. 14): the greatest fixed point of the squared blocking operator. Set-valued, anchored in mathlib's OrderHom.gfp via Set α's CompleteLattice instance.

All mathlib gfp lemmas (isGreatest_gfp, le_gfp, gfp_le, map_gfp, Park induction) immediately apply. Per-paper consumers typically prove superoptimalSet pairs profile = S by exhibiting S as an IsParkWitness (§4 below).

Renamed from superoptimalSet to superoptimal once the legacy list-based superoptimal in Evaluation.lean is retired.

Equations

• Core.Constraint.Evaluation.superoptimalSet pairs profile = OrderHom.gfp (Core.Constraint.Evaluation.superoptimalSetStepSq pairs profile)

theorem Core.Constraint.Evaluation.superoptimalSet_subset {F : Type u_1} {M : Type u_2} (pairs : Set (F × M)) (profile : F × M → List ℕ) : superoptimalSet pairs profile ⊆ pairs

structure Core.Constraint.Evaluation.IsParkWitness {F : Type u_1} {M : Type u_2} (pairs : Set (F × M)) (profile : F × M → List ℕ) (S : Set (F × M)) : Prop

IsParkWitness pairs profile S: structural witness via Park's induction that S is the greatest fixed point of superoptimalSetStepSq pairs profile. Three conditions:

• subset: S ⊆ pairs.
• unblocked: every p ∈ S is unblocked by S (i.e., S is a fixed point of the unsquared step).
• closure: every p ∈ pairs \ S is blocked by S (uniqueness: no proper extension of S is a fixed point).

Together they pin down S as the GFP via superoptimalSet_eq_of_witness. The unblocked and closure conditions decompose into per-pair blocking checks that are typically decide-able for finite literal S and pairs (via the Blocks.decidableOnFinset instance).

• subset : S ⊆ pairs
• unblocked (p : F × M) : p ∈ S → ¬Blocks profile S p
• closure (p : F × M) : p ∈ pairs → p ∉ S → Blocks profile S p

theorem Core.Constraint.Evaluation.superoptimalSet_eq_of_witness {F : Type u_1} {M : Type u_2} {pairs : Set (F × M)} {profile : F × M → List ℕ} {S : Set (F × M)} (h_finite : pairs.Finite) (h : IsParkWitness pairs profile S) : superoptimalSet pairs profile = S

Witness lemma: IsParkWitness pairs profile S implies superoptimalSet pairs profile = S.

Proof structure:

• S ≤ gfp via coinduction (OrderHom.le_gfp): S is a fixed point of superoptimalSetStep (from unblocked + closure), hence of its square.
• gfp ≤ S via Park rule (OrderHom.gfp_le) with minimum-profile descent: any post-fixed-point T violating T ⊆ S contains a profile-minimal p ∈ T \ S; the S-blocker for p (from closure) is unblocked by T (no S-element blocks it by unblocked; no smaller T \ S-element blocks it by minimality), hence in F(T), contradicting p ∈ F²(T). Descent terminates by Set.Finite.exists_minimalFor against the LexProfile preorder.

theorem Core.Constraint.Evaluation.superoptimalSet_eq_of_finset_witness {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] {pairs S : Finset (F × M)} {profile : F × M → List ℕ} (h_subset : S ⊆ pairs) (h_unblocked : ∀ p ∈ S, ¬Blocks profile (↑S) p) (h_closure : ∀ p ∈ pairs, p ∉ S → Blocks profile (↑S) p) : superoptimalSet (↑pairs) profile = ↑S

Finset-version witness lemma — for structural arguments where the abstract gfp form is needed. Hypotheses are Finset-bounded universals, hence decidable when paired with Blocks.decidableOnFinset. Per-paper consumers typically prefer superoptimal (the Finset-native computable form below) with one decide; this lemma is the bridge for theorems stated about superoptimalSet.

def Core.Constraint.Evaluation.superoptimalSetStep_TEMPFIN {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] (pairs : Finset (F × M)) (profile : F × M → List ℕ) (S : Finset (F × M)) : Finset (F × M)

Single iteration step on Finset: keep pairs in pairs not blocked by S. Decidability of Blocks on Finset witnesses (via Blocks.decidableOnFinset) makes this a computable Finset.filter.

Equations

• Core.Constraint.Evaluation.superoptimalSetStep_TEMPFIN pairs profile S = {p ∈ pairs | ¬Core.Constraint.Evaluation.Blocks profile (↑S) p}

@[simp]

theorem Core.Constraint.Evaluation.mem_superoptimalSetStep_TEMPFIN {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] {pairs : Finset (F × M)} {profile : F × M → List ℕ} {S : Finset (F × M)} {p : F × M} : p ∈ superoptimalSetStep_TEMPFIN pairs profile S ↔ p ∈ pairs ∧ ¬Blocks profile (↑S) p

def Core.Constraint.Evaluation.superoptimal {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] (pairs : Finset (F × M)) (profile : F × M → List ℕ) : Finset (F × M)

@cite{blutner-2000}'s superoptimality (Finset-native, computable). Iterates superoptimalSetStep_TEMPFIN from pairs (top) until fixed.

For consumer use, this is the canonical form — output equality with a literal Finset is decide-able directly:

theorem foo : superoptimal pairs profile = winner := by decide

For structural arguments (uniqueness, ranking-invariance across OT procedures), use superoptimalSet instead, with the Park-witness API. The bridge theorem superoptimal_coe_eq_gfp connects the two when needed.

Equations

• Core.Constraint.Evaluation.superoptimal pairs profile = Core.Constraint.Evaluation.superoptimalLoop✝ pairs profile pairs (2 * pairs.card + 1)

theorem Core.Constraint.Evaluation.superoptimal_subset {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] (pairs : Finset (F × M)) (profile : F × M → List ℕ) : superoptimal pairs profile ⊆ pairs

theorem Core.Constraint.Evaluation.superoptimal_isFixedPoint {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] (pairs : Finset (F × M)) (profile : F × M → List ℕ) (h : superoptimalSetStep_TEMPFIN pairs profile (superoptimal pairs profile) = superoptimal pairs profile) : superoptimalSetStep_TEMPFIN pairs profile (superoptimal pairs profile) = superoptimal pairs profile

The iteration converges: at the returned value, one more step yields the same set (i.e., it's a fixed point of the unsquared step), provided the iteration actually stabilized within the fuel budget.

theorem Core.Constraint.Evaluation.superoptimal_coe_eq_set {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] (pairs : Finset (F × M)) (profile : F × M → List ℕ) (h_converged : superoptimalSetStep_TEMPFIN pairs profile (superoptimal pairs profile) = superoptimal pairs profile) : ↑(superoptimal pairs profile) = superoptimalSet (↑pairs) profile

Bridge theorem: when the iteration converges (the Finset returned by superoptimal is a fixed point of the unsquared step), it coincides with the abstract superoptimalSet set under coercion. This is the connection that lets per-paper consumers prove output equalities via decide on the computable form, and lift those equalities to the abstract gfp form when needed for structural arguments.

Convergence is decide-able for finite literal pairs, so the hypothesis is typically discharged by by decide at use sites.

def Core.Constraint.Evaluation.IsStrongOptimal {F : Type u_1} {M : Type u_2} (pairs : Set (F × M)) (profile : F × M → List ℕ) (p : F × M) : Prop

@cite{blutner-2000}'s strong bidirectional OT (eq. 9): a pair p is strong-optimal iff it survives one step of the blocking operator starting from the full pair set. Equivalently: p ∈ pairs and no element of pairs blocks p (the Q- and I-principles are evaluated independently against the full candidate set, not against a mutually-constrained survivor set).

Set-valued Prop sibling of the Finset-native strongOptimal below; related to weak BiOT via the structural meta-theorem strong_subset_weak.

Equations

• Core.Constraint.Evaluation.IsStrongOptimal pairs profile p = (p ∈ pairs ∧ ¬Core.Constraint.Evaluation.Blocks profile pairs p)

@[simp]

theorem Core.Constraint.Evaluation.isStrongOptimal_iff_mem_superoptimalSetStep_self {F : Type u_1} {M : Type u_2} (pairs : Set (F × M)) (profile : F × M → List ℕ) (p : F × M) : IsStrongOptimal pairs profile p ↔ p ∈ superoptimalSetStep pairs profile pairs

Strong-optimal is exactly one step of the blocking operator.

@[implicit_reducible]

instance Core.Constraint.Evaluation.IsStrongOptimal.decidableOnFinset {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] (pairs : Finset (F × M)) (profile : F × M → List ℕ) (p : F × M) : Decidable (IsStrongOptimal (↑pairs) profile p)

Equations

• Core.Constraint.Evaluation.IsStrongOptimal.decidableOnFinset pairs profile p = id inferInstance

def Core.Constraint.Evaluation.strongOptimal {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] (pairs : Finset (F × M)) (profile : F × M → List ℕ) : Finset (F × M)

Finset-native strong-optimal computation: pairs in pairs not blocked by pairs. Computable via Blocks.decidableOnFinset; consumer-facing canonical form for per-paper decide proofs.

Equations

• Core.Constraint.Evaluation.strongOptimal pairs profile = {p ∈ pairs | ¬Core.Constraint.Evaluation.Blocks profile (↑pairs) p}

@[simp]

theorem Core.Constraint.Evaluation.mem_strongOptimal {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] {pairs : Finset (F × M)} {profile : F × M → List ℕ} {p : F × M} : p ∈ strongOptimal pairs profile ↔ p ∈ pairs ∧ ¬Blocks profile (↑pairs) p

theorem Core.Constraint.Evaluation.isStrongOptimal_imp_mem_superoptimalSet {F : Type u_1} {M : Type u_2} {pairs : Set (F × M)} {profile : F × M → List ℕ} {p : F × M} (hp : IsStrongOptimal pairs profile p) : p ∈ superoptimalSet pairs profile

@cite{blutner-2000} p. 12: "It is simple to prove that a pair which is optimal (strong bidirection), is super-optimal (weak bidirection) as well."

Mathlib-grounded structural proof: the singleton {p} is a post-fixed point of the squared blocking operator superoptimalSetStepSq whenever p is strong-optimal — the only candidate blocker for p from F({p}) ⊆ pairs is excluded by strong-optimality (no pairs-element blocks p) plus Blocks.mono. Coinduction (OrderHom.le_gfp) then delivers {p} ⊆ gfp, giving p ∈ superoptimalSet pairs profile.

No algorithmic detour through iterated removal — the result is a direct consequence of OrderHom.gfp being the supremum of post-fixed points on the Set α complete lattice.

theorem Core.Constraint.Evaluation.isStrongOptimal_subset_superoptimalSet {F : Type u_1} {M : Type u_2} (pairs : Set (F × M)) (profile : F × M → List ℕ) : {p : F × M | IsStrongOptimal pairs profile p} ⊆ superoptimalSet pairs profile

Set-valued strong ⊂ weak as a Set-inclusion.

theorem Core.Constraint.Evaluation.strongOptimal_subset_superoptimal {F : Type u_1} {M : Type u_2} [DecidableEq F] [DecidableEq M] (pairs : Finset (F × M)) (profile : F × M → List ℕ) (h_converged : superoptimalSetStep_TEMPFIN pairs profile (superoptimal pairs profile) = superoptimal pairs profile) : strongOptimal pairs profile ⊆ superoptimal pairs profile

Finset version of strong ⊂ weak: when superoptimal converges, every strong-optimal pair is also weak-optimal. Per-paper consumers prove the convergence hypothesis with by decide.