def is_321a (τ : ℤ → ℤ) : Prop

The 321-avoidance condition used in this file: every triple i < j < k has either τ i < τ j or τ j < τ k.

Equations

• is_321a τ = ∀ (i j k : ℤ), i < j → j < k → τ i < τ j ∨ τ j < τ k

structure ASP321a.set_321a_prop (I : Set (ℤ × ℤ)) : Prop

The abstract version of 321-avoidance for an ASP set: ASP-set axioms together with triangle-freeness.

• asp : AspSet_prop I
• tfree (u v w : ℤ) : (u, v) ∉ I ∨ (v, w) ∉ I

structure ASP321a.tfasextends AspSet : Type

A triangle-free ASP set.

• I : Set (ℤ × ℤ)
• prop : AspSet_prop self.I
• prop_321a : set_321a_prop self.I

theorem ASP321a.is_asp_of_is_321a (τ : ℤ → ℤ) (h_bij : Function.Bijective τ) (h_321a : is_321a τ) : is_asp τ

theorem ASP321a.tfree_of_is_321a (τ : ℤ → ℤ) (h_321a : is_321a τ) (u v w : ℤ) : (u, v) ∉ inv_set τ ∨ (v, w) ∉ inv_set τ

theorem ASP321a.is_321a_iff_set_321a_prop (τ : ℤ → ℤ) (hperm : Function.Bijective τ) : is_321a τ ↔ set_321a_prop (inv_set τ)

A bijection of ℤ is 321-avoiding exactly when its inversion set is a triangle-free ASP set.

def ASP321a.tfas_of_perm {τ : AspPerm} (h_321a : is_321a τ.func) : tfas

Equations

• ASP321a.tfas_of_perm h_321a = { toAspSet := AspSet.of_AspPerm τ, prop_321a := ⋯ }

