Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Discrete Sampling · Source section 10
Critical Point Analysis using the Field Dynamics
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
\[\mu_{\boldsymbol\lambda}(\sigma)\propto\mu(\sigma)\prod_{v\in V}\lambda_v^{\sigma_v}\]
A field tilt changes the distribution. Record stationary laws and the comparison theorem separately; transporting a gap requires quantitative bounds, not a change of notation.
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
- §10.1 · Field Dynamics printed/PDF p. 80
- §10.2 · SI implies Fast Mixing of Field Dynamics printed/PDF p. 82
- §10.3 · Fast Mixing of Glauber Dynamics from Field Dynamics printed/PDF p. 84