Partially ordered constraints

This file defines the partially ordered constraints (POC) model of variation of Kiparsky and Anttila. A POC grammar is a partial order on the constraint set, and each evaluation samples a total order consistent with it, a linear extension, whose OT optimum is the output. A single grammar therefore induces a distribution over outputs: Anttila's quantitative interpretation is the uniform measure uniformOn on the grammar's linear extensions, and the probability of an output is that measure at the rankings picking it. The central identities are division-free cardinality equations, which the rate theorems restate as values of the measure.

Main definitions

• stratified stratumOf inner: Tesar and Smolensky's stratified domination hierarchies, pulled back from mathlib's Prod.Lex along a ↦ (stratumOf a, a). Equality is the discrete grammar, with no ranking imposed.
• IsConsistent r σ: the ranking σ is a linear extension of r, that is, r ≤ σ.toRel.
• consistentTotalOrders r: the Finset of linear extensions of r, nonempty by Szpilrajn.
• toGrammar, orderIdealAntimatroid: a POC grammar as a Grammar, and its order-ideal antimatroid.
• active con i o o', favoring con i o o': the constraints distinguishing a candidate pair, and those preferring o.

Main results

• consistentTotalOrders_eq_linearExtensions: the linear extensions of a POC grammar are those of its simple ERC encoding toERCs.
• sum_measure_setOf_picksAt: under any probability measure on rankings, POC's uniform one or stochastic OT's, the outputs' probabilities sum to one, which produces intermediate frequencies, such as Coetzee and Pater's t/d-deletion rates, that no single ranking reproduces.
• picksAt_binary_iff_exists_favoring_isMinOn: a binary competition is decided by its σ-earliest active constraint.
• uniformOn_real_picksAt_discrete_binary, uniformOn_real_picksAt_stratified_binary: chosen wins at rate |favoring ∩ active| / |active|, restricted to the deciding stratum in the stratified case.
• uniformOn_picksAt_stratified_eq_one: a candidate that dominates every rival at the deciding stratum is the categorical output.

Implementation notes

Grammars are unbundled relations r : Fin n → Fin n → Prop with [IsPartialOrder (Fin n) r], never PartialOrder (Fin n) values, since a class-typed binder would become a local instance and capture the ≤ and < notation that must keep meaning the positional order of Fin n. This is mathlib's own idiom for orders treated as data (Szpilrajn's extend_partialOrder).

References

• P. Kiparsky, An OT Perspective on Phonological Variation (1993)
• A. Anttila, Deriving Variation from Grammar (1997)
• B. Tesar and P. Smolensky, The Learnability of Optimality Theory (1995)
• A. Prince, Entailed Ranking Arguments (2002)
• N. Merchant and J. Riggle, OT grammars, beyond partial orders: ERC sets and antimatroids (2016)
• R. P. Dilworth, Lattices with unique irreducible decompositions (1940)
• A. W. Coetzee and J. Pater, The Place of Variation in Phonological Theory (2011)

Grammars and their linear extensions

instance OptimalityTheory.instIsPartialOrderEq_linglib {α : Type u_1} : IsPartialOrder α fun (x1 x2 : α) => x1 = x2

Equality is the discrete partial order, relating nothing beyond reflexivity. As a POC grammar it is [Ant97]'s "no ranking imposed" baseline, of which every permutation is a consistent linear extension.

def OptimalityTheory.IsConsistent {n : ℕ} (r : Fin n → Fin n → Prop) (σ : Ranking (Fin n) n) : Prop

A permutation σ is consistent with grammar r when r is contained in the total order σ induces (Ranking.toRel) — σ is a linear extension of r. Unfolds to ∀ a b, r a b → σ.symm a ≤ σ.symm b.

Equations

• OptimalityTheory.IsConsistent r σ = (r ≤ σ.toRel)

@[instance_reducible]

instance OptimalityTheory.instDecidableIsConsistentOfDecidableRelFin {n : ℕ} (r : Fin n → Fin n → Prop) [DecidableRel r] (σ : Ranking (Fin n) n) : Decidable (IsConsistent r σ)

