OT — the ERC–Antimatroid isomorphism

[MR16] prove that consistent ERC sets over n constraints are isomorphic to antimatroids on Fin n. This file builds that correspondence on top of the framework-agnostic antimatroid theory in Linglib.Core.Combinatorics.Antimatroid (SetSystem, Antimatroid, Antimatroid.free/trace/RootedCircuit). The two maps Antimat (ERCs → antimatroids) and RCErc (antimatroids → ERCs) are mutually inverse homomorphisms preserving entailment/containment, so any antimatroid result transfers to OT.

ERC → Antimatroid pipeline

• MChain — maps a consistent ERC set to its feasible sets (Definition 1)
• Antimat — maps a consistent ERC set to an antimatroid (Definition 6)
• RCErc — maps an antimatroid to an ERC set (Definition 10)

Decidable feasibility and the simple-ERC fragment

• Feasible — the decidable, Finset-valued local feasibility condition; a sound over-approximation of the antimatroid family
• FeasiblePrefix — the faithful, also-decidable family (MChain over Finset)
• feasible_not_accessible — for general (disjunctive) ERCs Feasible strictly over-approximates and is not even accessible
• feasible_iff_feasiblePrefix_of_simple — on the simple-ERC fragment the two coincide (Birkhoff order-ideal ↔ linear-extension-prefix correspondence)
• Antimat.ofSimple — the resulting decidable antimatroid on a simple ERC set

Lemmas and theorems

• maximalChain_dominance — prefix sets are downward-closed under dominance
• MChain.union_closed — Lemma 3: MChain is union-closed
• Antimat_entailment — Theorem 3: entailment → containment (proved)
• RCErc_single_eq_simpleERC — two-element rooted circuits are simple ERCs (proved)
• Antimat_RCErc_inv — Theorem 1: Antimat ∘ RCErc = id (stated; proof sorry)
• RCErc_Antimat_inv — Theorem 2: RCErc ∘ Antimat = id up to entailment (stated; proof sorry)
• RCErc_entailment — Theorem 4: containment → entailment (stated; proof sorry)

The three sorrys are the general antimatroid → ERC direction, which rests on [Die87]'s rooted-circuit characterization of feasible sets.

References

[Die87] — A circuit set characterization of antimatroids [MR16] — OT grammars, beyond partial orders: ERC sets and antimatroids

def OptimalityTheory.maximalChain {n : ℕ} (r : Ranking n) : Fin (n + 1) → Set (Fin n)

A maximal chain in the power set lattice on n elements is a sequence of sets ∅ = S₀ ⊂ S₁ ⊂ ... ⊂ Sₙ = Fin n where each set differs from the previous by exactly one element.

Each maximal chain corresponds to a total order (ranking) on Fin n: the element added at step k is the constraint ranked at position k.

Equations

• OptimalityTheory.maximalChain r k = {i : Fin n | ↑((Equiv.symm r) i) < ↑k}

theorem OptimalityTheory.maximalChain_zero {n : ℕ} (r : Ranking n) : maximalChain r ⟨0, ⋯⟩ = ∅

The maximal chain starts at the empty set.

theorem OptimalityTheory.maximalChain_last {n : ℕ} (r : Ranking n) : maximalChain r ⟨n, ⋯⟩ = Set.univ

The maximal chain ends at the full set.

def OptimalityTheory.MChain {n : ℕ} (E : List (ERC n)) : Set (Fin n) → Prop

MChain E is the collection of subsets of Fin n that appear in some maximal chain consistent with ERC set E.

A set S is in MChain(E) iff there exists a ranking r that satisfies all ERCs in E and a position k such that S is the set of the top-k constraints under r.

[MR16] Definition 1.

Equations

• OptimalityTheory.MChain E S = ∃ (r : OptimalityTheory.Ranking n), OptimalityTheory.ERCSet.SatisfiedBy r E ∧ ∃ (k : Fin (n + 1)), OptimalityTheory.maximalChain r k = S

Local feasibility — a decidable sound over-approximation

def OptimalityTheory.Feasible {n : ℕ} (E : List (ERC n)) (S : Finset (Fin n)) : Prop

Local feasibility of a candidate prefix S against ERC set E: for every ERC, if S contains one of its losers then it contains one of its winners (one rooted circuit per loser). Decidable and decide-reducing.

