Partially Ordered Constraints (POC)

@cite{anttila-1997} @cite{kiparsky-1993b} @cite{coetzee-pater-2011}

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 Equiv.Perm (Fin 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 OTRealizes 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.
• 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 @cite{coetzee-pater-2011}'s t/d-deletion analysis) that no single OT ranking can reproduce.

Where this is used

Phenomena/Phonology/Studies/CoetzeePater2011.lean currently does its POC analysis by manually enumerating permutations constraints and filtering. A follow-up refactor would have CoetzeePater consume pocPredict and substrate-level POC theorems instead.

structure Core.Constraint.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).

• decidable_rel : DecidableRel self.rel

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

• refl (a : Fin n) : self.rel a a

  Reflexivity.

• trans {a b c : Fin n} : self.rel a b → self.rel b c → self.rel a c

  Transitivity.

• antisymm {a b : Fin n} : self.rel a b → self.rel b a → a = b

  Antisymmetry.

def Core.Constraint.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 @cite{anttila-1997}'s "no ranking imposed" baseline.

Equations

• Core.Constraint.PartialOrderConstraints.discrete n = { rel := Eq, decidable_rel := inferInstance, refl := ⋯, trans := ⋯, antisymm := ⋯ }

def Core.Constraint.PartialOrderConstraints.fromPermutation {n : ℕ} (σ : Equiv.Perm (Fin 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 Core.Constraint.PartialOrderConstraints.IsConsistent {n : ℕ} (p : PartialOrderConstraints n) (σ : Equiv.Perm (Fin 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 Core.Constraint.PartialOrderConstraints.instDecidableIsConsistent {n : ℕ} (p : PartialOrderConstraints n) (σ : Equiv.Perm (Fin n)) : Decidable (p.IsConsistent σ)

Equations

• p.instDecidableIsConsistent σ = id inferInstance

def Core.Constraint.PartialOrderConstraints.consistentTotalOrders {n : ℕ} (p : PartialOrderConstraints n) : Finset (Equiv.Perm (Fin n))

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

Equations

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

@[simp]

theorem Core.Constraint.PartialOrderConstraints.mem_consistentTotalOrders {n : ℕ} {p : PartialOrderConstraints n} {σ : Equiv.Perm (Fin n)} : σ ∈ p.consistentTotalOrders ↔ p.IsConsistent σ

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

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

theorem Core.Constraint.PartialOrderConstraints.isConsistent_fromPermutation {n : ℕ} (σ : Equiv.Perm (Fin n)) : (fromPermutation σ).IsConsistent σ

σ is consistent with the partial order it induces.

theorem Core.Constraint.PartialOrderConstraints.mem_consistentTotalOrders_fromPermutation {n : ℕ} (σ : Equiv.Perm (Fin n)) : σ ∈ (fromPermutation σ).consistentTotalOrders

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

theorem Core.Constraint.PartialOrderConstraints.fromPermutation_consistent_unique {n : ℕ} {σ τ : Equiv.Perm (Fin 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 Core.Constraint.PartialOrderConstraints.consistentTotalOrders_fromPermutation {n : ℕ} (σ : Equiv.Perm (Fin n)) : (fromPermutation σ).consistentTotalOrders = {σ}

theorem Core.Constraint.PartialOrderConstraints.consistentTotalOrders_nonempty_of_fromPermutation {n : ℕ} (σ : Equiv.Perm (Fin n)) : (fromPermutation σ).consistentTotalOrders.Nonempty

def Core.Constraint.SystemicProblem.POCRealizes {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 it has at least one consistent extension and every consistent extension realizes the target. This is the categorical realizability notion: target probability = 1 under POC sampling.

Equations

• P.POCRealizes p = (p.consistentTotalOrders.Nonempty ∧ ∀ σ ∈ p.consistentTotalOrders, P.OTRealizes σ)

def Core.Constraint.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 : Core.Constraint.PartialOrderConstraints n), P.POCRealizes p

theorem Core.Constraint.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 Core.Constraint.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 Core.Constraint.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.

def Core.Constraint.PartialOrderConstraints.PicksAt {Input : Type u_1} {Output : Type u_2} {n : ℕ} (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (σ : Equiv.Perm (Fin 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

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

@[implicit_reducible]

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

Equations

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

def Core.Constraint.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. Uses ℚ's 0/0 = 0 convention to handle the degenerate empty-consistent-set case without an explicit guard.

Equations

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

theorem Core.Constraint.PartialOrderConstraints.pocPredict_fromPermutation {Input : Type u_1} {Output : Type u_2} [DecidableEq Output] {n : ℕ} (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (σ : Equiv.Perm (Fin 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 Core.Constraint.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 = ↑{σ : Equiv.Perm (Fin 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!.

For binary candidate sets cands i = {chosen, other}, PicksAt σ i chosen reduces to LexStrictlyBetter (vp i chosen ∘ σ) (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.Constraint.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 Phenomena/Phonology/Studies/CoetzeePater2011.lean (English t/d-deletion; binary {retain, delete} outputs across 3 contexts).

theorem Core.Constraint.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) (σ : Equiv.Perm (Fin n)) : PicksAt cands vp σ i chosen ↔ ∃ x ∈ {k : Fin n | vp i chosen k < vp i other k}, (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 LexStrictlyBetter's ∃k form and the head-in-Y characterization.

theorem Core.Constraint.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) : ↑{σ : Equiv.Perm (Fin 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.Constraint.PermSubsetCombinatorics.perm_filter_head_in_rate (the rate form of the closed-form combinatorics).

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