Sign-changing inversions

Section 6 of the twice-marked banana paper proves the chain theorem (thm:bngChain, Theorem 1.13) through a single combinatorial estimate on the Demazure product: prop:sciInvStar (6.13). This file introduces the statistic it is about and states the two results, with the paper's proofs recorded as the plan for discharging them.

Where this sits

The Lean development already has:

• eq:tauGlued — Utilities.satisfiesTransmission_wedgeAddDivisor_star;
• the two-factor and ℓ-fold gluing of transmission existence (Utilities.ChainGluing), conditional on a factorization property;
• lem:tauChars — tauChars_rank_eq_southeast and its northwest twin;
• the raw-ℤ → ℤ-to-AspPerm bridge (Bananas/TransmissionBridge.lean).

Note that Utilities.ChainGluing reaches the chain statement by a different route from the paper: it asks for a length-budgeted factorization τ = α ⋆ β, whereas the paper never factors, and instead bounds sci (α ⋆ β) directly. The sci route below is the paper's, and is the one that does not require inventing a splitting.

Status

Both estimates are proved, with no sorry. This file proves the induction for prop:sciInvStar (6.13) from a named AffineReductionData k; the companion module AffineReduction.lean constructs that datum from the ordinary adjacent descent theorem and a direct count of periodic inversion classes, and exports the unconditional theorem sci_star_le. The base case is sci_star_le_of_kInversionCount_eq_zero.

sci_star_sigma_le (lem-SciSimpleRefl, 6.12) is unconditional.

Downstream: prop:sciLambda (6.10) relates sci (τ_D) to the Weierstrass partition and needs lem:tauChars (available as tauChars_rank_eq_southeast and its northwest twin) plus a Riemann-Roch telescoping sum; thm:glueBNGtoKGT (6.6) is then 6.10 + 6.13 + eq:tauGlued; prop:glueMarked (6.14) needs the wedge rank formula, available as Utilities.VertexWedgeRankFormula.vertexWedge_rank_ge_iff_profile_inequalities; and thm:bngChain (6.16) is the induction over the chain.

def Bananas.sciSet (α : ℤ → ℤ) : Set (ℤ × ℤ)

Paper source: Definition 6.9.

A sign-changing inversion of α is a pair u < v with α u > 0 and α v ≤ 0. Unlike an ordinary inversion this compares each value against the fixed threshold 0 rather than against the other value.

Equations

• Bananas.sciSet α = {p : ℤ × ℤ | p.1 < p.2 ∧ 0 < α p.1 ∧ α p.2 ≤ 0}

noncomputable def Bananas.sci (α : ℤ → ℤ) : ℕ

Paper source: Definition 6.9, the count sci(α).

As with kInversionCount, Set.ncard is 0 on an infinite set, so every statement below that bounds sci from above must either carry finiteness or be read only for α where the set is finite. For an almost-sign-preserving α it is automatically finite.

Equations

• Bananas.sci α = (Bananas.sciSet α).ncard

theorem Bananas.mem_sciSet_iff (α : ℤ → ℤ) (p : ℤ × ℤ) : p ∈ sciSet α ↔ p.1 < p.2 ∧ 0 < α p.1 ∧ α p.2 ≤ 0

theorem Bananas.sciSet_id : (sciSet fun (n : ℤ) => n) = ∅

A shift has no sign-changing inversions in the relevant range: this is the base case of the induction in prop:sciInvStar. Stated for the identity, which is the only case the induction actually consumes.

@[simp]

theorem Bananas.sci_id : (sci fun (n : ℤ) => n) = 0

def Bananas.affineSimpleReflection (k n : ℤ) : ℤ → ℤ

The affine simple reflection σ^k_n of Section 6: it swaps m and m + 1 for every m ≡ n (mod k) and fixes everything else.

The paper writes σ^k_n = σ_{n + kℤ}; the definition below makes that action explicit.

Equations

• Bananas.affineSimpleReflection k n m = if (m - n) % k = 0 then m + 1 else if (m - 1 - n) % k = 0 then m - 1 else m

The pigeonhole core of Lemma 6.12

The whole content of lem-SciSimpleRefl is that an α with few sign-changing inversions cannot flip sign twice within one residue class mod k. That statement involves neither the Demazure product nor σ_S, so it is isolated here.

theorem Bananas.sub_one_le_sci_of_two_signFlips (α : ℤ → ℤ) (k : ℤ) (hfin : (sciSet α).Finite) {m₁ m₂ : ℤ} (hlt : m₁ < m₂) (hdvd : k ∣ m₂ - m₁) (h₁ : 0 < α (m₁ + 1)) (h₂ : α m₂ ≤ 0) : k - 1 ≤ ↑(sci α)

Two sign flips of α at positions congruent mod k force k - 1 sign-changing inversions.

The injection is the paper's: for each u strictly between the two flip positions, either (u, m₂) or (m₁ + 1, u) is a sign-changing inversion, according to the sign of α u, and these are pairwise distinct.

theorem Bananas.sciSet_finite (α : AspPerm) : (sciSet α.func).Finite

An ASP permutation has finitely many sign-changing inversions.

isAsp says only finitely many n satisfy n * α n < 0. Choose N bounding that set together with α⁻¹ 0. Then every sign-changing inversion lies in the box [-N, N]²: if u < -N then u < 0 and u ∉ F force α u ≤ 0; if v > N then v > 0 and v ∉ F ∪ {α⁻¹ 0} force 0 < α v; and u < v propagates the two bounds to the other coordinates.

