Reduction theorems

This file formalizes the main theorems from the introduction of the paper: Theorem B (thm:starGreedy) characterizes α ⋆ β as a greedy maximum, and Theorem C (thm:reduce) reduces inequalities α ⋆ β ≥ γ to equalities of reduced products.

Bookkeeping helpers

theorem Reduction.star_left_witness (α β : AspPerm) : have α₁ := α ⋆ β * β⁻¹; α₁ * β = α ⋆ β ∧ α₁ ⋆ β = α ⋆ β ∧ α₁ ≤χ α

Multiplying α ⋆ β on the right by β⁻¹ recovers a permutation that lies weakly below α in Bruhat order, has the same shift as α, and whose product with β (ordinary or Demazure) returns α ⋆ β.

theorem Reduction.star_right_witness (α β : AspPerm) : have β₁ := α⁻¹ * (α ⋆ β); α * β₁ = α ⋆ β ∧ α ⋆ β₁ = α ⋆ β ∧ β₁ ≤χ β

Multiplying α ⋆ β on the left by α⁻¹ recovers a permutation that lies weakly below β in Bruhat order, has the same shift as β, and whose product with α (ordinary or Demazure) returns α ⋆ β.

theorem Reduction.mul_le_star_of_le {α₁ α₂ β₁ β₂ : AspPerm} (hα : α₁ ≤ α₂) (hβ : β₁ ≤ β₂) : α₁ * β₁ ≤ α₂ ⋆ β₂

The ordinary product of Bruhat-smaller factors lies below the Demazure product of the original factors. This is the ASP form of the bound used in Equation \eqref{eq:astarbBound}.

Theorem B: greedy characterization of ⋆

theorem Reduction.starGreedy_alpha (α β : AspPerm) : IsGreatest {x : AspPerm | ∃ (α₁ : AspPerm) (_ : α₁ ≤χ α), α₁ * β = x} (α ⋆ β)

Theorem B (thm:starGreedy), equation \eqref{eq:starGreedyAlpha}.

α ⋆ β is the Bruhat-maximum of the set $\{ \alpha_1 \beta : \alpha_1 \leq_\chi \alpha\}$.

theorem Reduction.starGreedy_beta (α β : AspPerm) : IsGreatest {x : AspPerm | ∃ (β₁ : AspPerm) (_ : β₁ ≤χ β), α * β₁ = x} (α ⋆ β)

Theorem B (thm:starGreedy), equation \eqref{eq:starGreedyBeta}.

α ⋆ β is the Bruhat-maximum of the set $\{ \alpha \beta_1 : \beta_1 \leq_\chi \beta\}$.

theorem Reduction.starGreedy (α β : AspPerm) : IsGreatest {x : AspPerm | ∃ (α₁ : AspPerm) (_ : α₁ ≤ α) (β₁ : AspPerm) (_ : β₁ ≤ β), α₁ * β₁ = x} (α ⋆ β)

Theorem B (thm:starGreedy), equation \eqref{eq:starGreedy}.

α ⋆ β is the Bruhat-maximum of the set $\{ \alpha_1 \beta_1 : \alpha_1 \leq \alpha, \beta_1 \leq \beta\}$.

Theorem C: reduction theorem for α ⋆ β ≥ γ

theorem Reduction.reduce_witness (α β γ : AspPerm) (h : α ⋆ β ≥ γ) : have α₁ := γ ◃ β⁻¹; have β₁ := α₁⁻¹ ▹ γ; α₁ * β₁ = γ ∧ α₁ ⋆ β₁ = γ ∧ α₁ ≤ α ∧ β₁ ≤ β

Theorem C (thm:reduce), second paragraph, Bruhat part.

If α ⋆ β ≥ γ, then α₁ = γ ◃ β⁻¹ and β₁ = α₁⁻¹ ▹ γ satisfy α₁ ⋆ β₁ = α₁ * β₁ = γ and α₁ ≤ α, β₁ ≤ β.

theorem Reduction.reduce_witness_chi (α β γ : AspPerm) (hχ : α.χ + β.χ = γ.χ) (h : α ⋆ β ≥ γ) : have α₁ := γ ◃ β⁻¹; have β₁ := α₁⁻¹ ▹ γ; α₁ * β₁ = γ ∧ α₁ ⋆ β₁ = γ ∧ α₁ ≤χ α ∧ β₁ ≤χ β

Theorem C (thm:reduce), second paragraph, including the shift identities. Under the additional hypothesis $\chi_\alpha + \chi_\beta = \chi_\gamma$ (which makes both shift equalities meaningful), we further have $\alpha_1 \leq_\chi \alpha$ and $\beta_1 \leq_\chi \beta$.