Feasible is a necessary condition for antimatroid feasibility — implied by FeasiblePrefix/MChain (feasible_of_satisfiedBy) — but strictly weaker for disjunctive (multi-W) ERCs: two ERCs can mutually cover each other's losers inside S with no consistent global order realizing it (feasible_not_accessible). It is exact only on the simple-ERC fragment (each ERC one W/one L = a Hasse edge = a partial order, feasible_iff_feasiblePrefix_of_simple). The faithful, also decidable notion is FeasiblePrefix.

Equations

• OptimalityTheory.Feasible E S = ∀ α ∈ E, (∃ (l : Fin n), α l = OptimalityTheory.ERCVal.L ∧ l ∈ S) → ∃ (w : Fin n), α w = OptimalityTheory.ERCVal.W ∧ w ∈ S

@[implicit_reducible]

instance OptimalityTheory.instDecidablePredFinsetFinFeasible {n : ℕ} (E : List (ERC n)) : DecidablePred (Feasible E)

Equations

• OptimalityTheory.instDecidablePredFinsetFinFeasible E S = id inferInstance

@[simp]

theorem OptimalityTheory.Feasible.empty {n : ℕ} (E : List (ERC n)) : Feasible E ∅

The empty prefix is locally feasible (no losers present).

theorem OptimalityTheory.Feasible.union_closed {n : ℕ} (E : List (ERC n)) {S T : Finset (Fin n)} (hS : Feasible E S) (hT : Feasible E T) : Feasible E (S ∪ T)

