Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Extended E4 · attached to Chapter 2
Hamiltonian proposals and geometric adapters
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?
Explain why deterministic numerical trajectories can be used inside an exact-target Markov kernel.
Primary §2.2; geometric comparisons also read Chapter 4.
\[H(x,p)=V(x)+\tfrac12p^TM^{-1}p\]
Proposed proof / reuse route
- Introduce the extended target and momentum law.
- Check reversibility/involution and volume or Jacobian conditions.
- Apply the acceptance construction on the extended state.
- Prove the desired marginal by projection.
Truth boundary
A Riemannian mass matrix requires determinant/volume and position-dependent corrections. A plain gradient replacement is not Riemannian HMC; no blanket acceleration or nonreversibility claim.
Planned consumers: mcmc, riemannian-optimization, log-concave-sampling. Planned sharing is not a compiled dependency or a priority claim.
Sources and exact scope
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