Equations

• OptimalityTheory.instDecidableIsConsistentOfDecidableRelFin r σ = decidable_of_iff (∀ (a b : Fin n), r a b → (Equiv.symm σ) a ≤ (Equiv.symm σ) b) ⋯

def OptimalityTheory.consistentTotalOrders {n : ℕ} (r : Fin n → Fin n → Prop) [DecidableRel r] : Finset (Ranking (Fin n) n)

consistentTotalOrders r is the finite set of linear extensions of r.

Equations

• OptimalityTheory.consistentTotalOrders r = Finset.filter (OptimalityTheory.IsConsistent r) Finset.univ

@[simp]

theorem OptimalityTheory.mem_consistentTotalOrders {n : ℕ} {r : Fin n → Fin n → Prop} [DecidableRel r] {σ : Ranking (Fin n) n} : σ ∈ consistentTotalOrders r ↔ IsConsistent r σ

theorem OptimalityTheory.isConsistent_mul_iff {n : ℕ} {r : Fin n → Fin n → Prop} {g σ : Ranking (Fin n) n} : IsConsistent r (g * σ) ↔ IsConsistent (fun (a b : Fin n) => r (g a) (g b)) σ

The ranking g * σ extends r iff σ extends the g-pullback of r, so consistency transports along constraint relabeling.

theorem OptimalityTheory.IsConsistent.mul {n : ℕ} {r : Fin n → Fin n → Prop} {g σ : Ranking (Fin n) n} (hg : ∀ (a b : Fin n), r (g a) (g b) ↔ r a b) (hσ : IsConsistent r σ) : IsConsistent r (g * σ)

The linear extensions of a grammar are closed under its symmetries, since a relabeling that preserves r acts on the consistent rankings.

theorem OptimalityTheory.consistentTotalOrders_discrete (n : ℕ) : (consistentTotalOrders fun (x1 x2 : Fin n) => x1 = x2) = Finset.univ

For the discrete grammar, every permutation is a linear extension.

theorem OptimalityTheory.isConsistent_toRel {n : ℕ} (σ : Ranking (Fin n) n) : IsConsistent σ.toRel σ

σ is consistent with the total order it induces — reflexivity of the relation lattice.

@[simp]

theorem OptimalityTheory.consistentTotalOrders_toRel {n : ℕ} (σ : Ranking (Fin n) n) : consistentTotalOrders σ.toRel = {σ}

A ranking-induced order has its ranking as unique consistent linear extension, by the rigidity of Ranking.toRel (Ranking.toRel_le_toRel_iff).

Szpilrajn — every grammar has a consistent linear extension

theorem OptimalityTheory.exists_isConsistent {n : ℕ} (r : Fin n → Fin n → Prop) [IsPartialOrder (Fin n) r] : ∃ (σ : Ranking (Fin n) n), IsConsistent r σ

Every grammar has a consistent linear extension, since Szpilrajn's theorem (extend_partialOrder) extends r to a linear order, which is the induced order of some ranking (Ranking.exists_toRel_eq).

theorem OptimalityTheory.consistentTotalOrders_nonempty {n : ℕ} (r : Fin n → Fin n → Prop) [IsPartialOrder (Fin n) r] [DecidableRel r] : (consistentTotalOrders r).Nonempty

theorem OptimalityTheory.consistentTotalOrders_card_pos {n : ℕ} (r : Fin n → Fin n → Prop) [IsPartialOrder (Fin n) r] [DecidableRel r] : 0 < (consistentTotalOrders r).card

Stratified grammars

Earlier strata dominate later ones wholesale, and within a stratum an inner order applies. With the discrete inner order this is the freely-ranked stratum grammar of [Ant97] eq. (50) — the Stratified Domination Hierarchy of [TS95] that constraint-demotion learning produces.

def OptimalityTheory.stratified {n s : ℕ} (stratumOf : Fin n → Fin s) (inner : Fin n → Fin n → Prop) : Fin n → Fin n → Prop

