Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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)y=\psi(x)

Statement

Let V⊆RmV\subseteq\mathbb R^m and W⊆Rm+nW\subseteq\mathbb R^{m+n} be open, let x0∈Vx_0\in V, let ψ:V→Rn\psi:V\to\mathbb R^n be differentiable at x0x_0, put a=(x0,ψ(x0))∈Wa=(x_0,\psi(x_0))\in W, and let f:W→Rf:W\to\mathbb R be differentiable at aa. If f∣W∩graph⁡(ψ)f|_{W\cap\operatorname{graph}(\psi)} has a local extremum at aa, then for G:V×Rn→RnG:V\times\mathbb R^n\to\mathbb R^n given by G(x,y)=y−ψ(x)G(x,y)=y-\psi(x) there is λ∈Rn\lambda\in\mathbb R^n such that ∇f(a)=DG(a)Tλ\nabla f(a)=DG(a)^T\lambda.

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).

[L2]

The gradient represents the derivative and the Jacobian records the derivative in coordinates (For a differentiable scalar field, Dvf(a)=⟨∇f(a),v⟩D_vf(a)=\langle\nabla f(a),v\rangle and the unit direction of steepest ascent is the normalized gradient, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

Proof

technique · direct
1.1

Parametrize the graph by Γ(x)=(x,ψ(x))\Gamma(x)=(x,\psi(x)). Since ψ\psi is differentiable at x0x_0, Γ\Gamma is continuous there; because VV and WW are open, for every v∈Rmv\in\mathbb R^m the curve t↦Γ(x0+tv)t\mapsto\Gamma(x_0+tv) is defined and lies in WW for sufficiently small tt. Apply [L1] to get Df(a)(v,Dψ(x0)v)=0Df(a)(v,D\psi(x_0)v)=0.

L1givenalgebra
2.1

In block gradient coordinates, step 1.1 says ∇xf(a)+Dψ(x0)T∇yf(a)=0\nabla_xf(a)+D\psi(x_0)^T\nabla_yf(a)=0.

step 1.1L2algebra
3.1

Set λ=∇yf(a)\lambda=\nabla_yf(a). Since DG(a)=(−Dψ(x0),In)DG(a)=(-D\psi(x_0),I_n), step 2.1 yields DG(a)Tλ=(∇xf(a),∇yf(a))=∇f(a)DG(a)^T\lambda=(\nabla_xf(a),\nabla_yf(a))=\nabla f(a).

step 2.1L2algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 59 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources