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.

σja has all partial sums positive exactly when Sa(i)>Sa(j) for every i>j

Statement

Let m1, let a be a word of length m of integers with a1, and let jZ (Cyclic shifts of an integer word and its periodic partial-sum function).

  1. For every r with 0rm,

    i<r(σja)i=Sa(j+r)Sa(j).

  2. Every partial sum i<r(σja)i with 1rm is positive if and only if Sa(i)>Sa(j) for every integer i>j.

Call jZ a strict right minimum of Sa when Sa(i)>Sa(j) for every integer i>j. Clause 2 says that the shift σja has all of its partial sums positive exactly when j is a strict right minimum of Sa.

Facts & Assumptions

Given: a natural number m1, a word a of length m of integers with a1, and an integer j.

[F1]

(σja)i=a(i+j)modm for 0i<m (Cyclic shifts of an integer word and its periodic partial-sum function).

[F2]

Sa(0)=0; Sa(j)Sa(j1)=a(j1)modm for every jZ; Sa(j+m)=Sa(j)+a for every jZ; and the finite sum satisfies i<0ci=0 and i<r+1ci=i<rci+cr (Cyclic shifts of an integer word and its periodic partial-sum function).

[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]

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).

Proof

technique · direct
1.1

Clause 1 holds by induction on r. At r=0 both sides are 0 by [F2]. If it holds at r with r<m, then the finite-sum clause gives i<r+1(σja)i=i<r(σja)i+(σja)r, which by the inductive hypothesis and [F1] is Sa(j+r)Sa(j)+a(j+r)modm, and the one-step difference identity of [F2] applied at j+r+1 turns the last two terms into Sa(j+r+1)Sa(j).

F1F2L1
2.1

For every tN and every iZ one has Sa(i+tm)=Sa(i)+ta: at t=0 this is trivial, and the step is the quasiperiodicity clause of [F2]. Hence, if every partial sum of σja over 1rm is positive, then Sa(j+r)>Sa(j) for those r by step 1.1, and for an arbitrary integer i>j we may write ij1=tm+r with 0r<m and t0 by [L2], since ij10; putting r:=r+1, so 1rm and i=j+r+tm, gives Sa(i)=Sa(j+r)+taSa(j+r)>Sa(j) because a1 and t0.

F2L1L2step 1.1
3.1

Conversely, if Sa(i)>Sa(j) for every integer i>j, then in particular Sa(j+r)>Sa(j) for 1rm, so every partial sum of σja over that range is positive by step 1.1. The two directions together are clause 2.

step 1.1step 2.1

Remarks

  • Why the condition is stated for all i>j and not for one period. The one-period form is what a shift's partial sums see, and the unbounded form is what the succession structure of the strict right minima is stated in. The equivalence needs a1: with weight 0 the function Sa is periodic, Sa(j+m)=Sa(j), and no index is a strict right minimum. In that case the full-period partial sum is also 0, so no shift has every nonempty partial sum positive.

  • The strict right minima are a property of Sa alone. They do not refer to the word except through its partial-sum function, and that is what makes the counting argument of the cycle lemma a statement about Z rather than about words.

Depends on

Used by

Dependency tree · two levels

18 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