ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Reverse-mode differentiation of an Euler trajectory tape

Example

Take two explicit Euler updates for $x^{'} = α x$ with step $h = 1 / 2$ , initial state $x_{0} = 1$ , and scalar output $J = x_{2}$ : $x_{k + 1} = x_{k} + h α x_{k}, k = 0, 1.$ At $α = 1$ , the tape has $x_{1} = 3 / 2$ and $x_{2} = 9 / 4$ ; reverse mode returns $d J / d α = 3 / 2$ .

Facts & Assumptions

Given: The two-step Euler graph, $x_{0} = 1$ , $h = 1 / 2$ , $α = 1$ , and output $J = x_{2}$ .

[F1]

Reverse-mode automatic differentiation for a scalar graph output: for each transition, reverse mode applies its local transpose derivative to the incoming cotangent and adds parameter contributions.

[F2]

Reverse mode computes the exact gradient of the real-arithmetic graph: the returned parameter cotangent equals the exact derivative of this scalar graph.

Verification

technique · direct recurrence and reverse tape

1.1givenalgebra

Substitution into the two Euler updates gives $x_{1} = 1 + (1 / 2) (1) (1) = 3 / 2$ and $x_{2} = (3 / 2) + (1 / 2) (1) (3 / 2) = 9 / 4$ . As a function of $α$ , $J (α) = (1 + h α)^{2} x_{0}$ , so $J^{'} (1) = 2 h (1 + h) x_{0} = 3 / 2$ .

2.1F1step 1.1algebra

Seed ${\overset{ˉ}{x}}_{2} = 1$ . At step $k = 1$ , $\partial x_{2} / \partial x_{1} = 1 + h α = 3 / 2$ and $\partial x_{2} / \partial α = h x_{1} = 3 / 4$ , so ${\overset{ˉ}{x}}_{1} = 3 / 2$ and the accumulated $\overset{ˉ}{α} = 3 / 4$ .

3.1F1step 2.1algebra

At step $k = 0$ , $\partial x_{1} / \partial x_{0} = 3 / 2$ gives ${\overset{ˉ}{x}}_{0} = (3 / 2) (3 / 2) = 9 / 4$ , while $\partial x_{1} / \partial α = h x_{0} = 1 / 2$ adds $(1 / 2) (3 / 2) = 3 / 4$ to $\overset{ˉ}{α}$ . Thus the total parameter cotangent is $3 / 2$ .

4.1F2step 1.1step 3.1∎

The reverse result equals the direct derivative in step 1.1, and [F2] identifies it as the derivative of the finite trajectory map.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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 (standard reference, not scraped)