Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Discrete Sampling · Source section 7
Matroids
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(B)=\frac{1}{|\mathcal B|},\qquad B\in\mathcal B\]
Use Mathlib matroid and finite-set primitives before defining a bases-exchange walk. The formula is the uniform target on a nonempty finite set of bases, not a mixing assertion.
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
- §7.1 · Matroids: Definitions printed/PDF p. 47
- §7.2 · Matroids: Examples printed/PDF p. 48
- §7.3 · Bases-exchange Walk printed/PDF p. 49
- §7.4 · Main Theorem: Fast Mixing of Bases-Exchange Walk printed/PDF p. 49
- §7.5 · Application: Reliability printed/PDF p. 49