Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22
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 Fréchet derivative is unique

Statement

Let U⊆X be open in a real Banach space X, let f:U→Y map to a real Banach space Y, and let x∈U. If A,B∈B(X,Y) both satisfy the Fréchet remainder condition for f at x, that is

lim⁡h→0h≠0∥f(x+h)−f(x)−Ah∥∥h∥=0andlim⁡h→0h≠0∥f(x+h)−f(x)−Bh∥∥h∥=0,

then A=B.

Facts & Assumptions

Given: An open U in a real Banach space X, a map f:U→Y, a point x∈U, and A,B∈B(X,Y) satisfying the two remainder conditions. Write rA(h):=f(x+h)−f(x)−Ah and rB(h):=f(x+h)−f(x)−Bh.

[L1]

The remainder condition means: for every real ε>0 there is a real δ>0 such that ∥rA(h)∥≤ε∥h∥ and ∥rB(h)∥≤ε∥h∥ whenever ∥h∥<δ and x+h∈U (Fréchet derivative between Banach spaces).

[L2]

The norm satisfies the triangle inequality ∥u+v∥≤∥u∥+∥v∥, absolute homogeneity ∥λu∥=∣λ∣∥u∥ for real λ, and separation ∥u∥=0⇒u=0 (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[L3]

Since U is open and x∈U, there is a real ρ>0 such that x+h∈U whenever ∥h∥<ρ (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).

Proof

technique · direct
1.1L3algebra

Fix v∈X with v≠0; by [L3] there is ρ>0 such that x+h∈U whenever ∥h∥<ρ, so x+tv∈U for every real t with ∣t∣ ∥v∥<ρ, that is for every t with ∣t∣<ρ/∥v∥.

2.1step 1.1L2algebra

For every real t≠0 with ∣t∣<ρ/∥v∥ the two remainders at h=tv satisfy rA(tv)−rB(tv)=−(tAv−tBv), hence t (A−B)v=rB(tv)−rA(tv),∥(A−B)v∥≤∥rA(tv)∥+∥rB(tv)∥∣t∣.

3.1L1step 2.1algebra

For real t with 0<∣t∣<ρ/∥v∥ one has ∥tv∥=∣t∣ ∥v∥, so the right-hand side of [step 2.1] equals ∥v∥(∥rA(tv)∥/∥tv∥+∥rB(tv)∥/∥tv∥), and the two quotients tend to 0 as t→0 by [L1] applied with h=tv, since ∥tv∥→0.

3.2L1step 2.1L2choose

Given a real ε>0, [L1] supplies δ>0 with ∥rA(h)∥≤ε∥h∥ and ∥rB(h)∥≤ε∥h∥ for ∥h∥<δ; applying [step 2.1] to h=tv with 0<∣t∣<min⁡{ρ/∥v∥,δ/∥v∥} gives ∥(A−B)v∥≤2∥v∥ε. As ε>0 was arbitrary, ∥(A−B)v∥=0, and [L2] gives (A−B)v=0.

4.1step 3.2algebra∎

The vector v≠0 was arbitrary, so (A−B)v=0 for every nonzero v; for v=0 linearity of A−B gives (A−B)0=0 as well. Hence A−B=0, that is A=B.

Depends on

Dependency tree · 2 levels

Sources