Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

The cycle lemma (Dvoretzky–Motzkin): if every ai1 and a=k1, then exactly k of the m cyclic shifts of a have all partial sums positive

Statement

Orientation convention, fixed here and cited wherever it is used. A shift σja is counted when all of its partial sums i<r(σja)i, for 1rm, are strictly positive, and shifts are indexed by starting position, so σja begins at position jmodm of a (Cyclic shifts of an integer word and its periodic partial-sum function).

  1. Let m1 and let a be a word of length m of integers with ai1 for every i<m and a=k1. Then exactly k of the m indices j with 0j<m are such that σja has all its partial sums positive.
  2. Boxes and circles. Let p,n,μN with m:=p+n1, and let a be a word of length m in which p positions carry the letter 1 and the remaining n positions carry the letter μ. Then a=pμn, and if pμn1 then exactly pμn of the m indices j with 0j<m are such that σja has all its partial sums positive.

Facts & Assumptions

Given: a natural number m1 and a word a of length m of integers, with the hypotheses of the clause being proved.

[F1]

a=i<mai; (σja)i=a(i+j)modm; 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]

For a1 and jZ: every partial sum i<r(σja)i with 1rm is positive if and only if Sa(i)>Sa(j) for every integer i>j, that is exactly when j is a strict right minimum of Sa (σja has all partial sums positive exactly when Sa(i)>Sa(j) for every i>j).

[L2]

If ai1 for every i<m and k=a1, then for every j0Z the set of strict right minima of Sa lying in {j0,,j0+m1} is finite with exactly k elements (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, clause 3).

[L3]

For a commutative monoid M and g:NM: i<p+ngi=(i<pgi)(j<ngp+j); and if π is a permutation of the von Neumann natural and hi=gπ(i) for every i<, then i<hi=i<gi (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, clauses 1 and 3).

[L4]

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

[L5]

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

Proof

technique · direct
1.1

By [L1] an index j is such that σja has all its partial sums positive exactly when j is a strict right minimum of Sa; so the set of indices to be counted in clause 1 is the set of strict right minima lying in {0,1,,m1}.

L1
2.1

By [L2] with j0=0 that set is finite with exactly k elements, which is clause 1.

L2L5step 1.1
3.1

For clause 2, first compute the weight. Reordering the positions is a permutation of the index set, so by the permutation clause of [L3] the weight of a equals the weight of the word b whose first p letters are 1 and whose remaining n letters are μ; the splitting clause of [L3] gives b=i<p1+j<n(μ), and induction with the finite-sum clause of [F1] evaluates a sum of p copies of 1 as p and a sum of n copies of μ as μn; hence a=pμn. Each letter is at most 1, since 11 and μ1 for μ0, so if pμn1 then clause 1 applies with k=pμn and gives clause 2.

F1L3L4step 2.1

Remarks

Depends on

Used by

Dependency tree · two levels

44 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