Partially Ordered Constraints (POC)

[Ant97] [Kip93] [CP11b]

A POC grammar is a partial order on the constraint set. Each evaluation samples a total order (i.e., a linear extension) consistent with the partial order, and the OT optimum under that ranking is the output. The induced distribution over outputs is uniform over consistent linear extensions.

This module provides the substrate counterpart to the per-paper POC analyses: every linear extension is a Ranking n, and every finite set of consistent extensions sits inside Finset.univ for that permutation type. The probability of an output is then a ratio of Finset cardinalities — a clean computation, no measure theory required.

Architecture

POC sits in the substrate alongside Cumulativity.SystemicProblem, sharing its multi-input optimization model and its realizedByRanking definition. The new content here is:

• PartialOrderConstraints n: a partial order on Fin n (constraint indices).
• IsConsistent p σ: σ is a linear extension of p.
• consistentTotalOrders p: the (decidable, finite) set of linear extensions.
• toERCSet p / consistentTotalOrders_eq_linearExtensions: the simple-ERC (Hasse-edge) encoding of p, identifying its consistent total orders with the lex-grounded ERCSet.linearExtensions — so POC's "linear extension" is the ERC one, not a third re-stipulation ([MR16]; [Pri02]).
• pocPredict P p i o: the probability that POC sampling under p selects output o for input i, computed as a ratio of consistent extensions realizing o vs. all consistent extensions.
• IsPOCRealizable P: some non-trivial partial order has every consistent extension realizing the target. This is the categorical realizability notion; the probabilistic story is captured by pocPredict.

Containments

• poc_realizable_imp_ot_realizable — trivial (pick any consistent extension).
• ot_realizable_imp_poc_realizable — non-trivial; the witness is the σ-induced total order, whose unique consistent extension is σ. The uniqueness step uses the standard fact that a strictly monotone bijection on a finite linear order is the identity (proof via StrictMono.id_le + dual).

The categorical containment OT ⊆ POC is somewhat misleading linguistically: POC's expressive advantage over OT is probabilistic, not categorical. The pocPredict API is the principled way to surface that — POC can produce intermediate frequencies (e.g., 8/24, 12/24 in [CP11b]'s t/d-deletion analysis) that no single OT ranking can reproduce.

Where this is used

Studies/CoetzeePater2011.lean and Studies/Zuraw2010.lean consume this substrate directly — pocPredict, PicksAt, and pocPredict_discrete_binary_rate over the discrete partial order — rather than enumerating rankings by hand.

Auxiliary — Strictly Monotone Bijection on Fin n is the Identity

PartialOrderConstraints

structure HarmonicGrammar.PartialOrderConstraints (n : ℕ) : Type

A partial order on Fin n constraint indices. The OT case is a total order; the POC case allows incomparable pairs (multiple consistent linear extensions).

