Segments halve every two steps

Proved

BlockCycleRotation.seg_add_two_le

by dbenbenn · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

algorithmsblock-cycle-rotationreal-analysis

For $0 \le x \le \tfrac12$ and every $i$ ,

\mathrm{seg}(x,i+2) \le \tfrac12\,\mathrm{seg}(x,i).

The geometric decay driving every convergence argument about $\psi$ : two steps of the recursion at least halve the current segment, so the series defining $\psi$ converges geometrically and the recursion depth needed for a given accuracy is logarithmic. This is what the continuity proof of Theorem 7 rests on.

Preamble

import Definitions.Def_BlockCycleRotation_Buffer
import Mathlib

open BlockCycleRotation
open Finset Filter Topology Real MeasureTheory BoxIntegral
open scoped ENNReal

Formal statement

theorem BlockCycleRotation.seg_add_two_le {x : ℝ} (hx0 : 0 ≤ x) (hx : x ≤ 1 / 2) (i : ℕ) :
    seg x (i + 2) ≤ 1 / 2 * seg x i := by sorry

Source

Valentin Blomer and Kai-Uwe Bux, "The cost of cyclic permutations and remainder sums in the Euclidean algorithm", AofA 2026, LIPIcs vol. 381, pp. 14:1-14:17, doi:10.4230/LIPIcs.AofA.2026.14. Numbering follows the full version, arXiv:2601.00979v1 -- §3. Lean source: https://github.com/dbenbenn/block-cycle-rotation/blob/f69003fd8b00c9b5d6d1a4f6807b4943bce0a92c/BlockCycleRotation/Buffer.lean#L297-L308

View graph