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

Warm-start generation meets accelerated high-accuracy sampling

Two primary-paper cases and one composition view; an extension to, not a mutation of, the pinned 34-row SampleWiki snapshot.

Main theorem routes remain source-pinned plans. Per-declaration compilation and independent reviews are recorded in the linked Frontier Cells and semantic registry; they do not certify either full paper.

  1. Smoothed Picard HMC and the proxy warm start

    Producer: low-accuracy transport control, then an implementable proxy warm start.

  2. Proximal BPS: high accuracy from a warm start

    Consumer: a Renyi-warm input becomes a high-accuracy position law through an augmented-state discrete chain.

  3. Cold start to high accuracy: the producer–consumer contract

    Composition view of SPHMC Theorem 1.3, not a third paper or an ASTIS novelty claim.

How the proposed proof graph changes

Replace two isolated complexity leaves by a producer, a proxy certificate, a robust kernel consumer and a separately charged composition. Share RGO geometry and reflection technology without identifying distinct theorems.

Two red source-case lanes meet through a TV-stable proxy handoff; all formalization remains open.
Open the SVG to zoom. This is a planned source-interface graph, not the Lean import graph.

Candidate bridge and reusable-hub roles, not computed centrality, proven novelty rankings or Lean implications.

  • Chapters 5–7: low accuracy, warm starts and high accuracy
  • Chapter 8: proximal sampling and conditional/RGO tools
  • MCMC: augmented states, PDMP implementation and nonreversible analysis
  • Optimal transport: finite-p-moment couplings and Gaussian regularization

A future certified compression must retain measure, regularity, oracle, moment, warmness, implementation and cost side conditions. No category or functor certificate exists.

Expand this frontier in the interactive proof graph → · Inspect the candidate certificate bridge →

Reading and formalization order

Read the two source contracts, then the composition proof. Formalize dependency-ready common technology before algorithm assemblies; the existing active Chewi 8.4.1 route stays unchanged.

Nine reusable technology contracts and four next-packet candidates →

Attribution and source status

These are ASTIS mathematical restatements and proof-route explanations, not reproduced paper prose. Both arXiv pages list the perpetual non-exclusive distribution license; ASTIS assumes no blanket right to republish them. No author endorsement or new Lean certificate is implied.