• rel : Fin n → Fin n → Prop

  The partial-order relation: rel a b reads "a is ranked at-most-as-low-as b", i.e., a takes priority over b (or they're equal).

• decidableRel : DecidableRel self.rel

  Decidability of the relation (required for consistentTotalOrders to be a computable Finset).

• isPartialOrder : IsPartialOrder (Fin n) self.rel

  rel is a partial order — reflexive, transitive, antisymmetric — bundled as mathlib's IsPartialOrder instance instead of three loose proof fields, so the order-relation API (antisymm_of, …) applies to it.

def HarmonicGrammar.PartialOrderConstraints.discrete (n : ℕ) : PartialOrderConstraints n

The discrete partial order on Fin n: rel a b iff a = b. No constraint pair is comparable beyond reflexivity. Every permutation is a consistent linear extension — this matches [Ant97]'s "no ranking imposed" baseline.

Equations

• HarmonicGrammar.PartialOrderConstraints.discrete n = { rel := Eq, decidableRel := instDecidableEqFin n, isPartialOrder := ⋯ }

def HarmonicGrammar.PartialOrderConstraints.fromPermutation {n : ℕ} (σ : OptimalityTheory.Ranking n) : PartialOrderConstraints n

The total order induced by a permutation σ: rel a b iff σ.symm a ≤ σ.symm b (i.e., a appears at least as early as b in σ's enumeration). This is a total order; its unique consistent linear extension is σ itself (fromPermutation_consistent_unique below).

Equations

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

def HarmonicGrammar.PartialOrderConstraints.IsConsistent {n : ℕ} (p : PartialOrderConstraints n) (σ : OptimalityTheory.Ranking n) : Prop

A permutation σ is consistent with the partial order p if σ⁻¹ respects rel: whenever rel a b holds, σ ranks a at least as early as b (σ.symm a ≤ σ.symm b). σ is a linear extension of p.

Equations

• p.IsConsistent σ = ∀ (a b : Fin n), p.rel a b → (Equiv.symm σ) a ≤ (Equiv.symm σ) b

@[implicit_reducible]

instance HarmonicGrammar.PartialOrderConstraints.instDecidableIsConsistent {n : ℕ} (p : PartialOrderConstraints n) (σ : OptimalityTheory.Ranking n) : Decidable (p.IsConsistent σ)

Equations

• p.instDecidableIsConsistent σ = id inferInstance

def HarmonicGrammar.PartialOrderConstraints.consistentTotalOrders {n : ℕ} (p : PartialOrderConstraints n) : Finset (OptimalityTheory.Ranking n)

The (decidable, finite) set of linear extensions of p.

Equations

• p.consistentTotalOrders = Finset.filter p.IsConsistent Finset.univ

@[simp]

theorem HarmonicGrammar.PartialOrderConstraints.mem_consistentTotalOrders {n : ℕ} {p : PartialOrderConstraints n} {σ : OptimalityTheory.Ranking n} : σ ∈ p.consistentTotalOrders ↔ p.IsConsistent σ

Grounding in the ERC lex API

A partial order is a set of dominance requirements; each strict related pair a ≠ b with rel a b is the Hasse-style ERC a ≫ b (simpleERC a b, [MR16]'s simple ERCs). Encoding p this way shows consistentTotalOrders p is the ERC linear-extension set ERCSet.linearExtensions, so the POC notion of "consistent total order" is not a third re-stipulation of "linear extension" but the lex-grounded ERC one ([Pri02]).

def HarmonicGrammar.PartialOrderConstraints.toERCSet {n : ℕ} (p : PartialOrderConstraints n) : OptimalityTheory.ERCSet n

The simple-ERC encoding of a partial order: one ERC a ≫ b (simpleERC a b) for each strict related pair (a ≠ b with rel a b). Transitively-implied pairs are included as well; they are entailed by the covering pairs, so this set has the same linear extensions as the Hasse-edge encoding. Built by computable enumeration over List.finRange so it carries no noncomputable marker.

Equations

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

theorem HarmonicGrammar.PartialOrderConstraints.mem_toERCSet {n : ℕ} {p : PartialOrderConstraints n} {α : OptimalityTheory.ERC n} : α ∈ p.toERCSet ↔ ∃ (a : Fin n) (b : Fin n), a ≠ b ∧ p.rel a b ∧ OptimalityTheory.simpleERC a b = α

theorem HarmonicGrammar.PartialOrderConstraints.satisfiedBy_toERCSet {n : ℕ} {p : PartialOrderConstraints n} {σ : OptimalityTheory.Ranking n} : OptimalityTheory.ERCSet.SatisfiedBy σ p.toERCSet ↔ p.IsConsistent σ

A ranking satisfies p.toERCSet exactly when it is a linear extension of p: the a ≫ b ERCs are the strict dominance requirements, and reflexive pairs impose nothing.

theorem HarmonicGrammar.PartialOrderConstraints.consistentTotalOrders_eq_linearExtensions {n : ℕ} (p : PartialOrderConstraints n) : p.consistentTotalOrders = p.toERCSet.linearExtensions

POC consistency is ERC linear extension. The consistent total orders of a partial order are exactly the linear extensions of its simple-ERC encoding — collapsing the POC consistentTotalOrders into the lex-grounded ERCSet.linearExtensions ([MR16]; [Pri02]).

theorem HarmonicGrammar.PartialOrderConstraints.consistentTotalOrders_discrete (n : ℕ) : (discrete n).consistentTotalOrders = Finset.univ

For the discrete partial order, every permutation is a linear extension.

theorem HarmonicGrammar.PartialOrderConstraints.isConsistent_fromPermutation {n : ℕ} (σ : OptimalityTheory.Ranking n) : (fromPermutation σ).IsConsistent σ

σ is consistent with the partial order it induces.

theorem HarmonicGrammar.PartialOrderConstraints.mem_consistentTotalOrders_fromPermutation {n : ℕ} (σ : OptimalityTheory.Ranking n) : σ ∈ (fromPermutation σ).consistentTotalOrders

The σ-induced total order has σ as a consistent linear extension.

theorem HarmonicGrammar.PartialOrderConstraints.fromPermutation_consistent_unique {n : ℕ} {σ τ : OptimalityTheory.Ranking n} (hτ : (fromPermutation σ).IsConsistent τ) : τ = σ

Uniqueness: the σ-induced total order has σ as its unique consistent linear extension. Any consistent τ must agree with σ pointwise (since τ.symm ∘ σ is a monotone bijection on Fin n, hence the identity by fin_monotone_bij_eq_id).

@[simp]

theorem HarmonicGrammar.PartialOrderConstraints.consistentTotalOrders_fromPermutation {n : ℕ} (σ : OptimalityTheory.Ranking n) : (fromPermutation σ).consistentTotalOrders = {σ}

theorem HarmonicGrammar.PartialOrderConstraints.consistentTotalOrders_nonempty {n : ℕ} (p : PartialOrderConstraints n) : p.consistentTotalOrders.Nonempty

Every POC has a consistent linear extension (Szpilrajn): for any partial order p, consistentTotalOrders p is nonempty. This is what the IsPartialOrder instance buys — it is the hypothesis of mathlib's extend_partialOrder. Consequently pocPredict's denominator (consistentTotalOrders.card) is provably positive for every POC, so pocPredict is a genuine distribution, not just on discrete/fromPermutation.

theorem HarmonicGrammar.PartialOrderConstraints.consistentTotalOrders_card_pos {n : ℕ} (p : PartialOrderConstraints n) : 0 < p.consistentTotalOrders.card

pocPredict's denominator consistentTotalOrders.card is strictly positive for any POC — the 0/0 guard in pocPredict is never exercised on a real partial order. Direct consequence of consistentTotalOrders_nonempty.

The order-ideal antimatroid of a POC

A POC partial order's Hasse-edge encoding is a consistent set of simple ERCs, so it has a Birkhoff antimatroid (Antimat.ofSimple). Its feasible sets are exactly the order ideals of p, giving the antimatroid theory its first grammar-level consumer ([Dil40]; [MR16]).

theorem HarmonicGrammar.PartialOrderConstraints.toERCSet_isSimpleSet {n : ℕ} (p : PartialOrderConstraints n) : p.toERCSet.IsSimpleSet

p.toERCSet consists of simple ERCs (each is a simpleERC of a strict pair).

theorem HarmonicGrammar.PartialOrderConstraints.toERCSet_consistent {n : ℕ} (p : PartialOrderConstraints n) : p.toERCSet.Consistent

p.toERCSet is consistent: any linear extension of p satisfies it.

def HarmonicGrammar.PartialOrderConstraints.pocAntimatroid {n : ℕ} (p : PartialOrderConstraints n) : Antimatroid (Fin n)

The order-ideal antimatroid of a POC partial order: the simple-ERC Birkhoff antimatroid (Antimat.ofSimple) of its Hasse-edge encoding. Its feasible sets are exactly the order ideals of p (pocAntimatroid_isFeasible_iff) — the Birkhoff correspondence between a partial order and its antimatroid ([Dil40]; [MR16]). This is the first grammar-level consumer of the antimatroid theory.

Equations

• p.pocAntimatroid = OptimalityTheory.Antimat.ofSimple p.toERCSet ⋯ ⋯

theorem HarmonicGrammar.PartialOrderConstraints.feasible_toERCSet_iff {n : ℕ} {p : PartialOrderConstraints n} {S : Finset (Fin n)} : OptimalityTheory.Feasible p.toERCSet S ↔ ∀ (a b : Fin n), p.rel a b → b ∈ S → a ∈ S

Local feasibility against p.toERCSet is exactly the order-ideal condition (downward-closed under rel): if b ∈ S and a dominates b (rel a b), then a ∈ S.

@[simp]

theorem HarmonicGrammar.PartialOrderConstraints.pocAntimatroid_isFeasible_iff {n : ℕ} {p : PartialOrderConstraints n} {S : Finset (Fin n)} : p.pocAntimatroid.IsFeasible ↑S ↔ ∀ (a b : Fin n), p.rel a b → b ∈ S → a ∈ S

The feasible sets of pocAntimatroid are the order ideals of p — the Birkhoff correspondence, made concrete and decidable.

POC Realizability of SystemicProblem

def HarmonicGrammar.SystemicProblem.realizedByPOC {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : SystemicProblem Input Output n) (p : PartialOrderConstraints n) : Prop

A partial order p POC-realizes the target if every consistent extension realizes it. There is always at least one consistent extension (consistentTotalOrders_nonempty), so this genuinely means target probability = 1 under POC sampling — not the vacuous empty case, which is why no explicit nonemptiness conjunct is needed.

Equations

• P.realizedByPOC p = ∀ σ ∈ p.consistentTotalOrders, P.realizedByRanking σ

def HarmonicGrammar.SystemicProblem.IsPOCRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : SystemicProblem Input Output n) : Prop

A SystemicProblem is POC-realizable if some partial order categorically realizes the target.

Equations

• P.IsPOCRealizable = ∃ (p : HarmonicGrammar.PartialOrderConstraints n), P.realizedByPOC p

Containments — OT ⊆ POC, POC ⊆ OT (categorical)

theorem HarmonicGrammar.poc_realizable_imp_ot_realizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : SystemicProblem Input Output n) : P.IsPOCRealizable → P.IsOTRealizable

Trivial direction: every POC-realized target is OT-realized (pick any single consistent extension).

theorem HarmonicGrammar.ot_realizable_imp_poc_realizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : SystemicProblem Input Output n) : P.IsOTRealizable → P.IsPOCRealizable

