(3.2) / (3.7) — a non-convergent infinite relaxation sequence has step lengths bounded away from 0

Proved

RelaxationMethod.LowDim.step_length_pos

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1reflexion-methodrelaxation-method

Let $A$ be the nonempty solution polytope, with affine span $L_r \neq E_n$ ( $r < n$ ), let $0 < \lambda \leqslant 2$ , and let $\{p_\nu\}$ be an infinite relaxation sequence with parameter $\lambda$ that does not converge. Then there is $c > 0$ with

|p_{\nu+1} - p_\nu| \geqslant c \qquad (\nu = 0, 1, \dots),

i.e. $\inf_\nu |p_{\nu+1} - p_\nu| > 0$ .

This is claim (a) of the proof of Theorem 2, Case 1, where it leads to a contradiction for $\lambda < 2$ ; for $\lambda = 2$ it is (3.7), a step of the proof of Theorem 2, Case 2.

Formalization Note The paper proves (3.2) under §7's standing assumptions $r < n$ , $0 < \lambda < 2$ , and restates it as (3.7) for $\lambda = 2$ in §8 ("Then (3.2) or (3.7) … again holds"). The statement covers $0 < \lambda \leqslant 2$ . The infimum is over all $\nu$ , as in (3.2).

Preamble

import Mathlib
import Definitions.Def_RelaxationMethod_LowDim_RelaxStep

open Filter Topology

Formal statement

namespace RelaxationMethod.LowDim

/-- (3.2), p. 400, and (3.7), p. 401: if `r < n`, `0 < λ ⩽ 2`, and an infinite relaxation
sequence does not converge, then its step lengths are bounded below by a positive constant,
`inf_ν |p_{ν+1} - p_ν| = c > 0`. -/
theorem step_length_pos {n m : ℕ} (a : Fin m → EuclideanSpace ℝ (Fin n)) (b : Fin m → ℝ)
    (hA : (polytope a b).Nonempty) (hr : affineSpan ℝ (polytope a b) ≠ ⊤)
    (lam : ℝ) (hlam0 : 0 < lam) (hlam2 : lam ≤ 2)
    (p : ℕ → EuclideanSpace ℝ (Fin n))
    (hrun : ∀ ν, p ν ∉ polytope a b → IsRelaxStep a b lam (p ν) (p (ν + 1)))
    (hinf : ∀ ν, p ν ∉ polytope a b) (hdiv : ¬ ∃ l, Tendsto p atTop (𝓝 l)) :
    ∃ c : ℝ, 0 < c ∧ ∀ ν, c ≤ dist (p (ν + 1)) (p ν) := by sorry

end RelaxationMethod.LowDim

Source

Motzkin and Schoenberg, The relaxation method for linear inequalities, Canad. J. Math. 6 (1954), DOI 10.4153/CJM-1954-038-x, p. 400, §7, (3.2); p. 401, §8, (3.7)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. Work in $\mathbb{R}^n$ with the standard inner product.

There are $m$ vectors $a_1,\dots,a_m\in\mathbb{R}^n$ and $m$ reals $b_1,\dots,b_m$ .
Each $i$ gives a half-space $H_i=\{x:\langle a_i,x\rangle+b_i\ge0\}$ .
The polytope is $A=\bigcap_i H_i$ . It is assumed nonempty.
The affine span $\operatorname{aff}(A)$ is assumed not to be all of $\mathbb{R}^n$ .
$d(p,S)$ is the distance from a point to a set, with $d(p,\emptyset)=0$ .
$\lambda$ is a real number with $0<\lambda\le2$ .
$(p_\nu)_{\nu\ge0}$ is a sequence in $\mathbb{R}^n$ .

Hypotheses.

$p_\nu\notin A$ for every $\nu$ .
For every $\nu$ $ν$ , $p_{\nu+1}$ $p_{ν + 1}$ comes from $p_\nu$ $p_{ν}$ by a relaxation step with parameter $\lambda$ $λ$ . This means there is an index $j$ $j$ (it may depend on $\nu$ $ν$ ) such that:
- $d(p_\nu,H_i)\le d(p_\nu,H_j)$ for all $i$ ;
- there is a $q\in H_j$ with $|p_\nu-q|=d(p_\nu,H_j)$ and $p_{\nu+1}=p_\nu+\lambda(q-p_\nu)$ .
$(p_\nu)$ does not converge to any point of $\mathbb{R}^n$ .

Claim. There is a real $c>0$ such that

c\le |p_{\nu+1}-p_\nu|\quad\text{for every } \nu\ge 0.

The claim is only a positive uniform lower bound. It does not assert that $c$ equals the infimum of the step lengths.

Degenerate cases:

$m=0$ gives $A=\mathbb{R}^n$ , which contradicts the hypothesis on $\operatorname{aff}(A)$ (and $p_\nu\notin A$ ), so the statement is vacuous.
$n=0$ makes the affine span of a nonempty set the whole space, so the statement is vacuous.
No non-convergent sequence. If every sequence satisfying the step hypotheses converges, the statement is vacuous.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph