§5 — the limit of a convergent infinite relaxation sequence is a boundary point of $A$

Proved

RelaxationMethod.LowDim.limit_mem_frontier

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

convergencep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1relaxation-method

Let $A$ be the nonempty solution polytope of a system of linear inequalities, let $0 < \lambda \leqslant 2$ , and let $\{p_\nu\}$ be an infinite relaxation sequence (every $p_\nu \notin A$ , each obtained from the previous one by a relaxation step with parameter $\lambda$ ). If $p_\nu \to l$ , then

l \in A \quad\text{and}\quad l \in \partial A.

The argument of §5 uses the function $d(x) = \max_i \operatorname{dist}(x, H_i)$ that vanishes exactly on $A$ . It is invoked in the proof of Theorem 2, Case 1 (§7) and, for $\lambda = 2$ , in §6 and §8.

Formalization Note The paper proves this in §5 for $r = n$ and $0 < \lambda < 2$ ; the argument uses neither assumption, and §7 ( $r < n$ ) and §8 ( $\lambda = 2$ ) reuse it, so it is stated without a dimension hypothesis and for $0 < \lambda \leqslant 2$ . The boundary is the topological frontier.

Preamble

import Mathlib
import Definitions.Def_RelaxationMethod_LowDim_RelaxStep

open Filter Topology

Formal statement

namespace RelaxationMethod.LowDim

/-- §5, p. 399: if an infinite relaxation sequence with `0 < λ ⩽ 2` converges to `l`, then `l`
belongs to `A`, and lies on the boundary of `A`. -/
theorem limit_mem_frontier {n m : ℕ} (a : Fin m → EuclideanSpace ℝ (Fin n)) (b : Fin m → ℝ)
    (hA : (polytope a b).Nonempty) (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) (l : EuclideanSpace ℝ (Fin n))
    (hl : Tendsto p atTop (𝓝 l)) :
    l ∈ polytope a b ∧ l ∈ frontier (polytope a b) := 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. 399, §5, (2.10)–(2.11)

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.
$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$ .
$l$ is a point of $\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\to l$ as $\nu\to\infty$ .

Claim.

l\in A \qquad\text{and}\qquad l\in\partial A.

Here $\partial A$ is the topological boundary of $A$ : the closure of $A$ minus its interior.

Degenerate cases:

$m=0$ . $A=\mathbb{R}^n$ , so the hypothesis $p_\nu\notin A$ cannot hold and the statement is vacuous.
$n=0$ . A nonempty $A$ is the whole one-point space, so the statement is vacuous.
No convergent sequence. If no sequence satisfying the hypotheses converges, the statement is vacuous for all $l$ .

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

§5 — the limit of a convergent infinite relaxation sequence is a boundary point of AAA

§5 — the limit of a convergent infinite relaxation sequence is a boundary point of $A$