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.
A total derivative computes every directional derivative, and its matrix is the Jacobian
Statement
If is totally differentiable at , then exists for every and equals . In particular , and the matrix of is .
Facts & Assumptions
Given: A total derivative and a direction .
The total-derivative definition supplies the normwise remainder estimate for every ; in positive source dimension this is equivalently the normalized remainder tending to zero as tends to zero (The total (Fréchet) derivative as the linear first-order approximation with remainder).
The directional derivative is the derivative of at zero, and partial derivatives use standard-basis directions (Directional derivatives and partial derivatives of a map ).
Proof
If , the line map has only the zero value, so its directional derivative is the zero vector by the zero-target case of [L2], and this is . Every column identity then has zero rows. The case of a zero-dimensional source has only and no partial directions; it is covered by the zero-direction argument below. For the remaining nonzero-direction argument assume .
If , then for every , so [L2] gives . For the remaining case assume . For sufficiently small , openness of gives and . Write , where by [L1].
Dividing by gives , and ; hence [L2] yields .
Taking identifies the th column of the matrix of with the vector of th partial derivatives, which is precisely the Jacobian.