Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-02
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 for a regular graph constraint y=ψ(x)

Statement

Let V⊆Rm and W⊆Rm+n be open, let x0∈V, let ψ:V→Rn be differentiable at x0, put a=(x0,ψ(x0))∈W, and let f:W→R be differentiable at a. If f∣W∩graph⁡(ψ) has a local extremum at a, then for G:V×Rn→Rn given by G(x,y)=y−ψ(x) there is λ∈Rn such that ∇f(a)=DG(a)Tλ.

Facts & Assumptions

Given: The hypotheses of the statement.

[L1]

A constrained local extremum annihilates every tangent velocity of a differentiable parametrization (A constrained local extremum annihilates every velocity of a differentiable parametrization).

Proof

technique · direct
1.1

Parametrize the graph by Γ(x)=(x,ψ(x)). Since ψ is differentiable at x0, Γ is continuous there; because V and W are open, for every v∈Rm the curve t↦Γ(x0+tv) is defined and lies in W for sufficiently small t. Apply [L1] to get Df(a)(v,Dψ(x0)v)=0.

L1givenalgebra
2.1

In block gradient coordinates, step 1.1 says ∇xf(a)+Dψ(x0)T∇yf(a)=0.

step 1.1L2algebra
3.1

Set λ=∇yf(a). Since DG(a)=(−Dψ(x0),In), step 2.1 yields DG(a)Tλ=(∇xf(a),∇yf(a))=∇f(a).

step 2.1L2algebra∎

Depends on

Used by

Dependency tree · two levels

11 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