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.

Choose a complete transport

Dashed paths: curated/proposed incidence. AND junction: all listed hypotheses and tail mechanisms. Solid proof dependencies remain in the separate generated Lean graph.

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

All inputs required

AND

Conditional outputs

Bounded-memory function representations

Mechanism: Keep local polynomial updates and branch routing together; neither alone proves the sampled source.
Hypothesis map: Endpoint jets, grid coordinate, boundary ownership and bit order agree.
Conclusion map: The finite core contraction equals the literal sampled Hermite function.
Failure boundary: A degree statement alone does not account for an arbitrary number of pieces.

Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.

QuantumBlockEncoding.HermiteFiniteChain.sourceChain_contract

Locate the same declaration in the Lean graph

Efficient Quantum Circuits for Accurate State Preparation of Smooth, Differentiable Functions

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

\{\text{explicit TT},\ Z>0,\text{local compiler}\}\Longrightarrow U|0^{m+q}\rangle=|g_k\rangle|0^q\rangle

All inputs required

AND

Conditional outputs

State-action and coherent preparation contracts

Mechanism: Compose the source, norm and primitive-circuit interfaces.
Hypothesis map: Real normalized scalar-boundary chain, rank bound, padded register layout and signed residual boundary.
Conclusion map: All target amplitudes and all non-clean sectors, plus actual primitive-list count.
Failure boundary: An existence-only TT representation or unknown normalizer is not a data-producing compiler.

Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.

QuantumBlockEncoding.ConstructiveHermitePreparation.prepare_spec

Locate the same declaration in the Lean graph

Efficient Quantum Circuits for Accurate State Preparation of Smooth, Differentiable Functions

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.

SP + SELECT gives an LCU block

proposal independent review pending

P^\dagger\operatorname{SELECT}(U)P\rightsquigarrow A/\alpha

All inputs required

AND

Conditional outputs

Block Encoding

Mechanism: The AND node explicitly includes controlled operator access and unpreparation.
Hypothesis map: Square-root coefficient amplitudes, SELECT unitaries, adjoint access and phase convention.
Conclusion map: A specified projected matrix block, not merely one state.
Failure boundary: No arrow from an isolated prepared state to arbitrary A; state copies do not supply controlled U or U-dagger.

No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.

Circuit complexity of quantum access models for encoding classical data

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.

BE + input + overlap gives a state branch

proposal independent review pending

\Pi U_A(|0\rangle|\psi\rangle)=A|\psi\rangle/\alpha

All inputs required

AND

Conditional outputs

State Preparation

Mechanism: Project the block, retain the accepted branch and account for success amplification.
Hypothesis map: Nonzero A psi, available input preparation and declared oracle inverses/controls.
Conclusion map: Normalized A psi conditional on success or an explicitly amplified approximation.
Failure boundary: Small overlap can dominate the cost; this is not an unconditional cheap reverse conversion.

No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.

Quantum State Preparation without Coherent Arithmetic

primary-metadata-checked Abstract; Physical Review Letters 136, 240603, published 18 June 2026

QET-based function preparation with few ancillas. Approximation, normalization and success probability remain separate costs.

Near-optimal ground state preparation

primary-metadata-checked Abstract: initial overlap, spectral-gap promise, energy information and lower bounds

Use the promised overlap/gap model; do not erase these costs in a generic strong-correlation claim.

Harmonic analysis to quantum evolution

proposal independent review pending

H_{\rm Sch}=D_p\otimes A_1-I\otimes A_2

All inputs required

AND

Conditional outputs

Block Encoding

Mechanism: The prepared auxiliary profile is one supplier; operator access and recovery remain separate.
Hypothesis map: Hermitian components, Fourier sign, finite grid and norm/recovery budget.
Conclusion map: Candidate Hamiltonian-access route for Schrödingerisation.
Failure boundary: SP certification alone proves neither the Hamiltonian block encoding nor end-to-end PDE accuracy.

No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.

No external source is attached to this local mechanism note. It remains authored exposition, not a literature-priority claim.

Sampling envelope meets function structure

proposal independent review pending

\kappa_{\rm env}=C\|g\|_2/\|f\|_2

All inputs required

AND

Conditional outputs

State Preparation

Mechanism: Search for an envelope with both a provable ratio bound and a constructive small representation.
Hypothesis map: Support domination, ratio degree/rank, phase access and charged reference preparation.
Conclusion map: A model-specific success and end-to-end cost target.
Failure boundary: A good classical envelope need not have a cheap coherent preparation; no universal cure for dimensionality.

No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.

Quantum Rejection Sampling

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.

Quantum state preparation for multivariate functions

primary-metadata-checked Abstract and article record

Multivariate preparation baseline; a tensor-product coefficient count is not automatically polynomial in dimension.

A coercivity mechanism, not an equality of samplers

proposal independent review pending

\text{invariance}+\text{quantitative dissipation}\Longrightarrow\text{a declared convergence rate}

