Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Discrete Sampling · Source section 11
Random Regular Graphs via 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
\[\text{random graph assumptions}\ +\ \text{field dynamics}\ \rightsquigarrow\ \text{mixing bound}\]
Random-regular-graph results have a probability-over-graphs contract. Keep that probability separate from sampler success and Markov-chain randomness; no worst-case general-graph claim follows.
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
- §11.1 · Proof Overview printed/PDF p. 85
- §11.2 · Proof of the trickle-down for the field dynamics printed/PDF p. 88