Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Discrete Sampling · Source section 12
Extensions to Other Spin Systems: Ising Model and Colorings
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
Search PMF/measure/kernel, finite matrix, conditional probability, variance and entropy APIs before adding route-local definitions.
Frontier Cells
Only genuinely missing mathematical edges become theorem-sized tasks.
Graph placement
Dependencies, consumers, cross-library bridges, and reusable shared interfaces.
Mathematical orientation
\[\pi_\beta(\sigma)=Z_\beta^{-1}\exp\!\left(\beta\sum_{\{u,v\}\in E}\sigma_u\sigma_v\right),\quad\sigma\in\{-1,+1\}^{V}\]
The display is the finite, zero-field Ising target in the monograph convention. The factor exp(beta|E|) cancels on normalization. Section 12 states results without proofs: follow the cited original papers before claiming closure. Temperature, sign, degree, fields and boundary conditions cannot be dropped.
This is ASTIS orientation, not a verbatim theorem or completed Lean proof. Pin each source theorem, hypotheses and clock before claiming a Frontier Cell.
Section source map
- §12.1 · Ising Model printed/PDF p. 90
- §12.2 · Multispin Systems: Colorings and Edge Colorings printed/PDF p. 91