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.
Directional derivatives and partial derivatives of a map
Definition
Let , , , and . If the line map is defined near , its derivative at is the directional derivative
For a standard basis vector (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension ), is the th partial derivative, written . For , these are ordinary vector-valued one-variable derivatives in the sense of The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral.
For , use the zero-space case directly, without invoking that supplier's positive-codomain standing hypothesis. The space has only its zero vector and carries the zero Euclidean norm and its induced metric (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension clause 5, The Euclidean inner product on , A norm on a real vector space, the induced metric, and the dictionary with the metric axioms). Whenever the line map is defined near , every difference quotient for real is this zero vector; define . This is the unique possible derivative value, and its normwise difference-quotient error is exactly zero for all such , so the real parameter still approaches an actual limit point. Every existing coordinate direction therefore has ; these zero-valued partial maps are continuous in the induced norm metrics. If the source dimension is zero, there are no partial indices and the sole direction is ; its constant line map is defined near .
Depends on
The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral
Vector-valued functions , their limits and continuity, with the dictionary to the metric notions
The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension
The Euclidean inner product on
A norm on a real vector space, the induced metric, and the dictionary with the metric axioms