SampleWiki in ASTIS
A mathematical reading interface for frontier sampling results. Every case separates what the source states, how the proof runs, what assumptions are inherited, and what Lean has actually verified.
Smooth auxiliary states for Schrödingerisation of PDEs
Jin–Liu–Ma’s Schrödingerisation construction for PDEs with physical boundary or interface conditions introduces a smooth auxiliary \(p\)-register initial state. If its \(2^{n_p}\) grid amplitudes are treated as unrelated data, generic loading is exponential in the register width. QuantumComputinglib/ASPBE instead exploits the exact Hermite–Bernstein/tensor-train representation and proves a constructive circuit bound
Thus, for fixed smoothness order \(k\), the gate count is linear in \(n_p\), rather than the generic \(\Theta(2^{n_p})\) amplitude-loading dependence. This is a SampleWiki-style lesson beyond sampling itself: the decisive question is often whether analytical structure exposes a bounded-memory representation before one accepts a black-box oracle or dense table.
Jin–Liu–Ma: source PDE / Schrödingerisation construction · Holmes–Matsuura: prior smooth-function-to-MPS state-preparation route
Open the Lean-verified QuantumComputinglib construction and proof →
Cross-library pointer only: Samplinglib does not claim this quantum theorem as a local Lean result, and the general function-to-MPS idea is prior art.