Bench / sampling
One random-site step is not one sweep
Discrete Sampling · natural-language: L1 (author-assigned; calibration pending)
Why this difficulty?
Read the time unit and update law of random scan without deriving balance, mixing or computational cost.
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 aligned proof-completion task for this QA. The verbal random-site interpretation, sweep/time-unit conventions, self-transition explanation and absence of mixing/query-cost conclusions are editorially checked rather than certified as an equivalent Lean statement.
- Neither the cited mixture definition nor the supplementary coordinate-retention evidence implements a conditional sampler or proves a target-specific null-fiber conditional law, ergodicity, mixing time or cost theorem.
Content-bound review status and evidence hashes · Independent reports and frozen inputs. Historical rejected wording is audit material, not training gold.
Assumptions and conventions
- The state space is a Boolean cube with \(m\ge 1\) sites and target probability \(μ\). For each site i, Kᵢ is the fixed coordinate heat-bath kernel, including its specified version on target-null fibers.
Natural-language question
Describe one uniform random-scan step and its mixture kernel. How does that time unit differ from a sweep of all sites? Does the mixture-law description itself specify a mixing time or an oracle-query cost?
Reference mathematical proof
One step first chooses one site I uniformly among the m sites, then draws the new state with kernel \(K_{I}\), retaining the other coordinates.
The transition law is the state-independent mixture \[K(x,A)=\frac1m\sum_{i=1}^{m}K_i(x,A).\] A coordinate resampling may return its previous value, so an update need not change the state.
A sweep applies coordinate updates across all sites according to a specified schedule; it is not this single random-site kernel step. Comparing bounds requires the same time convention.
A noncomputable transition-law definition alone supplies neither an implemented conditional sampler, its query cost, nor a mixing-time estimate. Those guarantees require additional algorithmic and analytic results.
Formal support and missing Lean alignment
The source defines the actual uniform random-site mixture, with \(m=n+1\). The complete terminology and time-convention QA is not an aligned proof-completion task.
Assessment rubric · 4 points
- Describes one uniformly chosen coordinate update with other coordinates retained. (1 point)
- States the 1/m mixture kernel and allows an unchanged state. (1 point)
- Distinguishes a single step from a scheduled sweep. (1 point)
- Does not infer a mixing or query-cost bound from the law definition. (1 point)
Lean view: not yet aligned
The source defines the actual uniform random-site mixture, with \(m=n+1\). The complete terminology and time-convention QA is not an aligned proof-completion task.
This support theorem does not certify the complete QA or its explanatory counterexamples.
What this does—and does not—verify
No efficient conditional-sampling implementation, ergodicity, mixing time or sweep complexity is asserted.
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 introductory reading of the local noncomputable random-scan transition law.
Exact local source and full context · Locate the owning module (declaration not yet indexed in this graph)
AutoSamplingTheory.TechnicalLemmas.Probability.RandomScanHeatBath.randomScan
ASTIS formal support (not an equivalent QA)
Mathlib facts / definitions
Binding SHA-256: 84145f82f459d1cb080b714a85ebad040ad8fd4d034c441b45d77e02c77830ca