Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Discrete Sampling · Source section 2
Properties of the Influence Matrix
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
\[\Psi_\mu(i,j)=\mu(\sigma_j=1\mid\sigma_i=1)-\mu(\sigma_j=1\mid\sigma_i=0)\quad(i\ne j)\]
Reuse covariance, symmetric matrix and weighted-inner-product algebra. The displayed off-diagonal binary influence assumes both conditional events are feasible; frozen sites need removal or an explicit convention.
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
- §2.1 · Nonnegative eigenvalues printed/PDF p. 14
- §2.2 · Bounding Spectral Radius of Influence Matrix printed/PDF p. 15
- §2.3 · Correlation Matrix printed/PDF p. 16
- §2.4 · Semidefinite Ordering printed/PDF p. 17
- §2.5 · Modified Influence Matrix printed/PDF p. 18