noncomputable def ASP321a.Perm321a_equiv_BijectiveFunc321a : ↑{τ : AspPerm | is_321a τ.func} ≃ { τ : ℤ → ℤ // Function.Bijective τ ∧ is_321a τ }

Equations

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

noncomputable def ASP321a.Perm321a_equiv_Tfas : ↑{τ : AspPerm | is_321a τ.func} ≃ tfas × ℤ

321-avoiding ASP permutations are equivalent to triangle-free ASP sets together with a shift parameter.

Equations

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

theorem ASP321a.inv_321a_char (I : Set (ℤ × ℤ)) : set_321a_prop I ↔ ∃ (τ : ℤ → ℤ), is_321a τ ∧ Function.Bijective τ ∧ inv_set τ = I

Characterize the sets of boxes that arise as inversion sets of 321-avoiding ASP permutations.

def ASP321a.is_src (τ : AspPerm) (u : ℤ) : Prop

Equations

• ASP321a.is_src τ u = ∃ (v : ℤ), (u, v) ∈ inv_set τ.func

theorem ASP321a.src_of_inv {τ : AspPerm} {u v : ℤ} (uv_inv : (u, v) ∈ inv_set τ.func) : is_src τ u

def ASP321a.is_snk (τ : AspPerm) (v : ℤ) : Prop

Equations

• ASP321a.is_snk τ v = ∃ (u : ℤ), (u, v) ∈ inv_set τ.func

theorem ASP321a.snk_of_inv {τ : AspPerm} {u v : ℤ} (uv_inv : (u, v) ∈ inv_set τ.func) : is_snk τ v

Source and Sink Geometry for a Fixed 321-Avoiding Permutation

Fix a 321-avoiding ASP permutation τ. This section develops the source/sink geometry and the duality identities for s and s' that drive the later factorization arguments.

theorem ASP321a.inv_is_321a {τ : AspPerm} (h_321a : is_321a τ.func) : is_321a τ⁻¹.func

theorem ASP321a.not_src_and_snk {τ : AspPerm} (h_321a : is_321a τ.func) (n : ℤ) : ¬is_src τ n ∨ ¬is_snk τ n

theorem ASP321a.snk_lt {τ : AspPerm} (h_321a : is_321a τ.func) {v x : ℤ} (v_snk : is_snk τ v) (v_lt_x : v < x) : τ.func v < τ.func x

theorem ASP321a.snk_le {τ : AspPerm} (h_321a : is_321a τ.func) {v x : ℤ} (v_snk : is_snk τ v) (v_le_x : v ≤ x) : τ.func v ≤ τ.func x

theorem ASP321a.src_gt {τ : AspPerm} (h_321a : is_321a τ.func) {u x : ℤ} (u_src : is_src τ u) (x_lt_u : x < u) : τ.func x < τ.func u

theorem ASP321a.src_ge {τ : AspPerm} (h_321a : is_321a τ.func) {u x : ℤ} (u_src : is_src τ u) (x_le_u : x ≤ u) : τ.func x ≤ τ.func u

structure ASP321a.between_inv_prop {τ : AspPerm} (u x v : ℤ) : Prop

• src_or_snk : is_src τ x ∨ is_snk τ x
• src_iff_right_inv : is_src τ x ↔ (x, v) ∈ inv_set τ.func
• src_iff_left_ninv : is_src τ x ↔ (u, x) ∉ inv_set τ.func
• snk_iff_left_inv : is_snk τ x ↔ (u, x) ∈ inv_set τ.func
• snk_iff_right_ninv : is_snk τ x ↔ (x, v) ∉ inv_set τ.func

theorem ASP321a.between_inv {τ : AspPerm} (h_321a : is_321a τ.func) {u x v : ℤ} (uv_inv : (u, v) ∈ inv_set τ.func) (u_le_x : u ≤ x) (x_le_v : x ≤ v) : between_inv_prop u x v

theorem ASP321a.inv_of_quadrants {τ : AspPerm} {a b u v : ℤ} (hu : u ∈ northwest_set τ.func a b) (hv : v ∈ southeast_set τ.func a b) : (u, v) ∈ inv_set τ.func

theorem ASP321a.split_s {τ : AspPerm} (h_321a : is_321a τ.func) {u v a b : ℤ} (u_lt_b : u < b) (b_le_v : b ≤ v) (τv_lt_a : τ.func v < a) (τu_ge_a : τ.func u ≥ a) : τ.s a v + τ.s (τ.func v) b = τ.s a b

theorem ASP321a.uv_duality {τ : AspPerm} (h_321a : is_321a τ.func) {u a b : ℤ} (u_lt_b : u < b) (τu_ge_a : τ.func u ≥ a) {m m' : ℤ} (m_pos : m > 0) (m'_pos : m' > 0) (m_sum : m + m' = τ.s a b + 1) : τ.func (τ.v b m_pos) = τ⁻¹.u a m'_pos

theorem ASP321a.uv_duality_ge {τ : AspPerm} (h_321a : is_321a τ.func) {a b m m' : ℤ} (m_pos : m > 0) (m'_pos : m' > 0) (m_sum : m + m' = τ.s a b + 1) : is_snk τ (τ.v b m_pos) → is_snk τ (τ⁻¹.func (τ⁻¹.u a m'_pos)) → τ.func (τ.v b m_pos) ≥ τ⁻¹.u a m'_pos ∧ τ.v b m_pos ≥ τ⁻¹.func (τ⁻¹.u a m'_pos)

theorem ASP321a.uv_duality_lt {τ : AspPerm} (h_321a : is_321a τ.func) (a b : ℤ) {m m' : ℤ} (m_pos : m > 0) (m'_pos : m' > 0) (h_sum : m + m' ≥ τ.s a b + 2) : have v := τ.v b m_pos; have w := τ⁻¹.u a m'_pos; is_snk τ v → is_snk τ (τ⁻¹.func w) → τ⁻¹.func w < v

theorem ASP321a.split_s' {τ : AspPerm} (h_321a : is_321a τ.func) {u v a b : ℤ} (u_lt_b : u < b) (b_le_v : b ≤ v) (τv_lt_a : τ.func v < a) (τu_ge_a : τ.func u ≥ a) : τ⁻¹.s b (τ.func u) + τ⁻¹.s u a = τ⁻¹.s b a

Passing to Left Weak Order Subpermutations

Here β ≤L τ is fixed. The lemmas compare the inversion geometry of β and τ, especially the way ramps, sources, sinks, and shifted inversion sets are inherited along left weak order.

theorem ASP321a.src_of_src {τ β : AspPerm} (h_L : β ≤L τ) {n : ℤ} (h_src : is_src β n) : is_src τ n

theorem ASP321a.snk_of_snk {τ β : AspPerm} (h_L : β ≤L τ) {n : ℤ} (h_snk : is_snk β n) : is_snk τ n

theorem ASP321a.is_321a_of_lel {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) : is_321a β.func

structure ASP321a.between_inv_lel_prop (β τ : AspPerm) (u x v : ℤ) : Prop

• propτ : between_inv_prop u x v
• propβ : between_inv_prop u x v
• inv_iff_left : (u, x) ∈ inv_set β.func ↔ (u, x) ∈ inv_set τ.func
• inv_iff_right : (x, v) ∈ inv_set β.func ↔ (x, v) ∈ inv_set τ.func
• src_iff : is_src β x ↔ is_src τ x
• snk_iff : is_snk β x ↔ is_snk τ x

theorem ASP321a.between_inv_lel {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {u x v : ℤ} (uv_inv : (u, v) ∈ inv_set β.func) (u_le_x : u ≤ x) (x_le_v : x ≤ v) : between_inv_lel_prop β τ u x v

def ASP321a.interval_sub (i₁ i₂ : ℤ × ℤ) : Prop

Equations

• (i₁ ≼ i₂) = (i₂.1 ≤ i₁.1 ∧ i₁.2 ≤ i₂.2)

def ASP321a.«term_≼_» : Lean.TrailingParserDescr

Equations

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

theorem ASP321a.inv_of_lel_iff {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {u v u' v' : ℤ} (uv_inv : (u, v) ∈ inv_set β.func) (nested : (u', v') ≼ (u, v)) : (u', v') ∈ inv_set β.func ↔ (u', v') ∈ inv_set τ.func

theorem ASP321a.sr_inv_of_ler_iff {τ : AspPerm} (h_321a : is_321a τ.func) {α : AspPerm} (h_R : α ≤R τ) {u v u' v' : ℤ} (uv_inv : (u, v) ∈ τ.sr α '' inv_set α.func) (nested : (u, v) ≼ (u', v')) : (u', v') ∈ τ.sr α '' inv_set α.func ↔ (u', v') ∈ inv_set τ.func

theorem ASP321a.set_321a_prop_of_func (avset : tfas) (χ : ℤ) : set_321a_prop (inv_set (avset.recon χ))

theorem ASP321a.eq_s_of_lel {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {u b v : ℤ} (uv_inv : (u, v) ∈ inv_set β.func) (u_lt_b : u < b) : β.s (β.func v) b = τ.s (τ.func v) b

theorem ASP321a.eq_s'_of_lel {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {u b v : ℤ} (uv_inv : (u, v) ∈ inv_set β.func) (b_le_v : b ≤ v) : β.s' b (β.func u) = τ.s' b (τ.func u)

theorem ASP321a.uv_eq_of_lel {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) (b : ℤ) {m n : ℤ} (m_pos : m > 0) (n_pos : n > 0) : (τ.u b n_pos, τ.v b m_pos) ∈ inv_set β.func → τ.u b n_pos = β.u b n_pos ∧ τ.v b m_pos = β.v b m_pos

theorem ASP321a.uv_eq_of_lel' {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) (b : ℤ) {m n : ℤ} (m_pos : m > 0) (n_pos : n > 0) : (β.u b n_pos, β.v b m_pos) ∈ inv_set β.func → β.u b n_pos = τ.u b n_pos ∧ β.v b m_pos = τ.v b m_pos

theorem ASP321a.lel_ramp {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) (b : ℤ) {m n : ℤ} (m_pos : m > 0) (n_pos : n > 0) : (τ.u b n_pos, τ.v b m_pos) ∈ inv_set β.func ↔ (m, n) ∈ β.ramp b

theorem ASP321a.lel_lamp {τ : AspPerm} (h_321a : is_321a τ.func) {α : AspPerm} (h_R : α ≤R τ) (a : ℤ) {m n : ℤ} (m_pos : m > 0) (n_pos : n > 0) : (τ⁻¹.u a m_pos, τ⁻¹.v a n_pos) ∈ inv_set α⁻¹.func ↔ (m, n) ∈ α.lamp a

theorem ASP321a.inv_of_lel_iff_ramp {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {u b v : ℤ} (u_lt_b : u < b) (b_le_v : b ≤ v) : have m := τ.s (τ.func v) b + 1; have n := τ.s' b (τ.func u); (u, v) ∈ inv_set β.func ↔ (m, n) ∈ β.ramp b

Two-Factor Demazure Factorization for 321-Avoiding ASP Permutations

This section proves the inversion-set criterion for a factorization τ = α ⋆ β in the 321-avoiding setting, first as upper and lower bounds and then as a full characterization.

theorem ASP321a.inversion_in_union {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) (a b u v : ℤ) (dprod : α.dprod_val_ge β a b (τ.s a b)) : u < b → b ≤ v → τ.func u ≥ a → τ.func v < a → (u, v) ∈ τ.sr α '' inv_set α.func ∪ inv_set β.func

theorem ASP321a.union_sufficient {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) (a b : ℤ) (h_union : inv_set τ.func ⊆ τ.sr α '' inv_set α.func ∪ inv_set β.func) : α.dprod_val_ge β a b (τ.s a b)

theorem ASP321a.excess_of_not_isolated {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) {u v₁ v₂ : ℤ} (v₁_lt_v₂ : v₁ < v₂) (uv₁_inv : (u, v₁) ∈ τ.sr α '' inv_set α.func) (uv₂_inv : (u, v₂) ∈ inv_set β.func) : have a := τ.func v₁ + 1; have b := v₁ + 1; α.dprod_val_ge β a b (τ.s a b + 1)

theorem ASP321a.not_isolated_of_domino {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (a b m m' n n' : ℤ) (m_pos : m ≥ 1) (m'_pos : m' ≥ 1) (n_pos : n ≥ 1) (n'_pos : n' ≥ 1) (msum : m + m' = τ.s a b + 2) (nsum : n + n' = τ⁻¹.s b a + 1) (hα : (m', n') ∈ α.lamp a) (hβ : (m, n) ∈ β.ramp b) : ∃ (I : ℤ × ℤ) (J : ℤ × ℤ), {I, J} ⊆ τ.sr α '' inv_set α.func ∩ inv_set β.func ∧ I ≼ J ∧ I ≠ J

theorem ASP321a.not_isolated_of_excess {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) {a b : ℤ} (h_s : α.dprod_val_ge β a b (τ.s a b + 1)) : ∃ (I : ℤ × ℤ) (J : ℤ × ℤ), {I, J} ⊆ τ.sr α '' inv_set α.func ∩ inv_set β.func ∧ I ≼ J ∧ I ≠ J

theorem ASP321a.dprod_ge_iff_union {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) : τ ≤ α ⋆ β ↔ inv_set τ.func ⊆ τ.sr α '' inv_set α.func ∪ inv_set β.func

In the 321-avoiding setting, the inequality τ ≤ α ⋆ β is equivalent to the inversion set of τ lying in the union of the shifted inversion set of α and the inversion set of β.

def ASP321a.isolated (S : Set (ℤ × ℤ)) : Prop

A set of boxes is isolated if it contains no two distinct comparable elements.

Equations

• ASP321a.isolated S = ∀ I ∈ S, ∀ J ∈ S, I ≼ J → I = J

theorem ASP321a.dprod_le_iff_isolated {τ : AspPerm} (h_321a : is_321a τ.func) {β : AspPerm} (h_L : β ≤L τ) {α : AspPerm} (h_R : α ≤R τ) (h_χ : τ.χ = α.χ + β.χ) : α ⋆ β ≤ τ ↔ isolated (τ.sr α '' inv_set α.func ∩ inv_set β.func)

In the 321-avoiding setting, the inequality α ⋆ β ≤ τ is equivalent to isolatedness of the overlap between the shifted inversion set of α and the inversion set of β.

theorem ASP321a.dprod_eq_iff {τ : AspPerm} (h_321a : is_321a τ.func) {β α : AspPerm} : τ = α ⋆ β ↔ α.χ + β.χ = τ.χ ∧ inv_set τ.func = τ.sr α '' inv_set α.func ∪ inv_set β.func ∧ isolated (τ.sr α '' inv_set α.func ∩ inv_set β.func)

Characterize the Demazure factorization τ = α ⋆ β by equality of shifts, a union formula for inversion sets, and isolatedness of the overlap.