§1 — a step towards a violated half-space is point-wise closer to $A$ (equality on $\pi_j$ for $\lambda = 2$ )

Proved

RelaxationMethod.FullDim.step_pointwise_closer

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

fejer-monotonep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1relaxation-method

Let $A = \bigcap_{i=1}^m H_i$ be the nonempty solution polytope of a system of linear inequalities $H_i : \langle a_i, x\rangle + b_i \ge 0$ in $E_n$ . Let $p$ be a point with $p \notin H_j$ for some index $j$ , let $q$ be the point of $H_j$ nearest to $p$ (the projection of $p$ on the boundary hyperplane $\pi_j : \langle a_j, x\rangle + b_j = 0$ ), let $0 < \lambda \le 2$ and put $p_1 = p + \lambda (q - p)$ . Then $p_1 \ne p$ and

|p_1 - a| \le |p - a| \qquad \text{for all } a \in A .

If $0 < \lambda < 2$ (so $p_1$ lies strictly between $p$ and the mirror image $p'$ of $p$ in $\pi_j$ ) the inequality is strict for every $a \in A$ : $p_1$ is point-wise closer than $p$ to $A$ in the sense of (1.1). If $\lambda = 2$ (so $p_1 = p'$ ) then, for $a \in A$ , equality $|p_1 - a| = |p - a|$ holds exactly when $a$ lies on $\pi_j$ .

This is the basic monotonicity of the relaxation method: every step, in particular the step (1.5)–(1.7) towards a farthest half-space, moves towards every solution of the system.

Formalization Note The paper states the claim for any violated half-space $H_j$ and a point $p_1$ on the segment from $p$ to $p'$ ; we state it in that generality, with $q$ given as a nearest point of $H_j$ (as in (1.6)), so it applies to every relaxation step (1.5)–(1.7). The claim $p_1 \ne p$ is condition (2.1) of Fejér-monotonicity. For $\lambda = 2$ we state the page's "with the exception that we have the equality sign for the points of $A$ which are on the boundary of $H_j$ " as an equivalence. 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

/-- §1, pp. 393–394: let `p ∉ H_j` for some `j`, let `q` be the point of `H_j` nearest to `p`
(the projection of `p` on the boundary hyperplane `π_j`), and let `p₁ = p + lam (q - p)` with
`0 < lam ≤ 2`. Then `p₁ ≠ p` and `|p₁ - a| ≤ |p - a|` for every `a` of the (nonempty)
polytope `A`. For `0 < lam < 2` the new point `p₁` is point-wise closer than `p` to `A` in the
sense of (1.1). For `lam = 2` (`p₁ = p′`, the mirror image of `p` in `π_j`) (1.1) again holds,
except that equality holds exactly at the points of `A` on the boundary `π_j` of `H_j`. -/
theorem step_pointwise_closer {n m : ℕ} (a : Fin m → EuclideanSpace ℝ (Fin n)) (b : Fin m → ℝ)
    (hA : (polytope a b).Nonempty) (lam : ℝ) (hlam0 : 0 < lam) (hlam2 : lam ≤ 2)
    (p q : EuclideanSpace ℝ (Fin n)) (j : Fin m) (hpj : p ∉ halfSpace (a j) (b j))
    (hq : q ∈ halfSpace (a j) (b j))
    (hpq : dist p q = Metric.infDist p (halfSpace (a j) (b j))) :
    p + lam • (q - p) ≠ p ∧
      (∀ x ∈ polytope a b, dist (p + lam • (q - p)) x ≤ dist p x) ∧
      (lam < 2 → IsPointwiseCloser (polytope a b) p (p + lam • (q - p))) ∧
      (lam = 2 → ∀ x ∈ polytope a b,
        (dist (p + lam • (q - p)) x = dist p x ↔ inner ℝ (a j) x + b j = 0)) := by sorry

end RelaxationMethod.FullDim

Source

Motzkin and Schoenberg, The relaxation method for linear inequalities, Canad. J. Math. 6 (1954), pp. 393–394, §1

Read-back

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

Setting. Let $n, m$ be natural numbers and work in Euclidean space $\mathbb{R}^n$ with the standard inner product $\langle\cdot,\cdot\rangle$ and the Euclidean distance $d(x,y) = \|x - y\|$ . The theorem takes these inputs:

a family of vectors $a_1, \dots, a_m \in \mathbb{R}^n$ , indexed by $\{0, \dots, m-1\}$ ;
real numbers $b_1, \dots, b_m$ ;
a real number $\lambda$ ;
two points $p, q \in \mathbb{R}^n$ ;
an index $j$ .

Three sets or relations come from imported definitions whose code is not shown here, so this read-back cannot unfold them:

$H(a_j, b_j)$ , called halfSpace in the code: a set in $\mathbb{R}^n$ built from $a_j$ and $b_j$ .
$A = \mathrm{polytope}(a, b)$ : a set in $\mathbb{R}^n$ built from the whole families $a$ and $b$ .
$\mathrm{IsPointwiseCloser}(A, p, p_1)$ : a relation between a set and two points, with the arguments in that order.

The names suggest a half-space, an intersection of half-spaces, and " $p_1$ is pointwise closer than $p$ to $A$ ". The exact inequality direction, the sign convention for $b_j$ , and whether the inequalities are strict are fixed only in those unseen definitions.

Hypotheses.

$A$ is nonempty.
$0 < \lambda \le 2$ .
$p \notin H(a_j, b_j)$ .
$q \in H(a_j, b_j)$ .
$d(p, q) = \inf_{y \in H(a_j,b_j)} d(p, y)$ . So $q$ is a point of $H(a_j,b_j)$ that attains the distance from $p$ to that set. Uniqueness of $q$ is not assumed, only that it attains the infimum.

Conclusion. Let $p_1 = p + \lambda (q - p)$ . The theorem asserts all four of the following:

$p_1 \neq p$ .
For every $x \in A$ :

d(p_1, x) \le d(p, x).

If $\lambda < 2$ , then $\mathrm{IsPointwiseCloser}(A, p, p_1)$ holds, whatever that unseen definition says.
If $\lambda = 2$ , then for every $x \in A$ :

d(p_1, x) = d(p, x) \iff \langle a_j, x\rangle + b_j = 0.

The equality condition is exactly $\langle a_j, x\rangle + b_j = 0$ , with $+b_j$ . Whether this set is the boundary of $H(a_j,b_j)$ depends on the unseen definition of $H$ .

Degenerate cases.

$m = 0$ : there is no index $j$ , so the statement is vacuous.
$n = 0$ : $\mathbb{R}^0$ has one point, so $p = q$ . Hypotheses 3 and 4 then contradict each other and the statement is vacuous.
$H(a_j, b_j)$ is empty: no $q$ satisfies hypothesis 4, so the statement is vacuous. (For an empty set the infimum in hypothesis 5 would default to $0$ , but this cannot arise here.)
$H(a_j, b_j)$ is all of $\mathbb{R}^n$ : hypothesis 3 fails, so the statement is vacuous. If $H(a_j,b_j)$ is defined by an affine inequality in $\langle a_j, x\rangle$ and $b_j$ , then $a_j = 0$ makes it either empty or everything, so $a_j = 0$ is vacuous as well.
$\lambda$ : it ranges only over $(0,2]$ . At $\lambda = 2$ the third conclusion is vacuous and only the equality characterization adds anything. For $\lambda < 2$ the fourth conclusion is vacuous.
Nonemptiness of $A$ : it is assumed, not derived. Whether $A$ can actually be nonempty for given $a, b$ depends on the unseen definition of polytope.

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

§1 — a step towards a violated half-space is point-wise closer to AAA (equality on πj\pi_jπj​ for λ=2\lambda = 2λ=2)

§1 — a step towards a violated half-space is point-wise closer to $A$ (equality on $\pi_j$ for $\lambda = 2$ )