ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge 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.

A finite-width quadratic feature network has a changing NTK

Example

Consider the scalar one-hidden-unit model $f_{a, w} (1) = a w^{2}$ with parameters $(a, w) \in R^{2}$ and cost $C (a, w) = \frac{1}{2} f_{a, w} (1)^{2}$ . At $(a, w) = (1, 1)$ , gradient flow for this cost has $\dot{a} = - 1$ and $\dot{w} = - 2$ . Its two parameter features are $\partial_{a} f = w^{2}$ and $\partial_{w} f = 2 a w$ , and its neural tangent kernel at the single input is $K (a, w) = w^{4} + 4 a^{2} w^{2}$ . Along the local gradient-flow solution from $(1, 1)$ , both features change immediately and $\frac{d}{d t} K (a (t), w (t)) ∣_{t = 0} = - 32$ , so this finite-width model does not have a fixed NTK.

Example references

Chizat, Oyallon, and Bach, §§1.1 and 2.1, tangent operator of a differentiable parameterized model

The scalar NTK is the sum of parameter-feature products

Facts & Assumptions

Given: The model $f_{a, w} (1) = a w^{2}$ , the cost $C = \frac{1}{2} f^{2}$ , and initial parameters $(a, w) = (1, 1)$ .

[F1]

The scalar neural tangent kernel is the sum of squares of the parameter derivatives (The neural tangent kernel of a differentiable parameterized function).

[F2]

A polynomial vector field has a unique local solution through each initial point (Picard-Lindelöf local existence and uniqueness for first-order systems).

Verification

technique · direct differentiation

1.1F1givenalgebra

Differentiating $f = a w^{2}$ gives $\partial_{a} f = w^{2}$ and $\partial_{w} f = 2 a w$ . By [F1], $K (a, w) = (w^{2})^{2} + (2 a w)^{2} = w^{4} + 4 a^{2} w^{2} .$ At $(1, 1)$ , $f = 1$ , $\partial_{a} C = f w^{2} = 1$ , and $\partial_{w} C = 2 f a w = 2$ , so the negative-gradient vector field has the stated initial velocity.

2.1F2step 1.1algebra∎

The vector field $(\dot{a}, \dot{w}) = (- a w^{4}, - 2 a^{2} w^{3})$ is polynomial, hence locally Lipschitz; [F2] gives a differentiable local solution through $(1, 1)$ . Along it, $\frac{d}{d t} K = 4 w^{3} \dot{w} + 8 a w^{2} \dot{a} + 8 a^{2} w \dot{w},$ which equals $- 8 - 8 - 16 = - 32$ at $t = 0$ . Also $\frac{d}{d t} (w^{2}) ∣_{0} = 2 w \dot{w} = - 4$ and $\frac{d}{d t} (2 a w) ∣_{0} = 2 (\dot{a} w + a \dot{w}) = - 6$ , so both parameter features vary. A differentiable scalar function with nonzero derivative at zero is not constant on any right neighborhood of zero.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

Lénaïc Chizat, Edouard Oyallon, and Francis Bach, On Lazy Training in Differentiable Programming (standard reference, not scraped)