LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)

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.

Second-order curvature tests on an affine feasible slice

Statement

Let $d \geq 0$ and $k \geq 0$ be integers, let $U \subseteq R^{d}$ be open and convex, let $A : R^{d} \to R^{k}$ be linear, let $b \in R^{k}$ , and let $x_{*} \in U$ satisfy $A x_{*} = b$ . Put $T = \ker A$ . Assume $f : U \to R$ is differentiable and has second directional derivatives represented by a continuous matrix field: there is a continuous map $H : U \to R^{d \times d}$ with symmetric values, and for every $x \in U$ and $h \in R^{d}$ ,

${\frac{d^{2}}{d t^{2}} f (x + t h) ∣}_{t = 0} = Q_{x} (h) : = h^{T} H (x) h .$

Assume stationarity $D f (x_{*}) h = 0$ for every $h \in T$ . If $Q_{x_{*}} (h_{0}) < 0$ for some $h_{0} \in T$ , then $x_{*}$ is not a local minimum of $f$ on ${x \in U : A x = b}$ . If $Q_{x_{*}} (h) > 0$ for every nonzero $h \in T$ , then $x_{*}$ is a strict local minimum on that feasible slice. If $T = {0}$ , the latter conclusion holds because $x_{*}$ is the only feasible point.

Facts & Assumptions

Given: The open convex domain, linear constraint, differentiable function, continuous symmetric matrix field, directional second-derivative identity, and stationarity in the Statement.

[F1]

A convex subset of $R^{m}$ contains every line segment between two of its points: the segment between two points of a convex set stays in that set.

[L1]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the Euclidean norm is $∥ h ∥_{2} = \sqrt{⟨ h, h ⟩}$ .

[L2]

Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ and The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement: $A$ is continuous and $T = A^{- 1} ({0})$ is closed.

[L3]

Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line: every closed bounded subset of $R^{d}$ is compact.

[L4]

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value: a continuous real function on a nonempty compact set attains its minimum.

[L5]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : if a real function is continuous on a closed interval and differentiable inside it, some interior derivative equals its endpoint secant slope.

Proof

technique · direct

1.1givenL1algebra

If $d = 0$ , then $R^{0}$ has only its zero vector, $U = {x_{*}}$ , and $T = {0}$ . There is no negative-curvature direction and $x_{*}$ is the only feasible point, so the strict-minimum conclusion holds. In the remaining argument suppose $d \geq 1$ . Suppose $h_{0} \in T$ and $Q_{x_{*}} (h_{0}) < 0$ . Set $ϕ (t) = f (x_{*} + t h_{0})$ for $t$ near $0$ . Openness of $U$ permits this definition; stationarity gives $ϕ^{'} (0) = 0$ . The identity in the Statement gives $ϕ^{''} (t) = Q_{x_{*} + t h_{0}} (h_{0})$ wherever defined, and continuity of the entries of $H$ makes this negative for every sufficiently small $t \geq 0$ .

1.2L1L2L3L4given

Suppose $T \neq {0}$ and $Q_{x_{*}} (h) > 0$ for each nonzero $h \in T$ . The unit sphere $S_{T} = {h \in T : ∥ h ∥_{2} = 1}$ is nonempty, closed by [L2] and continuity of the norm, and bounded; [L3] makes it compact. The quadratic polynomial $h \mapsto h^{T} H (x_{*}) h$ is continuous, so [L4] gives $λ = \min_{h \in S_{T}} Q_{x_{*}} (h) > 0$ .

2.1L5step 1.1algebra

Choose such a small $t > 0$ . Applying [L5] to $ϕ^{'}$ on $[0, t]$ gives $ϕ^{'} (t) - ϕ^{'} (0) = t ϕ^{''} (s) < 0$ for some $s \in (0, t)$ , hence $ϕ^{'} (t) < 0$ ; the same argument applies to every positive endpoint up to $t$ . Applying [L5] to $ϕ$ on $[0, t]$ gives $ϕ (t) - ϕ (0) = t ϕ^{'} (r) < 0$ for some $r \in (0, t)$ . Since $h_{0} \in \ker A$ , $x_{*} + t h_{0}$ is feasible, so $x_{*}$ is not a local minimum.

2.2F1L1step 1.2givenalgebra

By continuity of the finitely many entries of $H$ , choose $δ > 0$ so that $∥ x - x_{*} ∥_{2} < δ$ implies $∣ Q_{x} (h) - Q_{x_{*}} (h) ∣ < λ / 2$ for every unit vector $h$ : expand the difference as a finite sum of entry differences times $h_{i} h_{j}$ , each with $∣ h_{i} h_{j} ∣ \leq 1$ . If $y \neq x_{*}$ is feasible and $∥ y - x_{*} ∥_{2} < δ$ , put $v = y - x_{*}$ . Then $v \in T$ , and convexity of $U$ keeps $x_{*} + t v$ in $U$ for $0 \leq t \leq 1$ . For $ϕ (t) = f (x_{*} + t v)$ , stationarity gives $ϕ^{'} (0) = 0$ , while homogeneity of the quadratic form gives $ϕ^{''} (t) = Q_{x_{*} + t v} (v) \geq (λ / 2) ∥ v ∥_{2}^{2} > 0$ .

3.1L5step 2.2algebra∎

For any $t \in (0, 1]$ , [L5] applied to $ϕ^{'}$ on $[0, t]$ yields $ϕ^{'} (t) - ϕ^{'} (0) = t ϕ^{''} (s) > 0$ for some $s \in (0, t)$ , so $ϕ^{'} (t) > 0$ . Applying [L5] to $ϕ$ on $[0, 1]$ gives $ϕ (1) - ϕ (0) = ϕ^{'} (r) > 0$ for some $r \in (0, 1)$ . Thus every distinct feasible $y$ with $∥ y - x_{*} ∥_{2} < δ$ has $f (y) > f (x_{*})$ . If $T = {0}$ , $A y = A x_{*}$ implies $y - x_{*} \in T = {0}$ , so $x_{*}$ is the only feasible point.

Second-order curvature tests on an affine feasible slice

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources