Single-jump cumulation

This file proves the binomial cumulation bound for the abstract damped ladder Lean4LPD.Ladder, formalizing part (i) of apd:cor:norm_cumulation_jump:

N_{≥m}^{(g)} ≤ C(g, m) · sin^m(dt) · ‖O‖.

The proof follows the paper's: an induction over m whose inner step iterates the flow recursion over g and closes with the hockey-stick identity (sum_range_choose_real).

The base case is the reservoir bound N_{≥0}^{(l)} ≤ ‖O‖. Unitary invariance of the 2-norm gives it at every l, not only at l = 0, so the induction hypothesis and the conclusion have the same shape.

Main results

• Ladder.step_iterate: the flow recursion summed over the g steps.
• Ladder.cumulation: N m g ≤ C(g, m) · a^m · M.

theorem Lean4LPD.Ladder.step_iterate {a M : ℝ} (L : Ladder a M) {m : ℕ} (hm : 1 ≤ m) (g : ℕ) : L.N m g ≤ a * ∑ l ∈ Finset.range g, L.N (m - 1) l

Iterating the flow recursion over the g steps, using N m 0 = 0 for m ≥ 1 to kill the boundary term. This is the display N^{(g)}_{≥m} ≤ sin(dt) ∑_{l=0}^{g-1} N^{(l)}_{≥m-1} in the proof of apd:cor:norm_cumulation_jump.

Note this needs no sign hypothesis on the damping factor a: the paper states the recursion with a = sin(dt) ≥ 0, but the iteration itself is monotone regardless.

theorem Lean4LPD.Ladder.cumulation {a M : ℝ} (L : Ladder a M) (ha : 0 ≤ a) (m g : ℕ) : L.N m g ≤ ↑(g.choose m) * a ^ m * M

Single-jump cumulation. Formalizes apd:cor:norm_cumulation_jump (i): after any g Pauli rotations,

N_{≥m}^{(g)} ≤ C(g, m) · a^m · M,

where a = sin(dt) is the damping factor and M = ‖O‖_{2,normalized}.

The total mass enters with coefficient one: the base case m = 0 is the reservoir bound N 0 g ≤ M, valid for every g. The only sign hypothesis is 0 ≤ a, used to multiply the inductive hypothesis through the recursion.