Discrete Sampling · external extension shelf

OpenAI Math routes for Discrete Sampling

These routes are placed beside the chapters that can explain or consume them. They do not alter the primary source's chapter numbering, and they remain external until a reviewed ASTIS adapter or theorem compiles.

Back to Discrete Sampling All seven libraries

Extended chapters

E1 — Card shuffles and deterministic sweeps (Samplinglib extension; not a source-text chapter)
E2 — Exact sampling, approximate counting and IID factors (Samplinglib extension; not a source-text chapter)

11 mapped routes

Chapter and extension placement

Comparator-backed upstream endpointOpenAI Math result 238

Binary-sweep contraction and mixing

A discrete finite-chain theorem; no Langevin/SDE interpretation is inferred.

Samplinglib placement

Discrete Sampling: Chapter 3, Chapter 6, Extended E1: Card shuffles and deterministic sweeps — Kernel mixing foundations and an explicit shuffle extension meet here.

Pinned upstream paths and provenance

lean/OAI/Probability/BinarySweep

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)

OAI.binary_sweep_contraction_and_mixing

Comparator-backed, partial familyOpenAI Math result 238

Conditional information under coordinate sweeps

Conditional-information endpoints do not by themselves prove the entire Thorp mixing family.

Samplinglib placement

Discrete Sampling: Chapter 3, Extended E1: Card shuffles and deterministic sweeps — Conditional resampling and sweep composition extend the kernel foundations.

Pinned upstream paths and provenance

lean/OAI/Probability/CoordinateSweeps

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)

OAI.CoordinateSweeps.conditional_main
OAI.CoordinateSweeps.all_grid_moment

Comparator linked by upstream result noteOpenAI Math result 115

Exact sampling and approximate counting of contingency tables

Upstream documentation separates almost-sure exact sampling, bounded-time TV approximation and FPRAS counting; ASTIS must preserve all three cost/error contracts.

Samplinglib placement

Discrete Sampling: Extended E2: Exact sampling, approximate counting and IID factors — Exact combinatorial sampling and counting are outside the source textbook's spin/matroid spine.

Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Comparator-backed upstream endpointOpenAI Math result 131

Rapid mixing of graph switches

Connectivity, spectral/comparison estimates and TV mixing remain separate proof obligations.

Samplinglib placement

Discrete Sampling: Chapter 3, Chapter 4, Extended E2: Exact sampling, approximate counting and IID factors — Finite-chain foundations and comparison-based rapid mixing are the closest source chapters.

Pinned upstream paths and provenance

lean/OAI/Probability/SwitchChain

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)

OAI.Problem315.switch_chain_main
OAI.Problem315.switch_chain_tv_bound
OAI.Problem315.switch_connectivity

Comparator-backed, partial familyOpenAI Math result 238

Optimal logarithmic mixing of the Thorp shuffle

The family has multiple comparator endpoints; routing, compatibility, energy decay and final mixing must not be flattened into one implication.

Samplinglib placement

Discrete Sampling: Chapter 3, Extended E1: Card shuffles and deterministic sweeps — This is the dedicated card-shuffle extension after finite-chain foundations.

Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)

OAI.Thorp.Current.first_reciprocal_main
OAI.ThorpResults.remaining_main
OAI.ThorpNine.main
OAI.ThorpCompatibility.weightedCompatibility_main

Comparator linked by upstream result noteOpenAI Math result 231

Strongly Rayleigh laws, determinantal processes and IID factors

Negative-dependence infrastructure and the free uniform spanning forest result must remain distinguishable.

Samplinglib placement

Discrete Sampling: Chapter 7, Extended E2: Exact sampling, approximate counting and IID factors — Strong Rayleigh structure directly extends the matroid/negative-dependence route.

Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Comparator-backed upstream endpointOpenAI Math result 227

Critical SK heat-bath/Glauber mixing

Spin-glass-specific hypotheses are source binders; generic Dirichlet, entropy or TV leaves may be extracted only after audit.

Samplinglib placement

Discrete Sampling: Chapter 3, Chapter 6, Chapter 10, Chapter 12 — Glauber dynamics, optimal mixing, critical-point analysis and spin systems all participate.

Pinned upstream paths and provenance

lean/OAI/MathematicalPhysics/CriticalMixing

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)

OAI.CriticalSK.critical_mixing_bounds

Comparator-backed, partial familyOpenAI Math result 113

Perfect-matching entropy and approximate counting

The named entropy endpoint does not certify the complete FPRAS paper family.

Samplinglib placement

Discrete Sampling: Chapter 7, Extended E2: Exact sampling, approximate counting and IID factors — Matching laws and entropy sit beside matroid/negative-dependence tools, while counting remains an extension.

Pinned upstream paths and provenance

lean/OAI/Combinatorics/PerfectMatching

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)

OAI.MatchingEntropy.entropy_main

Comparator-backed, partial familyOpenAI Math result 114

FPRAS for common matroid bases

The formal endpoint covers equal-rank matroid bases with explicit oracle and error contracts, not the entire integer-polymatroid family.

Samplinglib placement

Discrete Sampling: Chapter 7, Extended E2: Exact sampling, approximate counting and IID factors — The theorem directly extends the source's matroid chapter into approximate counting.

Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)

OAI.common_bases_fpras

Comparator linked by upstream result noteOpenAI Math result 229

Three-state reconstruction above the Kesten-Stigum threshold

Upstream Lean covers only the supercritical direction; non-reconstruction, equality and stochastic-block-model consequences remain outside the selected statements.

Samplinglib placement

Discrete Sampling: Chapter 9, Chapter 12, Extended E2: Exact sampling, approximate counting and IID factors — Tree recursions and spin-system thresholds are the closest source route.

Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Comparator-backed upstream endpointOpenAI Math result 236

Factor-of-IID threshold for free Ising spins on trees

Finitary coding and coding-radius bounds are explicitly outside the upstream formalized endpoint.

Samplinglib placement

Discrete Sampling: Chapter 12, Extended E2: Exact sampling, approximate counting and IID factors — The Ising source chapter is the natural anchor; IID-factor semantics are an extension.

Pinned upstream paths and provenance

lean/OAI/Probability/FreeIsing

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)

OAI.Problem367.free_ising_factor_iff_threshold