Submodular Slipfaces and Recovery of ASP Permutations

This section shows that submodular slipfaces are exactly those arising from ASP permutations.

theorem Submodular.unique_a_helper {s : SlipFace} (hsub : s.submodular) (A A' b : ℤ) (hA : ∀ a ≤ A, s.func a b = 0) (hA' : ∀ a ≥ A', s.dual.func (b + 1) a = 0) : A ≤ A' ∧ ∑ a ∈ Finset.Ico A A', s.Δ a b = 1

theorem Submodular.unique_a {s : SlipFace} (hsub : s.submodular) (b : ℤ) : ∃! a : ℤ, (a, b) ∈ s.Γ

theorem Submodular.submodular_dual {s : SlipFace} (hsub : s.submodular) : s.dual.submodular

theorem Submodular.unique_b {s : SlipFace} (hsub : s.submodular) (a : ℤ) : ∃! b : ℤ, (a, b) ∈ s.Γ

noncomputable def Submodular.asp_func {s : SlipFace} (hsub : s.submodular) : ℤ → ℤ

Equations

• Submodular.asp_func hsub b = Exists.choose ⋯

theorem Submodular.asp_func_spec {s : SlipFace} (hsub : s.submodular) (a b : ℤ) : asp_func hsub b = a ↔ (a, b) ∈ s.Γ

theorem Submodular.asp_bijective {s : SlipFace} (hsub : s.submodular) : Function.Bijective (asp_func hsub)

noncomputable def Submodular.asp {s : SlipFace} (hsub : s.submodular) : AspPerm

Equations

• Submodular.asp hsub = { func := fun (b : ℤ) => Exists.choose ⋯, bijective := ⋯, asp := ⋯ }

theorem Submodular.asp_spec (s : SlipFace) (hsub : s.submodular) : (asp hsub).sf = s

theorem Submodular.submodular_iff_asp (s : SlipFace) : s.submodular ↔ ∃ (α : AspPerm), α.sf = s

A slipface is submodular if and only if it is of the form $s_\alpha$ for some ASP permutation α.

This is the paper's identification of $\mathrm{ASP}$ with the submodular slipfaces; in Lean the map $\alpha \mapsto s_\alpha$ is implemented as α ↦ α.sf. Proposition 4.3 (prop:imageASP).

Closure of Submodularity Under Product

This section proves that the slipface product of submodular slipfaces is submodular.

noncomputable def Submodular.AspValley (α β : AspPerm) (a b : ℤ) : Valley

The valley $\ell \mapsto s_\alpha(a,\ell) + s_\beta(\ell,b)$.

Its minimum is $s_{\alpha \star \beta}(a,b)$, and its rightmost minimizer is the paper's $M_{\alpha \star \beta}(a,b)$. In Lean that rightmost minimizer is (AspValley α β a b).M. Definition 4.5 (unlabeled in source).

Equations

• Submodular.AspValley α β a b = { f := fun (l : ℤ) => α.s a l + β.s l b, rises := ⋯ }

theorem Submodular.AspSlipValley (α β : AspPerm) (a b : ℤ) : AspValley α β a b = α.sf.SlipValley β.sf a b

theorem Submodular.AspValley_min_eq_s {α β τ : AspPerm} (dprod : τ.eq_dprod α β) (a b : ℤ) : (AspValley α β a b).min = τ.s a b

If τ = α ⋆ β in the Demazure sense, then the minimum of AspValley α β a b is τ.s a b.

theorem Submodular.sediment (v w : Valley) {A : ℤ} (low : ∀ l ≤ A, w.f l = v.f l + 1) (high : ∀ l > A, w.f l = v.f l) : ((v.M ≤ A → w.min = v.min + 1) ∧ (v.M > A → w.min = v.min)) ∧ v.M ≤ w.M

Compare the minima and rightmost minimizers of two valleys that differ by 1 below a cutoff and agree above it. Lemma 4.6 (lem:fg).

theorem Submodular.AspValley_step_a (α β : AspPerm) (a b : ℤ) : have v := AspValley α β a b; have w := AspValley α β (a + 1) b; (w.min = v.min + if v.M ≤ α⁻¹.func a then 1 else 0) ∧ v.M ≤ w.M

Incrementing the first coordinate changes the valley minimum by 1 exactly when the rightmost minimizer lies at or to the left of α⁻¹ a, and the rightmost minimizer can only move to the right. Lemma 4.7 (lem:Kstara+1), in slightly different phrasing.

theorem Submodular.AspValley_step_b (α β : AspPerm) (a b : ℤ) : have v := AspValley α β a b; have w := AspValley α β a (b + 1); (w.min = v.min - 1 + if v.M ≤ β.func b then 1 else 0) ∧ v.M ≤ w.M

Incrementing the second coordinate changes the valley minimum according to the position of the rightmost minimizer relative to β b, and the rightmost minimizer can only move to the right. Lemma 4.8 (lem:Kstarb+1), in slightly different phrasing.

theorem Submodular.AspValley_noninc (α β : AspPerm) (a b c : ℤ) (b_le_c : b ≤ c) : have v := AspValley α β a b; have w := AspValley α β a c; v.M ≤ w.M

theorem Submodular.submodular_of_basepoint_preserved (s : SlipFace) (a b : ℤ) : s.Δ a b ≥ 0 ↔ s.func (a + 1) b = s.func (a + 1) (b + 1) → s.func a b = s.func a (b + 1)

A local criterion for submodularity: if s (a + 1) b does not drop when b increases, then s a b does not drop either.

theorem Submodular.submodular_of_star {s t : SlipFace} (subS : s.submodular) (subT : t.submodular) : (s ⋆ t).submodular

The product of two submodular slipfaces is submodular. Theorem 4.4 (thm:starExists1), part 1/5.

Closure of Submodularity Under Contraction

This section proves that the slipface contraction operations preserve submodularity.

The paper phrases the argument using the rightmost maximizing witness $M_{\alpha \triangleleft \beta}(a,b)$. That maximum may be $\infty$ when the left contraction value is zero, since the set of maximizing witnesses may be unbounded above. Rather than extending $\mathbb{Z}$ to incluce $\infty$, we instead keep the whole witness set and express cutoff conditions on $M$ by quantifying over witnesses: a bound $M \leq m$ becomes a bound on every witness, while $M > m$ becomes the existence of a witness above $m$.

def Submodular.lc_witness_set (α β : AspPerm) (a b : ℤ) : Set ℤ

The set of witnesses attaining the maximum in $s_\alpha \triangleleft s_\beta(a,b)$.

Equations

• Submodular.lc_witness_set α β a b = {l : ℤ | (α.sf ◃ β.sf).func a b = α.s a l - β⁻¹.s b l}

theorem Submodular.lc_wit_mem_lc_witness_set (α β : AspPerm) (a b : ℤ) : α.sf.lc_wit β.sf a b ∈ lc_witness_set α β a b

theorem Submodular.lc_witness_set_nonempty (α β : AspPerm) (a b : ℤ) : (lc_witness_set α β a b).Nonempty

theorem Submodular.lc_candidate_le (α β : AspPerm) (a b l : ℤ) : α.s a l - β⁻¹.s b l ≤ (α.sf ◃ β.sf).func a b

Every candidate value for left contraction is at most its maximum.

theorem Submodular.lc_a_step_eq_iff_exists_witness (α β : AspPerm) (a b : ℤ) : (α.sf ◃ β.sf).func (a + 1) b = (α.sf ◃ β.sf).func a b ↔ ∃ l ∈ lc_witness_set α β (a + 1) b, α⁻¹.func a < l

Witness-set form of the left-contraction step in the first coordinate: the step is flat exactly when a witness for the new value lies to the right of the cutoff.

theorem Submodular.lc_a_step_one_iff_forall_witness (α β : AspPerm) (a b : ℤ) : (α.sf ◃ β.sf).func (a + 1) b = (α.sf ◃ β.sf).func a b + 1 ↔ ∀ l ∈ lc_witness_set α β (a + 1) b, l ≤ α⁻¹.func a

Witness-set form of the left-contraction step in the first coordinate: the step rises by one exactly when every witness for the new value is at or left of the cutoff.

theorem Submodular.lc_b_step_eq_iff_exists_witness (α β : AspPerm) (a b : ℤ) : (α.sf ◃ β.sf).func a (b + 1) = (α.sf ◃ β.sf).func a b ↔ ∃ l ∈ lc_witness_set α β a b, β.func b < l

Witness-set form of the left-contraction step in the second coordinate: the step is flat exactly when an old witness lies to the right of the cutoff. Here the cutoff is β b, from applying the first-coordinate step formula to the dual slipface $s_{\beta^{-1}}$.

theorem Submodular.lc_b_step_one_iff_forall_witness (α β : AspPerm) (a b : ℤ) : (α.sf ◃ β.sf).func a (b + 1) = (α.sf ◃ β.sf).func a b - 1 ↔ ∀ l ∈ lc_witness_set α β a b, l ≤ β.func b

Witness-set form of the left-contraction step in the second coordinate: the step drops by one exactly when every old witness is at or left of the cutoff.

theorem Submodular.lc_witness_move_a_down (α β : AspPerm) (a b l : ℤ) (hl : l ∈ lc_witness_set α β (a + 1) b) : ∃ l' ∈ lc_witness_set α β a b, l ≤ l'

Moving the first coordinate down transports any witness weakly to the right. This replaces the paper's inequality $M_{\alpha \triangleleft \beta}(a+1,b) \leq M_{\alpha \triangleleft \beta}(a,b)$.

theorem Submodular.lc_witness_move_b_up (α β : AspPerm) (a b l : ℤ) (hl : l ∈ lc_witness_set α β a b) : ∃ l' ∈ lc_witness_set α β a (b + 1), l ≤ l'

Moving the second coordinate up transports any witness weakly to the right. This replaces the paper's inequality $M_{\alpha \triangleleft \beta}(a,b) \leq M_{\alpha \triangleleft \beta}(a,b+1)$.

theorem Submodular.lc_witness_move_a_down_of_le (α β : AspPerm) (a c b l : ℤ) (hac : a ≤ c) (hl : l ∈ lc_witness_set α β c b) : ∃ l' ∈ lc_witness_set α β a b, l ≤ l'

Moving the first coordinate down through several steps transports a witness weakly to the right.

theorem Submodular.lc_witness_move_b_up_of_le (α β : AspPerm) (a b c l : ℤ) (hbc : b ≤ c) (hl : l ∈ lc_witness_set α β a b) : ∃ l' ∈ lc_witness_set α β a c, l ≤ l'

Moving the second coordinate up through several steps transports a witness weakly to the right.

theorem Submodular.submodular_of_left_contract {s t : SlipFace} (subS : s.submodular) (subT : t.submodular) : (s ◃ t).submodular

The left contraction $s \triangleleft t$ of submodular slipfaces is submodular. Theorem 4.10 (thm:tllExists), part 1/8.

theorem Submodular.submodular_of_right_contract {s t : SlipFace} (subS : s.submodular) (subT : t.submodular) : (s ▹ t).submodular

The right contraction $s \triangleright t$ of submodular slipfaces is submodular. Theorem 4.10 (thm:tllExists), part 1/8.

The operations $\star,\; \triangleleft,\; \triangleright$ on AspPerm

Using the slipface construction above, this section defines Demazure product and the two contraction operationson ASP permutations and proves its basic structural properties.

theorem AspPerm.eq_of_sf_eq {α β : AspPerm} (eq_sf : α.sf = β.sf) : α = β

Two ASP permutations are equal if their associated slipfaces are equal.

theorem AspPerm.star_exists (α β : AspPerm) : ∃! τ : AspPerm, τ.sf = α.sf ⋆ β.sf

The slipface product of two ASP permutations is represented by a unique ASP permutation. Theorem 4.4 (thm:starExists1), part 2/5.

theorem AspPerm.lc_exists (α β : AspPerm) : ∃! τ : AspPerm, τ.sf = α.sf ◃ β.sf

The slipface left contraction of two ASP permutations is represented by a unique ASP permutation. Theorem 4.10 (thm:tllExists), part 2/8.

theorem AspPerm.rc_exists (α β : AspPerm) : ∃! τ : AspPerm, τ.sf = α.sf ▹ β.sf

The slipface right contraction of two ASP permutations is represented by a unique ASP permutation. Theorem 4.10 (thm:tllExists), part 2/8.

noncomputable def AspPerm.star (α β : AspPerm) : AspPerm

The Demazure product on ASP permutations, characterized by $$ s_{\alpha \star \beta}(a,b) = \min_{\ell \in \mathbb{Z}} [s_\alpha(a,\ell) + s_\beta(\ell,b)]. $$

In Lean this operation is written α ⋆ β.

Equations

• α ⋆ β = Classical.choose ⋯

@[simp]

theorem AspPerm.star_spec (α β : AspPerm) : (α ⋆ β).sf = α.sf ⋆ β.sf

def AspPerm.«term_⋆_» : Lean.TrailingParserDescr

Equations

• AspPerm.«term_⋆_» = Lean.ParserDescr.trailingNode `AspPerm.«term_⋆_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋆ ") (Lean.ParserDescr.cat `term 71))