theorem Reduction.reduce (α β γ : AspPerm) (hχ : α.χ + β.χ = γ.χ) : α ⋆ β ≥ γ ↔ ∃ (α₁ : AspPerm) (β₁ : AspPerm), α₁ ≤χ α ∧ β₁ ≤χ β ∧ α₁ ⋆ β₁ = γ ∧ α₁ * β₁ = γ

Theorem C (thm:reduce), first paragraph, ASP form.

For all α, β, γ ∈ ASP with α.χ + β.χ = γ.χ, the inequality α ⋆ β ≥ γ is equivalent to the existence of α₁, β₁ with α₁ ≤χ α, β₁ ≤χ β, and α₁ ⋆ β₁ = α₁ * β₁ = γ.

Theorem 6.1 (tllStingy): stingy characterization of ◃

The dual story for ◃, mirroring Theorem B. Equation \eqref{eq:tllGreedyAlpha} in the paper.

theorem Reduction.left_contract_inv_mono_alpha {α α' β : AspPerm} (hα : α ≤ α') : α ◃ β⁻¹ ≤ α' ◃ β⁻¹

The contraction α ◃ β⁻¹ is monotone in α for fixed β.

This is the ASP-level lift of SlipFace.left_contract_mono.

theorem Reduction.left_contract_inv_antimono_beta {α β β' : AspPerm} (hβ : β' ≤ β) : α ◃ β⁻¹ ≤ α ◃ β'⁻¹

The contraction α ◃ β⁻¹ is anti-monotone in β: if β' ≤ β then α ◃ β⁻¹ ≤ α ◃ β'⁻¹.

theorem Reduction.left_contract_inv_le_mul {α α' β β' : AspPerm} (hα : α ≤ α') (hβ : β' ≤ β) : α ◃ β⁻¹ ≤ α' * β'⁻¹

Bounding the two factors puts an ordinary product above a left contraction. This is the ASP form of the bound used in Equation \eqref{eq:atllbBound}.

theorem Reduction.left_contract_stingy_alpha (α β : AspPerm) : IsLeast {x : AspPerm | ∃ (α₁ : AspPerm) (_ : α ≤χ α₁), α₁ * β⁻¹ = x} (α ◃ β⁻¹)

Theorem 6.1 (thm:tllStingy), equation \eqref{eq:tllGreedyAlpha}.

α ◃ β⁻¹ is the Bruhat-minimum of the set $\{\alpha_1 \beta^{-1}: \alpha_1 \geq_\chi \alpha\}$.

theorem Reduction.left_contract_stingy_beta (α β : AspPerm) : IsLeast {x : AspPerm | ∃ (β₁ : AspPerm) (_ : β₁ ≤χ β), α * β₁⁻¹ = x} (α ◃ β⁻¹)

Theorem 6.1 (thm:tllStingy), equation \eqref{eq:tllGreedyBeta}.

α ◃ β⁻¹ is the Bruhat-minimum of the set $\{\alpha \beta_1^{-1}: \beta_1 \leq_\chi \beta\}$.

theorem Reduction.left_contract_stingy (α β : AspPerm) : IsLeast {x : AspPerm | ∃ (α₁ : AspPerm) (_ : α ≤ α₁) (β₁ : AspPerm) (_ : β₁ ≤ β), α₁ * β₁⁻¹ = x} (α ◃ β⁻¹)

Theorem 6.1 (thm:tllStingy), equation \eqref{eq:tllGreedy}.

α ◃ β⁻¹ is the Bruhat-minimum of the set $\{\alpha_1 \beta_1^{-1}: \alpha_1 \geq \alpha,\, \beta_1 \leq \beta\}$.

Theorem 6.5 (reduceSeveral): three- and many-fold reduction

The reduction theorem for products of three or more permutations follows from reduce by induction. The list form below packages that induction.

theorem Reduction.eq_id_of_le_id_chi_zero {γ : AspPerm} (h : γ ≤ AspPerm.id) (hχ : γ.χ = 0) : γ = AspPerm.id

If γ ≤ id and γ has shift zero, then γ = id.

This is the shift-zero special case of the antisymmetry of Bruhat order.

theorem Reduction.reduceList (αs : List AspPerm) (γ : AspPerm) : (List.map AspPerm.χ αs).sum = γ.χ → AspPerm.DProd αs ≥ γ → ∃ (βs : List AspPerm), List.Forall₂ (fun (α β : AspPerm) => β ≤χ α) αs βs ∧ AspPerm.DProd βs = γ ∧ AspPerm.OrdProd βs = γ

Theorem 6.5 (thm:reduceSeveral), ASP-level (list version).

For any list of permutations αs and a target γ ∈ ASP with matching total shift, if the Demazure product over αs is Bruhat-≥ γ, then there exists a list of "reduced witnesses" βs of the same length, with βᵢ ≤χ αᵢ pointwise, whose Demazure product and ordinary product both equal γ.