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 every and , the strict right minima form a two-sided increasing list on which increases by exactly at each successive index
Statement
Let and let be a word of length of integers with for every and with (Cyclic shifts of an integer word and its periodic partial-sum function). Write for the set of strict right minima of , that is the set of with for every integer ( has all partial sums positive exactly when for every ).
- Existence and value. For every there is exactly one with . Writing for it, the map is a bijection with .
- Succession. is strictly increasing, and for every .
- Window count. For every the set is finite with exactly elements.
The hypothesis enters only in clause 1, where it is what forces the value at a strict right minimum to be exactly rather than merely at most .
Facts & Assumptions
Given: a natural number and a word of length of integers with for every and .
; for ; for every ; for every ; and for (Cyclic shifts of an integer word and its periodic partial-sum function).
An integer is a strict right minimum of when for every integer ( has all partial sums positive exactly when for every ).
A property that holds at and passes from every natural number to its successor holds at every natural number: if a property satisfies and () for all , then holds for all (The principle of mathematical induction).
The order on is total, antisymmetric and transitive, and is compatible with addition; positives are closed under multiplication (The integers form a totally ordered ring).
A nonempty with an upper bound has a unique greatest element, and a nonempty with a lower bound has a unique least element (A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element).
For with there is exactly one pair of integers with and (Division with remainder for any nonzero divisor: for and there are unique with and ).
For : is a bijection if and only if there is a function with and ( is a bijection if and only if there is a function with and ; such a is unique, equals the inverse relation , and is itself a bijection).
If is finite and is a bijection then is finite and ; and for a natural number (The cardinality of a finite set).
Proof
The integers have a least element : by induction on , every list has a least element, since the order on is total, so adjoining one further integer to a list with a least element leaves it with one.
For every the set is nonempty. If then . If then put , a positive integer; induction on with the quasiperiodicity clause of [F1] gives , and because , so .
Each has an upper bound. Let and write with by [L4], so by [F1] and step 1.1, whence . If then because , so ; and if then . So in either case , where is the greater of and , and therefore .
By [L3] the set has a greatest element . Every lies outside , so , and is a strict right minimum. Its value is exactly : the one-step difference identity of [F1] gives by hypothesis, while since is outside , so and hence .
At most one strict right minimum has a given value: if are both strict right minima then , so their values differ. With step 3.1 this gives, for each , exactly one with ; write for it. Every satisfies by that uniqueness, so is onto , and it is injective because ; by [L5] it is a bijection . This is clause 1.
is strictly increasing: if and , then either , forcing , or , and then the strict right minimum property of gives ; both contradict . And is a strict right minimum of value : for we have , so the quasiperiodicity clause of [F1] gives , and ; hence by step 4.1. This is clause 2.
Fix . Iterating clause 2 by induction gives for every , so the set is nonempty, taking with , and bounded below, since for with every has ; let be its least element by [L3]. Then , so and . Since is strictly increasing and every member of is some , the members of in are exactly , and is a bijection from the natural number onto that set; so by [L6] the set is finite with exactly elements, which is clause 3.
Remarks
-
Why the hypothesis cannot be dropped. It is used exactly once, in step 3.1, to force : without it the greatest element of can have a value strictly below , several values of then share one strict right minimum, and the succession structure of clause 2 fails. A word with a letter shows this at once, and it is the reason the cycle lemma is stated for words whose letters are at most .
-
Why the hypothesis cannot be dropped. It is what makes take arbitrarily large values to the right of any index and arbitrarily small ones to the left, which is what makes every nonempty and bounded above. With weight the function is periodic and is empty.
Depends on
- Cyclic shifts of an integer word and its periodic partial-sum function
- $\sigma^{j}a$ has all partial sums positive exactly when $S_a(i)>S_a(j)$ for every $i>j$
- A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element
- The integers as equivalence classes of pairs of naturals
- The principle of mathematical induction
- The integers form a totally ordered ring
- Division with remainder for any nonzero divisor: for $a \in \mathbb{Z}$ and $b \ne 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le r < |b|$
- $f : A \to B$ is a bijection if and only if there is a function $g : B \to A$ with $g \circ f = \Delta_A$ and $f \circ g = \Delta_B$; such a $g$ is unique, equals the inverse relation $f^{-1}$, and is itself a bijection
- The cardinality $\lvert A\rvert$ of a finite set
Used by
Dependency tree · two levels
47 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.1 (standard reference, not scraped)