noncomputable def AspPerm.left_contract (α β : AspPerm) : AspPerm

Left contraction on ASP permutations, characterized by $s_{\alpha \triangleleft \beta} = s_\alpha \triangleleft s_\beta$.

In Lean this operation is written α ◃ β. Theorem 4.10 (thm:tllExists), part 2/8.

Equations

• α ◃ β = Classical.choose ⋯

@[simp]

theorem AspPerm.left_contract_spec (α β : AspPerm) : (α ◃ β).sf = α.sf ◃ β.sf

Left contraction on ASP permutations has the defining slipface. Theorem 4.10 (thm:tllExists), part 2/8.

def AspPerm.«term_◃_» : Lean.TrailingParserDescr

Equations

• AspPerm.«term_◃_» = Lean.ParserDescr.trailingNode `AspPerm.«term_◃_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◃ ") (Lean.ParserDescr.cat `term 71))

noncomputable def AspPerm.right_contract (α β : AspPerm) : AspPerm

Right contraction on ASP permutations, characterized by $s_{\alpha \triangleright \beta} = s_\alpha \triangleright s_\beta$.

In Lean this operation is written α ▹ β. Theorem 4.10 (thm:tllExists), part 2/8.

Equations

• α ▹ β = Classical.choose ⋯

@[simp]