Local feasibility is union-closed (a one-liner): a loser in S ∪ T lies in one of them, whose winner then lies in S ∪ T. (This is union-closure of the over-approximation; the faithful family's union-closure is MChain.union_closed, [MR16] Lemma 3.)

def OptimalityTheory.prefixFinset {n : ℕ} (r : Ranking n) (k : Fin (n + 1)) : Finset (Fin n)

The top-k constraints under ranking r, as a Finset (the decidable counterpart of maximalChain r k).

Equations

• OptimalityTheory.prefixFinset r k = {i : Fin n | ↑((Equiv.symm r) i) < ↑k}

@[simp]

theorem OptimalityTheory.mem_prefixFinset {n : ℕ} (r : Ranking n) (k : Fin (n + 1)) (i : Fin n) : i ∈ prefixFinset r k ↔ ↑((Equiv.symm r) i) < ↑k

theorem OptimalityTheory.feasible_of_satisfiedBy {n : ℕ} {E : List (ERC n)} {r : Ranking n} (hr : ERCSet.SatisfiedBy r E) (k : Fin (n + 1)) : Feasible E (prefixFinset r k)

Forward representation (the easy half of [MR16]'s isomorphism): a prefix of a ranking that satisfies E is locally feasible. Winners dominate their losers, so a loser inside the prefix drags its winner in (maximalChain_dominance in Finset form).

FeasiblePrefix — the faithful, decidable antimatroid feasibility

def OptimalityTheory.FeasiblePrefix {n : ℕ} (E : List (ERC n)) (S : Finset (Fin n)) : Prop

Faithful feasibility: S is the top-k constraints of some ranking satisfying E — the Finset-valued form of MChain. Decidable by finite search over Ranking n (a Fintype) and Fin (n+1), so decide reduces — and unlike Feasible it is the genuine antimatroid family, not an over-approximation.

Equations

• OptimalityTheory.FeasiblePrefix E S = ∃ (r : OptimalityTheory.Ranking n), OptimalityTheory.ERCSet.SatisfiedBy r E ∧ ∃ (k : Fin (n + 1)), OptimalityTheory.prefixFinset r k = S

@[implicit_reducible]

instance OptimalityTheory.instDecidablePredFinsetFinFeasiblePrefix {n : ℕ} (E : List (ERC n)) : DecidablePred (FeasiblePrefix E)

Equations

• OptimalityTheory.instDecidablePredFinsetFinFeasiblePrefix E x✝ = Fintype.decidableExistsFintype

theorem OptimalityTheory.feasible_of_feasiblePrefix {n : ℕ} {E : List (ERC n)} {S : Finset (Fin n)} (h : FeasiblePrefix E S) : Feasible E S

The faithful predicate implies the over-approximation (feasible_of_satisfiedBy).

@[simp]

theorem OptimalityTheory.prefixFinset_coe {n : ℕ} (r : Ranking n) (k : Fin (n + 1)) : ↑(prefixFinset r k) = maximalChain r k

prefixFinset coerces to maximalChain.

theorem OptimalityTheory.mChain_coe_iff_feasiblePrefix {n : ℕ} (E : List (ERC n)) (S : Finset (Fin n)) : MChain E ↑S ↔ FeasiblePrefix E S

FeasiblePrefix is MChain over Finset — the decidable counterpart of the existential, Set-valued antimatroid family.

theorem OptimalityTheory.feasible_not_accessible : ∃ (E : List (ERC 4)) (S : Finset (Fin 4)), ERCSet.Consistent E ∧ Feasible E S ∧ ¬FeasiblePrefix E S ∧ S.Nonempty ∧ ¬∃ x ∈ S, Feasible E (S \ {x})

Feasible strictly over-approximates the antimatroid family. Two disjunctive (multi-W) ERCs over Fin 4 admit a locally-feasible {0,1} that is not a prefix of any consistent ranking (¬ FeasiblePrefix) and has no removable element — so {S | Feasible E S} is not accessible and cannot be an antimatroid for general ERC sets. Hence Antimat.IsFeasible stays MChain ([MR16]'s "beyond partial orders"); the local form is exact only on the simple-ERC fragment.

theorem OptimalityTheory.maximalChain_dominance {n : ℕ} (r : Ranking n) (k : Fin (n + 1)) (w l : Fin n) (hw : r.Dominates w l) (hl : l ∈ maximalChain r k) : w ∈ maximalChain r k

Prefix sets are downward-closed under dominance: if w dominates l under ranking r and l is in the prefix set at position k, then w is too (since r.symm w < r.symm l < k).

This is the key insight enabling the direct construction proof of union closure: any W-witness for an L-constraint in a prefix set must itself be in that prefix set.

theorem OptimalityTheory.MChain.union_closed {n : ℕ} (E : List (ERC n)) (_hcons : ERCSet.Consistent E) (S T : Set (Fin n)) (_hS : MChain E S) (_hT : MChain E T) : MChain E (S ∪ T)

MChain is closed under union.

Given S = maximalChain r₁ k₁ and T = maximalChain r₂ k₂ with both r₁, r₂ satisfying E, construct r₃ whose prefix set at position k₁ + |T \ S| equals S ∪ T.

Construction: r₃ orders elements in three blocks:

1. Elements of S, in r₁'s order
2. Elements of T \ S, in r₂'s order
3. Remaining elements, in r₁'s order

The position function f i assigns each element its rank in r₃:

• For i ∈ S: f i = r₁.symm i (positions 0 to k₁ - 1)
• For i ∈ T \ S: f i = k₁ + countBelow r₂ (T\S) i
• For i ∉ S ∪ T: f i = k₁ + |T\S| + countBelow r₁ rest i

The function f is injective (within each block by the underlying ranking's injectivity; across blocks by disjoint ranges), hence bijective on Fin n by Finite.injective_iff_bijective. The merged ranking r₃ is (Equiv.ofBijective f).symm.

ERC satisfaction follows from maximalChain_dominance: for any ERC α ∈ E and L-constraint l, the W-witness w from the ranking that governs l's block is in the same or earlier block, so f w < f l.

[MR16] Lemma 3.

def OptimalityTheory.Antimat {n : ℕ} (E : List (ERC n)) (hcons : ERCSet.Consistent E) : Antimatroid (Fin n)

Antimat E maps a consistent ERC set E to an antimatroid on Fin n. The ground set is Fin n (the constraint indices), and the feasible sets are MChain(E) — the subsets that appear in maximal chains consistent with E.

[MR16] Definition 6, Lemma 4.

Equations

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

Simple-ERC feasibility coincides with the antimatroid family

When every ERC is simple (one W, one L — a Hasse edge w ≫ l), the constraints carry a genuine partial order and the decidable local condition Feasible is exact: it agrees with the faithful FeasiblePrefix/MChain family. This is the Birkhoff correspondence between order ideals of a poset and the prefixes of its linear extensions ([MR16]). For non-simple E the agreement fails (feasible_not_accessible).

theorem OptimalityTheory.feasible_iff_feasiblePrefix_of_simple {n : ℕ} {E : List (ERC n)} (hcons : ERCSet.Consistent E) (hsimple : ERCSet.IsSimpleSet E) (S : Finset (Fin n)) : Feasible E S ↔ FeasiblePrefix E S

Birkhoff representation on the simple-ERC fragment. With every ERC simple, local feasibility coincides with the genuine antimatroid family: a set is locally feasible iff it is a prefix of some consistent ranking. The forward direction is the order-ideal ↔ linear-extension-prefix correspondence — reorder a witnessing ranking r₀ into the block S (in r₀'s order) followed by Sᶜ (in r₀'s order); winner-uniqueness makes every Hasse edge respected, so the result satisfies E and has S as its length-|S| prefix.

theorem OptimalityTheory.feasible_coe_iff_mChain {n : ℕ} {E : List (ERC n)} (hcons : ERCSet.Consistent E) (hsimple : ERCSet.IsSimpleSet E) (T : Set (Fin n)) : (∃ (S' : Finset (Fin n)), ↑S' = T ∧ Feasible E S') ↔ MChain E T

The Set-level feasible family of the simple fragment: a set is the coercion of a locally-feasible Finset iff it is MChain-feasible. (Bridges the decidable Finset side to Antimat's Set-valued MChain family.)

def OptimalityTheory.Antimat.ofSimple {n : ℕ} (E : List (ERC n)) (hcons : ERCSet.Consistent E) (hsimple : ERCSet.IsSimpleSet E) : Antimatroid (Fin n)

The simple-ERC Birkhoff antimatroid. A consistent set of simple ERCs yields an antimatroid on Fin n whose feasible sets are the locally feasible Finsets — the decidable form. On the simple fragment this family equals Antimat E's MChain family (feasible_coe_iff_mChain), so accessibility and union closure transfer from Antimat; concrete membership is checked by decide via ofSimple_isFeasible_coe. This is the order-ideal antimatroid of the constraint partial order ([MR16]).

Equations

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

@[simp]

theorem OptimalityTheory.ofSimple_isFeasible_coe {n : ℕ} {E : List (ERC n)} (hcons : ERCSet.Consistent E) (hsimple : ERCSet.IsSimpleSet E) (S : Finset (Fin n)) : (Antimat.ofSimple E hcons hsimple).IsFeasible ↑S ↔ Feasible E S

Concrete feasibility of Antimat.ofSimple is the decidable Feasible — the hook that lets decide settle membership queries.

noncomputable def OptimalityTheory.RCErc_single {n : ℕ} (A : Antimatroid (Fin n)) (rc : A.RootedCircuit) : ERC n

RCErc maps a rooted circuit of an antimatroid to an ERC.

Given a rooted circuit F : S(r) with root r and carrier S:

• W(α) = S \ {r} (constraints that must dominate r)
• L(α) = {r} (the root)
• e(α) = G \ S (constraints not in the carrier)

[MR16] Definition 10.

Equations

• OptimalityTheory.RCErc_single A rc k = if k ∈ rc.carrier ∧ k ≠ rc.root then OptimalityTheory.ERCVal.W else if k = rc.root then OptimalityTheory.ERCVal.L else OptimalityTheory.ERCVal.e

noncomputable def OptimalityTheory.RCErc {n : ℕ} (A : Antimatroid (Fin n)) : Set (ERC n)

RCErc A is the ERC set of antimatroid A: the image of A's rooted circuits under RCErc_single. This is the inverse of Antimat ([MR16] Theorems 1–2).

Represented as a Set (ERC n); a ranking r satisfies RCErc A when ∀ α ∈ RCErc A, ERC.SatisfiedBy r α — the Set analogue of ERCSet.SatisfiedBy, used to state the isomorphism theorems below.

Equations

• OptimalityTheory.RCErc A = Set.range (OptimalityTheory.RCErc_single A)

theorem OptimalityTheory.RCErc_single_eq_simpleERC {n : ℕ} (A : Antimatroid (Fin n)) (rc : A.RootedCircuit) {w l : Fin n} (hcarrier : rc.carrier = {w, l}) (hroot : rc.root = l) (hwl : w ≠ l) : RCErc_single A rc = simpleERC w l

Two-element rooted circuits are simple ERCs. A rooted circuit with a two-element carrier {w, l} rooted at l maps under RCErc_single to the simple ERC simpleERC w l (the Hasse edge w ≫ l). Larger carriers instead give a disjunctive, multi-W ERC — one L (the root) requiring some element of S \ {root} to dominate it — which is exactly the "beyond partial orders" content that makes the local Feasible predicate inexact (feasible_not_accessible).

theorem OptimalityTheory.Antimat_RCErc_inv {n : ℕ} (A : Antimatroid (Fin n)) (S : Set (Fin n)) : A.IsFeasible S ↔ ∃ (r : Ranking n), (∀ α ∈ RCErc A, ERC.SatisfiedBy r α) ∧ ∃ (k : Fin (n + 1)), maximalChain r k = S

Theorem 1 ([MR16]): Antimat is a left inverse of RCErc. For any antimatroid A, rebuilding from A's rooted-circuit ERCs recovers A — stated at the feasible-set level (Antimat (RCErc A) and A have the same feasible sets), since Antimat's feasible sets are by definition the maximal chains satisfying the ERC set.

The general proof rests on the rooted-circuit characterization of an antimatroid's feasible sets ([Die87]; [MR16] Lemmas 7, 9), which is why this direction carries an honest sorry.

theorem OptimalityTheory.RCErc_Antimat_inv {n : ℕ} (E : List (ERC n)) (hcons : ERCSet.Consistent E) (r : Ranking n) : (∀ α ∈ RCErc (Antimat E hcons), ERC.SatisfiedBy r α) ↔ ERCSet.SatisfiedBy r E

Theorem 2 ([MR16]): RCErc is a left inverse of Antimat up to entailment. For a consistent ERC set E, the rooted-circuit ERCs of Antimat E pick out exactly E's satisfying rankings — they are logically equivalent to E, not literally equal.

Literal set equality (RCErc (Antimat E) = {α | α ∈ E}) is false by transitive-reduction ambiguity: RCErc (Antimat [a≫b, b≫c]) also contains the implied edge a≫c (a rooted circuit of the chain antimatroid), a strict superset of the two-edge input — yet both pick out the single order a≫b≫c. Hence the statement is mutual entailment (same satisfying rankings), the form [MR16] actually proves. The general proof rests on [Die87]'s rooted-circuit characterization (via Lemmas 7, 9), so it carries an honest sorry.

theorem OptimalityTheory.Antimat_entailment {n : ℕ} (E F : List (ERC n)) (hE : ERCSet.Consistent E) (hF : ERCSet.Consistent F) (h : ERCSet.Entails E F) (S : Set (Fin n)) : (Antimat E hE).IsFeasible S → (Antimat F hF).IsFeasible S

Theorem 3 ([MR16]): Antimat preserves entailment.

If ERC set E entails F (every ranking satisfying E also satisfies F), then Antimat(E) ⊆ Antimat(F) (every feasible set of Antimat(E) is also feasible in Antimat(F)).

theorem OptimalityTheory.RCErc_entailment {n : ℕ} (A B : Antimatroid (Fin n)) (h : ∀ (S : Set (Fin n)), A.IsFeasible S → B.IsFeasible S) (r : Ranking n) : (∀ α ∈ RCErc A, ERC.SatisfiedBy r α) → ∀ α ∈ RCErc B, ERC.SatisfiedBy r α

Theorem 4 ([MR16]): RCErc preserves containment.

If antimatroid A ⊆ B (every feasible set of A is feasible in B), then RCErc(A) entails RCErc(B).

Rankings as maximal chains

A ranking is the same data as a maximal chain in the boolean lattice 2^(Fin n): its sequence of prefixes ∅ ⊂ … ⊂ univ, each step adding the next-ranked constraint. The design deliberately keeps this order-theoretic content outside the type of Ranking (which stays a permutation, [MR16]): rankingChainEquiv records the bijection without retyping rankings as chains.

theorem OptimalityTheory.prefixFinset_zero {n : ℕ} (r : Ranking n) : prefixFinset r 0 = ∅

The prefix ∅ at height 0.

theorem OptimalityTheory.prefixFinset_succ_eq {n : ℕ} (r : Ranking n) (k : Fin n) : prefixFinset r k.succ = insert (r k) (prefixFinset r k.castSucc)

The constraint at rank position k is the new element added passing from the height-k prefix to the height-k+1 prefix.

theorem OptimalityTheory.prefixFinset_apply_notMem {n : ℕ} (r : Ranking n) (k : Fin n) : r k ∉ prefixFinset r k.castSucc

structure OptimalityTheory.MaximalChain (n : ℕ) : Type

A maximal chain in the boolean lattice 2^(Fin n): an ascending family of finsets from ∅, each step adding exactly one new element (so it reaches univ at the top, toFun_last).

• toFun : Fin (n + 1) → Finset (Fin n)

  The chain, indexed by height 0 … n.

• bot : self.toFun 0 = ∅

  The chain starts at the empty set.

• step (k : Fin n) : ∃ x ∉ self.toFun k.castSucc, self.toFun k.succ = insert x (self.toFun k.castSucc)

  Each step adds exactly one new element.

theorem OptimalityTheory.MaximalChain.ext_iff {n : ℕ} {x y : MaximalChain n} : x = y ↔ x.toFun = y.toFun

theorem OptimalityTheory.MaximalChain.ext {n : ℕ} {x y : MaximalChain n} (toFun : x.toFun = y.toFun) : x = y

noncomputable def OptimalityTheory.MaximalChain.added {n : ℕ} (C : MaximalChain n) (k : Fin n) : Fin n

The unique element added at step k.

Equations

• C.added k = Classical.choose ⋯

theorem OptimalityTheory.MaximalChain.added_notMem {n : ℕ} (C : MaximalChain n) (k : Fin n) : C.added k ∉ C.toFun k.castSucc

theorem OptimalityTheory.MaximalChain.toFun_succ {n : ℕ} (C : MaximalChain n) (k : Fin n) : C.toFun k.succ = insert (C.added k) (C.toFun k.castSucc)

theorem OptimalityTheory.MaximalChain.mem_toFun_iff {n : ℕ} (C : MaximalChain n) (k : Fin (n + 1)) (i : Fin n) : i ∈ C.toFun k ↔ ∃ (j : Fin n), ↑j < ↑k ∧ C.added j = i

A constraint is in the height-k prefix iff it was added at some earlier step.

theorem OptimalityTheory.MaximalChain.added_injective {n : ℕ} (C : MaximalChain n) : Function.Injective C.added

theorem OptimalityTheory.MaximalChain.added_bijective {n : ℕ} (C : MaximalChain n) : Function.Bijective C.added

theorem OptimalityTheory.MaximalChain.toFun_last {n : ℕ} (C : MaximalChain n) : C.toFun (Fin.last n) = Finset.univ

A maximal chain reaches the full ground set at its top.

noncomputable def OptimalityTheory.MaximalChain.toRanking {n : ℕ} (C : MaximalChain n) : Ranking n

The ranking recovered from a maximal chain: position k holds the element added at step k.

Equations

• C.toRanking = Equiv.ofBijective C.added ⋯

theorem OptimalityTheory.MaximalChain.toRanking_apply {n : ℕ} (C : MaximalChain n) (k : Fin n) : C.toRanking k = C.added k

theorem OptimalityTheory.MaximalChain.added_toRanking_symm {n : ℕ} (C : MaximalChain n) (i : Fin n) : C.added ((Equiv.symm C.toRanking) i) = i

theorem OptimalityTheory.MaximalChain.prefixFinset_toRanking {n : ℕ} (C : MaximalChain n) (k : Fin (n + 1)) : prefixFinset C.toRanking k = C.toFun k

The prefixes of the recovered ranking are the original chain.

def OptimalityTheory.prefixChain {n : ℕ} (r : Ranking n) : MaximalChain n

The maximal chain of a ranking: its sequence of prefixes.

Equations

• OptimalityTheory.prefixChain r = { toFun := OptimalityTheory.prefixFinset r, bot := ⋯, step := ⋯ }

noncomputable def OptimalityTheory.rankingChainEquiv (n : ℕ) : Ranking n ≃ MaximalChain n

Rankings are maximal chains ([MR16]). A ranking and the maximal chain of its prefixes carry the same information — the "ranking is a chain" intuition, as a bijection rather than a retyping of Ranking.

Equations

• OptimalityTheory.rankingChainEquiv n = { toFun := OptimalityTheory.prefixChain, invFun := OptimalityTheory.MaximalChain.toRanking, left_inv := ⋯, right_inv := ⋯ }