The cycle lemma (Raney / Dvoretzky–Motzkin), sum = 1 case — PROVED

Sorry-free, kernel-axiom-clean (propext, Classical.choice, Quot.sound).

Raney's lemma: any integers summing to 1 have exactly one cyclic shift with all partial sums positive. We formalize it on a period-n sequence a : ℕ → ℤ with period-sum 1, via the partial sums Q k = ∑_{j<k} a j (so Q (k+n) = Q k + 1). A shift i is good iff Q i < Q t for all t ∈ (i, i+n); the unique good i ∈ [0,n) is the last argmin of Q over [0,n). The count #level-canonical = C(N,d-1)/d will follow (a_k = 1 - (level counts)).

def CriticalPortraits.Cycle.Q (a : ℕ → ℤ) (k : ℕ) : ℤ

Partial sums of a.

Equations

• CriticalPortraits.Cycle.Q a k = ∑ j ∈ Finset.range k, a j

theorem CriticalPortraits.Cycle.Q_zero (a : ℕ → ℤ) : Q a 0 = 0

theorem CriticalPortraits.Cycle.Q_succ (a : ℕ → ℤ) (k : ℕ) : Q a (k + 1) = Q a k + a k

theorem CriticalPortraits.Cycle.window_sum {n : ℕ} (a : ℕ → ℤ) (hper : ∀ (k : ℕ), a (k + n) = a k) (k : ℕ) : Q a (k + n) - Q a k = Q a n - Q a 0

A window of length n of a period-n sequence sums to the period sum.

theorem CriticalPortraits.Cycle.Q_periodic {n : ℕ} (a : ℕ → ℤ) (hper : ∀ (k : ℕ), a (k + n) = a k) (hsum : Q a n = 1) (k : ℕ) : Q a (k + n) = Q a k + 1

Periodicity of the partial sums: Q (k+n) = Q k + (period sum).

def CriticalPortraits.Cycle.Good (n : ℕ) (a : ℕ → ℤ) (i : ℕ) : Prop

Shift i is good: every partial sum of the shifted sequence is positive, i.e. Q i is a strict minimum of Q over the half-open window (i, i+n).

Equations

• CriticalPortraits.Cycle.Good n a i = ∀ (t : ℕ), i < t → t < i + n → CriticalPortraits.Cycle.Q a i < CriticalPortraits.Cycle.Q a t

theorem CriticalPortraits.Cycle.cycle_lemma {n : ℕ} (a : ℕ → ℤ) (hn : 0 < n) (hper : ∀ (k : ℕ), a (k + n) = a k) (hsum : Q a n = 1) : ∃! i : ℕ, i < n ∧ Good n a i

The cycle lemma (Raney), sum = 1. For a period-n integer sequence with period-sum 1, exactly one shift i ∈ [0,n) is good. The witness is the last argmin of Q over [0,n).