theorem AspPerm.right_contract_spec (α β : AspPerm) : (α ▹ β).sf = α.sf ▹ β.sf

Right contraction on ASP permutations has the defining slipface. Theorem 4.10 (thm:tllExists), part 2/8.

def AspPerm.«term_▹_» : Lean.TrailingParserDescr

Equations

• AspPerm.«term_▹_» = Lean.ParserDescr.trailingNode `AspPerm.«term_▹_» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ▹ ") (Lean.ParserDescr.cat `term 70))

theorem AspPerm.star_assoc (α β γ : AspPerm) : α ⋆ β ⋆ γ = α ⋆ (β ⋆ γ)

Demazure product on ASP permutations is associative. Theorem 4.4 (thm:starExists1), part 3/5.

theorem AspPerm.left_contract_assoc (α β γ : AspPerm) : α ◃ β ◃ γ = α ◃ (β ⋆ γ)

Left contraction associates with Demazure product on ASP permutations. Theorem 4.10 (thm:tllExists), part 3/8.

theorem AspPerm.right_contract_assoc (α β γ : AspPerm) : α ▹ β ▹ γ = (α ⋆ β) ▹ γ

Right contraction associates with Demazure product on ASP permutations. Theorem 4.10 (thm:tllExists), part 4/8.

theorem AspPerm.inverse_left_contract (α β : AspPerm) : (α ◃ β)⁻¹ = β⁻¹ ▹ α⁻¹

