Alphabeta MathHow 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 cycle lemma on the word
Example
Let
a word of length and weight . Its seven cyclic shifts and their partial sums are:
| shift | partial sums |
|---|---|
Facts & Assumptions
Given: the two words above and the weight-two word .
If every letter of a length- integer word is at most and its weight is , then exactly one starting index gives a cyclic shift whose nonempty partial sums are all positive (The cycle lemma (Dvoretzky–Motzkin): if every and , then exactly of the cyclic shifts of have all partial sums positive).
The cycle-lemma Catalan count gives (, a second derivation of the Catalan count).
Verification
In the table, only the second row has all partial sums strictly positive, so the word has exactly one good shift.
Deleting the leading from that good shift gives , which is the Dyck word UDUDUD of semilength .
This agrees with [L1] and [L2]: [L1] predicts one good shift, and [L2] reads , so .
The weight-two word has exactly the two good shifts and , so the general statement is visible too: the number of good shifts is the weight.
Remarks
- The good shift is the second row because the page's convention counts strict positivity of every partial sum, not nonnegativity.
Depends on
- The cycle lemma (Dvoretzky–Motzkin): if every $a_i\le1$ and $\lVert a\rVert=k\ge1$, then exactly $k$ of the $m$ cyclic shifts of $a$ have all partial sums positive
- $(2n+1)\,C_n=\binom{2n+1}{n}$, a second derivation of the Catalan count
- Cyclic shifts of an integer word and its periodic partial-sum function
- The set $[A]^{k}$ of $k$-element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$
- The Catalan number $C_n:=\lvert\mathcal{D}_n\rvert$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
38 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
- N. Dershowitz and S. Zaks, The Cycle Lemma and Some Applications (standard reference, not scraped)