ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 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.

The Möbius value of the rank-three interval [e,c] in S4 from the recurrence, with the parity and falling-chain checks

Example

In the notation of the type $A_{3}$ Coxeter group $W$ with simple reflections $s_{1}, s_{2}, s_{3}$ and one-line notation on the letters ${1, 2, 3, 4}$ (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4), the published $S_{4}$ on ${0, 1, 2, 3}$ under the letter shift $j \mapsto j - 1$ of The finite symmetric group $S_{n}$ , one-line notation, and cycle notation), let $c = s_{1} s_{2} s_{3} = 2341$ and $[e, c] = {1234; 2134, 1324, 1243; 2314, 2143, 1342; 2341}$ (Deleted-position labels from a fixed reduced expression, the lexicographic shelling criterion, and Möbius data).

(i) The recurrence. With $μ$ the Möbius function of $[e, c]$ (The integer-valued Möbius function $μ_{P}$ of a locally finite poset, The Möbius recurrence: $μ_{P} (x, x) = 1$ and both interval sums of $μ_{P}$ vanish when $x < y$ ) one has $μ (1234, 1234) = 1$ ; $μ (1234, s) = - 1$ for each atom $s \in {s_{1}, s_{2}, s_{3}}$ ; and $μ (1234, x) = - (1 - 1 - 1) = 1$ for each of the three rank-two elements $x$ , because the elements of $[1234, x]$ are exactly $1234$ , the two atoms covered by $x$ and $x$ itself. Hence $μ (1234, 2341) = - (1 - 3 + 3) = - 1 = (- 1)^{ℓ (2341) - ℓ (1234)} = (- 1)^{3}$ , in agreement with Bruhat intervals are Eulerian: parity balance of the elements, and the Möbius function of a full interval (ii).

(ii) Parity balance. $[e, c]$ has four elements of even length, $1234, 2314, 2143, 1342$ , and four of odd length, $2134, 1324, 1243, 2341$ ; so the interval contains equally many elements of each parity, and $\sum_{x \in [e, c]} (- 1)^{ℓ (x)} = 0$ , as required by Bruhat intervals are Eulerian: parity balance of the elements, and the Möbius function of a full interval (i) (The cardinality $∣ A ∣$ of a finite set).

(iii) Falling-chain check. The unique strictly falling maximal chain of $[e, c]$ is $2341 ⋗ 2314 ⋗ 2134 ⋗ 1234$ with label word $(3, 2, 1)$ ; the falling-chain formula of Lexicographic chain shelling and the falling-chain Möbius formula (ii), applicable through Deletion-labeled Bruhat intervals are lexicographically shellable, with the explicit earlier/later chain comparison, gives $μ (1234, 2341) = (- 1)^{3} \cdot 1 = - 1$ , consistent with (i) and with the count-one clause of Bruhat intervals are Eulerian: parity balance of the elements, and the Möbius function of a full interval (iii).

Facts & Assumptions

Given: The type $A_{3}$ Coxeter group $W$ with simple reflections $s_{1}, s_{2}, s_{3}$ , the element $c = s_{1} s_{2} s_{3} = 2341$ , the interval $[e, c]$ and the deleted-position labeling induced by the reduced expression $c = s_{1} s_{2} s_{3}$ .

[F1]

Subword characterization: " $u \leq w$ " holds if and only if some reduced expression of $u$ is a subword of a fixed reduced expression of $w$ ; "and the indices may be chosen with $k = ℓ (u)$ , so that $s_{i_{1}} \dots s_{i_{k}}$ is a reduced expression of $u$ " (The subword characterization of Bruhat order and its independence of the reduced expression).

[F2]

Reflection deletion: "Then $v_{i} = v t_{i}$ and $v_{i} < v$ ; moreover $v_{i}$ is covered by $v$ if and only if $ℓ (v_{i}) = q - 1$ , that is, if and only if the word $s_{1} \dots \hat{s_{i}} \dots s_{q}$ is reduced." (The lifting property in all four descent cases, the cover criterion, reflection deletion, and directedness (3)).

[F3]

Type $A$ : "Then $s_{i} \mapsto (i i + 1)$ extends to an isomorphism $W \to S_{n}$ (the letters $1, \dots, n$ carry the library's symmetric group by the order-preserving identification with ${0, \dots, n - 1}$ , under which $(i i + 1)$ is the adjacent transposition $(i - 1 i)$ ), and for every $w \in W$ , $ℓ (w) = inv (φ (w)),$ " (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4)).

[F4]

The Möbius recurrence: "Equivalently, off the diagonal, $μ_{P} (x, y) = - \sum_{x \leq z < y} μ_{P} (x, z) = - \sum_{x < z \leq y} μ_{P} (z, y) .$ " (The Möbius recurrence: $μ_{P} (x, x) = 1$ and both interval sums of $μ_{P}$ vanish when $x < y$ ).

[F5]

The labeling recursion: "the cover $x_{j} ⋗ x_{j + 1}$ determines a unique position $λ_{j + 1} (m) \in P_{j}$ with $x_{j + 1} = \prod_{p \in P_{j} ∖ {λ_{j + 1} (m)}} s_{p}$ " (Deleted-position labels from a fixed reduced expression, the lexicographic shelling criterion, and Möbius data (2)).

[F6]

Falling label words: "A maximal chain $m$ of $[x, y]$ is increasing if $λ_{1} (m) < λ_{2} (m) < \dots < λ_{n} (m)$ ; it is falling if $λ_{1} (m) \geq λ_{2} (m) \geq \dots \geq λ_{n} (m)$ " (Finite lattice congruences, interval endpoints and descending rooted-chain labels (3)).

[F7]

The sign formula for full intervals: " $μ (u, v) = (- 1)^{ℓ (v) - ℓ (u)}$ " for $u \leq v$ in $W$ (Bruhat intervals are Eulerian: parity balance of the elements, and the Möbius function of a full interval (ii)).

[F8]

The parity balance: if $u < v$ then " $[u, v]$ contains equally many elements of even and of odd length" (Bruhat intervals are Eulerian: parity balance of the elements, and the Möbius function of a full interval (i)).

[F9]

The deleted-position labeling satisfies (N) and (L) on every rooted interval: "On every rooted interval of $[u, v]$ the labeling satisfies the no-tie condition (N) and the lex-increasing property (L)" (Deletion-labeled Bruhat intervals are lexicographically shellable, with the explicit earlier/later chain comparison (i)).

[F10]

The falling-chain formula: for a finite graded poset with a descending rooted-chain labeling satisfying (N) and (L) on every rooted interval, " $μ (v, w) = (- 1)^{ρ (v, w)} \cdot # {maximal chains of [v, w] whose label word is strictly falling},$ " (Lexicographic chain shelling and the falling-chain Möbius formula (ii)).

[F11]

Cardinality of a finite set: "Let $A$ be a finite set. Then there is exactly one $n \in N$ with $A \approx n$ " (The cardinality $∣ A ∣$ of a finite set).

[F12]

Grading: "Every maximal chain in $[u, v]$ has exactly $ℓ (v) - ℓ (u)$ strict steps" (Finiteness of Bruhat intervals, the chain refinement property, and grading by length (3)).

Verification

technique · finite computation on the fixed reduced word $s_1s_2s_3$

1.1F1F2F3F12

