LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

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.

Under Foata's fundamental transformation, anti-excedances become descents

Statement

Let $σ \in S_{n}$ and let $w = F (σ)$ be Foata's fundamental transformation. Then a position $j$ is a descent of $w$ if and only if the entry $w (j)$ is an anti-excedance of $σ$ . In particular,

$des (w) = ∣ AExc (σ) ∣ .$

Facts & Assumptions

Given: A permutation $σ \in S_{n}$ , its standard cycle form

$(a_{1, 0} a_{1, 1} \dots a_{1, r_{1} - 1}) \dots (a_{s, 0} a_{s, 1} \dots a_{s, r_{s} - 1}),$

with each first entry $a_{t, 0}$ the largest in its cycle and $a_{1, 0} < \dots < a_{s, 0}$ , and the one-line word $w = F (σ)$ obtained by deleting the parentheses.

Proof

technique · direct

1.1

For every cycle and every $0 \leq j < r_{t} - 1$ , the cycle notation means $σ (a_{t, j}) = a_{t, j + 1}$ . Therefore $a_{t, j}$ is an anti-excedance of $σ$ exactly when $a_{t, j + 1} < a_{t, j}$ , which is exactly the condition that the adjacent pair $(a_{t, j}, a_{t, j + 1})$ contributes a descent in the stripped word $w$ .

given

1.2

Across cycle boundaries, the stripped word has no descent: the last entry of cycle $t$ is followed by the first entry $a_{t + 1, 0}$ of cycle $t + 1$ , and the standard cycle form orders these first entries increasingly, so $a_{t, r_{t} - 1} < a_{t + 1, 0}$ .

given

2.1

The last entry $a_{t, r_{t} - 1}$ of a cycle is never an anti-excedance, because $σ (a_{t, r_{t} - 1}) = a_{t, 0}$ and $a_{t, 0}$ is the largest element of the cycle.

step 1.1given

3.1

By steps 1.1, 2.1 and 1.2, the descents of $w$ occur exactly at the entries of $w$ that are anti-excedances of $σ$ . Counting them gives $des (w) = ∣ AExc (σ) ∣$ .

step 1.1step 2.1step 1.2∎

Depends on

Used by

Descents and excedances are equidistributed on Sₙ Theorem

Dependency tree · two levels

6 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

Andrew Lin, MIT 18.212 Algebraic Combinatorics, Lecture 10 (standard reference, not scraped)