Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedSession-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.

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

Statement

If a scalar-valued f:U→Rf:U\to\mathbb R is totally differentiable at aa, then Dvf(a)=⟨∇f(a),v⟩D_vf(a)=\langle\nabla f(a),v\rangle for every vv. Among unit vectors vv, this is at most ∥∇f(a)∥2\|\nabla f(a)\|_2; if the gradient is nonzero, equality holds exactly in the direction ∇f(a)/∥∇f(a)∥2\nabla f(a)/\|\nabla f(a)\|_2. If the gradient is zero, every unit direction has directional derivative zero.

Facts & Assumptions

Given: A scalar-valued totally differentiable ff at aa and a direction vv.

[L1]

A total derivative computes every directional derivative, and its matrix is the Jacobian (A total derivative computes every directional derivative, and its matrix is the Jacobian).

[L2]

Cauchy--Schwarz: ∣⟨u,v⟩∣≤∥u∥2∥v∥2|\langle u,v\rangle|\le\|u\|_2\|v\|_2 (Cauchy-Schwarz ∣⟨x,y⟩∣≤∥x∥2∥y∥2\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2 with its equality case, the triangle inequality for ∥⋅∥2\lVert\cdot\rVert_2, the parallelogram law and polarisation).

Proof

technique · cases
1.1

By [L1], Dvf(a)D_vf(a) is the Jacobian row applied to vv, namely ∑j∂jf(a)vj=⟨∇f(a),v⟩\sum_j\partial_jf(a)v_j=\langle\nabla f(a),v\rangle.

L1L2
2.1

If ∇f(a)≠0\nabla f(a)\ne0 and ∥v∥2=1\|v\|_2=1, [L2] gives Dvf(a)≤∥∇f(a)∥2D_vf(a)\le\|\nabla f(a)\|_2, with equality at v=∇f(a)/∥∇f(a)∥2v=\nabla f(a)/\|\nabla f(a)\|_2.

assume-case nonzerostep 1.1L2algebra
3.1

If ∇f(a)=0\nabla f(a)=0, step 1.1 makes every directional derivative zero; together with step 2.1 this proves the stated alternatives.

assume-case zerostep 1.1step 2.1cases-exhaustive∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 79 results over 22 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