demazure

This repository contains formalizations about the basic theory of the Demazure product on almost-sign-preserving permutations, as developed in the following paper.

N. Pflueger, An extended Demazure product on integer permutations via min-plus matrix multiplication

The code includes full formalizations of the main theorems of An extended Demazure product, following the style, definitions, and proof structure closely. The repository also includes some additional results not included in that article, especially the classification of Demazure factorizations of 321-avoiding permutations (not necessarily of finite length).

Documentation for this repository is auto-generated using doc-gen4. Note that documentation for all Mathlib dependencies is automatically generated along with this repo; you should select "Demazure" in the left column to find the documentation for this repository.

Project Structure

The Lean development in Demazure/ is organized as follows. Section numbers tell roughly where the material of that file is found in An extended Demazure product. In some cases, material from one section is spread across multiple files, or not yet formalized, and some formalized theorems are not in that article.

┌───────────────────────────────┐          ┌───────────────────────────────┐
│ Utils.lean                    │          │ Valley.lean                   │
│ Generic helper lemmas         │          │ Tools for tracking minima     │
│                               │          │ and argmin sets.              │
└───────────────┬───────────────┘          └───────────────┬───────────────┘
                │                                          │
                │                                          ▼
                │                          ┌───────────────┴───────────────┐
                │                          │ SlipFace.lean (§3)            │
                │                          │ Slipfaces and operations      │
                │                          │ on them.                      │
                │                          └───────────────┬───────────────┘
                │                                          │
                └──────────────────────────┬───────────────┘
                                           │
                                           ▼
                           ┌───────────────┴───────────────┐
                           │ AspPerm.lean (§2)             │
                           │ ASP permutations, inversion   │
                           │ sets, weak                    │
                           │ orders, ⋆ and ◃ predicates    │
                           └───────────────┬───────────────┘
                                           │
              ┌────────────────────────────┴────────────────────────────┐
              │                                                         │
              ▼                                                         ▼
┌─────────────┴─────────────────┐          ┌────────────────────────────┴──┐
│ InvSet.lean (§2)              │          │ Submodular.lean (§4)          │
│ Abstract ASP inversion sets   │          │ Submodular slipfaces;         │
│ and reconstruction            │          │ ⋆ and ◃ on ASP.               │
└───────────────┬───────────────┘          └───────────────┬───────────────┘
                │                                          │
                └─────────────────────┬────────────────────┴───────────────┐
                                      │                                    │
                                      ▼                                    ▼
                      ┌───────────────┴───────────────┐    ┌───────────────┴───────────────┐
                      │ Avoiding321.lean              │    │ ReducedProducts.lean (§5)     │
                      │ 321-avoiding permutations     │    │ Reduced products              │
                      │ and behavior of ⋆ on them     │    │ and relations to ⋆ and ◃      │
                      └───────────────┬───────────────┘    └───────────────┬───────────────┘
             ┌────────────────────────┴────┐                               │
             ▼                             ▼                               ▼
┌────────────┴────────────┐   ┌────────────┴────────────┐  ┌───────────────┴───────────────┐
│ Tableaux.lean           │   │ SkewShapes/Basic.lean   │  │ Reduction.lean (§6)           │
│ Hecke factorizations    │   │ Skew shapes and the     │  │ Greedy and stingy             │
│ and set-valued tableaux │   │ permutations σ_S        │  │ characterizations;            │
└─────────────────────────┘   └────────────┬────────────┘  │ reduction theorems            │
                                           │               └───────────────┬───────────────┘
              ┌────────────────────────────┤                               │
              ▼                            ▼                               ▼
┌─────────────┴─────────────┐ ┌────────────┴────────────┐  ┌───────────────┴───────────────┐
│ SkewShapes/               │ │ SkewShapes/             │  │ Transpositions.lean (§3, §8)  │
│ TwoTermFactorization.lean │ │ ShapeConstruction.lean  │  │ Adjacent transposition        │
│ Weak orders; two-factor   │ │ Skew shapes from        │  │ formulas for product          │
│ factorizations of σ_S     │ │ 321-avoiding perms      │  │ and residual                  │
└─────────────┬─────────────┘ └─────────────────────────┘  └───────────────────────────────┘
              │
              ▼
┌─────────────┴─────────────┐
│ SkewShapes/               │
│ HeckeFactorization.lean   │
│ Shape chains and Hecke    │
│ factorizations of σ_S     │
└───────────────────────────┘

Skew shapes

The folder Demazure/SkewShapes/ develops a combinatorial model for shift-0 321-avoiding ASP permutations in terms of skew shapes (convex, locally finite sets of boxes in ℤ × ℤ, in matrix coordinates). This material is not in An extended Demazure product.

