Discrete Sampling Library
Discrete Sampling
Ising / Glauber dynamics, hard-core models, colourings and matroids. Finite state spaces—not Euler discretization of continuous sampling.
Formalization contract
Map first, reuse first, prove only real gaps.
Search Samplinglib, Mathlib and compatible upstreams before defining anything. Reuse one shared probability/Dirichlet/entropy floor, keep finite-state adapters explicit, and publish conceptual mirrors through the independent-review protocol.
reuseadaptmissingout of scope
Book contents
Chapter scaffolds
01
scaffold
Source section 1 · printed/PDF p. 4. Source map, not Lean completion.
02
scaffold
Source section 2 · printed/PDF p. 14. Source map, not Lean completion.
03
scaffold
Source section 3 · printed/PDF p. 18. Source map, not Lean completion.
04
scaffold
Source section 4 · printed/PDF p. 26. Source map, not Lean completion.
05
scaffold
Source section 5 · printed/PDF p. 30. Source map, not Lean completion.
06
scaffold
Source section 6 · printed/PDF p. 37. Source map, not Lean completion.
07
scaffold
Source section 7 · printed/PDF p. 47. Source map, not Lean completion.
08
scaffold
Source section 8 · printed/PDF p. 50. Source map, not Lean completion.
09
scaffold
Source section 9 · printed/PDF p. 57. Source map, not Lean completion.
10
scaffold
Source section 10 · printed/PDF p. 78. Source map, not Lean completion.
11
scaffold
Source section 11 · printed/PDF p. 85. Source map, not Lean completion.
12
scaffold
Source section 12 · printed/PDF p. 90. Source map, not Lean completion.
Primary source and supplementary roles
Spectral Independence and Local-to-Global Techniques for Optimal Mixing of Markov Chains — Zongchen Chen, Daniel Štefankovič, Eric Vigoda. arXiv:2307.13826v4; 100 pages. This is a modern spectral-independence monograph, not an exhaustive book on every discrete sampler.
arXiv submission v4 is dated September 16; downloaded PDF title page reads September 18, 2025. Use the version and byte fingerprint, not date alone.
PDF SHA-256: 3cc2f911b33bb5538157ef8a70f0c7e0f3c812ecd06dc9c1d5ea0bfdae11a52a
Levin–Peres, with contributions by Wilmer: Markov Chains and Mixing Times, 2nd ed. (2017)
background textbook · Basic finite chains, coupling, spectral analysis and mixing-time lower bounds; not claimed to have an arXiv edition.
Source ↗Hugo Duminil-Copin: Lectures on the Ising and Potts models on the hypercubic lattice
model-background lecture notes · Ising/Potts equilibrium, finite/infinite volume and phase transitions. Not a replacement for a rapid-mixing proof.
Source ↗Blanca et al.: On Mixing of Markov Chains: Coupling, Spectral Independence, and Entropy Factorization
primary proof supplement · Pin theorem/version for coupling-to-SI and entropy-factorization adapters; preserve all assumptions.
Source ↗Chen–Liu–Vigoda: Optimal Mixing of Glauber Dynamics: Entropy Factorization via High-Dimensional Expansion
primary proof supplement · Source-specific entropy factorization and spin-system mixing proofs; audit cited statement, not just title.
Source ↗Jan Maas: Gradient flows of the entropy for finite Markov chains
conceptual transport source · Finite reversible irreducible chains and a chain-dependent logarithmic-mean transport metric; not ordinary W2 on a finite set.
Source ↗Start with the shared floor, not page order
Read §§1.1–1.3 and pull §3 forward for kernels, reversibility, Dirichlet forms and gap. Read §12.1 model definitions early for Ising; advanced mixing waits for exact proof prerequisites. Then branch through §2/§4.1 pinnings, §§4–6 local-to-global and entropy, or §§7–8 matroids.
Finite kernels do not wait for SDEs, spatial derivatives or manifold calculus. Shared scalar decay and probability algebra are reusable; a chain-dependent metric or finite-jump dissipation identity needs its own adapter.
Discrete Sampling Route · Functor Hypergraph · Lean Branches
Known source boundaries
Section 12 states Ising/colouring extensions without their proofs. Follow each cited original paper and keep model/temperature/field/degree assumptions. The general update at §1.3 p.5 also has a copy-index discrepancy between its formula and prose: a correction is a recorded repair candidate, not a silent rewrite.
Contributor protocol and clock contract ↗
All twelve pages are scaffolds. New conceptual bridges are explicitly candidate, awaiting independent review; none is a Lean-certified functor.
Read the supporting proofs
Mathematical derivations with optional Lean and source details.