Alphabeta Math
LemmaStatement: 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.

The total derivative at a point is unique

Statement

If L,M:Rm→RnL,M:\mathbb R^m\to\mathbb R^n both satisfy the total-differentiability remainder condition for ff at aa, then L=ML=M.

Facts & Assumptions

Given: Linear maps L,ML,M which both satisfy the definition of total derivative at aa.

[L1]

In the total-derivative definition, the normalized remainder tends to zero as hh tends to zero (The total (Fréchet) derivative Df(a)Df(a) as the linear first-order approximation with o(∥h∥2)o(\|h\|_2) remainder).

Proof

technique · direct
1.1

Subtracting the two remainder identities gives ∥(L−M)h∥2/∥h∥2→0\|(L-M)h\|_2/\|h\|_2\to0 as h→0h\to0.

L1
2.1

For any fixed v∈Rmv\in\mathbb R^m and nonzero real tt, linearity gives ∥(L−M)(tv)∥2/∥tv∥2=∥(L−M)v∥2/∥v∥2\|(L-M)(tv)\|_2/\|tv\|_2=\|(L-M)v\|_2/\|v\|_2 when v≠0v\ne0.

step 1.1algebra
3.1

Letting t→0t\to0 in step 2.1 forces (L−M)v=0(L-M)v=0 for every nonzero vv, and it is also zero at v=0v=0; hence L=ML=M.

step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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