TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-21

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A point outside a nonempty closed convex set is strictly separated from it

Statement

Let $n \geq 1$ , let $C \subseteq R^{n}$ be nonempty, closed, and convex, and let $x \notin C$ . Then there are $a \neq 0$ and $b \in R$ such that $⟨ a, z ⟩ \leq b < ⟨ a, x ⟩$ for every $z \in C$ . Thus a hyperplane strictly separates $x$ from $C$ (Supporting and strictly separating hyperplanes in Euclidean space).

Statement references

Supporting and strictly separating hyperplanes in Euclidean space

Facts & Assumptions

Given: The set and exterior point in the Statement; since $C$ is closed, the nearest point cannot equal $x$ (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

[L1]

If $p$ is the projection of $x$ onto $C$ , then $⟨ x - p, z - p ⟩ \leq 0 (z \in C) .$ (Metric projection onto a closed convex set satisfies the variational inequality)

[L2]

Every point of $R^{n}$ has a unique nearest point in a nonempty closed convex subset of $R^{n}$ (Every point has a unique nearest point in a nonempty closed Euclidean convex set).

Proof

technique · direct

1.1L1L2givenalgebra

Let $p$ be the nearest point supplied by [L2] and put $a = x - p$ . By [L1], $⟨ a, z ⟩ \leq ⟨ a, p ⟩$ for every $z \in C$ . Since $x \notin C$ , one has $a \neq 0$ and $⟨ a, x ⟩ = ⟨ a, p ⟩ + ∥ a ∥_{2}^{2} > ⟨ a, p ⟩ .$

2.1step 1.1∎

Taking $b = ⟨ a, p ⟩$ in step 1.1 gives the stated strict separation with a nonzero normal.

Depends on

Dependency tree · 2 levels

Sources

S. Boyd and L. Vandenberghe, Convex Optimization, §2.5.1