The stratified grammar induced by stratumOf and an inner order inner — mathlib's lexicographic order (Prod.Lex) pulled back along a ↦ (stratumOf a, a): strata compare strictly, ties defer to inner. The plain characterization is stratified_iff; cross-stratum inner edges are ignored.

Equations

• OptimalityTheory.stratified stratumOf inner a b = Prod.Lex (fun (x1 x2 : Fin s) => x1 < x2) inner (stratumOf a, a) (stratumOf b, b)

theorem OptimalityTheory.stratified_iff {n s : ℕ} {stratumOf : Fin n → Fin s} {inner : Fin n → Fin n → Prop} {a b : Fin n} : stratified stratumOf inner a b ↔ stratumOf a < stratumOf b ∨ stratumOf a = stratumOf b ∧ inner a b

Dominance in a stratified grammar holds iff a's stratum strictly precedes b's, or they share a stratum and the inner order relates them.

instance OptimalityTheory.instIsPartialOrderFinStratified {n s : ℕ} {stratumOf : Fin n → Fin s} {inner : Fin n → Fin n → Prop} [IsPartialOrder (Fin n) inner] : IsPartialOrder (Fin n) (stratified stratumOf inner)

@[instance_reducible]

instance OptimalityTheory.instDecidableRelFinStratified {n s : ℕ} {stratumOf : Fin n → Fin s} {inner : Fin n → Fin n → Prop} [DecidableRel inner] : DecidableRel (stratified stratumOf inner)

Equations

• OptimalityTheory.instDecidableRelFinStratified x✝¹ x✝ = decidable_of_iff (stratumOf x✝¹ < stratumOf x✝ ∨ stratumOf x✝¹ = stratumOf x✝ ∧ inner x✝¹ x✝) ⋯

theorem OptimalityTheory.IsConsistent.symm_lt_of_stratum_lt {n s : ℕ} {stratumOf : Fin n → Fin s} {inner : Fin n → Fin n → Prop} {σ : Ranking (Fin n) n} (hσ : IsConsistent (stratified stratumOf inner) σ) {a b : Fin n} (h : stratumOf a < stratumOf b) : (Equiv.symm σ) a < (Equiv.symm σ) b

Under a stratified grammar, an earlier-stratum constraint occupies a strictly earlier position in every consistent ranking.

