Structure before circuit tricks
Current Progress
One generated projection of the existing textbook and implementation frontier, alongside the new research contracts. No manual chapter-completion percentages and no credit transfer from prerequisites.
Compiled local results, source-complete theorems, reusable interfaces, rejected routes and research targets are different evidence classes. The counts below count records, not mathematical importance.
Textbook routes and their exact residual boundaries
Shared foundations Vectors, matrices, and basis states 2 mapped result records
Fix the finite matrix model, pointwise equality, dimensions, and resource records used by every later certificate.
Pointwise matrix equality
\[A = B \;\Longleftrightarrow\; \forall i\,j,\; A_{ij}=B_{ij}.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.Matrix.PointwiseEq
Mapped parents and route-closure names
- QuantumBlockEncoding.Matrix
- QuantumBlockEncoding.Matrix.PointwiseEq
Executable resource records
\[r=(q_{\mathrm{anc}},q_{\mathrm{tot}},d,n_{1q},n_{2q}).\]
Local: Compiled · Route: Compiled
Residual: None within the declared reusable route.
Mapped parents and route-closure names
- QuantumBlockEncoding.gridSize
- QuantumBlockEncoding.ExecutableResourceCertificate.resource_eq_program_resource
- QuantumBlockEncoding.ExecutableResourceCertificate.cost_gateCount
- QuantumBlockEncoding.ExecutableResourceCertificate.cost_depth
Shared foundations Gates, unitaries, and circuit meaning 4 mapped result records
Separate gate syntax from matrix evaluation and make register order an explicit part of the semantic boundary.
Circuit matrix evaluation
\[\mathrm{Eval}([g_1,\ldots,g_m])=G_m\cdots G_1.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.evalGateMatrices
Mapped parents and route-closure names
- QuantumBlockEncoding.GateMatrix
- QuantumBlockEncoding.Matrix
- QuantumBlockEncoding.evalGateMatrices
Flat and product-register clean blocks agree
\[\Pi_s U\Pi_s^\dagger=\operatorname{cleanBlockProduct}(s,U).\]
Local: Compiled · Route: Compiled
Residual: None within the declared reusable route.
QuantumBlockEncoding.ConcreteSemantics.signalSystemBlockProjection_eq_cleanBlockProduct
Mapped parents and route-closure names
- QuantumBlockEncoding.signalSystemBlockProjection
- QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct
- QuantumBlockEncoding.ConcreteSemantics.exactCleanBlockOfSignalProjection
- QuantumBlockEncoding.ConcreteSemantics.exactCleanBlockOfSignalProjection_correct
Circuit-to-block extraction target
\[(\langle0^a\rvert\otimes I)\,U\,(|0^a\rangle\otimes I)=A/\alpha.\]
Local: Compiled · Route: Compiled
Residual: None within the declared reusable route.
QuantumBlockEncoding.CircuitMatrixSemantics.blockExtractionTarget
Mapped parents and route-closure names
- QuantumBlockEncoding.CircuitMatrixSemantics
- QuantumBlockEncoding.signalSystemBlockProjection
- QuantumBlockEncoding.CertifiedCircuitBlockExtraction.extractionTarget
- QuantumBlockEncoding.CertifiedCircuitBlockExtraction.exactCleanBlock
- QuantumBlockEncoding.CertifiedCircuitBlockExtraction.exactCleanBlock_correct
Projected block and clean-branch action agree
\[\Pi U\Pi^\dagger=B\iff \langle0^a,i|U|0^a,j\rangle=B_{ij}.\]
Local: Compiled · Route: Compiled
Residual: None within the finite basis-action/projection bridge.
QuantumBlockEncoding.ConcreteSemantics.pointwiseProjection_iff_cleanBasisAction
Mapped parents and route-closure names
- QuantumBlockEncoding.ConcreteSemantics.cleanBasisActionAmplitude
- QuantumBlockEncoding.ConcreteSemantics.applyVec_basisKet
- QuantumBlockEncoding.ConcreteSemantics.cleanBasisActionAmplitude_eq_signalSystemBlockProjection
- QuantumBlockEncoding.ConcreteSemantics.pointwiseProjection_iff_cleanBasisAction
State preparation The state-preparation problem 3 mapped result records
Ask one concrete question: which unitary sends the all-zero basis state to the normalized state we want?
Hadamard prepares the plus state
\[H|0\rangle=(|0\rangle+|1\rangle)/\sqrt{2}.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate_prepares_plus
Mapped parents and route-closure names
- QuantumBlockEncoding.TextbookStatePreparation.hadamard_unitary
- QuantumBlockEncoding.TextbookStatePreparation.plusTarget_normalized
- QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate_prepares_plus
Pauli X prepares the one state
\[X|0\rangle=|1\rangle,\qquad X|1\rangle=|0\rangle.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate_prepares_one
Mapped parents and route-closure names
- QuantumBlockEncoding.TextbookStatePreparation.pauliX_unitary
- QuantumBlockEncoding.TextbookStatePreparation.oneTarget_normalized
- QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate_prepares_one
The state-preparation contract
\[U\lvert 0^n\rangle=\lvert\psi\rangle.\]
Local: Compiled · Route: Compiled
Residual: None within the declared reusable route.
QuantumBlockEncoding.StatePreparationCandidate.preparesTarget
Mapped parents and route-closure names
- QuantumBlockEncoding.StatePreparationTarget
- QuantumBlockEncoding.StatePreparationCandidate
- QuantumBlockEncoding.StatePreparationCandidate.certify
- QuantumBlockEncoding.StatePreparationCandidate.certify_firstColumn
State preparation Reading and reusing a preparation certificate 3 mapped result records
Connect the ket equation to a matrix column, package the proof, and reuse exact preparation where an approximate interface is expected.
The ket equation is a first-column statement
\[\operatorname{column}_0(U)=\psi\iff U\lvert0^n\rangle=\lvert\psi\rangle.\]
Local: Compiled · Route: Compiled
Residual: None within the declared reusable route.
QuantumBlockEncoding.ConcreteSemantics.firstColumnMatches_iff_applyVec_zeroKet
Mapped parents and route-closure names
- QuantumBlockEncoding.FirstColumnMatches
- QuantumBlockEncoding.ConcreteSemantics.applyVec_zeroKet
- QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.ofFirstColumn
- QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.verifiedOfFirstColumn
- QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.verifiedOfFirstColumn_preparesTarget
A verified preparer exposes its amplitudes
\[U_{i,0}=\psi_i.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.VerifiedStatePreparation.firstColumn
Mapped parents and route-closure names
- QuantumBlockEncoding.VerifiedStatePreparation
- QuantumBlockEncoding.VerifiedStatePreparation.firstColumn
Exact preparation can enter an approximate interface
\[\varepsilon=0.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.VerifiedStatePreparation.asZeroErrorApprox
Mapped parents and route-closure names
- QuantumBlockEncoding.VerifiedStatePreparation
- QuantumBlockEncoding.VerifiedStatePreparation.asZeroErrorApprox
Block encoding The block-encoding contract 2 mapped result records
State the block contract with normalization, explicit register layout, and a verifier-facing certificate record.
Candidate cost is derived from its layout
\[c(U)=(a,q,d,n_{1q},n_{2q},\ldots).\]
Local: Compiled · Route: Compiled
Residual: None within the declared reusable route.
QuantumBlockEncoding.OperatorBlockEncodingCandidate.cost
Mapped parents and route-closure names
- QuantumBlockEncoding.OperatorBlockEncodingCandidate
- QuantumBlockEncoding.RegisterLayout
- QuantumBlockEncoding.BlockEncodingCost
- QuantumBlockEncoding.OperatorBlockEncodingCandidate.cost_eq_fromLayoutAndResource
- QuantumBlockEncoding.OperatorBlockEncodingCandidate.certify
Exact certificates are zero-error approximate certificates
\[\left\|A-\alpha\Pi U\Pi^\dagger\right\|=0.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.VerifiedOperatorBlockEncoding.asZeroErrorApprox
Mapped parents and route-closure names
- QuantumBlockEncoding.VerifiedOperatorBlockEncoding
- QuantumBlockEncoding.QueryOperatorTarget
- QuantumBlockEncoding.VerifiedOperatorBlockEncoding.asZeroErrorApprox
Block encoding Construction routes and composition rules 4 mapped result records
Reuse permutation, one-sparse, LCU, product, dilation, and QSVT interfaces instead of rediscovering each route per benchmark.
Banded sparse address access
\[|0^{n-l}\rangle|s\rangle|i\rangle\mapsto|r_{s0}+i\bmod 2^n\rangle|i\rangle.\]
Local: Compiled · Route: Compiled
Residual: None within the declared semantic-plus-finite-compiler route. The paper's arbitrary-size one-qubit/CNOT upper bound remains a separate general compiler theorem.
QuantumBlockEncoding.BandedSparseAccess.accessEquiv_clean_slot
Mapped parents and route-closure names
- QuantumBlockEncoding.BandedSparseAccess.modularSumEquiv
- QuantumBlockEncoding.BandedSparseAccess.accessMatrix_unitary
- QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_eval
- QuantumBlockEncoding.BandedSparseAccess.accessMatrix_unitary
- QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3_cleanAction
- QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_eval
- QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_unitary
- QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_oracleCalls_eq_zero
Partial-permutation certificate
\[A_{ij}\in\{0,1\},\quad \text{at most one supported entry per routed index}.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.BlockEncodingClassics.partialPermutationCertificate
Mapped parents and route-closure names
- QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
- QuantumBlockEncoding.BlockEncodingClassics.partialPermutationCertificate
Product closure for exact clean blocks
\[\operatorname{block}(U_B U_A)=BA.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.BlockEncodingClassics.productExactCleanBlockCertificate
Mapped parents and route-closure names
- QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
- QuantumBlockEncoding.BlockEncodingClassics.matrix_mul_congr_pointwise
- QuantumBlockEncoding.BlockEncodingClassics.productExactCleanBlockCertificate
QSVT consumer boundary
\[U_A\leadsto p^{(\mathrm{SV})}(A/\alpha).\]
Local: Compiled · Route: Compiled
Residual: None within the declared reusable route.
QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract
Mapped parents and route-closure names
- QuantumBlockEncoding.BlockEncodingClassics.HermitianDilationContract
- QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity
- QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity_output
Block encoding Certified block-encoding cases 4 mapped result records
Distinguish completed local certificates from paper-facing contract models and historical experiments.
BE Case 1 block projection
\[\Pi U_{\mathrm{E1}}\Pi^\dagger=A_{\mathrm{E1}}/\alpha.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.coldE1Candidate_blockProjection
Mapped parents and route-closure names
- QuantumBlockEncoding.coldE1CandidateImage_permutation_certificate
- QuantumBlockEncoding.BlockEncodingClassics.partialPermutationCertificate
- QuantumBlockEncoding.coldE1Candidate_blockProjection
BE Case 2 exact Householder completion
\[\Pi U_{\mathrm{cubic}}\Pi^\dagger=D_{\mathrm{cubic}}/\alpha.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_complete
Mapped parents and route-closure names
- QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract_complete
- QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalRationalCompletion_backendSupport
- QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_complete
GHL Theorem 4: source-audited LCU composition to the Hamiltonian
\[A=\sum_kA_k,\quad A^\dagger=\sum_kA_k^\dagger,\quad H=S_1\otimes x_\xi+S_2\otimes I_\xi.\]
Local: Compiled · Route: Compiled
Residual: The source-audited Theorem-4 composition is closed. Uniform arbitrary-width primitive compilation of all Theorem-3 source oracles and their concrete gate/resource realization remains a separate compiler frontier.
QuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed
Mapped parents and route-closure names
- QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint_sumTerms
- QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare_unitary
- QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare_cleanEntry
- QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1
- QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1
- QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean_eq_S2
- QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint_sumTerms
- QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_lowerRight
- QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1
- QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1
- QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean_eq_S2
- QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H_eq_S1_tensor_xXi_add_S2_tensor_I
- QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_normalization_closed
- QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_layout_closed
- QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianResource_pureAncilla_closed
- QuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed
Robin raw-fold route is rejected
\[U_{00}\ne\sum_{s=0}^{6} B_s.\]
Local: Compiled · Route: Compiled
Residual: The rejected branch is closed. Fixed-N8 source circuits and the GHL Theorem-4 A-to-H composition are compiled; arbitrary-width primitive compilers for the general source oracles remain separately scoped.
QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3
Mapped parents and route-closure names
- QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryBackendExpansionStatement_not_n3
- QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryBackendExpansionStatement_equivUnitaryEntryFold_n3
- QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3
System and evidence Candidate comparison and executable exports 4 mapped result records
Keep formal validity lexicographically ahead of resource quality, then expose accepted candidates to executable tooling.
Control only the middle of a conjugation
\[C(V^\dagger U V)=(I\otimes V^\dagger)\,C(U)\,(I\otimes V).\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.PromiseGateOptimization.controlledConjugation_matrix
Mapped parents and route-closure names
- QuantumBlockEncoding.PromiseGateOptimization.controlledConjugation_equiv
- QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix_mul
- QuantumBlockEncoding.PromiseGateOptimization.controlledConjugation_matrix
Replace a clean flag by a dirty flag
\[U^2=I\Longrightarrow(c,b,|\psi\rangle)\mapsto(c,b,U^{[c]}|\psi\rangle).\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolution_action
Mapped parents and route-closure names
- QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolutionEquiv
- QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolution_unitary
- QuantumBlockEncoding.PromiseGateOptimization.dirtyControlledInvolution_action
Lexicographic candidate comparison
\[c_1\prec_{\mathrm{lex}}c_2.\]
Local: Compiled · Route: Compiled
Residual: None for this local declaration.
QuantumBlockEncoding.BlockEncodingCost.betterThan
Mapped parents and route-closure names
- QuantumBlockEncoding.BlockEncodingCost
- QuantumBlockEncoding.BlockEncodingCost.betterThan
Finite cubic amplitude oracle
\[\Pi_0U_{\mathrm{cubic},2}\Pi_0^\dagger=\operatorname{diag}(0,(1/4)^3,(2/4)^3,(3/4)^3).\]
Local: Compiled · Route: Compiled
Residual: None within the fixed n=2 primitive route. Scalable arithmetic and general QSVT phase synthesis remain separately scoped research routes.
QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveVerifiedBlockEncoding
Mapped parents and route-closure names
- QuantumBlockEncoding.compileUniformlyControlledRy_eval_controlledRyBlockMatrix
- QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram_cleanEntry
- QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary_unitary
- QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveProgram_cleanEntry
- QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary_unitary
- QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveFlatUnitary_cleanBlock
- QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveVerifiedBlockEncoding
- QuantumBlockEncoding.CubicDiagonalOracle.cubicN2Primitive_oracleCalls_eq_zero
System and evidence Search control, evidence, and open work 2 mapped result records
Show how typed stages, agent layers, candidate populations, proof gates, and explicit open problems coordinate without overstating evidence.
Three-layer agent contracts
\[\text{upper}\rightarrow\text{middle}\rightarrow\text{lower}\rightarrow\text{reviewer}\rightarrow\text{accepted}.\]
Local: Compiled · Route: Compiled
Residual: None within the typed handoff and acceptance route. Running external models remains engineering evidence rather than a Lean theorem.
QuantumBlockEncoding.threeLayerAgentContracts
Mapped parents and route-closure names
- QuantumBlockEncoding.AutomationStage
- QuantumBlockEncoding.AutomationTask
- QuantumBlockEncoding.ThreeLayerTrace
- QuantumBlockEncoding.threeLayerCanonicalTrace_allValid
- QuantumBlockEncoding.threeLayerCanonicalTrace_reachesAccepted
- QuantumBlockEncoding.threeLayerAccepted_requiresLeanGate
- QuantumBlockEncoding.threeLayerAccepted_requiresReviewerApproval
- QuantumBlockEncoding.threeLayerFailedGateTrace_notAccepted
Open problems are first-class data
\[\mathcal O=[o_1,\ldots,o_7],\qquad \operatorname{Nodup}(\operatorname{id}(\mathcal O)).\]
Local: Compiled · Route: Compiled
Residual: The registry route is closed; its seven mathematical problems remain intentionally open and are not presented as solved theorems.
QuantumBlockEncoding.openProblems
Mapped parents and route-closure names
- QuantumBlockEncoding.OpenProblem
- QuantumBlockEncoding.openProblemIds
- QuantumBlockEncoding.openProblems_count
- QuantumBlockEncoding.openProblemIds_nodup
- QuantumBlockEncoding.openProblems_all_actionable
- QuantumBlockEncoding.openProblemRegistry_compiled
Existing source-paper routes
Quantum Framework for Simulating Linear PDEs with Robin Boundary Conditions
reproduced-fixed-benchmark
Source anchors: Eq. (9), Theorem 3, Theorem 4, Fig. 4
Current scope: Theorem 3/4 are mapped to explicit Lean scope. The fixed N=8 Robin benchmark closes source normal forms, an exact XOR four-slot winner, and same-tier resource comparisons; the arbitrary-width primitive compiler remains a separate frontier.
Residual / next acceptance boundary: Theorem 3/4 are mapped to explicit Lean scope. The fixed N=8 Robin benchmark closes source normal forms, an exact XOR four-slot winner, and same-tier resource comparisons; the arbitrary-width primitive compiler remains a separate frontier.
No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.
Transformation of quantum states using uniformly controlled rotations
finite-benchmark-formalized
Source anchors: Eq. (6), Eq. (7), Eq. (8), Fig. 3
Current scope: An exact dense two-qubit target, full unitary completion, typed root-RY plus one-control-UCRY circuit, exact clean-input state action, and the circuit-derived resource tuple (5 gates, depth 4, no auxiliary qubits, no unresolved oracle calls).
Residual / next acceptance boundary: General n-qubit state-to-state synthesis, phase layer, analytic rotation-angle construction at arbitrary width, and the paper-wide CNOT/one-qubit rotation count theorem.
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseTarget_normalized
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseMatrix_unitary
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitive_prepares_target
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseVerified_cost
Creating superpositions that correspond to efficiently integrable probability distributions
structured-benchmark-formalized
Source anchors: Eq. (1), Eq. (3), Eq. (5), Eq. (6)
Current scope: An exact two-bit product distribution, a typed generic binary-tree circuit and typed factorized circuit preparing the same target, and a Lean-certified resource improvement from (5,4,0,0) to (2,1,0,0).
Residual / next acceptance boundary: The general efficiently-integrable recursive probability-loading theorem and an end-to-end arithmetic/integration oracle compiler.
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphProductTarget_normalized
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_prepares_target
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTree_prepares_target
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeVerified_cost
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedVerified_cost
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_betterThan_tree
Nearly Optimal Circuit Size for Sparse Quantum State Preparation
finite-sparse-benchmark-formalized
Source anchors: Eq. (1), Eq. (2), Theorem 1
Current scope: An exact n=3, d=3 witness of Eq. (2), a typed pruned UCRY route, a same-target typed dense zero-fill baseline, and a Lean-certified resource improvement from (15,13,0,0) to (5,4,0,0).
Residual / next acceptance boundary: The asymptotic sparse synthesis constructions, ancilla/circuit-size tradeoffs, and the matching lower bounds of Theorem 1.
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeTarget_normalized
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeMatrix_unitary
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.sparsePruned_prepares_target
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTree_prepares_target
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeVerified_cost
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedVerified_cost
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.sparsePruned_betterThan_denseTree
Trading T gates for dirty qubits in state preparation and unitary synthesis
resource-lemma-formalized
Source anchors: Eq. (2), Eq. (5), Table 2, Fig. 1(c,d)
Current scope: The clean-qubit SelectSwap T-count formula at the repository arithmetic tier, including N=16, b=1 values 72 at lambda=1 and 48 at lambda=4, plus the strict finite comparison 48<72.
Residual / next acceptance boundary: Approximate Clifford+T state preparation, coherent lookup/SelectSwap semantics, dirty-qubit correctness, error accounting, and the full asymptotic optimality theorem.
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.StatePreparationBenchmarks.selectSwapCleanTCount_16_1_1
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.selectSwapCleanTCount_16_1_4
Locate the same declaration in the Lean graph
QuantumBlockEncoding.StatePreparationBenchmarks.selectSwapCleanTCount_lambda4_better_lambda1
Asymptotically Optimal Circuit Depth for Quantum State Preparation and General Unitary Synthesis
queued
Source anchors:
Current scope: Not yet reproduced in Lean.
Residual / next acceptance boundary: The ancilla-sensitive state-preparation construction, depth/size upper bounds, and the matching optimal-depth statements across the claimed parameter regimes.
No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.
Quantum-state preparation with universal gate decompositions
queued
Source anchors:
Current scope: Not yet reproduced in Lean.
Residual / next acceptance boundary: Universal state-preparation decomposition and its CNOT/depth counts, including the four-qubit benchmark.
No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.
Synthesis of Quantum Logic Circuits
queued
Source anchors:
Current scope: The local uniformly-controlled-RY compiler provides a related reusable primitive, but this paper is not claimed reproduced.
Residual / next acceptance boundary: Paper-faithful quantum-multiplexor/state-initialization synthesis, its CNOT complexity theorem, and the lower-bound comparison.
No local transport theorem is bound to this record. Do not infer formal truth from its position in the atlas.
Existing implementation frontier — preserved, not overwritten
Prepare the one-qubit plus state
\[H|0\rangle=(|0\rangle+|1\rangle)/\sqrt2\]
Compiled
Obligation: Normalization, Mathlib unitarity, state action, and logical cost
Existing parents: hadamard_unitary; plusTarget_normalized; hadamard_prepares_plus
Residual / next boundary: None for this textbook route
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate_prepares_plus
Prepare the one-qubit basis state one
\[X|0\rangle=|1\rangle\]
Compiled
Obligation: Permutation unitarity, state action, and logical cost
Existing parents: pauliX_unitary; oneTarget_normalized; pauliX_prepares_one
Residual / next boundary: None for this textbook route
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate_prepares_one
Prepare a finite target state
\[U|0^n\rangle=|\psi\rangle\]
Compiled
Obligation: Normalization, unitarity, and first-column equality supplied to the promotion constructor
Existing parents: StatePreparationCandidate.certify; textbook Pauli-X and Hadamard witnesses
Residual / next boundary: None for the reusable promotion route; each new target family supplies its own proof terms
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.StatePreparationCandidate.preparesTarget
Consume a verified prepared state
\[U_{i0}=\psi_i\]
Compiled
Obligation: First-column projection
Existing parents: VerifiedStatePreparation
Residual / next boundary: None locally
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
Read first-column evidence as state action
\[\operatorname{column}_0(U)=\psi\iff U|0^n\rangle=|\psi\rangle\]
Compiled
Obligation: Finite basis-ket matrix-action bridge
Existing parents: FirstColumnMatches; applyVec_zeroKet
Residual / next boundary: Candidate normalization and unitarity remain separate
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.ConcreteSemantics.firstColumnMatches_iff_applyVec_zeroKet
Evaluate a gate list
\[\mathrm{Eval}(C)=G_m\cdots G_1\]
Compiled
Obligation: Fixed fold and register order
Existing parents: GateMatrix; Matrix
Residual / next boundary: None locally
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
Extract a block from a circuit
\[\Pi U\Pi^\dagger=A/\alpha\]
Compiled
Obligation: Typed circuit semantics, selected projection equality, and finite identity witness
Existing parents: CertifiedCircuitBlockExtraction; teachingIdentityBlockExtraction
Residual / next boundary: None for the reusable extraction route; each concrete circuit supplies its unitary and entry proof
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.CircuitMatrixSemantics.blockExtractionTarget
Move between flat and product-register block views
\[\Pi_s U\Pi_s^\dagger=\operatorname{cleanBlockProduct}(s,U)\]
Compiled
Obligation: Shared register-order projection equality
Existing parents: signalSystemBlockProjection; cleanBlockProduct
Residual / next boundary: Candidate-level block and unitarity proofs remain separate
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.ConcreteSemantics.signalSystemBlockProjection_eq_cleanBlockProduct
Package an exact block encoding
\[\Pi U\Pi^\dagger=A/\alpha\]
Compiled
Obligation: Candidate unitarity and exact block identity supplied to the promotion constructor
Existing parents: OperatorBlockEncodingCandidate.certify; certified finite cases
Residual / next boundary: None for the reusable promotion route; concrete candidate fields remain route-specific inputs
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
Reuse an exact certificate approximately
\[\|A-\alpha\Pi U\Pi^\dagger\|=0\]
Compiled
Obligation: Zero-error conversion
Existing parents: VerifiedOperatorBlockEncoding
Residual / next boundary: Positive-error analyses are route-specific
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.VerifiedOperatorBlockEncoding.asZeroErrorApprox
Certify a partial permutation
\[\operatorname{block}(U)=A\]
Compiled
Obligation: Finite routed-entry proof
Existing parents: ExactCleanBlock
Residual / next boundary: None locally
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.BlockEncodingClassics.partialPermutationCertificate
Compose exact block encodings
\[\operatorname{block}(U_BU_A)=BA\]
Compiled
Obligation: Projected product equality
Existing parents: ExactCleanBlock; matrix_mul_congr_pointwise
Residual / next boundary: Register compatibility for each application
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.BlockEncodingClassics.productExactCleanBlockCertificate
Close BE Case 1
\[\Pi U_{\mathrm{E1}}\Pi^\dagger=A_{\mathrm{E1}}/\alpha\]
Compiled
Obligation: Transfer-operator projection
Existing parents: coldE1CandidateImage_permutation_certificate
Residual / next boundary: None locally
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
Close BE Case 2
\[\Pi U_{\mathrm{cubic}}\Pi^\dagger=D/\alpha\]
Compiled
Obligation: Exact rational Householder completion
Existing parents: Householder input; rational backend support
Residual / next boundary: None for the selected exact route
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_complete
Feed a certified clean block to a typed polynomial consumer
\[U_D\leadsto p^{(\mathrm{SV})}(D/\alpha)\]
Compiled
Obligation: Source certificate, side conditions, and a finite degree-one identity realization
Existing parents: QSVTConsumerContract.identity; teachingIdentityQSVTConsumer
Residual / next boundary: None for the typed identity consumer; general phase synthesis and approximation checking remain roadmap items
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract
Compile a finite banded sparse-access witness
\[|s\rangle|i\rangle|0\rangle\mapsto|s\oplus3+i\bmod8\rangle|i\rangle|0\rangle\]
Compiled
Obligation: Primitive refinement, clean workspace, unitarity, and zero oracle calls
Existing parents: modularAdd3ReversibleProgram; compileReversibleProgram_eval
Residual / next boundary: Arbitrary-width source gate upper bounds remain a separate compiler theorem
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_eval
Compile a finite cubic diagonal amplitude oracle
\[\Pi_0U\Pi_0^\dagger=\operatorname{diag}((j/4)^3)\]
Compiled
Obligation: Exact multiplexed RY semantics, clean projection, and verified BE packaging
Existing parents: UniformlyControlledRy; PrimitiveBasisLE; exact RY bridge
Residual / next boundary: Scalable arithmetic and general QSVT phase synthesis are separate routes
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveVerifiedBlockEncoding
Verify three-layer harness promotion
\[\text{upper}\to\text{middle}\to\text{lower}\to\text{reviewer}\to\text{accepted}\]
Compiled
Obligation: Logged artifacts, valid role order, Lean gate, and reviewer approval
Existing parents: ThreeLayerHandoff.validFlag; ThreeLayerTrace.finalPhase
Residual / next boundary: External model execution remains engineering evidence
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.threeLayerCanonicalTrace_reachesAccepted
Audit the open-problem registry
\[|\mathcal O|=7\land\operatorname{Nodup}(\operatorname{id}(\mathcal O))\]
Compiled
Obligation: Unique identifiers and nonempty actionable fields
Existing parents: openProblemIds_nodup; openProblems_all_actionable
Residual / next boundary: The registered mathematical problems intentionally remain open
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
Compose the GHL one-dimensional Hamiltonian
\[A=\sum_kA_k,\ A^\dagger=\sum_kA_k^\dagger,\ H=S_1\otimes x_\xi+S_2\otimes I_\xi\]
Compiled
Obligation: Finite sum/adjoint bridge, Hermitian S1/S2 split, and final Hamiltonian composition
Existing parents: adjoint_sumTerms; verified ComplexLCU kernel; eq29PrintedClean_ne_S1; eq29PhaseBalancedClean_eq_S1; eq30Clean_eq_S2
Residual / next boundary: None for the source-audited Theorem-4 composition; arbitrary-width primitive one-term gate/resource compilation is a separate frontier
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed
Close the historical Robin raw-fold branch
\[U_{00}\ne\sum_s B_s\]
Compiled
Obligation: Convert the raw fold to the refuted backend expansion
Existing parents: Equivalence bridge; all-one counterexample
Residual / next boundary: None for the rejected branch; cited oracle implementations remain experimental
Named Lean substrates below have their own exact signatures. They do not certify every sentence or proposed generalization on this page.
QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3
Previously pending work
These are the existing roadmap entries, not newly invented completions. Each resumes by fixing the source target and checking which compiled interfaces genuinely discharge it.
Arbitrary-width banded-access source resource compiler
Planned
Next: freeze an arbitrary-width/source contract; connect current semantic leaves to the actual primitive compiler; prove the resource theorem; then pass independent source fidelity and publication gates.
General QSVT phase synthesis and approximation checker
Planned
Next: freeze an arbitrary-width/source contract; connect current semantic leaves to the actual primitive compiler; prove the resource theorem; then pass independent source fidelity and publication gates.
Arbitrary-width GHL one-term primitive resource compiler
Planned
Next: freeze an arbitrary-width/source contract; connect current semantic leaves to the actual primitive compiler; prove the resource theorem; then pass independent source fidelity and publication gates.
StatePreparationWiki execution queue
Priority 1 · research target
Coherent parameter-dependent families
Use an affine parameterized Hermite or Gaussian family as a small exact model before time-dependent PDE source histories.
First acceptance test: One matrix action for arbitrary parameter superpositions.
Priority 1 · research target
Preconditioned function preparation with an explicit envelope
First close the support-aware probability identity, then study anisotropic product envelopes and a controlled perturbation class.
First acceptance test: All amplitudes including zero-reference entries and complex phases agree; normalizer nonzero.
Priority 1 · research target
High-dimensional structured function states
Start from the Hermite corridor; add a tensor-product or shallow coupled class with a proved rank bound before claiming general high dimension.
First acceptance test: A source-faithful class predicate and formula-to-core action theorem, including phases and supports.
Priority 2 · research target
CV–DV function preparation and non-Gaussian resources
Choose a finite-energy Hermite-smoothed profile and one embedding before comparing grid, oscillator or GKP implementations.
First acceptance test: Inner products and normalization match the stated quadrature/Fock convention.
Priority 2 · research target
Fault-tolerant resource trade-offs for structured preparation
Treat the current Hermite bit-complexity boundary as the first local target rather than reopening its exact-real correctness proof.
First acceptance test: All arbitrary-real comparisons and small pivots have explicit handling.
Priority 2 · research target
Data loading without a free QRAM assumption
Reuse existing sparse/LCU routes only after auditing their oracle contracts and compiler frontiers.
First acceptance test: Separate data construction, coherent calls, memory and update costs.
Priority 2 · research target
Joint design of preparation and experimental verification
Verify the primary hardware reference first; start formal work from a small exactly analyzable MPS witness.
First acceptance test: Outcome law, confidence and noise assumptions are formal objects.
Priority 3 · research target
Low-temperature Gibbs preparation with quantitative mixing
Use a finite-dimensional warm-up and then separate the high-temperature baseline from the intended low-temperature regime.
First acceptance test: Exact generator, Gibbs normalizer and adjoint convention.
Priority 3 · research target
Useful trial states for strong-correlation ground-state preparation
Begin with a controlled family with a rigorous trial-state overlap, not arbitrary strongly correlated molecules.
First acceptance test: Gap, overlap, energy information and success convention match the source.
Contribution admission
Source statement → exact Lean statement → source-blind reconstruction → independent comparison → separately reviewed repairs. Authors do not self-certify a review. A graph delta records add-node, shortcut, reorganisation or bridge, while global novelty remains a separate literature judgement.
Read the adapted ASPBE publication protocol · Download this generated progress snapshot