§5 — the limit of an infinite relaxation sequence lies on the boundary of $A$

Proved

RelaxationMethod.FullDim.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 in $E_n$ and let $0 < \lambda \le 2$ . Let $p_0, p_1, \dots$ be a run of the relaxation process with parameter $\lambda$ that never terminates ( $p_\nu \notin A$ for all $\nu$ ). If

\lim_{\nu\to\infty} p_\nu = l ,

then $l$ belongs to the boundary of $A$ : $l \in A$ , and $l$ is not an interior point of $A$ .

Together with Lemma 1 this completes the proof of Theorem 1, Case 1, and it is the second step of the proof of Theorem 1, Case 2.

Formalization Note The paper proves this in §5 for $0 < \lambda < 2$ and uses the same argument in §6 for $\lambda = 2$ ; we state it for $0 < \lambda \le 2$ . No dimension hypothesis is needed. "Boundary" is the topological frontier frontier A; since $A$ is closed this means $l \in A \setminus \operatorname{int} A$ . The parameter $\lambda$ is named lam.

Preamble

import Mathlib
import Definitions.Def_RelaxationMethod_FullDim_RelaxStep
import Definitions.Def_RelaxationMethod_FullDim_FejerMonotone
open Filter Topology

Formal statement

namespace RelaxationMethod.FullDim

/-- §5, p. 399 (reused in §6): if an infinite run of the relaxation process with `0 < lam ≤ 2`
converges to `l`, then `l` lies on the boundary of the nonempty polytope `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 : IsRelaxRun a b lam p)
    (hinf : ∀ ν : ℕ, p ν ∉ polytope a b) (l : EuclideanSpace ℝ (Fin n))
    (hl : Tendsto p atTop (𝓝 l)) :
    l ∈ frontier (polytope a b) := by sorry

end RelaxationMethod.FullDim

Source

Motzkin and Schoenberg, The relaxation method for linear inequalities, Canad. J. Math. 6 (1954), p. 399, §5, (2.10)–(2.11), and §6

Read-back

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

Fix natural numbers $n$ and $m$ . Take vectors $a_0,\dots,a_{m-1}\in\mathbb{R}^n$ and reals $b_0,\dots,b_{m-1}$ . Let $H_i=\{x:\langle a_i,x\rangle+b_i\ge 0\}$ and $A=\bigcap_{i<m}H_i$ .

Hypotheses:

$A$ is nonempty.
$\lambda$ is a real number with $0<\lambda\le 2$ .
$p_0,p_1,\dots$ is a relaxation run with parameter $\lambda$ . That is, whenever $p_\nu\notin A$ , there is an index $j$ with $d(p_\nu,H_i)\le d(p_\nu,H_j)$ for all $i$ , and a point $q\in H_j$ with $|p_\nu-q|=d(p_\nu,H_j)$ , such that $p_{\nu+1}=p_\nu+\lambda(q-p_\nu)$ . Here $d$ is the infimum distance, taken as $0$ to an empty set.
$p_\nu\notin A$ for every $\nu$ .
$l\in\mathbb{R}^n$ and $p_\nu\to l$ .

Conclusion. $l$ lies in the topological boundary of $A$ :

l\in\overline{A}\setminus\operatorname{int}A ,

where $\overline{A}$ is the closure of $A$ and $\operatorname{int}A$ its interior. No assumption is made on the dimension of $A$ . If $A$ has empty interior, the conclusion just says that $l$ is in the closure of $A$ .

Degenerate cases:

$m=0$ : $A=\mathbb{R}^n$ , so the hypothesis that every $p_\nu\notin A$ cannot hold and the statement is vacuous.
$n=0$ : A nonempty $A$ is the whole one-point space, so again 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

§5 — the limit of an infinite relaxation sequence lies on the boundary of AAA

§5 — the limit of an infinite relaxation sequence lies on the boundary of $A$