theorem OptimalityTheory.stratified_swap_apply_iff {n s : ℕ} {stratumOf : Fin n → Fin s} {inner : Fin n → Fin n → Prop} {k : Fin s} {d d' : Fin n} [Std.Refl inner] (h_triv : ∀ (a b : Fin n), stratumOf a = k → stratumOf b = k → inner a b → a = b) (hd : stratumOf d = k) (hd' : stratumOf d' = k) (a b : Fin n) : stratified stratumOf inner ((Equiv.swap d d') a) ((Equiv.swap d d') b) ↔ stratified stratumOf inner a b

Swapping two constraints of a stratum on which the inner order is trivial is a symmetry of the stratified grammar.

theorem OptimalityTheory.isConsistent_swap_mul {n s : ℕ} {stratumOf : Fin n → Fin s} {inner : Fin n → Fin n → Prop} {k : Fin s} {d d' : Fin n} {σ : Ranking (Fin n) n} [Std.Refl inner] (h_triv : ∀ (a b : Fin n), stratumOf a = k → stratumOf b = k → inner a b → a = b) (hd : stratumOf d = k) (hd' : stratumOf d' = k) (hσ : IsConsistent (stratified stratumOf inner) σ) : IsConsistent (stratified stratumOf inner) (Equiv.swap d d' * σ)

Consistent rankings of a stratified grammar are closed under swapping two constraints of a stratum on which the inner order is trivial.

Grounding in the ERC lex API

A partial order is a set of dominance requirements — each related pair is a simple ERC a ≫ b ([MR16b]), and under this encoding the consistent total orders are exactly ERC.linearExtensions ([Pri02]).

def OptimalityTheory.toERCs {n : ℕ} (r : Fin n → Fin n → Prop) [DecidableRel r] : Finset (ERC (Fin n))

The simple-ERC encoding of a grammar, with one ERC a ≫ b (simpleERC a b) for each related pair — diagonal pairs give trivial ERCs, matching toRel's reflexivity. Transitively-implied pairs are entailed by the covering pairs, so the encoding has the same linear extensions as the Hasse-edge one.

Equations

• OptimalityTheory.toERCs r = Finset.image (fun (p : Fin n × Fin n) => OptimalityTheory.simpleERC p.1 p.2) {p : Fin n × Fin n | r p.1 p.2}

theorem OptimalityTheory.mem_toERCs {n : ℕ} {r : Fin n → Fin n → Prop} [DecidableRel r] {α : ERC (Fin n)} : α ∈ toERCs r ↔ ∃ (a : Fin n) (b : Fin n), r a b ∧ simpleERC a b = α

theorem OptimalityTheory.satisfiedBy_toERCs {n : ℕ} {r : Fin n → Fin n → Prop} [DecidableRel r] {σ : Ranking (Fin n) n} : (∀ α ∈ toERCs r, ERC.SatisfiedBy σ α) ↔ IsConsistent r σ

A ranking satisfies toERCs r exactly when it is a linear extension of r: per pair, satisfaction of simpleERC a b is σ.toRel a b.

theorem OptimalityTheory.consistentTotalOrders_eq_linearExtensions {n : ℕ} (r : Fin n → Fin n → Prop) [DecidableRel r] : consistentTotalOrders r = ERC.linearExtensions (toERCs r)

The consistent total orders of a grammar are exactly the linear extensions of its simple-ERC encoding ([MR16b]; [Pri02]).

The order-ideal antimatroid of a POC

A grammar's Hasse-edge encoding is a consistent set of simple ERCs, so it has a Birkhoff antimatroid whose feasible sets are exactly the order ideals of r ([Dil40]; [MR16b]).

theorem OptimalityTheory.toERCs_isSimple_or_isTrivial {n : ℕ} (r : Fin n → Fin n → Prop) [DecidableRel r] (α : ERC (Fin n)) : α ∈ toERCs r → α.IsSimple ∨ α.IsTrivial

Every member of toERCs r is a simple ERC or (on the diagonal) trivial.

theorem OptimalityTheory.toERCs_consistent {n : ℕ} (r : Fin n → Fin n → Prop) [IsPartialOrder (Fin n) r] [DecidableRel r] : (ERC.linearExtensions (toERCs r)).Nonempty

Some linear extension of r satisfies toERCs r, so it is consistent.

def OptimalityTheory.orderIdealAntimatroid {n : ℕ} (r : Fin n → Fin n → Prop) [IsPartialOrder (Fin n) r] [DecidableRel r] : Antimatroid (Fin n)

The order-ideal antimatroid of a partial order is the antimatroid of its encoding as simple ERCs, whose feasible sets are its order ideals (orderIdealAntimatroid_isFeasible_iff).

Equations

• OptimalityTheory.orderIdealAntimatroid r = OptimalityTheory.ERC.toAntimatroid ↑(OptimalityTheory.toERCs r) ⋯

theorem OptimalityTheory.forall_isFeasible_toERCs_iff {n : ℕ} (r : Fin n → Fin n → Prop) [IsPartialOrder (Fin n) r] [DecidableRel r] {S : Finset (Fin n)} : (∀ α ∈ toERCs r, ERC.IsFeasible {α} ↑S) ↔ ∀ (a b : Fin n), r a b → b ∈ S → a ∈ S

A set is feasible for each ERC of the encoding of r exactly when it is an order ideal of r, containing every constraint above one of its members.

@[simp]

theorem OptimalityTheory.orderIdealAntimatroid_isFeasible_iff {n : ℕ} (r : Fin n → Fin n → Prop) [IsPartialOrder (Fin n) r] [DecidableRel r] {S : Finset (Fin n)} : (orderIdealAntimatroid r).IsFeasible ↑S ↔ ∀ (a b : Fin n), r a b → b ∈ S → a ∈ S

The feasible sets of orderIdealAntimatroid are the order ideals of r.

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.ofERCs (toERCs r) ([MR16b]).

def OptimalityTheory.toGrammar {n : ℕ} (r : Fin n → Fin n → Prop) [IsPartialOrder (Fin n) r] [DecidableRel r] : Grammar n

The Grammar whose legs are r's consistent total orders.

Equations

• OptimalityTheory.toGrammar r = OptimalityTheory.Grammar.ofERCs (OptimalityTheory.toERCs r) ⋯

@[simp]

theorem OptimalityTheory.toGrammar_legs {n : ℕ} (r : Fin n → Fin n → Prop) [IsPartialOrder (Fin n) r] [DecidableRel r] : (toGrammar r).legs = consistentTotalOrders r

The quantitative interpretation

A POC grammar draws one of its linear extensions uniformly at each evaluation ([Ant97]), so it is the probability measure uniformOn ↑(consistentTotalOrders r) on rankings, and the probability that it selects o for input i is that measure at {σ | PicksAt cands con σ i o}: the fraction of linear extensions picking o.

instance OptimalityTheory.instIsProbabilityMeasureRankingFinUniformOnCoeFinsetConsistentTotalOrdersOfIsPartialOrder {n : ℕ} (r : Fin n → Fin n → Prop) [IsPartialOrder (Fin n) r] [DecidableRel r] : MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.uniformOn ↑(consistentTotalOrders r))

def OptimalityTheory.active {n : ℕ} {Input : Type u_1} {Output : Type u_2} (con : ConstraintSet (Input × Output) (Fin n)) (i : Input) (o o' : Output) : Finset (Fin n)

The constraints active on the candidate pair o, o' at input i are those assigning the two candidates different violation counts ([Ant97]'s decisive constraints). Inactive constraints cannot affect the competition.

Equations

• OptimalityTheory.active con i o o' = {c : Fin n | con c (i, o) ≠ con c (i, o')}

