Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Discrete Sampling · Source section 8
Trickle-Down Theorem
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
\[\text{local spectral control}\ \rightsquigarrow\ \text{global walk gap}\]
Track links, local walks and pinning operators. Log-concavity of a generating polynomial is not the same predicate as log-concavity of a Euclidean density. The display is a proof-program orientation, not a theorem.
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
- §8.1 · Simplical Complexes printed/PDF p. 50
- §8.2 · Trickle-Down Statement printed/PDF p. 50
- §8.3 · Rapid Mixing of Bases-Exchange Walk: Proof of Theorem 1.15 printed/PDF p. 51
- §8.4 · Connections to Spectral Independence and Log-Concavity printed/PDF p. 52
- §8.5 · Proof of the Trickle-Down Theorem: Proof of Theorem 8.1 printed/PDF p. 53
- §8.6 · Proofs of Technical Lemmas printed/PDF p. 55