Math and TheoryA rational five-cycle for two-block ADMM with multiplier step below two
Problem and result
- Problem
- Convergence of two-block ADMM with multiplier (dual) step size τ in (0, 2)
- Posed in
- Question commonly associated with Glowinski; discussed by Tao and Yuan, J. Optim. Theory Appl. 179 (2018)
- Status
- Counterexample
- Result
- For two-block ADMM with penalty one and multiplier-only step τ = 199/100, two explicit compact convex polytopes in ℝ⁴ give a nonconstant period-five orbit with squared primal residual at least 500000, so ADMM fails to converge.
Abstract
An exact period-five orbit for multiplier-only two-block ADMM at step 199/100.
Details
- Year
- 2026
- Discipline
- Mathematics
- Area
- Optimization
- Subject
- Optimization
- Result type
- Standalone theorem and reproducible proof package
- Formal proof
- Standalone Lean package
- Family
admm-counterexample- Keywords
- ADMM, alternating direction method of multipliers, ADMM divergence, periodic orbit, dual step size, counterexample
Statement and scope
Formal scope. Seven modules and eleven endpoint audits cover the orbit, minimizers and optimizer. Analytic regularity of the finite strongly convex extension retains a conventional proof.
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.pdf314 KB- PDF on GitHub
papers/mathematics/ admm-counterexample/ paper/ admm_counterexample.pdf - LaTeX source
papers/mathematics/ admm-counterexample/ paper/ admm_counterexample.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/7 Lean filesmathematics/ admm-counterexample/ - Lakefile
papers/mathematics/ admm-counterexample/ lakefile.toml - Toolchain
leanprover/lean4:v4.19.0 - Library roots
Reproduce
The commands below are quoted from papers/, which gives their context and working directory.
Reproduce with Lake
lake update
lake exe cache get
lake build
lake env lean Research/ADMMCounterexample.lean
lake env lean Research/ADMMHingeTrajectory.leanReproduce using an existing mathlib cache
python3 verify_lean.py \
--mathlib /absolute/path/to/mathlib4 \
--lean /absolute/path/to/lean-4.19.0/bin/leanReproduce using an existing mathlib cache
python3 verify_lean.pyExact arithmetic and optional discovery
python3 verify_admm_five_cycle.py
python3 audits/audit_geometry.py
python3 audits/audit_independent_arithmetic.pyThe same file gives further commands.
- README
papers/mathematics/ admm-counterexample/ README.md - Verification record
papers/mathematics/ admm-counterexample/ VERIFICATION.md - Repository guide
verification/README.md - Unfinished proofs
UNFINISHED.md
Source and prior work
Questions and answers
Does two-block ADMM converge for every dual step size τ in (0, 2)?
Not universally. For the update that scales only the multiplier step, with penalty one, the preprint gives two explicit compact convex polytopes in ℝ⁴, both containing the origin, on which ADMM with τ = 199/100 has a nonconstant five-periodic trajectory whose squared primal residual stays at least 500000. A further exact check, outside the core Lean theorem, gives the same cycle for every τ in [140111/70637, 2).
Does this determine the largest convergent step size?
No. The classical sufficient range 0 < τ < (1+√5)/2 is unaffected, and the result does not show that the golden ratio is the sharp boundary. It concerns only the multiplier-only update, not other overrelaxed ADMM variants, and its relation to the question associated with Glowinski (discussed by Tao and Yuan) is stated with literature limits and no priority claim.
Is the counterexample formally verified?
Yes for the core claims: seven Lean 4 modules with eleven axiom-audited endpoints certify the orbit, the unique projection minimizers over the full convex hulls, the nonvanishing residual and a finite-objective extension with a unique optimizer. The strong convexity, C² regularity and Lipschitz-gradient properties of the smooth extension are proved in the text only.
Cite
Citation file papers/. For the whole collection, use CITATION.cff or CITATION.bib.
@unpublished{Goyal2026ADMMFiveCycle,
author = {Goyal, Dev D.},
title = {A rational five-cycle for two-block ADMM with multiplier step below two},
year = {2026},
note = {Preprint; not peer reviewed}
}