Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 every ai1 and a1, the strict right minima form a two-sided increasing list on which Sa increases by exactly 1 at each successive index

Statement

Let m1 and let a be a word of length m of integers with ai1 for every i<m and with k:=a1 (Cyclic shifts of an integer word and its periodic partial-sum function). Write R for the set of strict right minima of Sa, that is the set of jZ with Sa(i)>Sa(j) for every integer i>j (σja has all partial sums positive exactly when Sa(i)>Sa(j) for every i>j).

  1. Existence and value. For every MZ there is exactly one jR with Sa(j)=M. Writing ρ(M) for it, the map ρ:ZR is a bijection with Sa(ρ(M))=M.
  2. Succession. ρ is strictly increasing, and ρ(M+k)=ρ(M)+m for every MZ.
  3. Window count. For every j0Z the set R{j0,j0+1,,j0+m1} is finite with exactly k elements.

The hypothesis ai1 enters only in clause 1, where it is what forces the value at a strict right minimum to be exactly M rather than merely at most M.

Facts & Assumptions

Given: a natural number m1 and a word a of length m of integers with ai1 for every i<m and k=a1.

[F1]

Sa(0)=0; Sa(j)=i<jai for 0jm; Sa(j)Sa(j1)=a(j1)modm for every jZ; Sa(j+m)=Sa(j)+a for every jZ; and Sa(qm+r)=qa+i<rai for 0r<m (Cyclic shifts of an integer word and its periodic partial-sum function).

[F2]

An integer j is a strict right minimum of Sa when Sa(i)>Sa(j) for every integer i>j (σja has all partial sums positive exactly when Sa(i)>Sa(j) for every i>j).

[L1]

A property that holds at 0 and passes from every natural number to its successor holds at every natural number: if a property P satisfies P(0) and (P(n)P(σ(n))) for all n, then P(n) holds for all nN (The principle of mathematical induction).

[L2]

The order on Z is total, antisymmetric and transitive, and is compatible with addition; positives are closed under multiplication (The integers form a totally ordered ring).

[L3]

A nonempty SZ with an upper bound has a unique greatest element, and a nonempty SZ 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).

[L4]

For x,bZ with b0 there is exactly one pair (q,r) of integers with x=qb+r and 0r<b (Division with remainder for any nonzero divisor: for aZ and b0 there are unique q,rZ with a=qb+r and 0r<b).

[L5]
[L6]

If A is finite and f:AB is a bijection then B is finite and B=A; and n=n for a natural number n (The cardinality A of a finite set).

Proof

technique · direct
1.1

The integers Sa(0),Sa(1),,Sa(m1) have a least element μ: by induction on t, every list Sa(0),,Sa(t) has a least element, since the order on Z is total, so adjoining one further integer to a list with a least element leaves it with one.

F1L1L2
1.2

For every MZ the set TM:={iZ:Sa(i)M} is nonempty. If M0 then Sa(0)=0M. If M<0 then put t:=M, a positive integer; induction on t with the quasiperiodicity clause of [F1] gives Sa(tm)=tk, and tkt because k1, so Sa(tm)t=M.

F1L1L2
2.1

Each TM has an upper bound. Let iTM and write i=qm+r with 0r<m by [L4], so Sa(i)=qk+Sa(r)qk+μ by [F1] and step 1.1, whence qkMμ. If q1 then qqk because k1, so qMμ; and if q0 then q0. So in either case qB, where B is the greater of 0 and Mμ, and therefore iBm+m1.

F1L2L4step 1.1
3.1

By [L3] the set TM has a greatest element jM. Every i>jM lies outside TM, so Sa(i)>MSa(jM), and jM is a strict right minimum. Its value is exactly M: the one-step difference identity of [F1] gives Sa(jM+1)Sa(jM)=ajMmodm1 by hypothesis, while Sa(jM+1)>M since jM+1 is outside TM, so M<Sa(jM+1)Sa(jM)+1M+1 and hence Sa(jM)=M.

F1F2L3step 1.2step 2.1
4.1

At most one strict right minimum has a given value: if j<j are both strict right minima then Sa(j)>Sa(j), so their values differ. With step 3.1 this gives, for each M, exactly one jR with Sa(j)=M; write ρ(M) for it. Every jR satisfies j=ρ(Sa(j)) by that uniqueness, so ρ is onto R, and it is injective because Sa(ρ(M))=M; by [L5] it is a bijection ZR. This is clause 1.

F2L5step 3.1
5.1

ρ is strictly increasing: if M<M and ρ(M)ρ(M), then either ρ(M)=ρ(M), forcing M=M, or ρ(M)<ρ(M), and then the strict right minimum property of ρ(M) gives M=Sa(ρ(M))>Sa(ρ(M))=M; both contradict M<M. And ρ(M)+m is a strict right minimum of value M+k: for i>ρ(M)+m we have im>ρ(M), so the quasiperiodicity clause of [F1] gives Sa(i)=Sa(im)+k>Sa(ρ(M))+k=Sa(ρ(M)+m), and Sa(ρ(M)+m)=M+k; hence ρ(M+k)=ρ(M)+m by step 4.1. This is clause 2.

F1F2step 4.1
6.1

Fix j0Z. Iterating clause 2 by induction gives ρ(M+tk)=ρ(M)+tm for every tN, so the set {M:ρ(M)j0} is nonempty, taking t with tmj0ρ(0), and bounded below, since for t with ρ(0)tm<j0 every Mtk has ρ(M)ρ(tk)=ρ(0)tm<j0; let M0 be its least element by [L3]. Then ρ(M01)<j0ρ(M0), so ρ(M0+k)=ρ(M0)+mj0+m and ρ(M0+k1)=ρ(M01)+m<j0+m. Since ρ is strictly increasing and every member of R is some ρ(M), the members of R in {j0,,j0+m1} are exactly ρ(M0),,ρ(M0+k1), and iρ(M0+i) is a bijection from the natural number k onto that set; so by [L6] the set is finite with exactly k elements, which is clause 3.

L1L3L6step 4.1step 5.1

Remarks

  • Why the hypothesis ai1 cannot be dropped. It is used exactly once, in step 3.1, to force Sa(jM)=M: without it the greatest element of TM can have a value strictly below M, several values of M then share one strict right minimum, and the succession structure of clause 2 fails. A word with a letter 2 shows this at once, and it is the reason the cycle lemma is stated for words whose letters are at most 1.

  • Why the hypothesis a1 cannot be dropped. It is what makes Sa take arbitrarily large values to the right of any index and arbitrarily small ones to the left, which is what makes every TM nonempty and bounded above. With weight 0 the function is periodic and R is empty.

Depends on

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