Math and TheoryPeriodic obstructions to small-extrapolation Chambolle–Pock
Problem and result
- Problem
- Small-extrapolation convergence region of the Chambolle–Pock (PDHG) method
- Posed in
- Left open in the conclusion of Upadhyaya, arXiv:2604.06423v2 (improving the small-θ region)
- Status
- Counterexample
- Result
- For unmodified Chambolle–Pock, every step product κ = τσ‖L‖² > 2 admits polytopes in ℝ⁴ with periodic nonconvergent iterates for all small θ ≥ 0, so any universal condition κ < c(θ) has limsup c(θ) ≤ 2 as θ ↓ 0.
Abstract
For the unmodified primal-first Chambolle–Pock iteration with extrapolation θ and step product κ = τσ‖L‖², every κ > 2 admits fixed compact polytopes in R⁴ whose iteration cycles without converging for all sufficiently small θ ≥ 0. Any universal sufficient condition κ < c(θ) therefore satisfies limsup c(θ) ≤ 2 as θ ↓ 0, while bilinear and quadratic problems allow κ < 4/(1+2θ). A nonconstant three-cycle of actual proximal updates exists exactly when κ²(1+θ)² − 2κ(1+3θ) − 3 ≥ 0, attained by compact triangles, and a rational seven-cycle has an open set of nonconvergent starting points. The obstructing θ-intervals are very small and the bound two is not shown to be sharp.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Optimization
- Subject
- Optimization
- Result type
- Counterexample families, exact threshold and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
chambolle-pock-cycles- Keywords
- Chambolle–Pock, Chambolle-Pock, PDHG, primal-dual hybrid gradient, extrapolation parameter, periodic orbits
Statement and scope
Formal scope. The universal three-cycle threshold and its attainment, the seven-cycle with its open basin, the four-dimensional family for every κ > 2 and the quadratic eigenmode comparison are formalized in 21 Lean modules. The limsup consequence, numerical observations of larger θ-intervals and basin sizes, and the finite-dimensional matrix-convergence bridge are conventional or observational.
A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.
Manuscript
- PDF on this site
manuscript.pdf347 KB- PDF on GitHub
papers/mathematics/ chambolle-pock-cycles/ manuscript.pdf - LaTeX source
papers/mathematics/ chambolle-pock-cycles/ manuscript.tex
Formal proof
This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.
- Proof package
papers/mathematics/ chambolle-pock-cycles/ - Lean project
papers/22 Lean filesmathematics/ chambolle-pock-cycles/ lean/ - Lakefile
papers/mathematics/ chambolle-pock-cycles/ lean/ lakefile.lean - Toolchain
leanprover/lean4:v4.19.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
lake exe cache get
python3 verify_lean.py --mathlib .lake/packages/mathlib --output ../verification-replaypython3 exact_certificate/verify_period7.py- README
papers/mathematics/ chambolle-pock-cycles/ README.md - Verification guide
papers/mathematics/ chambolle-pock-cycles/ verification/ README.md - Verification record
papers/mathematics/ chambolle-pock-cycles/ VERIFICATION.md - Authorship
papers/mathematics/ chambolle-pock-cycles/ AUTHORSHIP.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Questions and answers
Does Chambolle–Pock converge at small extrapolation θ for all step products below 4/(1+2θ)?
Not for all convex problems. For every fixed κ = τσ‖L‖² > 2 the preprint builds compact polytopes in ℝ⁴ on which the unmodified Chambolle–Pock iteration has a nonconstant periodic, nonconvergent orbit for all 0 ≤ θ ≤ ε, so any universal sufficient condition κ < c(θ) must satisfy limsup c(θ) ≤ 2 as θ ↓ 0. The obstructing θ-intervals are very small, and the bound 2 is not shown to be sharp.
What else is proved, and how does it relate to known convergence results?
A nonconstant three-cycle of actual proximal updates exists exactly when κ²(1+θ)² − 2κ(1+3θ) − 3 ≥ 0, and a rational seven-cycle on 2.499 ≤ κ ≤ 2.501, 0 ≤ θ ≤ 1/400 has an open set of nonconvergent starts. These results do not contradict the convergence theorems of Banert, Upadhyaya and Giselsson (θ > 1/2, κ < 4/(1+2θ)) or Upadhyaya's small-θ sufficient condition; the full small-θ convergence region remains open.
Is the proof formally verified?
The three-cycle threshold and its attainment, the seven-cycle with its open basin, the four-dimensional family for every κ > 2 and the quadratic eigenmode comparison are formalized in 21 Lean 4 modules. The limsup consequence and the numerical observations of larger θ-intervals and basin sizes are conventional or observational.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@misc{goyal2026chambollepockcycles,
author = {Goyal, Dev D.},
title = {Periodic Obstructions to Small-Extrapolation {Chambolle--Pock}},
year = {2026},
month = oct,
note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/chambolle-pock-cycles}
}