LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + 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.

If $∥ a ∥ = 1$ then $j \mapsto # {r : 0 \leq r < m, S_{a} (j + r) \leq S_{a} (j)}$ is a bijection from ${0, \dots, m - 1}$ onto ${1, \dots, m}$

Statement

Let $m \geq 1$ and let $a$ be a word of length $m$ of integers with $∥ a ∥ = 1$ (Cyclic shifts of an integer word and its periodic partial-sum function). For $j \in Z$ put

$X (j) : = ∣ {r \in N : 0 \leq r < m, S_{a} (j + r) \leq S_{a} (j)} ∣,$

the number of the $m$ partial sums of the shift $σ^{j} a$ , counted from $r = 0$ , at which $S_{a}$ has not risen strictly above its value at $j$ . Then

$X : {0, 1, \dots, m - 1} ⟶ {1, 2, \dots, m}$

is a bijection (Injection, surjection, bijection). In particular each of the values $1, 2, \dots, m$ is realised by exactly one $j$ in ${0, \dots, m - 1}$ .

Facts & Assumptions

Given: a natural number $m \geq 1$ and a word $a$ of length $m$ of integers with $∥ a ∥ = 1$ .

[F1]

$S_{a} (j + m) = S_{a} (j) + ∥ a ∥$ for every $j \in Z$ ; $S_{a} (0) = 0$ ; and $j m o d m$ is the unique $r$ with $j = q m + r$ and $0 \leq r < m$ (Cyclic shifts of an integer word and its periodic partial-sum function).

[L1]

For $d, x \in Z$ , $d$ divides $x$ when $x = d q$ for some $q \in Z$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[L2]

For $x, b \in Z$ with $b \neq 0$ there is exactly one pair $(q, r)$ of integers with $x = q b + r$ and $0 \leq r < ∣ b ∣$ (Division with remainder for any nonzero divisor: for $a \in Z$ and $b \neq 0$ there are unique $q, r \in Z$ with $a = q b + r$ and $0 \leq r < ∣ b ∣$ ).

[L3]

Let $A$ be a finite set and $B \subseteq A$ ; then $B$ is finite, $∣ B ∣ \leq ∣ A ∣$ , and $∣ B ∣ = ∣ A ∣$ if and only if $B = A$ (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , clauses 1, 2 and 3).

[L4]

If $m^{'} < n^{'}$ then there is no injection from $n^{'}$ to $m^{'}$ (The pigeonhole principle on $N$ , clause 2).

[L5]

$∣ n ∣ = n$ for a natural number $n$ , and a bijection transports finiteness and cardinality (The cardinality $∣ A ∣$ of a finite set).

[L6]

A function is a bijection when it is both injective and surjective (Injection, surjection, bijection).

Proof

technique · direct

1.1F1algebra

The integer key $T (i) : = m S_{a} (i) - i$ is $m$ -periodic: $T (i + m) = m (S_{a} (i) + 1) - (i + m) = m S_{a} (i) - i = T (i)$ , using $∥ a ∥ = 1$ in the quasiperiodicity clause of [F1].

1.2L1L2algebra

$T$ is injective on ${0, \dots, m - 1}$ : if $T (i) = T (j)$ with $i, j$ in that range, then $m (S_{a} (i) - S_{a} (j)) = i - j$ , so $m$ divides $i - j$ while $- m < i - j < m$ , and writing $i - j = m q$ forces $q = 0$ by [L2], since $q \geq 1$ would give $i - j \geq m$ and $q \leq - 1$ would give $i - j \leq - m$ .

1.3F1algebra

For every $j \in Z$ and every $r$ with $0 \leq r < m$ : $S_{a} (j + r) \leq S_{a} (j)$ if and only if $T (j + r) \leq T (j)$ . Put $d : = S_{a} (j + r) - S_{a} (j)$ , so $T (j + r) - T (j) = m d - r$ . If $d \leq 0$ then $m d - r \leq - r \leq 0$ ; if $d \geq 1$ then $m d - r \geq m - r \geq 1$ , and this is the only place the hypothesis $r < m$ is used. So the sign of $m d - r$ decides, and the two conditions agree.

2.1F1L5step 1.1step 1.3

For $0 \leq j < m$ one has $X (j) = ∣ {i \in N : i < m, T (i) \leq T (j)} ∣$ . Indeed $r \mapsto (j + r) m o d m$ is a bijection of ${0, \dots, m - 1}$ onto itself, with inverse $i \mapsto (i - j) m o d m$ ; by step 1.1 and the periodicity of $T$ one has $T ((j + r) m o d m) = T (j + r)$ , and $T (j)$ is the value at $j$ itself since $j m o d m = j$ in this range; so step 1.3 identifies the set counted by $X (j)$ with the displayed set through that bijection, and [L5] preserves the count.

3.1L3step 1.2step 2.1

$X$ is injective on ${0, \dots, m - 1}$ . Let $i \neq j$ lie in that range; by step 1.2 the values $T (i)$ and $T (j)$ differ, say $T (i) < T (j)$ . Then ${l < m : T (l) \leq T (i)}$ is contained in ${l < m : T (l) \leq T (j)}$ and does not contain $j$ , which the second set does; so it is a proper subset of a finite set and [L3] gives a strictly smaller cardinality, that is $X (i) < X (j)$ by step 2.1.

3.2L3L5step 2.1

$X$ takes values in ${1, \dots, m}$ : the index $r = 0$ always satisfies $S_{a} (j) \leq S_{a} (j)$ , so the counted set is nonempty and $X (j) \geq 1$ ; and it is a subset of an $m$ -element set, so $X (j) \leq m$ by [L3] and [L5].

4.1L4L5L6step 3.1step 3.2∎

Both ${0, \dots, m - 1}$ and ${1, \dots, m}$ have exactly $m$ elements. If $X$ omitted a value of ${1, \dots, m}$ , then by steps 3.1 and 3.2 it would be an injection from an $m$ -element set into a set of at most $m - 1$ elements, which [L4] forbids; so $X$ is surjective as well as injective and is a bijection by [L6].

Remarks

This is not the cycle lemma. The cycle lemma counts the shifts all of whose partial sums are positive, and for weight $1$ that is exactly one shift. This lemma sorts every shift, by how many of its partial sums fail to rise above the starting value, and finds that the $m$ shifts realise the $m$ possible counts once each. The shift with count $1$ is the one the cycle lemma singles out.
Why an integer key and not a rational one. The source perturbs $S_{a}$ by $i / m$ to break ties; multiplying through by $m$ gives $T (i) = m S_{a} (i) - i$ , which does the same work without leaving $Z$ . The tie-breaking is exactly the injectivity of step 1.2.

Depends on

Used by

The Chung–Feller theorem: for each k with 0≤ k≤ n, exactly Cₙ of the diagonal paths from (0,0) to (2n,0) have exactly 2k steps lying above level 0 Theorem

Dependency tree · two levels

34 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

A. Huq, Generalized Chung-Feller Theorems for Lattice Paths (PhD thesis, Brandeis University, 2009), Theorem 2.1.1 (standard reference, not scraped)

If ∥a∥=1∥a∥=1 then j↦#{r:0≤r<m, Sa(j+r)≤Sa(j)}j↦#{r:0≤r<m, Sa​(j+r)≤Sa​(j)} is a bijection from {0,…,m−1}{0,…,m−1} onto {1,…,m}{1,…,m}