LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-10-08

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Verma's sign identity over Bruhat intervals

Facts & Assumptions

Given: $n \geq 1$ and the Laurent coefficients $r_{x, z}$ from The $R$ -coefficient recursion, support, degree bounds and inversion.

[F1]

For all $a, b \in S_{n}$ , $\sum_{y} r_{a, y} \overline{r_{y, b}} = δ_{a, b}$ and $\overline{r_{y, b}} = s g n (y) s g n (b) r_{y, b}$ (The $R$ -coefficient recursion, support, degree bounds and inversion, parts (d),(e)).

[F2]

$r_{a, b} = 0$ unless $a \leq b$ ; for $a \leq b$ , with $d = ℓ (b) - ℓ (a)$ , the least-degree term of $r_{a, b}$ is $s g n (a) s g n (b) v^{- d}$ and all exponents are congruent to $- d$ modulo $2$ (The $R$ -coefficient recursion, support, degree bounds and inversion, parts (b),(c)).

[F3]

Bruhat order on $S_{n}$ is graded by $ℓ$ and has finite intervals; in particular $x < z$ implies $ℓ (x) < ℓ (z)$ (Basic properties of the Bruhat order on $S_{n}$ ).

Statement

For all $x < z$ in $S_{n}$ , with $s g n (y) = (- 1)^{ℓ (y)}$ , $\sum_{y \in S_{n}, x \leq y \leq z} s g n (y) = 0.$

Proof

technique · extract the lowest Laurent degree from the R-matrix identity

1.1F1F2F3algebra

Reduce to the interval. Fix $x < z$ and set $d : = ℓ (z) - ℓ (x)$ . Bruhat gradedness gives $d > 0$ . The R-matrix identity and bar symmetry yield $0 = \sum_{y} r_{x, y} \overline{r_{y, z}} = s g n (z) \sum_{y} s g n (y) r_{x, y} r_{y, z}$ . By support, a nonzero summand requires both $x \leq y$ and $y \leq z$ , so $0 = \sum_{x \leq y \leq z} s g n (y) r_{x, y} r_{y, z}$ .

2.1F1F2F3step 1.1algebra∎

Extract the lowest degree. For each $y \in [x, z]$ , let $d_{1} : = ℓ (y) - ℓ (x)$ and $d_{2} : = ℓ (z) - ℓ (y)$ , so $d_{1} + d_{2} = d$ . The least exponent in $r_{x, y} r_{y, z}$ is $- d$ and its coefficient is $s g n (x) s g n (y)^{2} s g n (z) = s g n (x) s g n (z)$ . The external factor $s g n (y)$ in step 1.1 makes the coefficient of $v^{- d}$ in that summand $s g n (x) s g n (z) s g n (y)$ . Since every other exponent in each factor is strictly above its least exponent, no other product terms contribute to degree $- d$ . Taking that coefficient in the zero sum of step 1.1 gives $0 = s g n (x) s g n (z) \sum_{x \leq y \leq z} s g n (y)$ . The prefactor is $\pm 1$ , proving the claim. The interval is finite, and no choice principle is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

G. Lusztig, Hecke Algebras with Unequal Parameters (revised book version, arXiv:math/0208154v2) — Proposition 4.8 (printed p. 27): Verma's alternating-sign sum over Bruhat intervals, derived from the R-matrix identity and the lowest-degree term of the R-coefficients. (standard reference, not scraped)