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

Bench / sampling

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

Adaptive hybrid error does not certify expected cost

SampleWiki research problems / Markov Chain Monte Carlo · natural-language: L4 (author-assigned; calibration pending)

Why this difficulty?

Compose conditional error averaging, common-suffix contraction and finite telescoping under actual history laws; reject an invalid unbounded-cost transfer.

Editorial review and exact formal-coverage boundary

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

  • No aligned Lean view is admitted for the entire QA. Constructing a consistent algorithmic sequence of adjacent hybrids/history laws, and any adapters identifying the abstract kernels with a concrete recursive algorithm, remain outside the component theorems.
  • The TV/expected-cost counterexample, uniform-integrability or tail-control discussion, recursion/stopping/cap comparisons and source-paper noncompletion explanation are NL-reviewed obligations, not certified by the local telescope 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

  • There are finitely many n adjacent hybrid pairs. At slot i the pair shares a probability law \(ρᵢ\) on histories, conditional Markov kernels Kᵢ,Lᵢ and a common downstream Markov kernel Sᵢ.
  • A measurable integrable real \(εᵢ\) bounds \(|Kᵢ(x,A)-Lᵢ(x,A)|\) for \(ρᵢ\)-almost every x and every measurable event A. Let \(βᵢ=\int εᵢ\) \(dρᵢ\). Total variation means the supremum of absolute event-probability differences, with no extra factor of two.

Natural-language question

Derive an eventwise discrepancy bound \(Σᵢβᵢ\) between the first and last output laws. State why actual history laws and a fixed finite call range matter. Then refute the claim that vanishing TV distance alone transfers an unbounded expected query-cost bound.

Reference mathematical proof

  1. For each slot and fixed event A, Markov event probabilities are measurable and bounded by one, hence integrable under \(ρᵢ\). Integrating the almost-everywhere conditional bound yields an averaged discrepancy at most \(βᵢ\). The error function \(εᵢ\) is explicitly integrable; measurability of a supremum over all events was not assumed for free.

  2. A common downstream Markov kernel preserves this uniform event bound by total-variation data processing. The same suffix must be used for the two members of the adjacent pair; otherwise that contraction argument is not applicable.

  3. For a fixed final event A, telescope the n adjacent probability differences and use the triangle inequality: \[|P_n(A)-P_0(A)|\le\sum_{i=0}^{n-1}\beta_i.\] Take the event supremum if desired. Each \(βᵢ\) uses its actual shared prefix-history law, not an unrelated ideal or proxy input law.

  4. For integers \(N\ge 2\) on the nonnegative reals, take \(μ_{N}=δ_{0}\), \(ν_{N}=(1-1/N)δ_{0}+(1/N)δ_{N^{2}}\) and \(c(x)=x\). Then \(TV(μ_{N},ν_{N})=1/N\to 0\), but \(E_{ν_{N}}c-E_{μ_{N}}c=N\). All these individual expectations are finite; their gap is unbounded. A uniform cost bound, uniform integrability/tail control, or a separate actual-input cost analysis is needed.

  5. A random recursion depth or stopping cap is not automatically this deterministic finite telescope. Its history construction, stopping/cap comparison, accumulated errors and actual-input expected cost remain separate obligations. This argument alone does not complete the Gaussian Cloud paper.

Formal support and missing Lean alignment

Existing formal components support averaging and common-suffix contraction; this multi-component QA and its cost counterexample have no single admitted equivalent Lean view yet.

Assessment rubric · 4 points
  1. Justifies event measurability/integrability and error averaging under the actual history law. (1 point)
  2. Uses the same downstream kernel and finite adjacent telescoping with the stated TV convention. (1 point)
  3. Computes both TV=1/N and expected-cost gap=N in a valid probability example. (1 point)
  4. Keeps recursive stopping, cap comparison and actual-input cost as separate obligations. (1 point)

Lean view: not yet aligned

Existing formal components support averaging and common-suffix contraction; this multi-component QA and its cost counterexample have no single admitted equivalent Lean view yet.

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

What this does—and does not—verify

No recursive algorithm, stopping theorem, uncapped/capped comparison, expected oracle cost theorem or full paper result is claimed.

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 exercise based on local hybrid-kernel components. Their module cites arXiv:2609.38710v1 Lemma 6.3; this exercise is not a reproduction or completion of that paper statement.

Exact local source and full context · Locate the existing Lean declaration

AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope.abs_real_comp_commonSuffix_sub_le_integral_eventBound

ASTIS formal support (not an equivalent QA)

  • AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope.abs_real_comp_sub_le_integral_eventBound
  • AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope.abs_sub_zero_le_sum_range_of_adjacent
  • AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation.abs_real_comp_sub_le

Mathlib facts / definitions

    Binding SHA-256: a4e2d5d2fd1273d0cadc2054858c9597b4e090dd0fec5fda5ecdfd5c7d206b78