ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Lagrange multipliers locate the extrema of a linear functional on a sphere

Example

Let $m \geq 1$ , let $R > 0$ , and let $a \in R^{m}$ . On the sphere $∥ x ∥_{2} = R$ , the linear functional $f (x) = ⟨ a, x ⟩$ has maximum $R ∥ a ∥_{2}$ and minimum $- R ∥ a ∥_{2}$ . If $a \neq 0$ , they occur uniquely at $x = R a / ∥ a ∥_{2}$ and $x = - R a / ∥ a ∥_{2}$ respectively; if $a = 0$ , every point is both a maximum and a minimum.

Facts & Assumptions

Given: A natural $m \geq 1$ , the radius $R > 0$ , vector $a \in R^{m}$ , objective $f (x) = ⟨ a, x ⟩$ , and constraint $G (x) = ∥ x ∥_{2}^{2} - R^{2}$ .

[L1]

The sphere constraint is regular, and the one-constraint multiplier rule gives $\nabla f (x) = λ \nabla G (x)$ at every constrained local extremum (A Euclidean sphere is a regular level set with tangent hyperplanes, For one regular constraint, the objective gradient is a scalar multiple of the constraint gradient).

[L2]

Cauchy-Schwarz gives $∣ ⟨ a, x ⟩ ∣ \leq ∥ a ∥_{2} ∥ x ∥_{2}$ , with equality precisely for linearly dependent vectors (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

Verification

technique · direct

1.1givenL1algebra

If $a \neq 0$ , [L1] gives $a = 2 λ x$ . The constraint forces $x = \pm R a / ∥ a ∥_{2}$ , and direct substitution gives the values $\pm R ∥ a ∥_{2}$ .

2.1givenL2

By [L2], every constrained point satisfies $- R ∥ a ∥_{2} \leq f (x) \leq R ∥ a ∥_{2}$ , with equality only at the two points from step 1.1.

3.1step 1.1step 2.1∎

Hence those points are the unique global extrema when $a \neq 0$ . When $a = 0$ , $f$ is identically zero, so every constrained point is both an extremum.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

University of Toronto MAT237 notes, Section 2.8 (standard reference, not scraped)