Inversion swaps left contraction for right contraction. Theorem 4.10 (thm:tllExists), part 5/8.

theorem AspPerm.chi_left_contract (α β : AspPerm) : (α ◃ β).χ = α.χ + β.χ

The shift of left contraction is the sum of shifts. Theorem 4.10 (thm:tllExists), part 6/8.

theorem AspPerm.chi_right_contract (α β : AspPerm) : (α ▹ β).χ = α.χ + β.χ

The shift of right contraction is the sum of shifts. Theorem 4.10 (thm:tllExists), part 6/8.

theorem AspPerm.star_valley (α β : AspPerm) (a b : ℤ) : (α ⋆ β).s a b = (Submodular.AspValley α β a b).min

theorem AspPerm.star_sf_isleast (α β : AspPerm) (a b : ℤ) : IsLeast {x : ℤ | ∃ (l : ℤ), α.s a l + β.s l b = x} ((α ⋆ β).s a b)

theorem AspPerm.inverse_star (α β : AspPerm) : (α ⋆ β)⁻¹ = β⁻¹ ⋆ α⁻¹

Inversion reverses Demazure products. Theorem 4.4 (thm:starExists1), part 4/5.

theorem AspPerm.chi_star (α β : AspPerm) : (α ⋆ β).χ = α.χ + β.χ

The shift of a Demazure product satisfies (α ⋆ β).χ = α.χ + β.χ, i.e. $\chi_{\alpha \star \beta} = \chi_\alpha + \chi_\beta$. Theorem 4.4 (thm:starExists1), part 5/5.

@[reducible, inline]

noncomputable abbrev AspPerm.DProd (L : List AspPerm) : AspPerm

Demazure product of a list of ASP permutations.

Equations

• AspPerm.DProd L = List.foldr AspPerm.star AspPerm.id L

@[reducible, inline]

noncomputable abbrev AspPerm.OrdProd (L : List AspPerm) : AspPerm

Ordinary product of a list of ASP permutations.

Equations

• AspPerm.OrdProd L = List.foldr (fun (x1 x2 : AspPerm) => x1 * x2) AspPerm.id L

@[simp]

theorem AspPerm.DProd_nil : DProd [] = id

@[simp]

theorem AspPerm.DProd_cons (α : AspPerm) (L : List AspPerm) : DProd (α :: L) = α ⋆ DProd L

@[simp]

theorem AspPerm.OrdProd_nil : OrdProd [] = id

@[simp]

theorem AspPerm.OrdProd_cons (α : AspPerm) (L : List AspPerm) : OrdProd (α :: L) = α * OrdProd L

theorem AspPerm.chi_DProd (L : List AspPerm) : (DProd L).χ = (List.map χ L).sum

The shift of a Demazure list product is the sum of the shifts.

theorem AspPerm.chi_OrdProd (L : List AspPerm) : (OrdProd L).χ = (List.map χ L).sum

The shift of an ordinary list product is the sum of the shifts.

theorem AspPerm.id_s_eq (a b : ℤ) : id.s a b = max (a - b) 0

theorem AspPerm.id_sf : id.sf = SlipFace.id

theorem AspPerm.id_star (α : AspPerm) : id ⋆ α = α

theorem AspPerm.star_id (α : AspPerm) : α ⋆ id = α

instance AspPerm.instPartialOrder : PartialOrder AspPerm

Equations

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

def AspPerm.le_chi (σ τ : AspPerm) : Prop

The paper's relation $\alpha \leq_\chi \beta$: Bruhat order together with equality of shifts. In Lean this is the infix ≤χ.

Equations

• (σ ≤χ τ) = (σ ≤ τ ∧ σ.χ = τ.χ)

def AspPerm.«term_≤χ_» : Lean.TrailingParserDescr

Equations

• AspPerm.«term_≤χ_» = Lean.ParserDescr.trailingNode `AspPerm.«term_≤χ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤χ ") (Lean.ParserDescr.cat `term 51))

theorem AspPerm.sf_le_iff (α β : AspPerm) : α.sf ≤ β.sf ↔ α ≤ β

Bruhat order on ASP permutations agrees with pointwise order on their slipfaces.

