LemmaStatement: AI-adaptedProof: 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.

Cyclic shifting is an action of $Z / m$ on the words of length $m$ over a set

Statement

Let $X$ be a set and $m \geq 1$ , and let $X^{m}$ be the set of words of length $m$ over $X$ , with the shifts $σ^{j}$ of Cyclic shifts of an integer word and its periodic partial-sum function.

$σ^{0}$ is the identity of $X^{m}$ , and $σ^{j} (σ^{k} a) = σ^{j + k} a$ for all $j, k \in Z$ and $a \in X^{m}$ .
$σ^{j} a = σ^{j^{'}} a$ whenever $j \equiv j^{'} (m o d m)$ . Hence $[j]_{m} \cdot a : = σ^{j} a$ is a well-defined left action of the additive group $Z / m$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ , For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold) on $X^{m}$ , in the sense of Left group actions, transitive actions, and faithful actions.
For every $x \in X$ the number of positions of $σ^{j} a$ carrying the letter $x$ equals the number of positions of $a$ carrying $x$ . In particular, for a word of integers, $∥ σ^{j} a ∥ = ∥ a ∥$ .

Facts & Assumptions

Given: a set $X$ , a natural number $m \geq 1$ , and words of length $m$ over $X$ .

[F1]

$(σ^{j} a)_{i} = a_{(i + j) m o d m}$ for $0 \leq i < m$ , where $j m o d m$ is the unique $r$ with $j = q m + r$ and $0 \leq r < m$ ; and $∥ a ∥ = \sum_{i < m} a_{i}$ for a word of integers (Cyclic shifts of an integer word and its periodic partial-sum function).

[L1]

A left action of a group $G$ with identity $e$ on a set $X$ is a function $G \times X \to X$ with $e \cdot x = x$ and $(g h) \cdot x = g \cdot (h \cdot x)$ for all $g, h \in G$ and $x \in X$ (Left group actions, transitive actions, and faithful actions).

[L2]

$[j]_{m} = [j^{'}]_{m}$ holds exactly when $j \equiv j^{'} (m o d m)$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ ).

[L3]

$Z / m$ is a commutative ring under the induced operations, so in particular its addition makes it an abelian group with identity $[0]_{m}$ (For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

[L4]

For a commutative monoid $M$ and $g : N \to M$ , if $π$ is a permutation of the von Neumann natural $n$ and $h_{i} = g_{π (i)}$ for every $i < n$ , then $\prod_{i < n} h_{i} = \prod_{i < n} g_{i}$ (Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either, clause 3).

[L5]

If $A$ is finite and $f : A \to B$ is a bijection then $B$ is finite and $∣ B ∣ = ∣ A ∣$ (The cardinality $∣ A ∣$ of a finite set).

[L6]

For $f : A \to B$ : $f$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ( $f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = Δ_{A}$ and $f \circ g = Δ_{B}$ ; such a $g$ is unique, equals the inverse relation $f^{- 1}$ , and is itself a bijection).

Proof

technique · direct

1.1F1algebra

For every integer $x$ and every $k \in Z$ one has $((x m o d m) + k) m o d m = (x + k) m o d m$ , because $x - (x m o d m)$ is a multiple of $m$ and adding a multiple of $m$ to the argument changes neither the remainder nor its defining inequalities.

2.1F1L6step 1.1

The map $π_{j} : i \mapsto (i + j) m o d m$ is a permutation of ${0, \dots, m - 1}$ : the map $i \mapsto (i - j) m o d m$ is a two-sided inverse of it, since by step 1.1 both composites send $i$ to $i m o d m$ , which is $i$ for $0 \leq i < m$ .

2.2F1step 1.1

Clause 1 holds: $(σ^{0} a)_{i} = a_{i m o d m} = a_{i}$ for $0 \leq i < m$ , and $(σ^{j} (σ^{k} a))_{i} = (σ^{k} a)_{(i + j) m o d m} = a_{(((i + j) m o d m) + k) m o d m} = a_{(i + j + k) m o d m} = (σ^{j + k} a)_{i}$ using step 1.1.

2.3F1L1L2L3step 1.1

Clause 2 holds: if $j \equiv j^{'} (m o d m)$ then $(i + j) m o d m = (i + j^{'}) m o d m$ for every $i$ , since the two arguments differ by a multiple of $m$ , so $σ^{j} a = σ^{j^{'}} a$ ; by [L2] the rule $[j]_{m} \cdot a : = σ^{j} a$ is therefore well defined on $Z / m$ , and by [L3] together with clause 1 it satisfies the two axioms of [L1] with $e = [0]_{m}$ .

3.1F1L4L5step 2.1

Clause 3 holds: by step 2.1 the map $π_{j}$ is a permutation of the index set, and it carries the positions of $σ^{j} a$ carrying $x$ bijectively onto the positions of $a$ carrying $x$ , since $(σ^{j} a)_{i} = x$ exactly when $a_{π_{j} (i)} = x$ ; so the two counts agree by [L5]. For a word of integers, [L4] applied with $π = π_{j}$ gives $∥ σ^{j} a ∥ = \sum_{i < m} a_{π_{j} (i)} = \sum_{i < m} a_{i} = ∥ a ∥$ .

4.1step 2.2step 2.3step 3.1∎

The three clauses are established.

Remarks

Why the acting group is $Z / m$ and not $Z$ . Both act, and the $Z$ -action factors through $Z / m$ by clause 2. Taking the finite group is what makes the orbit and stabiliser counts below available, and it is the only reason the reduction is recorded.
Clause 3 is what confines the action to a level set. The shift preserves the number of positions carrying each letter, so it acts on the words with a prescribed letter count and on the words of a prescribed weight. The cycle lemma is a statement about one such orbit.

Depends on

Used by

Dependency tree · two levels

43 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", Europ. J. Combinatorics 11 (1990) 35–40, §1 (standard reference, not scraped)

Cyclic shifting is an action of Z/mZ/m on the words of length mm over a set