Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Discrete Sampling · Source section 5
Random Walk Theorem: Proof of Local-to-Global
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
\[\operatorname{gap}(P)=\inf_{\operatorname{Var}_\pi(f)>0}\frac{\mathcal E_P(f,f)}{\operatorname{Var}_\pi(f)}\]
Use one canonical variance/Dirichlet/Rayleigh-quotient API and explicit up/down-walk adapters. The displayed variational formula assumes a finite reversible nontrivial chain.
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
- §5.1 · Up and Down Walks printed/PDF p. 30
- §5.2 · Spectrum of Up-Down Chains printed/PDF p. 33
- §5.3 · Proof Setup printed/PDF p. 33
- §5.4 · Key Technical Lemma printed/PDF p. 34
- §5.5 · Inductive Proof of Random Walk Theorem: Proof of Theorem 4.1 printed/PDF p. 36