theorem AspPerm.le_chi_inv_iff (α β : AspPerm) : α ≤χ β ↔ α⁻¹ ≤χ β⁻¹

Inversion preserves Bruhat comparisons between ASP permutations of the same shift. Lemma 2.4 (lem:bruhatInverse).

theorem AspPerm.id_le_of_chi_nonneg {τ : AspPerm} (hχ : 0 ≤ τ.χ) : id ≤ τ

An ASP permutation of nonnegative shift lies above the identity in Bruhat order. This is the $\chi = 0$ case of the paper's minimum-shift observation after Definition 2.5.

theorem AspPerm.star_mono {α₁ α₂ β₁ β₂ : AspPerm} (hα : α₁ ≤ α₂) (hβ : β₁ ≤ β₂) : α₁ ⋆ β₁ ≤ α₂ ⋆ β₂

Demazure product on ASP permutations is Bruhat-increasing in both arguments. This lifts the slipface comparison of Lemma 3.8.

theorem AspPerm.ge_star_iff_ge_left_contract (α β τ : AspPerm) : α ≥ τ ◃ β⁻¹ ↔ α ⋆ β ≥ τ

The left contraction $\tau \triangleleft \beta^{-1}$ is the Bruhat minimum of the ASP permutations $\alpha$ such that $\alpha \star \beta \geq \tau$. Theorem 4.10 (thm:tllExists), part 7/8.

theorem AspPerm.ge_star_iff_ge_right_contract (α β τ : AspPerm) : β ≥ α⁻¹ ▹ τ ↔ α ⋆ β ≥ τ

The right contraction $\alpha^{-1} \triangleright \tau$ is the Bruhat minimum of the ASP permutations $\beta$ such that $\alpha \star \beta \geq \tau$. Theorem 4.10 (thm:tllExists), part 8/8.

theorem AspPerm.le_star_iff (τ α β : AspPerm) : τ ≤ α ⋆ β ↔ τ.le_dprod α β

Comparison τ ≤ α ⋆ β is equivalent to the lower Demazure-product inequalities defining τ.le_dprod α β.

theorem AspPerm.ge_star_iff (τ α β : AspPerm) : α ⋆ β ≤ τ ↔ τ.ge_dprod α β

Comparison α ⋆ β ≤ τ is equivalent to the upper Demazure-product inequalities defining τ.ge_dprod α β.

theorem AspPerm.eq_star_iff {τ α β : AspPerm} : τ = α ⋆ β ↔ τ.eq_dprod α β

Equality τ = α ⋆ β is equivalent to satisfying both Demazure comparison conditions.

Weak-Order Consequences of Demazure Product

The final results in this file record the weak-order inequalities satisfied by the factors of a Demazure product.

theorem Submodular.lel_of_dprod (α β : AspPerm) : β ≤L α ⋆ β

In a Demazure product α ⋆ β, the factor β lies below the product in left weak order. Lemma 4.9 (lem:invStar), part 1.

theorem Submodular.ler_of_dprod (α β : AspPerm) : α ≤R α ⋆ β

In a Demazure product α ⋆ β, the factor α lies below the product in right weak order. Lemma 4.9 (lem:invStar), part 2.

Weak-Order Consequences of Contraction

theorem Submodular.reducedProduct_of_left_contract (α β : AspPerm) : (α ◃ β).ReducedProduct β⁻¹

Left contraction forms a reduced product with the inverse of its right factor. Lemma 4.14 (lem:invTri), part 1/2.

theorem Submodular.ler_of_left_contract (α β : AspPerm) : α ◃ β ≤R α

Left contraction is below its left factor in right weak order. Lemma 4.14 (lem:invTri), part 2/2.

theorem Submodular.reducedProduct_of_right_contract (α β : AspPerm) : α⁻¹.ReducedProduct (α ▹ β)

Right contraction forms a reduced product with the inverse of its left factor. Corollary 4.15 (cor:reducedTlr), part 1/2.

theorem Submodular.lel_of_right_contract (α β : AspPerm) : α ▹ β ≤L β

Right contraction is below its right factor in left weak order. Corollary 4.15 (cor:reducedTlr), part 2/2.