TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck pass

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.

Forward mode computes the exact directional derivative of the real-arithmetic graph

Statement

Let $f : Ω \to R$ be the output of a finite $C^{1}$ program on a fixed strict branch. For every admissible $x \in Ω$ and direction $v \in R^{n}$ , the forward-mode algorithm returns $D f (x) v$ .

Facts & Assumptions

Given: The graph, admissible input, fixed strict branch, and direction $v$ .

[F1]

Finite straight-line computational programs and real-arithmetic tapes: each operation node is a primitive applied to its earlier parent values; the scalar output is either an input coordinate or an operation value.

[F2]

A finite straight-line C1 program defines a C1 map on each fixed strict branch: every node is $C^{1}$ on the fixed branch, with derivative given by the chain rule through its parents.

[F3]

Forward-mode automatic differentiation on a finite computational graph: input tangents are $v_{i}$ , and each node tangent is the local derivative applied to its parent tangents.

[F4]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : $D (g \circ h) (x) = D g (h (x)) D h (x)$ under the stated finite-dimensional differentiability hypotheses.

Proof

technique · induction on the topological order

1.1F1F3givenalgebra

For each input coordinate map $x \mapsto x_{i}$ , its directional derivative in direction $v$ is $v_{i}$ , exactly the initialized tangent in [F3].

2.1F1F2F3F4step 1.1algebra

Suppose the tangent at every parent of node $j$ equals the derivative of that parent value in direction $v$ . The node map is the composition of its primitive with the tuple of parent maps. By [F2] and [F4], its directional derivative is $D ϕ_{j}$ applied to that parent-direction tuple, which is exactly the tangent assigned by [F3]. Finite induction proves this identity for every node.

3.1F1step 1.1step 2.1∎

If $o$ is an operation node, step 2.1 gives ${\dot{z}}_{o} = D f (x) v$ . If $o$ is input coordinate $i$ , then $f (x) = x_{i}$ and step 1.1 gives the returned tangent ${\dot{x}}_{i} = v_{i} = D f (x) v$ . Thus in either case the algorithm returns the asserted directional derivative.

Depends on

Used by

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

MIT OpenCourseWare 18.S096, Matrix Calculus for Machine Learning and Beyond, complete lecture notes, Chapter 8 §§8.3–8.4.1 (standard reference, not scraped)