Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

Bench / sampling

sogb-006 · public-dev · editorial and formal status separate

Null atoms in a random-scan balance proof

Discrete Sampling / Markov Chain Monte Carlo · natural-language: L3 (author-assigned; calibration pending)

Why this difficulty?

Separate two null-mass cases, apply a conditional formula only at supported starts, then distinguish balance from irreducibility.

Editorial review and exact formal-coverage boundary

AI editorial review accepted. This is not canonical theorem publication, full Lean coverage or empirical difficulty calibration.

  • There is no admitted equivalent Lean task. The arbitrary-kernel explanation, 00/11 nonirreducibility example and convergence discussion are NL obligations beyond the cited local reversibility declaration.

Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.

Assumptions and conventions

  • \(μ\) is any probability measure on the finite Boolean cube with n+1 coordinates. K is its uniform random-site heat-bath kernel, with the project's fixed conditional versions at null fibers.
  • At any start y with \(μ(\{y\})>0\), the exact singleton transition formula is the sum over coordinates of the retained-coordinate indicator times \(μ(\{x\})\) divided by the corresponding fiber mass, averaged by 1/(n+1). No such formula is assumed at an unsupported start.

Natural-language question

In the detailed-balance proof, handle a target-null atom x without applying the positive-start singleton formula at x. Why is zero mass alone insufficient for an arbitrary kernel? Give a reversible heat-bath example which is not irreducible.

Reference mathematical proof

  1. If \(μ(\{x\})=μ(\{y\})=0\), both weighted transition masses vanish: finite Markov transition masses make multiplication by zero harmless.

  2. If \(μ(\{x\})=0\) but \(μ(\{y\})>0\), use the positive-start formula at y, not x. Each relevant fiber contains y, so its mass is at least \(μ(\{y\})>0\). Every summand for a jump from y to x contains \(μ(\{x\})=0\), hence \(K(y,\{x\})=0\). Both fluxes are again zero.

  3. For an arbitrary kernel, a zero target atom does not imply \(K(y,\{x\})=0\): that conclusion used the actual heat-bath transition law. Target-null starts may have nontrivial transition rules, but their outgoing flux is multiplied by zero.

  4. On the two-bit cube, let \(μ\) give mass 1/2 to each of 00 and 11 and zero to the other states. Updating a single coordinate from either supported state leaves it unchanged. The kernel is reversible for \(μ\), but 00 and 11 cannot communicate. Thus balance supplies neither irreducibility nor convergence from every start.

Formal support and missing Lean alignment

The null-start split follows the existing private balance proof, while the explanatory counterexample is not an aligned checked Lean task.

Assessment rubric · 4 points
  1. Separates the both-null and single-null cases without dividing by zero. (1 point)
  2. Uses the singleton formula at the positive-mass reverse start and proves fiber positivity. (1 point)
  3. Explains why an arbitrary kernel need not avoid a target-null atom. (1 point)
  4. Checks the 00/11 heat-bath counterexample and distinguishes reversibility from irreducibility. (1 point)

Lean view: not yet aligned

The null-start split follows the existing private balance proof, while the explanatory counterexample is not an aligned checked Lean task.

This support theorem does not certify the complete QA or its explanatory counterexamples.

What this does—and does not—verify

No mixing time, spectral independence, full-support theorem or hard-core ergodicity claim follows from this balance argument.

Existing library mathematics reused; no new mathematical leaf or paper-completion credit. The editorial panel records the exact current review scope and remaining unformalized explanation.

Sources, graph location and dependencies

Original question based on the actual finite heat-bath implementation, retaining its null-fiber boundary.

Exact local source and full context · Locate the owning module (declaration not yet indexed in this graph)

AutoSamplingTheory.TechnicalLemmas.Probability.RandomScanHeatBath.randomScan_isReversible

ASTIS formal support (not an equivalent QA)

  • AutoSamplingTheory.TechnicalLemmas.Probability.RandomScanHeatBath.randomScan_apply_singleton

Mathlib facts / definitions

    Binding SHA-256: 74f08b42811ce2c35e4669f9e631246262c6038119faa990aea98efb42431cb3