Generated links · Curated route status
Implementation Map
Trace a mathematical statement to the exact Lean declaration, source line, dependencies, current status, and work that remains. The map is grouped by the same learning tracks used throughout the site.
Shared foundations
| Mathematical goal | Contract | Proof obligation | Lean declaration | Module / line | Dependencies | Status | Missing step | Reader links |
|---|---|---|---|---|---|---|---|---|
| Evaluate a gate list | \(\mathrm{Eval}(C)=G_m\cdots G_1\) | Fixed fold and register order | QuantumBlockEncoding.evalGateMatrices |
QuantumBlockEncoding/CircuitSemantics.lean:54 |
GateMatrix; Matrix | Compiled | None locally | chapter · Blueprint |
| Extract a block from a circuit | \(\Pi U\Pi^\dagger=A/\alpha\) | Typed circuit semantics, selected projection equality, and finite identity witness | QuantumBlockEncoding.CircuitMatrixSemantics.blockExtractionTarget |
QuantumBlockEncoding/CircuitSemantics.lean:786 |
CertifiedCircuitBlockExtraction; teachingIdentityBlockExtraction | Compiled | None for the reusable extraction route; each concrete circuit supplies its unitary and entry proof | chapter · Blueprint |
| Move between flat and product-register block views | \(\Pi_s U\Pi_s^\dagger=\operatorname{cleanBlockProduct}(s,U)\) | Shared register-order projection equality | QuantumBlockEncoding.ConcreteSemantics.signalSystemBlockProjection_eq_cleanBlockProduct |
QuantumBlockEncoding/ConcreteSemantics.lean:194 |
signalSystemBlockProjection; cleanBlockProduct | Compiled | Candidate-level block and unitarity proofs remain separate | chapter · Blueprint |
State preparation
| Mathematical goal | Contract | Proof obligation | Lean declaration | Module / line | Dependencies | Status | Missing step | Reader links |
|---|---|---|---|---|---|---|---|---|
| Prepare the one-qubit plus state | \(H|0\rangle=(|0\rangle+|1\rangle)/\sqrt2\) | Normalization, Mathlib unitarity, state action, and logical cost | QuantumBlockEncoding.TextbookStatePreparation.hadamardCertificate_prepares_plus |
QuantumBlockEncoding/TextbookStatePreparation.lean:168 |
hadamard_unitary; plusTarget_normalized; hadamard_prepares_plus | Compiled | None for this textbook route | chapter · Blueprint |
| Prepare the one-qubit basis state one | \(X|0\rangle=|1\rangle\) | Permutation unitarity, state action, and logical cost | QuantumBlockEncoding.TextbookStatePreparation.pauliXCertificate_prepares_one |
QuantumBlockEncoding/TextbookStatePreparation.lean:162 |
pauliX_unitary; oneTarget_normalized; pauliX_prepares_one | Compiled | None for this textbook route | chapter · Blueprint |
| Prepare a finite target state | \(U|0^n\rangle=|\psi\rangle\) | Normalization, unitarity, and first-column equality supplied to the promotion constructor | QuantumBlockEncoding.StatePreparationCandidate.preparesTarget |
QuantumBlockEncoding/StatePreparation.lean:43 |
StatePreparationCandidate.certify; textbook Pauli-X and Hadamard witnesses | Compiled | None for the reusable promotion route; each new target family supplies its own proof terms | chapter · Blueprint |
| Consume a verified prepared state | \(U_{i0}=\psi_i\) | First-column projection | QuantumBlockEncoding.VerifiedStatePreparation.firstColumn |
QuantumBlockEncoding/StatePreparation.lean:98 |
VerifiedStatePreparation | Compiled | None locally | chapter · Blueprint |
| Read first-column evidence as state action | \(\operatorname{column}_0(U)=\psi\iff U|0^n\rangle=|\psi\rangle\) | Finite basis-ket matrix-action bridge | QuantumBlockEncoding.ConcreteSemantics.firstColumnMatches_iff_applyVec_zeroKet |
QuantumBlockEncoding/ConcreteSemantics.lean:76 |
FirstColumnMatches; applyVec_zeroKet | Compiled | Candidate normalization and unitarity remain separate | chapter · Blueprint |
Block encoding
| Mathematical goal | Contract | Proof obligation | Lean declaration | Module / line | Dependencies | Status | Missing step | Reader links |
|---|---|---|---|---|---|---|---|---|
| Package an exact block encoding | \(\Pi U\Pi^\dagger=A/\alpha\) | Candidate unitarity and exact block identity supplied to the promotion constructor | QuantumBlockEncoding.VerifiedOperatorBlockEncoding |
QuantumBlockEncoding/BlockEncoding.lean:131 |
OperatorBlockEncodingCandidate.certify; certified finite cases | Compiled | None for the reusable promotion route; concrete candidate fields remain route-specific inputs | chapter · Blueprint |
| Reuse an exact certificate approximately | \(\|A-\alpha\Pi U\Pi^\dagger\|=0\) | Zero-error conversion | QuantumBlockEncoding.VerifiedOperatorBlockEncoding.asZeroErrorApprox |
QuantumBlockEncoding/BlockEncoding.lean:173 |
VerifiedOperatorBlockEncoding | Compiled | Positive-error analyses are route-specific | chapter · Blueprint |
| Certify a partial permutation | \(\operatorname{block}(U)=A\) | Finite routed-entry proof | QuantumBlockEncoding.BlockEncodingClassics.partialPermutationCertificate |
QuantumBlockEncoding/BlockEncodingClassics.lean:662 |
ExactCleanBlock | Compiled | None locally | chapter · Blueprint |
| Compose exact block encodings | \(\operatorname{block}(U_BU_A)=BA\) | Projected product equality | QuantumBlockEncoding.BlockEncodingClassics.productExactCleanBlockCertificate |
QuantumBlockEncoding/BlockEncodingClassics.lean:811 |
ExactCleanBlock; matrix_mul_congr_pointwise | Compiled | Register compatibility for each application | chapter · Blueprint |
| Close BE Case 1 | \(\Pi U_{\mathrm{E1}}\Pi^\dagger=A_{\mathrm{E1}}/\alpha\) | Transfer-operator projection | QuantumBlockEncoding.coldE1Candidate_blockProjection |
QuantumBlockEncoding/ColdStartTransferE1.lean:191 |
coldE1CandidateImage_permutation_certificate | Compiled | None locally | chapter · Blueprint |
| Close BE Case 2 | \(\Pi U_{\mathrm{cubic}}\Pi^\dagger=D/\alpha\) | Exact rational Householder completion | QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_complete |
QuantumBlockEncoding/CubicStatePreparation.lean:2879 |
Householder input; rational backend support | Compiled | None for the selected exact route | chapter · Blueprint |
| Feed a certified clean block to a typed polynomial consumer | \(U_D\leadsto p^{(\mathrm{SV})}(D/\alpha)\) | Source certificate, side conditions, and a finite degree-one identity realization | QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract |
QuantumBlockEncoding/BlockEncodingClassics.lean:857 |
QSVTConsumerContract.identity; teachingIdentityQSVTConsumer | Compiled | None for the typed identity consumer; general phase synthesis and approximation checking remain roadmap items | chapter · Blueprint |
| Compile a finite banded sparse-access witness | \(|s\rangle|i\rangle|0\rangle\mapsto|s\oplus3+i\bmod8\rangle|i\rangle|0\rangle\) | Primitive refinement, clean workspace, unitarity, and zero oracle calls | QuantumBlockEncoding.BandedSparseAccess.primitiveAccess3Program_eval |
QuantumBlockEncoding/BandedSparseAccessPrimitive.lean:77 |
modularAdd3ReversibleProgram; compileReversibleProgram_eval | Compiled | Arbitrary-width source gate upper bounds remain a separate compiler theorem | chapter · Blueprint |
| 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\) | Finite sum/adjoint bridge, Hermitian S1/S2 split, and final Hamiltonian composition | QuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed |
QuantumBlockEncoding/GHLHamiltonian.lean:502 |
adjoint_sumTerms; verified ComplexLCU kernel; eq29PrintedClean_ne_S1; eq29PhaseBalancedClean_eq_S1; eq30Clean_eq_S2 | Compiled | None for the source-audited Theorem-4 composition; arbitrary-width primitive one-term gate/resource compilation is a separate frontier | chapter · Blueprint |
| Close the historical Robin raw-fold branch | \(U_{00}\ne\sum_s B_s\) | Convert the raw fold to the refuted backend expansion | QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3 |
QuantumBlockEncoding/RobinMatrix.lean:26952 |
Equivalence bridge; all-one counterexample | Compiled | None for the rejected branch; cited oracle implementations remain experimental | chapter · Blueprint |
System and evidence
| Mathematical goal | Contract | Proof obligation | Lean declaration | Module / line | Dependencies | Status | Missing step | Reader links |
|---|---|---|---|---|---|---|---|---|
| Compile a finite cubic diagonal amplitude oracle | \(\Pi_0U\Pi_0^\dagger=\operatorname{diag}((j/4)^3)\) | Exact multiplexed RY semantics, clean projection, and verified BE packaging | QuantumBlockEncoding.CubicDiagonalOracle.cubicN2PrimitiveVerifiedBlockEncoding |
QuantumBlockEncoding/CubicAmplitudePrimitive.lean:209 |
UniformlyControlledRy; PrimitiveBasisLE; exact RY bridge | Compiled | Scalable arithmetic and general QSVT phase synthesis are separate routes | chapter · Blueprint |
| Verify three-layer harness promotion | \(\text{upper}\to\text{middle}\to\text{lower}\to\text{reviewer}\to\text{accepted}\) | Logged artifacts, valid role order, Lean gate, and reviewer approval | QuantumBlockEncoding.threeLayerCanonicalTrace_reachesAccepted |
QuantumBlockEncoding/AutomationTrace.lean:117 |
ThreeLayerHandoff.validFlag; ThreeLayerTrace.finalPhase | Compiled | External model execution remains engineering evidence | chapter · Blueprint |
| Audit the open-problem registry | \(|\mathcal O|=7\land\operatorname{Nodup}(\operatorname{id}(\mathcal O))\) | Unique identifiers and nonempty actionable fields | QuantumBlockEncoding.openProblemRegistry_compiled |
QuantumBlockEncoding/OpenProblemsAudit.lean:49 |
openProblemIds_nodup; openProblems_all_actionable | Compiled | The registered mathematical problems intentionally remain open | chapter · Blueprint |