Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Discrete Sampling · Source section 4
Rapid Mixing from Spectral Independence
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^\tau(\sigma)=\mu(\sigma\mid\sigma_S=\tau),\qquad \mu(\sigma_S=\tau)>0\]
Uniform control must cover every feasible pinning required by the theorem, not just the unconditional law. Separate conditional support bookkeeping from spectral estimates.
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
- §4.1 · Pinnings printed/PDF p. 26
- §4.2 · Rapid Mixing Theorem printed/PDF p. 27
- §4.3 · Local to Global: Random Walk Theorem of Alev-Lau printed/PDF p. 27
- §4.4 · Local Walk Connection to Influence Matrix printed/PDF p. 28
- §4.5 · Proof of Rapid Mixing (Theorem 1.4) printed/PDF p. 29