§2, (1.10) — the equidistant locus is a sphere having $L_r$ as its axis

Proved

RelaxationMethod.LowDim.axisSphere_eq

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

affine-subspaceorthogonal-projectionp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1sphere

Let $L$ be a nonempty flat of $E_n$ with direction space $V$ , and let $p \notin L$ . Let $b$ be the orthogonal projection of $p$ onto $L$ and $X = \{x : |x - a| = |p - a| \text{ for every } a \in L\}$ the locus (1.10). Then:

$X$ is the sphere, inside the flat through $b$ normal to $L$ , with centre $b$ passing through $p$ :

X = \{x : x - b \in V^{\perp},\ |x - b| = |p - b|\};

$L$ is exactly the set of points equidistant from all points of $X$ :

L = \{a : |x - a| = |p - a| \text{ for every } x \in X\}.

This is the claim of §2 that justifies calling $X$ a spherical surface $S_{n-r-1}$ with axis $L$ ; it identifies the set on which Theorem 2, Case 2 places the tail of a reflexion sequence.

Formalization Note The flat is an arbitrary nonempty AffineSubspace ℝ (EuclideanSpace ℝ (Fin n)); the paper's $0 \leqslant r \leqslant n-1$ follows from $p \notin L$ . The orthogonal projection is Mathlib's EuclideanGeometry.orthogonalProjection, and "the $(n-r)$ -flat normal to $L_r$ at $b$ " is written as $x - b \in V^{\perp}$ . The dimension count $n - r - 1$ of the sphere is not part of the statement.

Preamble

import Mathlib
import Definitions.Def_RelaxationMethod_LowDim_AxisSphere

Formal statement

namespace RelaxationMethod.LowDim

/-- §2, p. 395: for a flat `L` and a point `p ∉ L`, with `b` the orthogonal projection of `p`
onto `L`, the locus (1.10) is the sphere of the flat through `b` normal to `L`, centred at `b`
and passing through `p`; and `L` is exactly the set of points equidistant from all points of
that sphere. -/
theorem axisSphere_eq {n : ℕ} (L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin n))) [Nonempty L]
    (p : EuclideanSpace ℝ (Fin n)) (hp : p ∉ L) :
    axisSphere L p =
        {x | x -ᵥ (EuclideanGeometry.orthogonalProjection L p : EuclideanSpace ℝ (Fin n)) ∈
              L.directionᗮ ∧
            dist x (EuclideanGeometry.orthogonalProjection L p : EuclideanSpace ℝ (Fin n)) =
              dist p (EuclideanGeometry.orthogonalProjection L p : EuclideanSpace ℝ (Fin n))} ∧
      (L : Set (EuclideanSpace ℝ (Fin n))) =
        {a | ∀ x ∈ axisSphere L p, dist x a = dist p a} := 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. 395, §2, (1.10)

Read-back

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

Setting. Work in $\mathbb{R}^n$ with Euclidean distance.

$L$ is a nonempty affine subspace of $\mathbb{R}^n$ , with direction (linear subspace) $\vec L$ .
$p\in\mathbb{R}^n$ is a point with $p\notin L$ .
$b$ is the orthogonal projection of $p$ onto $L$ .
For any affine subspace $M$ and point $c$ , write

S(M,c)=\{x: |x-a|=|c-a|\ \forall a\in M\}.

Claim. Both of the following hold.

The locus is a sphere in the normal flat through $b$ :

S(L,p)=\{x\in\mathbb{R}^n : x-b\in \vec L^{\perp}\ \text{ and }\ |x-b|=|p-b|\}.

This is the set of points $x$ such that $x-b$ is orthogonal to every direction vector of $L$ , and $x$ is at the same distance from $b$ as $p$ is. 2. $L$ can be recovered from the locus:

L=\{a\in\mathbb{R}^n : |x-a|=|p-a| \text{ for every } x\in S(L,p)\}.

Degenerate cases:

$L=\mathbb{R}^n$ is impossible. The hypothesis $p\notin L$ rules it out, so in particular $n\ge 1$ .
$L$ empty is excluded by hypothesis.
$L$ a single point $\{b\}$ . Then $\vec L=\{0\}$ and $\vec L^\perp=\mathbb{R}^n$ , so the right side of part 1 is the full sphere of radius $|p-b|>0$ about $b$ .
$L$ a hyperplane. $\vec L^\perp$ is a line, so the right side of part 1 consists of exactly two points.

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

§2, (1.10) — the equidistant locus is a sphere having LrL_rLr​ as its axis

§2, (1.10) — the equidistant locus is a sphere having $L_r$ as its axis