Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

Reusable proof technology

Shared identities, explicit consumers and separate adapters. These targets do not reschedule the active mathematical frontier.

RED · reusable target, not a compiled leaf

Density smoothing and score regularity

Normalized convolution, conditional score/covariance representatives and controlled higher derivatives.

Source: 2609.06906v1. Section 3.1; Lemmas 4.1–4.3; Appendix C

Parents: Independent root candidate

Consumers: Picard trajectory and quadrature error

Failure boundary

Not potential averaging; not an exactly unbiased score oracle.

Existing Lean reuse-search locations

Inspect exact ASTIS and pinned Mathlib types before declaring reuse. No new source theorem or wrapper is introduced by this list.

RED · reusable target, not a compiled leaf

Picard trajectory and quadrature error

Integral Hamiltonian flow, local bias/variance and Wp propagation with finite moments.

Source: 2609.06906v1. Sections 3.2, 4–5; Appendix B

Parents: Density smoothing and score regularity

Consumers: Truncation and reverse transport

Failure boundary

Higher derivatives of the smoothed density do not strengthen assumptions on the original potential for free; oracle bias must be paid.

Existing Lean reuse-search locations

Inspect exact ASTIS and pinned Mathlib types before declaring reuse. No new source theorem or wrapper is introduced by this list.

RED · reusable target, not a compiled leaf

Truncation and reverse transport

A probability-law witness with separate TV distance and Renyi certificate, using p-moment and heat-flow inputs.

Source: 2609.06906v1. Lemmas 6.2–6.3; Theorem 7.1(ii)

Parents: Picard trajectory and quadrature error · Quadratic RGO composition

Consumers: Proxy-stable kernel composition

Failure boundary

An actual sample law is not its comparison witness; smoothing and recursion cannot be removed.

Existing Lean reuse-search locations

Inspect exact ASTIS and pinned Mathlib types before declaring reuse. No new source theorem or wrapper is introduced by this list.

RED · reusable target, not a compiled leaf

Quadratic RGO composition

Complete the square once; keep potential equality up to a constant separate from equality of normalized conditional kernels.

Source: 2609.06906v1 · 2609.06905v1. SPHMC Lemma 6.4; PBPS Section 2.2

Parents: Independent root candidate

Consumers: Truncation and reverse transport · Conditional harmonic flight and bounce kernel

Failure boundary

Positive variance, normalization and parameter measurability are real obligations.

Existing Lean reuse-search locations

Inspect exact ASTIS and pinned Mathlib types before declaring reuse. No new source theorem or wrapper is introduced by this list.

RED · reusable target, not a compiled leaf

Two reflections with different roles

Velocity reflection R_h with R_0=I; separately the augmented involution (x,y) ↦ (x,2x-y).

Source: 2609.06905v1. (2.4); Proposition 2.1; Section 3.2

Parents: Independent root candidate

Consumers: Conditional harmonic flight and bounce kernel · Micro–macro modified-L2 contraction

Failure boundary

Isometry or involution alone does not prove process invariance, ergodicity or convergence.

Existing Lean reuse-search locations

Inspect exact ASTIS and pinned Mathlib types before declaring reuse. No new source theorem or wrapper is introduced by this list.

RED · reusable target, not a compiled leaf

Conditional harmonic flight and bounce kernel

Non-explosive event process, path reversal, conditional invariance and the averaged half-turn kernel.

Source: 2609.06905v1. Propositions 3.1–3.2; Appendix A

Parents: Two reflections with different roles · Quadratic RGO composition

Consumers: Micro–macro modified-L2 contraction

Failure boundary

Not a free-flight vanilla BPS semigroup; preserve fixed-reference and zero-rate conventions.

Existing Lean reuse-search locations

Inspect exact ASTIS and pinned Mathlib types before declaring reuse. No new source theorem or wrapper is introduced by this list.

RED · reusable target, not a compiled leaf

Micro–macro modified-L2 contraction

Conditional-expectation projection, reflection coupling, operator interpolation and norm-equivalent modified energy.

Source: 2609.06905v1. Theorem 3.5; Appendices B–D

Parents: Two reflections with different roles · Conditional harmonic flight and bounce kernel

Consumers: Implementation coupling and query caps

Failure boundary

Do not import reversible Dirichlet coercivity or continuous-time hypocoercivity without an explicit discrete adapter.

Existing Lean reuse-search locations

Inspect exact ASTIS and pinned Mathlib types before declaring reuse. No new source theorem or wrapper is introduced by this list.

RED · reusable target, not a compiled leaf

Implementation coupling and query caps

Ideal mixing, RGO error, solver fallback, event-rate cap and actual-input expected query bounds.

Source: 2609.06905v1. Theorem 4.3; (4.17)–(4.18)

Parents: Micro–macro modified-L2 contraction

Consumers: Proxy-stable kernel composition

Failure boundary

Exact ideal invariance and approximate implemented accuracy remain distinct.

Existing Lean reuse-search locations

Inspect exact ASTIS and pinned Mathlib types before declaring reuse. No new source theorem or wrapper is introduced by this list.

RED · reusable target, not a compiled leaf

Proxy-stable kernel composition

TV data processing plus triangle inequality; separate conditional expected-cost addition.

Source: 2609.06906v1 · 2609.06905v1. SPHMC Section 7.2; PBPS (4.18)

Parents: Truncation and reverse transport · Implementation coupling and query caps

Consumers: Composition view

Failure boundary

Markov-kernel measurability and mass one; no unbounded-cost transfer from TV alone.

Existing Lean reuse-search locations

Inspect exact ASTIS and pinned Mathlib types before declaring reuse. No new source theorem or wrapper is introduced by this list.

Next dependency-ready packet candidates

  1. Branch persistence and finite-depth RGO parameter threshold

    RGOCalculus and both scalar regime estimates now compile; exact independent admission is tracked in their cells. RecursiveVariance includes zero initial precision and a guarded finite-previous-variance comparison, with c<1/4 generalized away only for the selected scalar formula. Next inspect the actual condition-number update for branch persistence, then geometric progress toward the finite positive threshold with exact stage indexing. These successor claims remain planned, not proved.

    Exclude: Do not relax the algorithm's source schedule or infer termination directly from a single-step inequality. Recursive error, terminal FORS work, reference-point cost, implemented sampling and actual-input expected query costs remain independent. TV proximity does not transfer unbounded expected cost.

  2. Source-detail audits of analytic and process consumers

    Separate conditional score/covariance representatives, domination, event-process domains and discrete modified-energy contracts. Reuse the existing Gaussian law, reflection and normalization results.

    Exclude: Preserve earlier Chewi 8.4.1 evidence; do not require the whole SDE library before reachable paper lemmas or infer process invariance from reflection algebra.