ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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.

Finite-step leapfrog energy error

Example

For the one-dimensional standard-normal potential $U (q) = q^{2} / 2$ , unit mass, $ϵ = 1$ , one leapfrog step, and initial phase point $(0, 1)$ , the proposed energy rises by $1 / 8$ and the Metropolis acceptance probability is $e^{- 1 / 8}$ .

Facts & Assumptions

Given: AC, $H (q, p) = (q^{2} + p^{2}) / 2$ , $ϵ = 1$ , $L = 1$ , and $(q_{0}, p_{0}) = (0, 1)$ .

[F1]

A leapfrog step applies a half kick, full drift, then half kick; the proposal flips the final momentum. One-step leapfrog map as force and drift shears The HMC correction uses $\min {1, e^{- H (z^{*}) + H (z)}}$ . Hamiltonian Monte Carlo

[F2]

The algorithm retains the original position if the proposal is rejected. Leapfrog Hamiltonian Monte Carlo

[F3]

The exponential is positive and strictly increasing, and $\exp (- x) = 1 / \exp (x)$ for every real $x$ ; at $x = 0$ , positivity and the reciprocal identity give $\exp (0)^{2} = 1$ , hence $\exp (0) = 1$ . The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , The exponential function is strictly increasing

Proof

technique · direct substitution

1.1F1givenalgebra

The first half kick gives $p_{1 / 2} = 1 - \frac{1}{2} U^{'} (0) = 1$ . The drift gives $q_{1} = 0 + 1 \cdot p_{1 / 2} = 1$ . The final half kick gives $p_{1} = 1 - \frac{1}{2} U^{'} (1) = 1 / 2$ , so the flipped proposal is $(q^{*}, p^{*}) = (1, - 1 / 2)$ .

2.1givenstep 1.1algebra

The initial energy is $H (0, 1) = 1 / 2$ , while the proposed energy is $H (1, - 1 / 2) = 1 / 2 + 1 / 8 = 5 / 8$ . The discrete step therefore does not conserve $H$ at this point.

3.1F1F2F3step 2.1algebra∎

The acceptance probability is $\min {1, e^{- 5 / 8 + 1 / 2}} = e^{- 1 / 8} < 1$ , since $- 1 / 8 < 0$ and [F3] gives $e^{- 1 / 8} < e^{0} = 1$ ; rejection retains $q = 0$ by [F2]. This finite calculation distinguishes energy error from the exact target-invariance statement proved for the full Metropolized kernel.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

Radford M. Neal, MCMC Using Hamiltonian Dynamics, Handbook of Markov Chain Monte Carlo, Chapter 5 (standard reference, not scraped)
Michael Betancourt, A Conceptual Introduction to Hamiltonian Monte Carlo (standard reference, not scraped)