Basic.lean: skew shapes and their reflections, the fringe boxes U(x) and V(x) of each box x, the set I(S) of pairs (u(x), v(x)), and the shift-0 321-avoiding ASP permutation σ_S whose inversion set is I(S).
TwoTermFactorization.lean: the left and right weak orders on skew shapes, matching the weak orders below σ_S, and the classification of Demazure factorizations σ_S = α ⋆ β into shift-0 factors by pairs of shapes A ≤R S, B ≤L S that cover S and overlap in a nonattacking set of boxes.
HeckeFactorization.lean: the classification of Hecke factorizations σ_S = α₁ ⋆ ⋯ ⋆ αₙ into shift-0 factors by shape chains.
ShapeConstruction.lean: the converse construction. Given a shift-0 ASP permutation τ and a set U containing every source and no sink of an inversion of τ (such a U exists exactly when τ is 321-avoiding), a lattice path determined by U places one box for each inversion, and the resulting skew shape has σ = τ. Every skew shape arises this way from its own boundary path.

Paper Coverage

The formalization mostly follows Sections 2--6 of An extended Demazure product, with some later results and some additional material developed beyond that article. Lean statements are often split into several lemmas rather than matching the article's statements verbatim.

Paper material	Main Lean files	Coverage notes
Introduction: Theorems A, B, C and the operation `◃`	`Submodular.lean`, `Reduction.lean`, `Transpositions.lean`	The main theorem statements are formalized as component lemmas: existence and associativity of `⋆`, the min-plus formula, the greedy and stingy characterizations, the reduction theorem, and the adjacent-transposition formulas.
Section 2: ASP permutations, shift, inversions, weak orders, reduced products, inversion-set reconstruction	`AspPerm.lean`, `InvSet.lean`	Directly formalized, with reconstruction from inversion sets isolated in `InvSet.lean`. Some helper infrastructure for finite sets and integer counts lives in `Utils.lean`.
Section 3: Slipface functions and the operations `⋆`, `◃`, `▹` on slipfaces	`SlipFace.lean`, `Transpositions.lean`	Directly formalized, including duality, monotonicity, operation existence, associativity identities, witness-set reductions, and the formulas for products with non-overlapping adjacent transpositions.
Section 4: Submodular slipfaces and the induced operations on `AspPerm`	`Valley.lean`, `Submodular.lean`	Directly formalized. `Valley.lean` packages the rightmost-minimum argument used in the proof of closure under `⋆`; `Submodular.lean` formalizes closure under `⋆`, `◃`, and `▹`, inverse compatibility, shift formulas, and weak-order consequences.
Section 5: When `⋆`, `◃`, and `▹` are ordinary products	`ReducedProducts.lean`	Directly formalized, including the reduced-product criteria and the comparison between weak and strong Bruhat orders.
Section 6: Greediness, stinginess, and the reduction theorem	`Reduction.lean`	Directly formalized, including the two-factor reduction theorem and a list version of the many-factor reduction statement.
Section 7: Bounded-difference permutations and the essential set	`AspPerm.lean`, `SlipFace.lean`, `Submodular.lean`	Partially formalized, including the essential set of a slipface, the bounded-difference criterion, and the compatibility of the essential set with the associated slipface.
Section 8: Subgroups closed under `⋆` and `◃`	`Transpositions.lean`	Partially formalized. The adjacent-transposition computation used for symmetric and affine symmetric groups is formalized, but the downward-closed subgroup framework is not broadly formalized in this repository.
Additional material outside An extended Demazure product	`Avoiding321.lean`, `Tableaux.lean`	These files develop 321-avoiding ASP permutations, triangle-free inversion sets, Demazure factorization criteria, Hecke factorizations, chains of inversion boxes, and set-valued tableaux.
Additional material: skew shapes	`SkewShapes/Basic.lean`, `SkewShapes/TwoTermFactorization.lean`, `SkewShapes/HeckeFactorization.lean`, `SkewShapes/ShapeConstruction.lean`	Shift-0 321-avoiding ASP permutations as permutations of skew shapes, with weak orders, two-term and Hecke factorizations, and the reconstruction of a skew shape from its permutation, described in terms of boxes.

Installation

To download and build this code, follow the steps below.

Install Lean 4 and Lake: Follow the Lean 4 installation guide.

Clone the Repository:

git clone https://github.com/npflueger/demazure.git
cd demazure

Build the Project: Use the Lake build tool to compile and set up dependencies.
```
lake exe cache get
lake build
```

For further information about working with Lean 4/Mathlib projects, consult the Mathlib project guide.

Generative AI disclosure

Portions of this repository were built with the assistance of generative AI, primarily OpenAI Codex and Claude Code. The extent of such tool use varies in different parts of the project. The file AGENTS.md contains instructions given to these agents when writing proofs, and may be informative about the manner in which these tools have been used. In particular, proofs that have been written primarily by an AI tool are indicated with a comment identifying the model used. The overall design, and all formalized theorem statements, were written by the author.