Checked on this commit4,524 public declarationscommit 4e2c5b2c0be5Build record
Structure before circuit tricks
Functor Hypergraph
Follow mathematical mechanisms across fields without confusing an analogy, a conditional construction and a formal implication.
All tails of a hyperedge are required together (AND). Incidence lines are not separate implications. Every transport here is curated or proposed; no Lean-certified categorical functor is asserted.
Dashed paths: curated/proposed incidence. AND junction: all listed hypotheses and tail mechanisms. Solid proof dependencies remain in the separate generated Lean graph.
Walsh phases + interference + nonzero branch
proposal Source-planning edge; independent conceptual review pending; no local transport theorem
Combine a controlled diagonal phase supplier with ancilla interference, postselection and a normalized-error theorem.
Hypothesis map
Real function, source bit order, supplied coefficients, retained zero mode, explicit input and inverse access, small-angle/truncation bounds and nonzero accepted branch.
Conclusion map
An approximate amplitude state with a declared infidelity and success-dependent total cost, not an unconditional n-independent loader.
Failure boundary
Constant-term removal changes the controlled circuit; small filling fraction or poor sparsity can remove the advantage.
No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.
primary-text-checked arXiv v1 full HTML, Sections II.2–II.3, Eq. (11), Fig. 2: controlled zero-order term; checked 29 September 2026.
Companion adversarial implementation review, not a refutation of the WSL theory. Retain the constant Walsh coefficient in a controlled phase circuit; use constant and constant-plus-parity regression cases.
primary-text-checked arXiv v4, 21 January 2025; checked 29 September 2026: II.1, III.1–III.2, IV.1 Eqs. (15)–(16), V.1 Eqs. (19)–(21), VI A, VIII.1 and Tables I–II. Figure 4 signal-sector and III.2/VIII.1 accounting ambiguities remain explicit source obligations.
Parallel scheduling trades ancillas for depth, not automatically total size. Table I uses spectral-norm error; Eq. (18) bounds normalized-block error delta, corresponding to total-scale times delta in the unscaled-operator convention. Exact-block success in source notation is ||D psi||^2/(alpha^2 dmax^2); alpha>1 controls the transformed-angle derivative in smooth approximation. No local source theorem or resolution of source ambiguities is claimed.
primary-text-checked 29 April 2026 public 447-page edition; PDF SHA256 56825000d53025dea4c2998dd6a061592b8fb2b9a446c3194c5f408183327599. First bounded source slice: Chapter 9 Section 9.1, printed pages 141–143, equations (9.2), (9.9), (9.10), (9.12); standing partial-application convention Definition 2.25, page 37. Parts I–IV remain curriculum anchors, not completed formalisation.
Peer Part IV curriculum anchor, reusing existing ASPBE state-preparation/block-encoding APIs. New Chapter 9 adapters, operator-norm approximation, scientific constructions and resource certificates still require separate production admission. No whole-section/book completion is claimed.
Exact function structure to bounded memory
curated-transport independent conceptual review pending; local Lean roots have their own build evidence
\[\{\text{degree and subdivision},\text{bit/branch contract}\}\Longrightarrow R\le2k+6\]
primary-metadata-checked Abstract: explicit function to MPS to circuit; requested v1 HTML was unavailable in this audit
Prior art for function-to-MPS preparation. The ASPBE Hermite specialization must not be credited with inventing polynomial-to-MPS or sequential MPS preparation.
Normalize AND compile AND clean
curated-transport independent conceptual review pending; not a certified functor
primary-metadata-checked Abstract: explicit function to MPS to circuit; requested v1 HTML was unavailable in this audit
Prior art for function-to-MPS preparation. The ASPBE Hermite specialization must not be credited with inventing polynomial-to-MPS or sequential MPS preparation.
primary-text-checked Results: circuit complexity lower bound; construction of LCU-based block-encoding; Methods: state preparation
Explicit access construction is not a free oracle. PREPARE together with SELECT and uncomputation can supply a block encoding; a single prepared state alone does not determine an arbitrary operator.
primary-metadata-checked Authors' publication page: quantum state generation, query characterization and matching lower bound
Prior art for coherent amplitude reweighting. Novelty must be in an explicit structured envelope, guarantees, implementation or model-matched bound, not in rejection sampling itself.
primary-text-checked Article abstract and Gibbs-sampler construction; Communications in Mathematical Physics 406, 67
Invariant Gibbs state and efficient mixing are different obligations. A low-temperature polynomial mixing claim needs additional model-specific evidence.
Design attribution. QuantumComputinglib has its own register, oracle, clean-ancilla and resource contracts; Samplinglib is not an imported Lean dependency.
Preserved contract: Same discrete normalized Hermite state and clean-output convention; exact-real primitive gate model.
Curated repository contribution. Function-to-MPS and sequential preparation are prior art; the metadata does not certify global novelty, optimality or a finite-bit speedup.
Actual Git module/import delta: computed. This is not an elaborated proof-term delta.
Loading the computed Git delta; complete source data is linked below.
Solid lines: added imports. Dashed lines: removed imports. This is the changed module-import neighborhood, not a theorem proof graph or an automatically inferred novelty classification.