All inputs required

AND

Conditional outputs

Gibbs invariance versus mixing

Mechanism: Compare the role of a functional inequality in classical and quantum semigroups.
Hypothesis map: Different state spaces, noncommutativity, detailed-balance conventions and divergences remain explicit.
Conclusion map: A hypothesis-mapped conceptual mirror with candidate shared matrix/semigroup lemmas.
Failure boundary: Classical LSI or reversibility is not automatically a quantum KMS mixing certificate.

No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.

Efficient Quantum Gibbs Samplers with Kubo–Martin–Schwinger Detailed Balance Condition

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.

Samplinglib theorem-publication and conceptual-mirror protocols

primary-text-checked Author once; graph contribution; independent encoder–denoiser; unchanged historical audit debt

Design attribution. QuantumComputinglib has its own register, oracle, clean-ancilla and resource contracts; Samplinglib is not an imported Lean dependency.

Preparation structure plus measurement contract

proposal independent review pending

\Pr[|\widehat F-F|\le\epsilon]\ge1-\delta

All inputs required

AND

Conditional outputs

Verification and metrology

Mechanism: Use the state description to propose a measurement witness; formal circuit proof and statistical evidence remain separate.
Hypothesis map: Experimental measurement access, noise, sample model, epsilon and delta.
Conclusion map: Candidate low-sample verification protocol for a specified family.
Failure boundary: An ideal Lean proof is not a hardware fidelity certificate.

No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.

Efficient quantum state preparation on Quantinuum hardware (candidate reference)

primary-source-unavailable User-supplied arXiv identifier; primary fetch failed; do not use reported hardware numbers as evidence

Retained in the candidate queue rather than silently promoted from secondary indexing.

Hermite: dense tree to bounded-memory construction

add-nodeshortcutreorganisationbridge

Before

Generic amplitude tree retains one independent branch per sample; exponential gate count in the data-qubit count, not exponential ancillas.

After

Preserve the formula through Bernstein subdivision and bounded TT cores, then reuse a generic local-isometry compiler.

R=2k+6,\quad q=\lceil\log_2R\rceil,\quad G\le48mR^3

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.

Inspect changed import edges around a module

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.

Added modules at the pinned contribution

module:QuantumBlockEncoding.AdjacentGivens
module:QuantumBlockEncoding.ConstructiveHermitePreparation
module:QuantumBlockEncoding.ConstructiveIsometryCompletion
module:QuantumBlockEncoding.ConstructiveIsometryLocal
module:QuantumBlockEncoding.ConstructiveTensorTrain
module:QuantumBlockEncoding.ConstructiveTensorTrainCompiler
module:QuantumBlockEncoding.ConstructiveThinLQ
module:QuantumBlockEncoding.GrayBasis
module:QuantumBlockEncoding.GrayGivensCompiler
module:QuantumBlockEncoding.HermiteBernstein
module:QuantumBlockEncoding.HermiteBoundaryInjection
module:QuantumBlockEncoding.HermiteCutRank
module:QuantumBlockEncoding.HermiteFiniteChain
module:QuantumBlockEncoding.HermiteFiniteNorm
module:QuantumBlockEncoding.HermiteIntervalMass
module:QuantumBlockEncoding.HermitePolynomialPreparation
module:QuantumBlockEncoding.HermitePolynomialResources
module:QuantumBlockEncoding.HermiteSampleStructure
module:QuantumBlockEncoding.HermiteTransferCores
module:QuantumBlockEncoding.MatrixProductChain
module:QuantumBlockEncoding.PrimitiveDepthBound
module:QuantumBlockEncoding.PrimitiveWireRename
module:QuantumBlockEncoding.RealIsometryCompletion
module:QuantumBlockEncoding.RectangularGivens
module:QuantumBlockEncoding.SelectedRyPlane
module:QuantumBlockEncoding.SelectedRyTrace
module:QuantumBlockEncoding.SequentialBondPreparation
module:QuantumBlockEncoding.SequentialPrimitiveAssembly
module:QuantumBlockEncoding.StoredBernstein
module:QuantumBlockEncoding.StoredGivens
module:QuantumBlockEncoding.StoredIsometryCompletion
module:QuantumBlockEncoding.StoredRectangularGivens
module:QuantumBlockEncoding.StoredTensorTrain
module:QuantumBlockEncoding.StoredThinLQ
module:QuantumBlockEncoding.TensorTrainCanonical
module:QuantumBlockEncoding.TensorTrainLocalCompiler
module:QuantumBlockEncoding.TensorTrainNormEnvironment
module:QuantumBlockEncoding.TensorTrainPrimitivePreparation
module:QuantumBlockEncoding.TensorTrainSchedule
module:QuantumBlockEncoding.TensorTrainWord
module:QuantumBlockEncoding.ThinLQ

Download baseline/head and exact module-import delta