Transport along an adjacent-transposition permutation

def Bananas.flipSet (α : ℤ → ℤ) (S : Set ℤ) : Set ℤ

The positions in S at which α flips from nonpositive to positive. These are exactly the pairs that σ_S can turn into a new sign-changing inversion.

Equations

• Bananas.flipSet α S = {l : ℤ | l ∈ S ∧ α l ≤ 0 ∧ 0 < α (l + 1)}

theorem Bananas.sci_comp_sigmaFun_le (α : ℤ → ℤ) (S : Set ℤ) (hS : Transpositions.NoConsecutive S) (hfin : (sciSet α).Finite) (hsub : (flipSet α S).Subsingleton) : (sci fun (m : ℤ) => α (Transpositions.sigmaFun S m)) ≤ sci α + 1

Precomposing with σ_S creates at most one new sign-changing inversion, provided α has at most one flip position in S.

This is the transport half of lem-SciSimpleRefl. Note that no "rising" hypothesis on S is needed: a pair that σ_S moves out of order is forced to be (l, l + 1) with l a flip position, and those are counted by flipSet.

theorem Bananas.sci_star_sigma_le (k : ℤ) (α : AspPerm) (S : Set ℤ) (hS : Transpositions.NoConsecutive S) (hcong : ∀ l₁ ∈ S, ∀ l₂ ∈ S, k ∣ l₂ - l₁) (hfin : (sciSet α.func).Finite) (hsci : ↑(sci α.func) ≤ k - 2) : ↑(sci (α ⋆ Transpositions.sigma S hS).func) ≤ ↑(sci α.func) + 1

Paper source: lem-SciSimpleRefl (Lemma 6.12).

Composing with one σ_S whose support lies in a single residue class mod k raises the sign-changing inversion count by at most one, as soon as sci α ≤ k - 2. The paper states this for σ^k_n = σ_{n + kℤ}; the only property of that set the argument uses is that any two of its elements are congruent mod k, so it is assumed directly.

Proof. Demazure.Transpositions.starSigma (eq:starSigma, [PflDemProd, Thm 8.7]) replaces the Demazure product by the ordinary product with σ_R, R the rising set. sci_comp_sigmaFun_le then reduces the claim to α having at most one flip position in R, and two flip positions congruent mod k would give k - 1 sign-changing inversions by sub_one_le_sci_of_two_signFlips, contradicting sci α ≤ k - 2.

Inversion-free factors

The base case of the induction in prop:sciInvStar. The paper argues that a k-affine permutation with no k-inversions is a shift; in fact all that is needed is that it has no inversions at all, which is both weaker and enough.

theorem Bananas.inv_set_eq_empty_of_kInversionCount_eq_zero (k : ℕ) (hk : 0 < k) (β : AspPerm) (hβ : IsKAffine k β.func) (hcount : kInversionCount k β.func = 0) : invSet β.func = ∅

A k-affine permutation with no k-inversions has no inversions at all: any inversion translates into the fundamental range [0, k) by k-affinity.

theorem Bananas.sci_star_le_of_kInversionCount_eq_zero (k : ℕ) (hk : 0 < k) (α β : AspPerm) (hβ : IsKAffine k β.func) (hcount : kInversionCount k β.func = 0) : sci (α ⋆ β).func ≤ sci α.func

Base case of prop:sciInvStar: a factor with no k-inversions cannot raise the sign-changing inversion count.

With no inversions the product is reduced, so the Demazure product is the ordinary one, and β carries sciSet (α ∘ β) injectively into sciSet α because it preserves the order of every pair.

structure Bananas.AffineReductionData (k : ℕ) : Prop

The one fact about the affine Coxeter structure of Aff~_k that the induction in prop:sciInvStar still consumes, isolated as a named input: a k-affine permutation with a k-inversion has a simple descent n, and factoring out the affine simple reflection σ^k_n on the left drops the k-inversion count by exactly one, the product being reduced.

The local module AffineReduction.lean supplies this structure by reducing to the ordinary adjacent-descent theorem and counting normalized periodic inversion representatives. The base case above needs no such input.

• reduce (β : AspPerm) : IsKAffine k β.func → 0 < kInversionCount k β.func → ∃ (S : Set ℤ) (hS : Transpositions.NoConsecutive S) (β' : AspPerm), (∀ l₁ ∈ S, ∀ l₂ ∈ S, ↑k ∣ l₂ - l₁) ∧ β = Transpositions.sigma S hS ⋆ β' ∧ IsKAffine k β'.func ∧ kInversionCount k β'.func + 1 = kInversionCount k β.func

  A k-inversion yields a reduced factorization by one affine simple reflection, dropping the count by one.

theorem Bananas.sci_star_le_of_affineReductionData (k : ℕ) (hdata : AffineReductionData k) (α β : AspPerm) (hβ : IsKAffine k β.func) (hbudget : ↑(sci α.func) + ↑(kInversionCount k β.func) < ↑k) : ↑(sci (α ⋆ β).func) ≤ ↑(sci α.func) + ↑(kInversionCount k β.func)

Paper source: prop:sciInvStar (Proposition 6.13).

As long as the budget k strictly exceeds the two statistics combined, the Demazure product does not overshoot their sum. This is the estimate the whole chain theorem rests on.

The induction is the paper's, on inv_k β: the base case is the shift clause, and the inductive step splits off one affine simple reflection with reduce, bounds its effect by sci_star_sigma_le (Lemma 6.12), and reapplies the hypothesis to the smaller factor. The budget survives the step because 6.12 costs one and the count drops by one.