Demazure character formula for reductive algebraic groups

### What is the conjecture

Let $G$ be a reductive algebraic group over a field $k$, with Lie algebra $\mathfrak{g}$, and let $B$ be a Borel subalgebra. The Weyl group $W$ acts on the weight lattice $P$. For a dominant weight $\lambda \in P^+$, let $V(\lambda)$ denote the finite-dimensional irreducible representation of highest weight $\lambda$.

For each $w \in W$, the **Demazure module** $V_w(\lambda)$ is defined as the $B$-submodule of $V(\lambda)$ generated by the weight space $V(\lambda)_{w\lambda}$ under the action of the enveloping algebra $U(\mathfrak{b})$.

The **Demazure character formula** gives an explicit expression for the formal character of $V_w(\lambda)$ as:
$$\text{ch}(V_w(\lambda)) = \sum_{w' \leq w} (-1)^{\ell(w) - \ell(w')} e^{w'(\lambda + \rho) - \rho}$$
where the sum is over elements $w' \in W$ with $w' \leq w$ in the Bruhat order, $\ell$ denotes the length function, and $\rho$ is the half-sum of positive roots.

The **Demazure conjecture** states that this character formula holds for any reductive algebraic group, generalizing the classical Weyl character formula. It was formulated by Demazure in 1974 and subsequently proved: V. Lakshmibai, C. Musili, and C. S. Seshadri (1979) proved it for classical groups via standard monomial theory, and Peter Littelmann extended the proof to all reductive algebraic groups.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Demazure_conjecture, https://en.wikipedia.org/wiki/Demazure_module, https://arxiv.org/abs/1605.04953, https://link.springer.com/article/10.1007/BF01388527

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-03-14)

Building blocks (1-3; from search results):
- Weyl groups and Bruhat order (structure on Coxeter groups, length functions)
- Weight lattices and dominant weights for reductive algebraic groups
- Finite-dimensional representations and Borel subalgebras

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definitions of reductive algebraic groups and their Lie algebras in Lean
- Character formulas and formal character ring with the explicit Bruhat order sum formula for Demazure modules

Rating justification (1-2 sentences): While Weyl groups, weight lattices, and basic representation theory have some presence in Mathlib (e.g., root systems, Coxeter groups), the statement requires substantial theory development around reductive groups, Borel subalgebras, and the character ring. The Demazure character formula itself would require significant new definitions connecting representation-theoretic objects with combinatorial expressions over the Bruhat order.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-20
* ams-14
* ams-17

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

No repository file, test, or entry point is named. Start by checking the stated prerequisites—Weyl groups and Bruhat order, weight lattices, reductive groups, Borel subalgebras, and character rings—and compare them with existing Mathlib support. Done means a corrected, formalizable Demazure character formula is added with the required supporting definitions and verification.

Written by the indexing model from the issue text.