§8 — an infinite reflexion sequence ( $\lambda = 2$ ) does not converge

Proved

RelaxationMethod.LowDim.reflexion_not_tendsto

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

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

Let $A$ be the nonempty solution polytope of a system of linear inequalities, and let $\{p_\nu\}$ be an infinite sequence produced by the reflexion process ( $\lambda = 2$ ): every $p_\nu \notin A$ , and $p_{\nu+1}$ is the mirror image of $p_\nu$ in the boundary of a half-space at maximal distance. Then $\{p_\nu\}$ does not converge.

This is the first step of the proof of Theorem 2, Case 2: a limit would lie in $A$ (§5), and from some index on every reflecting hyperplane would pass through it (§6), so the distance to the limit would stay constant and positive.

Formalization Note §8 assumes $r < n$ throughout, but the argument it cites (§5 and §6) does not use the dimension, so the statement has no dimension hypothesis. For $r = n$ it is also a consequence of Theorem 1, Case 2.

Preamble

import Mathlib
import Definitions.Def_RelaxationMethod_LowDim_RelaxStep

open Filter Topology

Formal statement

namespace RelaxationMethod.LowDim

/-- §8, p. 401 (by §5 and §6): an infinite sequence produced by the reflexion process
(`λ = 2`) does not converge. -/
theorem reflexion_not_tendsto {n m : ℕ} (a : Fin m → EuclideanSpace ℝ (Fin n)) (b : Fin m → ℝ)
    (hA : (polytope a b).Nonempty) (p : ℕ → EuclideanSpace ℝ (Fin n))
    (hrun : ∀ ν, p ν ∉ polytope a b → IsRelaxStep a b 2 (p ν) (p (ν + 1)))
    (hinf : ∀ ν, p ν ∉ polytope a b) :
    ¬ ∃ l, Tendsto p atTop (𝓝 l) := 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. 401, §8 (by §5, p. 399, and §6, p. 399)

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$ .
$(p_\nu)_{\nu\ge0}$ is a sequence in $\mathbb{R}^n$ .

No assumption is made about the dimension of $A$ .

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=2$ $λ = 2$ . 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}=2q-p_\nu$ .

Claim. There is no point $l\in\mathbb{R}^n$ with $p_\nu\to l$ .

Degenerate cases:

$m=0$ . $A=\mathbb{R}^n$ , so the hypotheses cannot be satisfied and the statement is vacuous.
$n=0$ . A nonempty $A$ is the whole one-point space, so 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

§8 — an infinite reflexion sequence (λ=2\lambda = 2λ=2) does not converge

§8 — an infinite reflexion sequence ( $\lambda = 2$ ) does not converge