Partially Ordered Constraints (POC)

A POC grammar is a partial order on the constraint set ([Ant97]; [Kip93]) — represented as mathlib represents orders-as-data (extend_partialOrder): a bare relation r : Fin n → Fin n → Prop with [IsPartialOrder (Fin n) r], and [DecidableRel r] where counting needs it. Each evaluation samples a total order consistent with the partial order — a linear extension — and the OT optimum under that ranking is the output, so a single grammar induces a distribution over outputs, uniform over consistent linear extensions. The load-bearing identities are division-free cardinality equations (sum_card_filter_picksAt here, the head-fiber counting in Core.Optimization.PermSubsetCombinatorics); winProb and its rate theorems are a ℚ veneer over them.

Main definitions

• Grammars: Eq (the discrete grammar — no rankings), Ranking.toRel σ (the total order a ranking induces), and stratified stratumOf inner (mutually-ranked strata refined by an inner order — [TS95]'s Stratified Domination Hierarchies — defined as mathlib's Prod.Lex pulled back along a ↦ (stratumOf a, a), characterized by stratified_iff).
• IsConsistent r σ: σ is a linear extension of r, defined as containment r ≤ σ.toRel in the pointwise lattice of relations. consistentTotalOrders r is the (nonempty, by Szpilrajn) Finset of them.
• winProb cands vp r i o: the probability that sampling under r selects output o for input i — a genuine distribution (winProb_nonneg, winProb_le_one, sum_winProb_eq_one).
• active vp i o o' / favoring vp i o o': the constraints distinguishing a candidate pair, and those preferring o.

Main statements

• consistentTotalOrders_eq_linearExtensions: POC's linear extensions are the ERC ones — the simple-ERC (Hasse-edge) encoding toERCs identifies consistentTotalOrders with ERC.linearExtensions ([MR16]; [Pri02]). toGrammar routes POC through the Grammar hub, and orderIdealAntimatroid realizes the Birkhoff correspondence with order-ideal antimatroids ([Dil40]).
• winProb produces intermediate frequencies (e.g. [CP11b]'s 8/24 vs 12/24 t/d-deletion rates) that no single ranking reproduces; categorically, partial orders add nothing over OT (RealizationProblem.isOTRealizable_iff_isPartialOrderRealizable in HarmonicGrammar.Expressivity).
• winProb_discrete_binary_rate / winProb_stratified_binary_rate: closed-form win rates for binary competitions. A ranking is decided by its earliest active constraint (picksAt_binary_iff_head_mem_favoring), so chosen wins at rate |favoring ∩ active| / |active| — restricted to the deciding stratum in the stratified case — with no enumeration of rankings.

Implementation notes

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

Grammars and their linear extensions

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

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

def OptimalityTheory.IsConsistent {n : ℕ} (r : Fin n → Fin n → Prop) (σ : Ranking 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 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 n)

The (decidable, 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 n} : σ ∈ consistentTotalOrders r ↔ IsConsistent r σ

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

Consistency transports along constraint relabeling: g * σ extends r iff σ extends the g-pullback of r.

theorem OptimalityTheory.IsConsistent.mul {n : ℕ} {r : Fin n → Fin n → Prop} {g σ : Ranking 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: 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 n) : IsConsistent σ.toRel σ

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

@[simp]

theorem OptimalityTheory.consistentTotalOrders_toRel {n : ℕ} (σ : Ranking 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 n), IsConsistent r σ

Every grammar has a consistent linear extension: Szpilrajn (extend_partialOrder) extends r to a linear order, which is some ranking's induced order (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 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 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 ([MR16]), 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 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 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 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 ([MR16]; [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]; [MR16]).

theorem OptimalityTheory.toERCs_isSimple_or_isTrivial {n : ℕ} (r : Fin n → Fin n → Prop) [DecidableRel r] (α : ERC 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

toERCs r is consistent: any linear extension of r satisfies it.

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 grammar — the simple-ERC Birkhoff antimatroid (Antimat.ofSimple) of its Hasse-edge encoding, whose feasible sets are exactly the order ideals of r (orderIdealAntimatroid_isFeasible_iff).

Equations

• OptimalityTheory.orderIdealAntimatroid r = OptimalityTheory.Antimat.ofSimple (OptimalityTheory.toERCs r) ⋯ ⋯

theorem OptimalityTheory.feasible_toERCs_iff {n : ℕ} (r : Fin n → Fin n → Prop) [DecidableRel r] {S : Finset (Fin n)} : Feasible (toERCs r) S ↔ ∀ (a b : Fin n), r a b → b ∈ S → a ∈ S

Local feasibility against toERCs r is exactly the order-ideal condition — whenever b ∈ S and a dominates b, also a ∈ S.

@[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 — the Birkhoff correspondence, made concrete and decidable.

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) ([MR16]).

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

Probabilistic POC — winProb

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

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

Equations

• OptimalityTheory.active vp i o o' = {c : Fin n | vp i o c ≠ vp i o' c}

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

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

Equations

• OptimalityTheory.favoring vp i o o' = {c : Fin n | vp i o c < vp i o' c}

@[simp]

theorem OptimalityTheory.mem_active {n : ℕ} {Input : Type u_1} {Output : Type u_2} {vp : Input → Output → Fin n → ℕ} {i : Input} {o o' : Output} {c : Fin n} : c ∈ active vp i o o' ↔ vp i o c ≠ vp i o' c

@[simp]

theorem OptimalityTheory.mem_favoring {n : ℕ} {Input : Type u_1} {Output : Type u_2} {vp : Input → Output → Fin n → ℕ} {i : Input} {o o' : Output} {c : Fin n} : c ∈ favoring vp i o o' ↔ vp i o c < vp i o' c

theorem OptimalityTheory.favoring_subset_active {n : ℕ} {Input : Type u_1} {Output : Type u_2} {vp : Input → Output → Fin n → ℕ} {i : Input} {o o' : Output} : favoring vp i o o' ⊆ active vp i o o'

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

theorem OptimalityTheory.picksAt_unique {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {vp : Input → Output → Fin n → ℕ} {σ : Ranking n} {i : Input} {o o' : Output} (h : PicksAt cands vp σ i o) (h' : PicksAt cands vp σ 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} {vp : Input → Output → Fin n → ℕ} {i : Input} (h_ne : (cands i).Nonempty) (h_inj : Set.InjOn (vp i) ↑(cands i)) (σ : Ranking n) : ∃ o ∈ cands i, PicksAt cands vp σ 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] (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (σ : Ranking n) (i : Input) (o : Output) : Decidable (PicksAt cands vp σ i o)

Equations

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

def OptimalityTheory.winProb {n : ℕ} {Input : Type u_1} {Output : Type u_2} [DecidableEq Output] (cands : Input → Finset Output) (vp : Input → Output → Fin n → ℕ) (r : Fin n → Fin n → Prop) [DecidableRel r] (i : Input) (o : Output) : ℚ

The probability that sampling under grammar r selects output o for input i — the fraction of consistent extensions picking o. The denominator is positive (consistentTotalOrders_card_pos), so this is a genuine probability.

Equations

• OptimalityTheory.winProb cands vp r i o = ↑{σ ∈ OptimalityTheory.consistentTotalOrders r | OptimalityTheory.PicksAt cands vp σ i o}.card / ↑(OptimalityTheory.consistentTotalOrders r).card

theorem OptimalityTheory.winProb_toRel {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {vp : Input → Output → Fin n → ℕ} {σ : Ranking n} {i : Input} {o : Output} [DecidableEq Output] : winProb cands vp σ.toRel i o = if PicksAt cands vp σ i o then 1 else 0

For the σ-induced total order, winProb collapses to a point mass — probability 1 if σ picks o and 0 otherwise.

theorem OptimalityTheory.winProb_discrete {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {vp : Input → Output → Fin n → ℕ} {i : Input} {o : Output} [DecidableEq Output] : winProb cands vp (fun (x1 x2 : Fin n) => x1 = x2) i o = ↑{σ : Ranking n | PicksAt cands vp σ i o}.card / ↑Finset.univ.card

Under the discrete grammar, winProb is the fraction of all n! rankings picking o.

winProb is a probability distribution

theorem OptimalityTheory.winProb_nonneg {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {vp : Input → Output → Fin n → ℕ} {r : Fin n → Fin n → Prop} {i : Input} {o : Output} [DecidableEq Output] [DecidableRel r] : 0 ≤ winProb cands vp r i o

theorem OptimalityTheory.winProb_le_one {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {vp : Input → Output → Fin n → ℕ} {r : Fin n → Fin n → Prop} {i : Input} {o : Output} [DecidableEq Output] [IsPartialOrder (Fin n) r] [DecidableRel r] : winProb cands vp r i o ≤ 1

theorem OptimalityTheory.sum_card_filter_picksAt {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {vp : 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 (vp i) ↑(cands i)) : ∑ o ∈ cands i, {σ ∈ consistentTotalOrders r | PicksAt cands vp σ 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 core of sum_winProb_eq_one.

theorem OptimalityTheory.sum_winProb_eq_one {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {vp : Input → Output → Fin n → ℕ} {r : Fin n → Fin n → Prop} {i : Input} [DecidableEq Output] [IsPartialOrder (Fin n) r] [DecidableRel r] (h_ne : (cands i).Nonempty) (h_inj : Set.InjOn (vp i) ↑(cands i)) : ∑ o ∈ cands i, winProb cands vp r i o = 1

Over a candidate set with pairwise-distinct violation profiles the win probabilities sum to 1, for any grammar — every consistent ranking picks exactly one winner.

theorem OptimalityTheory.winProb_binary_add_eq_one {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {vp : Input → Output → Fin n → ℕ} {r : Fin n → Fin n → Prop} {i : Input} [DecidableEq Output] [IsPartialOrder (Fin n) r] [DecidableRel r] {o₁ o₂ : Output} (h_two : cands i = {o₁, o₂}) (h_ne : o₁ ≠ o₂) (h_vp : vp i o₁ ≠ vp i o₂) : winProb cands vp r i o₁ + winProb cands vp r i o₂ = 1

Two distinct candidates with distinct violation profiles split the probability mass.

Bridge — binary PicksAt is decided by the σ-earliest active constraint

For binary candidate sets cands i = {chosen, other}, PicksAt σ i chosen reduces to lex domination of chosen's permuted profile, which is decided at the first position where the profiles differ — i.e., chosen wins iff the σ-earliest constraint of active vp i chosen other lies in favoring vp i chosen other. Combined with the head-fiber counting of Core.Optimization.PermSubsetCombinatorics, this yields closed-form rates for binary POC competitions without enumerating rankings.

theorem OptimalityTheory.picksAt_binary_iff_head_mem_favoring {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {vp : Input → Output → Fin n → ℕ} {i : Input} {chosen other : Output} [DecidableEq Output] (h_two : cands i = {chosen, other}) (h_ne : chosen ≠ other) (σ : Ranking n) : PicksAt cands vp σ i chosen ↔ ∃ x ∈ favoring vp i chosen other, (Core.Optimization.PermSubsetCombinatorics.permDList σ (active vp i chosen other)).head? = some 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.winProb_discrete_binary_rate {n : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {vp : Input → Output → Fin n → ℕ} {i : Input} {chosen other : Output} [DecidableEq Output] (h_two : cands i = {chosen, other}) (h_ne : chosen ≠ other) : winProb cands vp (fun (x1 x2 : Fin n) => x1 = x2) i chosen = ↑(favoring vp i chosen other ∩ active vp i chosen other).card / ↑(active vp i chosen other).card

With binary candidates, the fraction of all n! rankings picking chosen is |favoring ∩ active| / |active| — each ranking is decided by its σ-earliest active constraint, and every active constraint is equally likely to come first.

Deciding-stratum rate for stratified grammars

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

theorem OptimalityTheory.winProb_stratified_binary_rate {n s : ℕ} {Input : Type u_1} {Output : Type u_2} {cands : Input → Finset Output} {vp : 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 → vp i chosen c = vp i other c) (h_dec : {x ∈ active vp i chosen other | stratumOf x = k}.Nonempty) : winProb cands vp (stratified stratumOf inner) i chosen = ↑(favoring vp i chosen other ∩ {x ∈ active vp i chosen other | stratumOf x = k}).card / ↑{x ∈ active vp 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 won by chosen at rate |favoring ∩ Dₖ| / |Dₖ|, where Dₖ is the active set restricted to stratum k. Later strata cannot affect the outcome.