ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

Zero state error can coexist with nonzero log-density quadrature error

Example

Assume Countable Choice. Let $f (t, x) = t x$ on $[0, 1] \times R$ , start at $x (0) = 0$ , take $h = 1 / N$ , and choose any strictly positive continuous probability density $p_{0}$ on $R$ . Initialize ${\hat{ℓ}}_{0} = \log p_{0} (0)$ . The exact and Euler state paths are both identically zero, but the left-Euler divergence update has terminal log-density error $h / 2$ . Replacing only this scalar update by midpoint quadrature makes the terminal log density exact.

Facts & Assumptions

Given: Countable Choice, $T = 1$ , $N \geq 1$ , $h = 1 / N$ , $f (t, x) = t x$ on $[0, 1] \times R$ , $x (0) = 0$ , a positive continuous probability density $p_{0}$ on $R$ , and the Euler state update with scalar initialization ${\hat{ℓ}}_{0} = \log p_{0} (0)$ and either left-Euler or midpoint divergence quadrature.

[A1]

Countable Choice is the assertion that every countable family of nonempty sets has a choice function (The Axiom of Countable Choice ( ${A C}_{ω}$ )); it is used only for the density interpretation inherited from [F1].

[F1]

Along a C¹ diffeomorphic flow, $p_{t} (Φ_{t} (x_{0})) = p_{0} (x_{0}) / \det D Φ_{t} (x_{0})$ and the exact log-density derivative is $- {div}_{x} f$ (A continuous flow changes log density by minus its divergence).

[F2]

The error bound separates the global state error, the state sensitivity of the scalar quadrature update, and its exact-start quadrature defect (Global continuous-flow log-density error from state and quadrature bounds).

[F3]

Euler on a bounded C² tube satisfies the proved state and log-density error bounds when its divergence update uses left-Euler quadrature (Euler global state and log-density error on a bounded C² tube).

[F4]

The real exponential is defined by its power series and has derivative $\exp$ (The real exponential function and the number $e$ by a power series, The exponential function is smooth and $(\exp)^{'} = \exp$ ).

[F5]

The derivative of $t \mapsto \exp (t^{2} / 2)$ is $t \exp (t^{2} / 2)$ , by the power rule, scalar-multiple rule, and chain rule (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F6]

$\exp (t) > 0$ and $1 / \exp (t) = \exp (- t)$ (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

[F7]

For positive $u, v$ , $\log (u / v) = \log u - \log v$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F8]

The natural logarithm is the inverse of $\exp$ on positive reals, so $\log (\exp u) = u$ (The natural logarithm as the inverse of the exponential function).

Verification

1.1givenF3F4F5F6algebrainduction

Define $Φ_{t} (x_{0}) : = \exp (t^{2} / 2) x_{0}$ for $t \in [0, 1]$ . By [F5], $\partial_{t} Φ_{t} (x_{0}) = t \exp (t^{2} / 2) x_{0} = t Φ_{t} (x_{0}) = f (t, Φ_{t} (x_{0}))$ , and $Φ_{0} (x_{0}) = x_{0}$ ; [F6] makes each slice a C¹ diffeomorphism $R \to R$ with inverse $y \mapsto y / \exp (t^{2} / 2)$ . Thus $x (t) = Φ_{t} (0) = 0$ is the exact path. Euler has $x_{n + 1} = x_{n} + h t_{n} x_{n}$ , hence $x_{n} = 0$ for every $n$ by induction. The compact convex state set $K = [- 1, 1]$ contains the exact and Euler states, and the bounded convex open set $U = (- 1, 2) \times (- 2, 2)$ contains $[0, 1] \times K$ ; $f (t, x) = t x$ is C² with bounded derivatives there, so [F3] applies to its left-Euler density update.

2.1givenA1F1F2F6F7F8step 1.1algebrainduction∎

Since $D Φ_{1} (0) = \exp (1 / 2)$ , [F1] gives $p_{1} (0) / p_{0} (0) = 1 / \exp (1 / 2) = \exp (- 1 / 2)$ by [F6]. Since $p_{0} (0) > 0$ , [F7] and [F8] give the exact log-density change $\log p_{1} (0) - \log p_{0} (0) = - 1 / 2$ . The left-Euler update gives $- h \sum_{n = 0}^{N - 1} t_{n} = - h^{2} \sum_{n = 0}^{N - 1} n = - h^{2} N (N - 1) / 2 = - 1 / 2 + h / 2$ : the sum formula holds at $N = 1$ , and if it holds at $N$ then adding the next term $N$ gives $(N + 1) N / 2$ . Thus its absolute log-density error is $h / 2 > 0$ . For midpoint quadrature, $- h \sum_{n = 0}^{N - 1} (t_{n} + h / 2) = - h^{2} (N (N - 1) / 2 + N / 2) = - h^{2} N^{2} / 2 = - 1 / 2$ , so its error is zero with the state solver unchanged. In [F2], state sensitivity vanishes because the integrand $t$ is independent of $x$ , and midpoint quadrature has zero local defect because $t$ is affine.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

64 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

Ricky T. Q. Chen, Yulia Rubanova, Jesse Bettencourt, and David Duvenaud, Neural Ordinary Differential Equations (standard reference, not scraped)
George Papamakarios, Eric Nalisnick, Danilo Jimenez Rezende, Shakir Mohamed, and Balaji Lakshminarayanan, Normalizing Flows for Probabilistic Modeling and Inference (standard reference, not scraped)