Non-trivial direction: every OT-realized target is POC-realized (the witness is the σ-induced total order, whose unique consistent extension is σ itself by fromPermutation_consistent_unique).

theorem HarmonicGrammar.isOTRealizable_iff_isPOCRealizable {Input : Type u_1} {Output : Type u_2} {n : ℕ} (P : SystemicProblem Input Output n) : P.IsOTRealizable ↔ P.IsPOCRealizable

Categorical equivalence: under categorical realizability, OT-realizable and POC-realizable coincide. POC's probabilistic advantage over OT is captured separately by pocPredict (next section); no categorical theorem distinguishes them.

Probabilistic POC — pocPredict

def HarmonicGrammar.PartialOrderConstraints.PicksAt {Input : Type u_1} {Output : Type u_2} {n : ℕ} (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (σ : OptimalityTheory.Ranking n) (i : Input) (o : Output) : Prop

σ picks output o for input i if o is the unique strict OT winner (every other in-set candidate is lex-strictly worse than o under σ).

Bare-args version: takes cands and vp directly rather than bundled in a SystemicProblem. POC analyses don't need a target — they're about distribution over outputs, not realization of a chosen one.

Equations

• HarmonicGrammar.PartialOrderConstraints.PicksAt cands vp σ i o = (o ∈ cands i ∧ ∀ o' ∈ cands i, o' ≠ o → (toLex fun (k : Fin n) => vp i o (σ k)) < toLex fun (k : Fin n) => vp i o' (σ k))

@[implicit_reducible]

instance HarmonicGrammar.PartialOrderConstraints.instDecidablePicksAt {Input : Type u_1} {Output : Type u_2} [DecidableEq Output] {n : ℕ} (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (σ : OptimalityTheory.Ranking n) (i : Input) (o : Output) : Decidable (PicksAt cands vp σ i o)

Equations

• HarmonicGrammar.PartialOrderConstraints.instDecidablePicksAt cands vp σ i o = id inferInstance

def HarmonicGrammar.PartialOrderConstraints.pocPredict {Input : Type u_1} {Output : Type u_2} [DecidableEq Output] {n : ℕ} (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (p : PartialOrderConstraints n) (i : Input) (o : Output) : ℚ

The probability that POC sampling under partial order p selects output o for input i: ratio of consistent extensions picking o to total consistent extensions. The denominator is always positive (consistentTotalOrders_card_pos), so this is a genuine probability; ℚ's 0/0 = 0 convention is a harmless fallback never exercised on a real POC.

Equations

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

theorem HarmonicGrammar.PartialOrderConstraints.pocPredict_fromPermutation {Input : Type u_1} {Output : Type u_2} [DecidableEq Output] {n : ℕ} (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (σ : OptimalityTheory.Ranking n) (i : Input) (o : Output) : pocPredict cands vp (fromPermutation σ) i o = if PicksAt cands vp σ i o then 1 else 0

For the σ-induced total order, pocPredict collapses to a δ at σ's OT-pick: probability 1 if σ picks o, probability 0 otherwise.

theorem HarmonicGrammar.PartialOrderConstraints.pocPredict_discrete {Input : Type u_1} {Output : Type u_2} [DecidableEq Output] {n : ℕ} (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (i : Input) (o : Output) : pocPredict cands vp (discrete n) i o = ↑{σ : OptimalityTheory.Ranking n | PicksAt cands vp σ i o}.card / ↑Finset.univ.card

Discrete-PO predict: uniform over all permutations (no ranking imposed). Counts the σ's that pick o, divides by n!.

Bridge — PicksAt for binary candidates ↔ head-in-Y on permDList

For binary candidate sets cands i = {chosen, other}, PicksAt σ i chosen reduces to lex domination of vp i chosen ∘ σ over vp i other ∘ σ (the ∀-quantifier collapses to a single check). And that lex predicate is exactly "the highest-ranked constraint in the distinguishing set D favors chosen" — i.e., head of permDList σ D ∈ Y where D = {k : vp chosen k ≠ vp other k} and Y = {k : vp chosen k < vp other k}.

This bridges POC's lex-strict-better predicate to Core.Optimization.PermSubsetCombinatorics.perm_filter_head_in_card's closed form, letting any binary-candidate POC study compute its pocPredict value in closed form (n! × |Y ∩ D| / |D|) without enumerating n! rankings.

Used by Studies/CoetzeePater2011.lean (English t/d-deletion; binary {retain, delete} outputs across 3 contexts).

theorem HarmonicGrammar.PartialOrderConstraints.picksAt_binary_iff_permDList_head_lt {Input : Type u_1} {n : ℕ} {Output : Type u_2} [DecidableEq Output] (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (i : Input) (chosen other : Output) (h_two : cands i = {chosen, other}) (h_ne : chosen ≠ other) (σ : OptimalityTheory.Ranking n) : PicksAt cands vp σ i chosen ↔ ∃ x ∈ {k : Fin n | vp i chosen k < vp i other k}, (Core.Optimization.PermSubsetCombinatorics.permDList σ {k : Fin n | vp i chosen k ≠ vp i other k}).head? = some x

For binary candidate sets, PicksAt σ i chosen is equivalent to "the head of permDList σ D lies in Y", where D is the set of constraints distinguishing chosen from other and Y is the favoring subset (vp chosen < vp other).

The bridge uses permDList_head_eq_some_iff + permToList_split_at + permToList_eq_append_cons_imp_apply (substrate) to translate between the lex ∃k form and the head-in-Y characterization.

Closed-form rate for binary candidates

theorem HarmonicGrammar.PartialOrderConstraints.picksAt_rate_eq {Input : Type u_2} {Output : Type u_3} [DecidableEq Output] {n : ℕ} (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (i : Input) (chosen other : Output) (h_two : cands i = {chosen, other}) (h_ne : chosen ≠ other) (D Y : Finset (Fin n)) (h_D : ∀ (k : Fin n), k ∈ D ↔ vp i chosen k ≠ vp i other k) (h_Y : ∀ (k : Fin n), k ∈ Y ↔ vp i chosen k < vp i other k) : ↑{σ : OptimalityTheory.Ranking n | PicksAt cands vp σ i chosen}.card / ↑n.factorial = ↑(Y ∩ D).card / ↑D.card

Closed-form rate for binary pocPredict under the discrete partial order: when cands i = {chosen, other}, the fraction of all n! permutations that pick chosen for input i equals |Y ∩ D| / |D|, where D is the distinguishing set (constraints where vp differs) and Y is the favoring set (constraints where chosen has fewer violations).

Combines picksAt_binary_iff_permDList_head_lt (the bridge from PicksAt to head-of-permDList) with Core.Optimization.PermSubsetCombinatorics.perm_filter_head_in_rate (the rate form of the closed-form combinatorics).

Consumed by Studies/CoetzeePater2011.lean (binary {retain, delete} over Fin 4) and Studies/Zuraw2010.lean (binary {yes, no} over Fin 6).

theorem HarmonicGrammar.PartialOrderConstraints.pocPredict_discrete_binary_rate {Input : Type u_2} {Output : Type u_3} [DecidableEq Output] {n : ℕ} (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (i : Input) (chosen other : Output) (h_two : cands i = {chosen, other}) (h_ne : chosen ≠ other) (D Y : Finset (Fin n)) (h_D : ∀ (k : Fin n), k ∈ D ↔ vp i chosen k ≠ vp i other k) (h_Y : ∀ (k : Fin n), k ∈ Y ↔ vp i chosen k < vp i other k) : pocPredict cands vp (discrete n) i chosen = ↑(Y ∩ D).card / ↑D.card

Closed-form rate for pocPredict under the discrete partial order with binary candidate sets: pocPredict cands vp (.discrete n) i chosen = |Y ∩ D| / |D|. Composes pocPredict_discrete with picksAt_rate_eq, absorbing the Fintype.card_perm/Fintype.card_fin arithmetic bridge.

This is the user-facing rate identity every binary-candidate POC study wants. Consumed by Studies/CoetzeePater2011.lean (3 contexts), Studies/Anttila1997.lean (2 grammar tiers), and Studies/Zuraw2010.lean.

Bridge to the Grammar hub

A partial order on constraints is the simple-ERC fragment of an OT grammar: its consistent total orders are exactly the legs of Grammar.ofERCSet p.toERCSet, routing POC through the canonical Grammar type rather than its own bespoke linear-extension plumbing ([MR16]). The simple-ERC encoding is consistent via toERCSet_consistent (Szpilrajn, above).

def HarmonicGrammar.PartialOrderConstraints.toGrammar {n : ℕ} (p : PartialOrderConstraints n) : OptimalityTheory.Grammar n

The grammar of a partial order: the Grammar whose legs are p's consistent total orders — the simple-ERC fragment of the hub.

Equations

• p.toGrammar = OptimalityTheory.Grammar.ofERCSet p.toERCSet ⋯

@[simp]

theorem HarmonicGrammar.PartialOrderConstraints.toGrammar_legs {n : ℕ} (p : PartialOrderConstraints n) : p.toGrammar.legs = p.consistentTotalOrders