def OptimalityTheory.favoring {n : ℕ} {Input : Type u_1} {Output : Type u_2} (con : ConstraintSet (Input × Output) (Fin n)) (i : Input) (o o' : Output) : Finset (Fin n)

The constraints favoring o over o' at input i are those assigning o strictly fewer violations.

Equations

• OptimalityTheory.favoring con i o o' = {c : Fin n | con c (i, o) < con c (i, o')}

@[simp]

theorem OptimalityTheory.mem_active {n : ℕ} {Input : Type u_1} {Output : Type u_2} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} {o o' : Output} {c : Fin n} : c ∈ active con i o o' ↔ con c (i, o) ≠ con c (i, o')

@[simp]

theorem OptimalityTheory.mem_favoring {n : ℕ} {Input : Type u_1} {Output : Type u_2} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} {o o' : Output} {c : Fin n} : c ∈ favoring con i o o' ↔ con c (i, o) < con c (i, o')

theorem OptimalityTheory.favoring_subset_active {n : ℕ} {Input : Type u_1} {Output : Type u_2} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} {o o' : Output} : favoring con i o o' ⊆ active con i o o'

def OptimalityTheory.PicksAt {n : ℕ} {Input : Type u_1} {Output : Type u_2} {ι : Type u_3} (cands : Input → Finset Output) (con : ConstraintSet (Input × Output) ι) (σ : 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 σ.

Equations

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

theorem OptimalityTheory.picksAt_unique {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {i : Input} {o o' : Output} {ι : Type u_3} {con : ConstraintSet (Input × Output) ι} {σ : Ranking ι n} (h : PicksAt cands con σ i o) (h' : PicksAt cands con σ i o') : o = o'

A ranking picks at most one output, since strict lex domination is asymmetric.

theorem OptimalityTheory.exists_picksAt {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} (h_ne : (cands i).Nonempty) (h_inj : Set.InjOn (fun (o : Output) (x : Fin n) => con x (i, o)) ↑(cands i)) (σ : Ranking (Fin n) n) : ∃ o ∈ cands i, PicksAt cands con σ i o

With pairwise-distinct violation profiles, every ranking picks some output — the candidate with the lex-minimal permuted profile wins strictly.

@[instance_reducible]

instance OptimalityTheory.instDecidablePicksAt {n : ℕ} {Input : Type u_1} {Output : Type u_2} [DecidableEq Output] {ι : Type u_3} (cands : Input → Finset Output) (con : ConstraintSet (Input × Output) ι) (σ : Ranking ι n) (i : Input) (o : Output) : Decidable (PicksAt cands con σ i o)

Equations

• OptimalityTheory.instDecidablePicksAt cands con σ i o = id inferInstance

theorem OptimalityTheory.sum_card_filter_picksAt {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {con : ConstraintSet (Input × Output) (Fin n)} {r : Fin n → Fin n → Prop} {i : Input} [DecidableEq Output] [DecidableRel r] (h_ne : (cands i).Nonempty) (h_inj : Set.InjOn (fun (o : Output) (x : Fin n) => con x (i, o)) ↑(cands i)) : ∑ o ∈ cands i, {σ ∈ consistentTotalOrders r | PicksAt cands con σ i o}.card = (consistentTotalOrders r).card

With pairwise-distinct violation profiles the picks-fibers over the candidate set partition the consistent extensions, the division-free form of sum_measure_setOf_picksAt.

theorem OptimalityTheory.card_filter_picksAt_binary_add {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {con : ConstraintSet (Input × Output) (Fin n)} {r : Fin n → Fin n → Prop} {i : Input} [DecidableEq Output] [DecidableRel r] {o₁ o₂ : Output} (h_two : cands i = {o₁, o₂}) (h_ne : o₁ ≠ o₂) (h_vp : (fun (x : Fin n) => con x (i, o₁)) ≠ fun (x : Fin n) => con x (i, o₂)) : {σ ∈ consistentTotalOrders r | PicksAt cands con σ i o₁}.card + {σ ∈ consistentTotalOrders r | PicksAt cands con σ i o₂}.card = (consistentTotalOrders r).card

Two distinct candidates with distinct violation profiles partition the consistent rankings.

theorem OptimalityTheory.sum_measure_setOf_picksAt {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} (μ : MeasureTheory.Measure (Ranking (Fin n) n)) [MeasureTheory.IsProbabilityMeasure μ] (h_ne : (cands i).Nonempty) (h_inj : Set.InjOn (fun (o : Output) (x : Fin n) => con x (i, o)) ↑(cands i)) : ∑ o ∈ cands i, μ {σ : Ranking (Fin n) n | PicksAt cands con σ i o} = 1

With pairwise-distinct violation profiles every ranking picks exactly one candidate, so under any probability measure on rankings, a POC grammar's or stochastic OT's, the candidates' probabilities sum to one.

Binary competitions are decided by the earliest active constraint

For binary candidate sets cands i = {chosen, other}, PicksAt σ i chosen reduces to lex domination of the permuted profile of chosen, which is decided at the first position where the profiles differ. So chosen wins exactly when the σ-earliest constraint of active con i chosen other, the one at which σ.symm is least, lies in favoring con i chosen other. Counting rankings by their σ-earliest active constraint (Equiv.Perm.card_filter_isMinOn_symm_mul_card) then gives closed-form rates for binary POC competitions without enumerating rankings.

theorem OptimalityTheory.lex_lt_iff_exists_favoring_isMinOn {n : ℕ} {Input : Type u_1} {Output : Type u_2} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} {o o' : Output} (σ : Ranking (Fin n) n) : ((toLex fun (k : Fin n) => con (σ k) (i, o)) < toLex fun (k : Fin n) => con (σ k) (i, o')) ↔ ∃ x ∈ favoring con i o o' ∩ active con i o o', IsMinOn (⇑(Equiv.symm σ)) (↑(active con i o o')) x

The output o lex-dominates o' under σ exactly when the σ-earliest active constraint favors o.

theorem OptimalityTheory.picksAt_binary_iff_exists_favoring_isMinOn {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} {chosen other : Output} [DecidableEq Output] (h_two : cands i = {chosen, other}) (h_ne : chosen ≠ other) (σ : Ranking (Fin n) n) : PicksAt cands con σ i chosen ↔ ∃ x ∈ favoring con i chosen other ∩ active con i chosen other, IsMinOn (⇑(Equiv.symm σ)) (↑(active con i chosen other)) x

For binary candidate sets, PicksAt σ i chosen holds exactly when the σ-earliest active constraint favors chosen.

Closed-form rate for binary candidates

theorem OptimalityTheory.card_filter_picksAt_discrete_binary {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} {chosen other : Output} [DecidableEq Output] (h_two : cands i = {chosen, other}) (h_ne : chosen ≠ other) : {σ : Ranking (Fin n) n | PicksAt cands con σ i chosen}.card * (active con i chosen other).card = n.factorial * (favoring con i chosen other ∩ active con i chosen other).card

With binary candidates, the rankings picking chosen number n! · |favoring ∩ active| / |active|, stated without division. Each ranking is decided by its σ-earliest active constraint, and every active constraint comes first equally often.

theorem OptimalityTheory.uniformOn_real_picksAt_discrete_binary {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} {chosen other : Output} [DecidableEq Output] (h_two : cands i = {chosen, other}) (h_ne : chosen ≠ other) : (ProbabilityTheory.uniformOn Set.univ).real {σ : Ranking (Fin n) n | PicksAt cands con σ i chosen} = ↑(favoring con i chosen other ∩ active con i chosen other).card / ↑(active con i chosen other).card

Under the discrete grammar, with every ranking a linear extension, the uniform measure on rankings picks chosen at rate |favoring ∩ active| / |active|.

Deciding-stratum rate for stratified grammars

A binary competition whose variants tie on every stratum before k is decided within stratum k, and later strata, including any inner rankings among them, are provably irrelevant. This is [Ant97]'s tableau-count shortcut stated against the full grammar rather than a per-stratum sub-grammar.

theorem OptimalityTheory.isMinOn_active_iff_isMinOn_filter_stratum {n s : ℕ} {Input : Type u_1} {Output : Type u_2} {con : ConstraintSet (Input × Output) (Fin n)} {σ : Ranking (Fin n) n} {i : Input} {chosen other : Output} {stratumOf : Fin n → Fin s} {inner : Fin n → Fin n → Prop} {k : Fin s} (hσ : IsConsistent (stratified stratumOf inner) σ) (h_tie : ∀ (c : Fin n), stratumOf c < k → con c (i, chosen) = con c (i, other)) (h_dec : {x ∈ active con i chosen other | stratumOf x = k}.Nonempty) {x : Fin n} : x ∈ active con i chosen other ∧ IsMinOn (⇑(Equiv.symm σ)) (↑(active con i chosen other)) x ↔ x ∈ {x ∈ active con i chosen other | stratumOf x = k} ∧ IsMinOn (⇑(Equiv.symm σ)) (↑({x ∈ active con i chosen other | stratumOf x = k})) x

On a consistent ranking of a stratified grammar, the σ-earliest active constraint is the σ-earliest active constraint of the deciding stratum k, since earlier strata are inactive (h_tie) and every constraint of stratum k precedes the later strata.

theorem OptimalityTheory.card_filter_picksAt_stratified_binary {n s : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} {chosen other : Output} [DecidableEq Output] {stratumOf : Fin n → Fin s} {inner : Fin n → Fin n → Prop} [IsPartialOrder (Fin n) inner] [DecidableRel inner] {k : Fin s} (h_two : cands i = {chosen, other}) (h_ne : chosen ≠ other) (h_triv : ∀ (a b : Fin n), stratumOf a = k → stratumOf b = k → inner a b → a = b) (h_tie : ∀ (c : Fin n), stratumOf c < k → con c (i, chosen) = con c (i, other)) (h_dec : {x ∈ active con i chosen other | stratumOf x = k}.Nonempty) : {σ ∈ consistentTotalOrders (stratified stratumOf inner) | PicksAt cands con σ i chosen}.card * {x ∈ active con i chosen other | stratumOf x = k}.card = (consistentTotalOrders (stratified stratumOf inner)).card * (favoring con i chosen other ∩ {x ∈ active con i chosen other | stratumOf x = k}).card

Under a stratified grammar, a binary competition whose variants tie on every stratum before k, with k freely ranked internally (h_triv) and containing an active constraint (h_dec), is decided within stratum k. The rankings picking chosen, times the active constraints Dₖ of that stratum, equal all consistent rankings times those favoring chosen, and later strata cannot affect the outcome.

theorem OptimalityTheory.uniformOn_real_picksAt_stratified_binary {n s : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} {chosen other : Output} [DecidableEq Output] {stratumOf : Fin n → Fin s} {inner : Fin n → Fin n → Prop} [IsPartialOrder (Fin n) inner] [DecidableRel inner] {k : Fin s} (h_two : cands i = {chosen, other}) (h_ne : chosen ≠ other) (h_triv : ∀ (a b : Fin n), stratumOf a = k → stratumOf b = k → inner a b → a = b) (h_tie : ∀ (c : Fin n), stratumOf c < k → con c (i, chosen) = con c (i, other)) (h_dec : {x ∈ active con i chosen other | stratumOf x = k}.Nonempty) : (ProbabilityTheory.uniformOn ↑(consistentTotalOrders (stratified stratumOf inner))).real {σ : Ranking (Fin n) n | PicksAt cands con σ i chosen} = ↑(favoring con i chosen other ∩ {x ∈ active con i chosen other | stratumOf x = k}).card / ↑{x ∈ active con i chosen other | stratumOf x = k}.card

Under a stratified grammar, the uniform measure on its linear extensions picks chosen at the deciding-stratum rate |favoring ∩ Dₖ| / |Dₖ|.

Categorical outcomes under stratified grammars

theorem OptimalityTheory.picksAt_stratified_of_dominates {n s : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {con : ConstraintSet (Input × Output) (Fin n)} {σ : Ranking (Fin n) n} {i : Input} {o : Output} {stratumOf : Fin n → Fin s} {inner : Fin n → Fin n → Prop} (hσ : IsConsistent (stratified stratumOf inner) σ) (ho : o ∈ cands i) (h : ∀ o' ∈ cands i, o' ≠ o → ∃ (k : Fin s), (∀ (c : Fin n), stratumOf c < k → con c (i, o) = con c (i, o')) ∧ {x ∈ active con i o o' | stratumOf x = k}.Nonempty ∧ {x ∈ active con i o o' | stratumOf x = k} ⊆ favoring con i o o') : PicksAt cands con σ i o

Under a stratified grammar, a consistent ranking picks o when, against every rival, the first stratum on which they differ has all its active constraints favoring o.

theorem OptimalityTheory.uniformOn_picksAt_stratified_eq_one {n s : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {con : ConstraintSet (Input × Output) (Fin n)} {i : Input} {o : Output} {stratumOf : Fin n → Fin s} {inner : Fin n → Fin n → Prop} [IsPartialOrder (Fin n) inner] [DecidableRel inner] (ho : o ∈ cands i) (h : ∀ o' ∈ cands i, o' ≠ o → ∃ (k : Fin s), (∀ (c : Fin n), stratumOf c < k → con c (i, o) = con c (i, o')) ∧ {x ∈ active con i o o' | stratumOf x = k}.Nonempty ∧ {x ∈ active con i o o' | stratumOf x = k} ⊆ favoring con i o o') : (ProbabilityTheory.uniformOn ↑(consistentTotalOrders (stratified stratumOf inner))) {σ : Ranking (Fin n) n | PicksAt cands con σ i o} = 1

A candidate dominating every rival at the deciding stratum wins with probability one.