The eight elements and the twelve covers. The word $s_{1} s_{2} s_{3}$ is reduced and its subword products are $1234, 2134, 1324, 1243, 2314, 2143, 1342, 2341$ , each reduced of its number of letters because its inversion number equals its length [F3]; by [F1] these are exactly the elements of $[e, c]$ , of ranks $0, 1, 1, 1, 2, 2, 2, 3$ . By [F2] the elements covered by $c$ are the single-letter deletions of $s_{1} s_{2} s_{3}$ whose remaining word is reduced, namely $s_{2} s_{3} = 1342$ , $s_{1} s_{3} = 2143$ , $s_{1} s_{2} = 2314$ , the three elements of length $2$ ; each atom covers $e$ ; and for a length-two element $x = t_{i} t_{j}$ the subword products of the reduced word $t_{i} t_{j}$ are exactly $e, t_{i}, t_{j}, x$ , so the atoms below $x$ are $t_{i}$ and $t_{j}$ and every other adjacent-rank pair involving $x$ is incomparable, which yields the six covers $1342 ⋗ 1243$ , $1342 ⋗ 1324$ , $2143 ⋗ 1243$ , $2143 ⋗ 2134$ , $2314 ⋗ 1324$ , $2314 ⋗ 2134$ . This is the same twelve-cover diagram used for the label words below, and by [F12] every maximal chain of $[e, c]$ has three steps.

2.1F4step 1.1

The atoms. By step 1.1 the three atoms $2134, 1324, 1243$ cover $e$ and have nothing strictly between, so the recurrence [F4] gives $μ (e, s) = - (μ (e, e)) = - 1$ for each of them.

2.2F3F8F11step 1.1

Parity balance. The lengths of the eight elements are $0, 1, 1, 1, 2, 2, 2, 3$ [F3], so four elements have even and four have odd length and $\sum_{x \in [e, c]} (- 1)^{ℓ (x)} = 4 - 4 = 0$ , as required by the parity-balance statement [F8]; the count is a cardinality of a finite set [F11].

3.1F4step 1.1step 2.1

The rank-two elements. By step 1.1 the elements of $[e, x]$ other than $x$ are exactly $e$ and the two atoms it covers, so the recurrence [F4] gives $μ (e, x) = - (1 - 1 - 1) = 1$ for $x = 1342, 2143, 2314$ .

4.1F3F4F7step 2.1step 3.1

The top value. The elements of $[e, c]$ other than $c$ are $e$ , the three rank-one elements and the three rank-two elements, so the recurrence [F4] gives $μ (e, c) = - (1 + 3 \cdot (- 1) + 3 \cdot 1) = - (1 - 3 + 3) = - 1$ , which equals $(- 1)^{ℓ (c) - ℓ (e)} = (- 1)^{3}$ by [F3] and agrees with the sign formula [F7].

5.1F5F6F7F9F10F12step 1.1step 4.1

The falling-chain check. Reading off deletions from the cover diagram of step 1.1 with the recursion [F5] gives the six label words $(1, 2, 3)$ and $(1, 3, 2)$ for the chains through $1342$ , $(2, 1, 3)$ and $(2, 3, 1)$ for those through $2143$ , and $(3, 1, 2)$ and $(3, 2, 1)$ for those through $2314$ ; since these are the six permutations of ${1, 2, 3}$ , exactly one maximal chain has a strictly falling word [F6], namely $2341 ⋗ 2314 ⋗ 2134 ⋗ 1234$ with word $(3, 2, 1)$ . By [F9] the deleted-position labeling satisfies (N) and (L) on every rooted interval and by [F12] the interval $[e, c]$ is finite and graded, so the falling-chain formula [F10] applies and gives $μ (e, c) = (- 1)^{ℓ (c) - ℓ (e)} \cdot 1 = - 1$ , consistent with step 4.1 and with the count-one clause of [F7].

6.1F8F10step 2.2step 4.1step 5.1∎

Conclusion. Steps 4.1, 2.2 and 5.1 compute $μ (1234, 2341) = - 1 = (- 1)^{3}$ from the recurrence and confirm the two independent checks of the Eulerian theorem: the equal numbers of even and odd elements [F8] and the single strictly falling maximal chain [F10].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

70 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

Anders Björner and Francesco Brenti, Combinatorics of Coxeter Groups (Graduate Texts in Mathematics 231, Springer 2005; author-hosted complete PDF) (standard reference, not scraped)
Yufei Zhao, On the Bruhat order of the symmetric group and its shellability (expository notes, MIT, 12 December 2007) (standard reference, not scraped)