Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Extended E7 · attached to Chapter 4
Lifting, bouncy dynamics and PDMP limits
Stable source-facing chapter environment inside the shared Samplinglib reader.
scaffoldsource mapFull source closure not claimed
Planned route
Source → theorem map → reusable Lean nodes
Upstream alignment
Use one canonical shared node where types match. Formal/source audit is still required.
Frontier Cells
Only genuinely missing mathematical edges become theorem-sized tasks.
Graph placement
Dependencies, consumers, cross-library bridges, and reusable shared interfaces.
ASTIS extended material, not a chapter of Fearnhead–Nemeth–Oates–Sherlock. No Lean closure asserted.
Why this extension?
Changing the state and clock connects deterministic proposals and event-driven samplers, but not via an unconditional equivalence.
Primary Chapters 4–5; refreshment-limit source candidate.
\[(X,V)\longmapsto X\]
Proposed proof / reuse route
- Specify the augmented law and its projection.
- Audit deterministic flow and jump/refreshment kernels.
- State the exact limiting regime.
- Only compare efficiency under a fixed observable and cost.
Truth boundary
Nonreversibility is not uniformly faster. HMC may be reversible at the position-kernel level. A limit theorem is neither equality of finite algorithms nor an identity/composition certificate.
Planned consumers: mcmc, log-concave-sampling, riemannian-optimization. Planned sharing is not a compiled dependency or a priority claim.
Sources and exact scope
MCMC using bouncy Hamiltonian dynamics: A unifying framework for Hamiltonian Monte Carlo and piecewise deterministic Markov process samplers ↗
Andrew Chin, Akihiko Nishimura · 2405.08290v1
Dynamics construction and frequent-refreshment limit; source-level extension candidate, exact theorem audit pending
version-pinned; theorem-level audit pending
MCMC using Hamiltonian dynamics ↗
Radford M. Neal · 1206.1901v1
Hamiltonian dynamics, volume preservation and Metropolis-corrected integrators; pinpoint each theorem before formalization
version-pinned; theorem-level audit pending