Start with a linear PDE containing derivatives, variable coefficients, a source term, and Robin boundary conditions.
Read the paper map as a quantum-algorithm story
Why does this paper build block encodings at all?
Hamiltonian-simulation papers often begin by saying 'assume an oracle for H' or 'assume a block encoding of H'. Guseynov, Huang, and Liu ask what it actually costs to build that access for finite-difference PDE operators with Robin boundaries and piecewise coefficients. Their goal is explicit gate-level construction rather than leaving matrix access as a black box.
From the PDE to something a quantum circuit can simulate
Replace spatial derivatives by a sparse matrix A on N=2^n grid points. Boundary rows differ from the periodic bulk.
Embed the non-Hermitian evolution into a larger Hermitian Hamiltonian H so it can be simulated by unitary quantum dynamics.
Build an explicit unitary U_H whose clean ancilla block equals H/alpha.
Use the block encoding as the input oracle for a polynomial transformation approximating exp(-iHt).
Apply the evolution to the encoded initial state and postselect the auxiliary registers to recover a state proportional to the PDE solution.
Figure 4 without the notation overload
Selector/register labels
The sparse selector s says which finite-difference band/position is being addressed; the system register j stores the grid index.
PREPARE
Create a coherent superposition over sparse slots instead of classically looping over them.
Indicator
Mark whether j belongs to the periodic-like bulk or the Robin boundary region.
RY coefficient loading
Turn a normalized matrix coefficient into an amplitude on a clean coefficient qubit.
Sparse access / SELECT
Reversibly move from (slot,column) to the matrix row addressed by that slot.
Uncompute
Undo temporary address/indicator information so the selected ancillas return to |0>; only then does the clean projected block have the desired matrix meaning.
GHL Theorem 3 · source theorem, faithfully restated
One-term block encoding for f(x) times a sparse Robin derivative
\[A_k\sim f(x)\,\frac{\partial^m}{\partial x^m},\qquad U_{A_k}^{(1)}\text{ is an }(N_DN_f\kappa,\lceil\log_2n\rceil+\lceil\log_2G_f\rceil+\lceil\log_2\kappa\rceil+4,0)\text{-block encoding}\]
For a piecewise-continuous coefficient f with G_f pieces and polynomial complexity Q_g, and a 2^n by 2^n kappa-sparse finite-difference derivative matrix with Robin boundaries, the paper constructs a one-term block encoding. Its stated gate complexity is O(sum_g Q_g n log n + kappa n) with 2n pure ancillas.
Proof story
- Exploit periodic bulkAway from the boundary, the Robin stencil agrees with the familiar periodic stencil, so one reusable sparse-amplitude construction handles most indices.
- Mark the boundaryAn indicator qubit distinguishes bulk indices from the O(1)-width boundary region.
- Load derivative coefficientsUse the sparse derivative amplitude oracle in the bulk and controlled RY rotations for individual boundary entries.
- Apply sparse accessA reversible banded-sparse-access map transports the selector and grid index to the matrix location required by the derivative stencil.
- Load f(x)Multiply in the piecewise coefficient through its amplitude/block-encoding construction.
- Swap and uncomputeTransport the registers back through the inverse access maps so workspace is clean.
- Read the clean blockPREPARE/unprepare interference leaves A_k/(N_D N_f kappa) in the ancilla-zero block.
Show the Lean proof checkpoints
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
GHL Theorem 4 · source theorem, faithfully restated
Combine the one-term blocks into the full Schrodingerised Hamiltonian
\[A=\sum_{k=0}^{\eta-1}A_k,\quad S_1=\begin{pmatrix}(A+A^\dagger)/2&B/2\\B/2&0\end{pmatrix},\quad S_2=\begin{pmatrix}(A-A^\dagger)/(2i)&B/(2i)\\-B/(2i)&0\end{pmatrix},\quad H=S_1\otimes x_\xi+S_2\otimes I_\xi\]
The paper states that the structured one-dimensional Hamiltonian H has an O(kappa ||H||_max)-normalized block encoding using logarithmic selector/register overhead, with total gate complexity obtained from the coefficient-function loaders, the one-term sparse derivative blocks, and the x_xi diagonal block. The theorem reports 2n+2 pure ancillas.
Proof story
- Build every A_kUse the one-term result for each coefficient-times-derivative term.
- LCU to form ACombine the A_k block encodings into a block encoding of A=sum_k A_k; the adjoint circuit gives A^dagger.
- Build B and x_xiUse the diagonal-function block-encoding theorem for the source/homogenization block B and the Schrodingerisation coordinate x_xi.
- LCU to form S1 and S2Combine controlled A/A^dagger with X tensor B and Y tensor B so the clean blocks become the two Hermitian matrices S1 and S2.
- Final LCUCombine U_S1, U_S2, and the block encoding of x_xi one last time to obtain H.
- Source-fidelity auditASPBE also checks the printed phase choices in the first S1 LCU line: the literal full-clean-matrix reading leaves a filler term, so the site records the discrepancy and the phase-balanced correction instead of silently changing the paper.
Show the Lean proof checkpoints
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint_sumTermsQuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.Adagger_eq_sum_term_adjointsQuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean_eq_S2QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H_eq_S1_tensor_xXi_add_S2_tensor_IQuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed
Do not overread the formalization
Paper theorem → exact Lean scope
The source theorem and the machine-checked theorem do not automatically have the same scope. These cards state exactly which layer is closed and which general compiler statement remains separate.
GHL Theorem 3 · source theorem, faithfully restated · paper scope → Lean scope
One-term block encoding for f(x) times a sparse Robin derivative
Paper scope: an arbitrary-width one-term construction with the stated asymptotic resource bound. Lean scope: the theorem metadata and reusable sparse-access semantics are formalized, and the N=8 Figure-4 specialization is closed through an exact primitive VerifiedOperatorBlockEncoding. A uniform arbitrary-width primitive compiler proving every source-oracle gate bound remains a separate planned frontier; the fixed-N=8 roots below must not be read as that stronger compiler theorem.
Show the Lean alignment roots
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
GHL Theorem 4 · source theorem, faithfully restated · paper scope → Lean scope
Combine the one-term blocks into the full Schrodingerised Hamiltonian
Paper scope: the one-dimensional A-to-H Hamiltonian composition. Lean scope: the finite-sum adjoint bridge, S1/S2 clean-block algebra, final H formula, normalization/layout records, and the source phase audit are compiled. The printed first S1 phase pair is proved inconsistent under the literal full-clean-matrix reading, and a phase-balanced correction is separately proved before the aggregate Theorem-4 route is marked closed.
Show the Lean alignment roots
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint_sumTermsQuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.Adagger_eq_sum_term_adjointsQuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean_eq_S2QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H_eq_S1_tensor_xXi_add_S2_tensor_IQuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed
Paper assumption → plain language → Lean evidence
Source conventions translated before the audit log
These are the conventions that change the mathematical or resource contract. Read the explanation first; the raw transcription and implementation audit remains collapsed later on the page.
A query oracle is an access contract, not a free physical gate
Paper assumption / source issue. The paper contrasts an abstract digital matrix-entry query O_H with explicit sparse-access and amplitude/block-encoding circuits.
Plain language. When an algorithm says it makes one query, it means one call to a promised reversible data-access subroutine. The arithmetic, memory lookup, boundary tests, and ancillas hidden inside that call may still be expensive to build.
Why it matters. GHL's construction is useful precisely because it opens this black box for the structured Robin operator; ASPBE therefore reports oracle calls separately from primitive gates.
Show the Lean evidence
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
Figure 4 applies its bulk indicator to D-transpose
Paper assumption / source issue. The source circuit's indicator is interpreted on a row of D-transpose, so the fixed N=8 realization selects the corresponding columns of D rather than a naively read row window.
Plain language. The circuit is moving between row and column viewpoints. Reading the indicator against the wrong orientation changes which boundary entries receive special treatment.
Why it matters. This choice changes the executable circuit, so ASPBE proves the transported bulk action before accepting the Figure-4 clean block.
Show the Lean evidence
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
Standard RY uses a half angle
Paper assumption / source issue. Equation (27) prints a single arccos coefficient angle; under the standard RY(theta) convention the executable angle must be 2 arccos(c).
Plain language. An RY rotation places cos(theta/2), not cos(theta), in the clean amplitude. To load coefficient c exactly, theta must therefore equal 2 arccos(c).
Why it matters. Using the printed single-arccos expression would certify the wrong amplitude. ASPBE retains the typo transcript but proves the corrected standard-RY circuit.
Show the Lean evidence
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
Seven source slots are an LCU decomposition, not a sparse-enumeration oracle
Paper assumption / source issue. The historical split-seven weighted-permutation representation can send distinct nonzero slots to the same matrix entry.
Plain language. Two selector labels may contribute amplitudes to the same matrix location. That is legal for a linear-combination-of-unitaries construction, but it is not the promise made by a one-nonzero-per-slot sparse enumerator.
Why it matters. Treating the seven labels as a sparse oracle would silently strengthen the access promise. ASPBE instead proves the weighted-permutation sum and records the duplicate access explicitly.
Show the Lean evidence
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
Only the clean projected block is the encoded operator
Paper assumption / source issue. Temporary selector, indicator, coefficient, and address workspaces are uncomputed before the clean block is read.
Plain language. A block encoding does not claim that the full unitary equals the PDE matrix. It claims that when designated ancillas start and end at zero, the selected submatrix equals the normalized target.
Why it matters. Full-space behavior on dirty workspace states may be compiler-dependent; the theorem must therefore prove the declared zero-workspace projection, not an informal whole-unitary equality.
Show the Lean evidence
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
The Theorem-4 phase discrepancy is recorded, not silently repaired
Paper assumption / source issue. With Eq. (29)'s filler convention, the printed first-line phases pi and -pi in Eq. (30) both contribute -1 and leave a nonzero lower-right filler block.
Plain language. The two printed phases do not cancel: exp(i*pi)=exp(-i*pi)=-1. A literal matrix sum therefore cannot equal the displayed S1 block unless the filler is corrected.
Why it matters. Source fidelity requires distinguishing what the paper prints from the corrected executable identity. Lean proves the obstruction and then proves a phase-balanced S1 construction; S2 closes as printed.
Show the Lean evidence
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
The 106-vs-312-vs-881 claim lives on one frozen compiler tier
Paper assumption / source issue. For the N=8 comparison, all candidates use exact {X, RY, RZ, CX} primitive programs, all-to-all connectivity, the same target/normalizer, and zero abstract oracle calls.
Plain language. Resource numbers are comparable only after the target, gate vocabulary, connectivity, ancilla convention, and oracle accounting have been frozen. Otherwise a smaller number may simply be using a different cost model.
Why it matters. ASPBE's winner is a strict same-tier theorem, not a universal circuit lower bound. The evolved circuit is better in gate count, depth, and auxiliary-qubit coordinates while oracle calls stay equal.
Show the Lean evidence
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
What ASPBE improves
Evolved theorem: a strictly cheaper exact block encoding for the frozen Robin benchmark
\[c_{\mathrm{XOR}}=(106,96,3,0)\prec_{\mathrm{lex}}c_{\mathrm{paper7}}=(312,266,5,0),\qquad c_{\mathrm{XOR}}\prec_{\mathrm{lex}}c_{\mathrm{Fig.4}}=(881,674,6,0)\]
All three circuits encode the same dimensionless N=8 target with alpha=56/3, zero error, the same exact primitive basis {X,RY,RZ,CX}, the same all-to-all connectivity convention, and clean workspaces. Lean certifies the XOR four-slot circuit and proves both strict comparisons. This is a benchmark/compiler theorem, not a global lower bound over all possible quantum circuits.
Why the proof is allowed to say “better”
- Use centrosymmetryPair matrix indices related by reversal so the 8 by 8 target decomposes into two smaller symmetry sectors.
- Use four XOR slotsWithin each sector, index the required positions by two selector bits using XOR rather than a carry-producing modular adder.
- Load exact amplitudesA uniformly controlled RY compiler realizes the 32 exact coefficient branches with structured exact-angle semantics.
- Simplify SELECTThe XOR addressing rule reduces SELECT to two CX gates on the pair-coordinate bits.
- Refine to primitivesLean proves the product of the emitted X/RY/RZ/CX gates equals the previously verified logical unitary, not merely a floating-point approximation.
- Inherit the clean-block theoremExact primitive equality transports the already-proved logical clean block to the primitive circuit.
- Compute and compare costResource tuples are derived from the primitive programs and the betterThan theorems establish strict same-tier dominance.
Show the Lean winner/comparison theorems
The mathematical explanation above is the reading layer. These compiled declarations are the proof authority.
QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitive_eval_eq_flatUnitaryQuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveBlockContainsTarget_proofQuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveVerifiedBlockEncodingQuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_paperSevenQuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_figure4QuantumBlockEncoding.Robin.warmRobinBestVerified
Paper reproduction · source-to-Lean reading map
Robin boundary block encoding
The source paper proposes a general circuit family for differential operators with Robin boundaries. ASPBE separates that general route from a fixed (N=8) benchmark, where three exact primitive block encodings and their same-tier resource comparison now compile.
The concrete case
What matrix is being encoded?
The benchmark fixes the fourth-order-accurate second-derivative stencil. Keeping (M=12A) integral makes every decomposition identity exact in Lean.
\[A=\frac1{12}\begin{pmatrix}-30&32&-2&0&0&0&0&0\\16&-31&16&-1&0&0&0&0\\-1&16&-30&16&-1&0&0&0\\0&-1&16&-30&16&-1&0&0\\0&0&-1&16&-30&16&-1&0\\0&0&0&-1&16&-30&16&-1\\0&0&0&0&-1&16&-31&16\\0&0&0&0&0&-2&32&-30\end{pmatrix},\qquad \Pi U\Pi^\dagger=\frac{A}{56/3}=\frac{M}{224}.\]
The clean projector fixes selector and coefficient registers to zero. The remaining three-qubit register indexes the rows and columns of (A).
Show verification-tier/status discipline
This is the formal publication policy separating a compiled declaration from a fully closed route.
Status discipline
A compiled declaration is not automatically the paper theorem
The left badge says that the named Lean object compiles in this checkout. The right badge says whether the entire paper route is closed. Contract records, transcript equalities, finite diagnostics, and counterexamples are valuable formal results, but they do not replace the final projected-block theorem.
Current conclusion.
The arbitrary-size paper theorem remains partial. The fixed (N=8),
homogeneous
f=1 benchmark is closed separately: Lean certifies
paper-seven, the standard-RY-corrected Figure-4 realization, and the XOR
four-slot candidate in the exact {X, RY, RZ, CX} basis. It
proves the candidate strictly better than both source realizations under
the frozen compiler and lexicographic score. This is not a global
optimality theorem.
| Verification layer | Status in this build | Required root |
|---|---|---|
| Candidate exact primitive certificate | Compiled | QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveVerifiedBlockEncoding |
| True source sparse-slot decomposition | Compiled | QuantumBlockEncoding.Robin.warmRobinSourceSevenSparseDecomposition |
| Paper-seven exact primitive normal form | Compiled | QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveVerifiedBlockEncoding |
| Figure-4 fixed-N8 exact primitive realization | Compiled | QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveVerifiedBlockEncoding |
| Candidate better than paper-seven | Compiled | QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_paperSeven |
| Candidate better than Figure 4 | Compiled | QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_figure4 |
| Frozen benchmark winner | Compiled | QuantumBlockEncoding.Robin.warmRobinBestVerified |
| Fixed publication state is consistent | Compiled | QuantumBlockEncoding.Robin.warmRobinPublicationState_consistent |
Advanced source-fidelity notes (implementation details)
You do not need these notes to understand the theorem. They record conventions, transcription discrepancies, and full-space implementation choices for readers reproducing the source circuit.
Source audit
Advanced source-fidelity notes
The fixed circuit is explicit about choices that cannot safely remain hidden in a transcription.
- The historical split-seven weighted-permutation LCU is not used as a sparse enumeration because distinct nonzero slots can address the same matrix entry.
- The Figure-4 indicator is applied to a row of D-transpose, so the fixed source circuit selects columns 3 and 4 of D rather than the row window 2 through 5.
- Equation (27) omits a factor of two. The certified circuit uses theta = 2 arccos(c), as required by the standard RY(theta) half-angle convention; the printed single-arccos expression remains visible only as a source-typo transcript.
- The unexplained literal gamma-1 normalization is not assumed. The fixed realization proves its actual executable stage states and final projected block.
- The full-space unitary uses the compiler's actual reversible behavior on dirty workspace states, while the block contract projects every declared workspace to zero.
- The fixed benchmark has f=1, and Lean proves that coefficient stage is identity before it is constant-folded.
- The paper's numerical experiment leaves multi-controlled rotations undecomposed. ASPBE's 881, 312, and 106 counts are exact primitive {X, RY, RZ, CX} lists and are compared only within that frozen compiler tier.
- Theorem 4 is part of the source paper: the one-term A_k and A_k-dagger ingredients are combined into A and A-dagger, then S1 and S2, and finally H = S1 tensor x_xi + S2 tensor I_xi. GHLHamiltonian.lean now formalizes that composition; only uniform primitive compilation of the general-width source oracles remains separate.
- Source audit for Eq. (30): with Eq. (29)'s L1(phi), L2(phi) definitions, the printed first-line phases pi and -pi both contribute exp(i phi)=-1 on the filler block. A literal full-clean-matrix sum therefore leaves -N_A I rather than the displayed zero lower-right block. Lean proves this obstruction and separately proves a phase-balanced correction; the S2 line closes as printed.
Fixed N=8 evolution
Three comparable primitive circuits
Every tuple is ordered as gates, depth, auxiliary qubits, and oracle calls.
\[A/(56/3)=M/224\]
Source Figure 4 · (881,674,6,0)
Fixed-N8 circuit
Indicator, bulk and boundary loaders, two distinct sparse transports, register swap, and clean uncomputation follow the corrected source order.
Source normal form · (312,266,5,0)
Paper seven
A true padded-seven sparse table compiles directly through PREPARE, amplitude loading, modular SELECT, and unprepare.
Certified winner · (106,96,3,0)
XOR four slot
Robin centrosymmetry reduces the selector and turns SELECT into two CX gates. Lean proves both strict same-tier comparisons.
Open the theorem-linked evolution visualization
Executable replicas. Canonical IR,
gate-by-gate Qiskit, and strict OpenQASM 3 files are generated separately for
all three circuits. Their numerical checks are debugging evidence; the Lean
refinement and projected-block declarations above are the proof authority.
Open the detailed paper-to-Lean correspondence map
Each expanded row compares a source-paper anchor with the exact declaration and source location.
Guseynov-Huang-Liu 2025
Paper statement to Lean structure
Expand a row to compare the source LaTeX, the exact Lean statement, and its location in the Library Explorer and Blueprint.
Lemma 2, citing Lemma 1 of arXiv:2405.12855
Write the banded sparse column address into an n-qubit register while preserving the row register.
Local declarationsCompiled
Paper-wide routePartial route
\[\hat{O}^{BS}_D\ket{0}^{n-l}\ket{s}^l\ket{i}^n := \ket{r_{si}}^n\ket{i}^n,\qquad r_{si}=r_{s0}+i\bmod 2^n.\]
What Lean currently establishes
Robin Lemma 2 imports the banded-sparse primitive from Lemma 1 of arXiv:2405.12855. ASPBE now proves the arbitrary-size semantic construction: a supplied reversible first-row loader followed by modular SUM preserves the row, produces r_(s,0)+i modulo 2^n, and induces a unitary permutation matrix. The paper's general one-qubit/CNOT upper bounds remain source-facing until a general gate compiler realizes the loader and adder at those counts.
Corresponding declarations
QuantumBlockEncoding.GHL2025.BandedSparseAccessPaperContractQuantumBlockEncoding.BandedSparseAccess.accessEquiv_clean_slotQuantumBlockEncoding.BandedSparseAccess.accessMatrix_unitaryQuantumBlockEncoding.GHL2025.robinBandedSparseAccessCitationChain_eqQuantumBlockEncoding.GHL2025.bandedSparseAccessPaperAddress_lt_gridSize_of_two_leQuantumBlockEncoding.GHL2025.bandedSparseAccessPaperMatrix_eq_image
Show the paper-side LaTeX
\hat{O}^{BS}_D\ket{0}^{n-l}\ket{s}^l\ket{i}^n := \ket{r_{si}}^n\ket{i}^n,\qquad r_{si}=r_{s0}+i\bmod 2^n.QuantumBlockEncoding.GHL2025.BandedSparseAccessPaperContract
structure BandedSparseAccessPaperContract where
sourceAnchor : String
rowRegisterQubits : Nat
paddedZeroQubits : Nat
sparseIndexQubits : Nat
outputAddressQubits : Nat
inputKet : String
outputKet : String
imageFormula : String
cleanInputDomain : ObligationRecord
widthCompatible : ObligationRecordQuantumBlockEncoding.BandedSparseAccess.accessEquiv_clean_slot
theorem accessEquiv_clean_slot
(n : Nat) {l : Nat}
(offset : Fin (2 ^ l) → Word n)
(loader : Equiv.Perm (Word n))
(loader_spec : ∀ slot, loader (slotWord n slot) = offset slot)
(slot : Fin (2 ^ l)) (row : Word n) :
accessEquiv n loader (slotWord n slot, row) =
(offset slot + row, row) := byQuantumBlockEncoding.BandedSparseAccess.accessMatrix_unitary
theorem accessMatrix_unitary (n : Nat) (loader : Equiv.Perm (Word n)) :
accessMatrix n loader ∈
_root_.Matrix.unitaryGroup (Word n × Word n) ℂ :=
Robin.ComplexLCU.equivPermutationMatrix_unitary _
/-- Source-facing single-qubit upper bound printed in Lemma 1 of
arXiv:2405.12855v3. Natural subtraction is appropriate only in the paper's
stated nontrivial register regime. -/QuantumBlockEncoding.GHL2025.robinBandedSparseAccessCitationChain_eq
@[simp] theorem robinBandedSparseAccessCitationChain_eq :
robinBandedSparseAccessCitationChain = [
"Guseynov-Huang-Liu 2025, arXiv:2506.20478, Lemma 2",
"Guseynov-Huang-Liu 2024, arXiv:2405.12855v3, Lemma 1"
] := rfl
/--
The prior PDE source does not unblock the QBE unused-zero-branch extension.
This is the compiled guard for the source audit: the cited theorem is recorded,
but lower proof search for Robin unused-branch injectivity, cleanup, andQuantumBlockEncoding.GHL2025.bandedSparseAccessPaperAddress_lt_gridSize_of_two_le
theorem bandedSparseAccessPaperAddress_lt_gridSize_of_two_le
(p : OneTermRobinParameters) (j : Nat) (_hn : 2 ≤ p.n) :
bandedSparseAccessPaperAddress p j < gridSize p.n := byQuantumBlockEncoding.GHL2025.bandedSparseAccessPaperMatrix_eq_image
theorem bandedSparseAccessPaperMatrix_eq_image (p : OneTermRobinParameters)
(i j : Fin (qubitDim (oneTermRobinTotalQubits p))) :
bandedSparseAccessPaperMatrix p i j =
if i.val = bandedSparseAccessPaperImage p j.val then Coeff.rat 1 else Coeff.rat 0 := byBulk indicator U_indic
Flip one indicator qubit exactly on rows in the bulk window K1 through K2.
Local declarationsCompiled
Paper-wide routePartial route
\[U_{\mathrm{indic}}(K_1,K_2)|i\rangle|0\rangle=|i\rangle|\mathbf{1}_{K_1\le i\le K_2}\rangle.\]
What Lean currently establishes
Lean proves the finite image is self-inverse, hence bijective, and that the corresponding matrix is a permutation matrix. This closes the local unitary, not the whole Robin block encoding.
Corresponding declarations
QuantumBlockEncoding.GHL2025.indicatorOracleImage_self_inverseQuantumBlockEncoding.GHL2025.indicatorOracleMatrix_is_permutationQuantumBlockEncoding.RobinEvolution.warmRobinIndicatorCertificate
Show the paper-side LaTeX
U_{\mathrm{indic}}(K_1,K_2)|i\rangle|0\rangle=|i\rangle|\mathbf{1}_{K_1\le i\le K_2}\rangle.QuantumBlockEncoding.GHL2025.indicatorOracleImage_self_inverse
theorem indicatorOracleImage_self_inverse (p : OneTermRobinParameters) (j : Nat) :
indicatorOracleImage p (indicatorOracleImage p j) = j := byQuantumBlockEncoding.GHL2025.indicatorOracleMatrix_is_permutation
theorem indicatorOracleMatrix_is_permutation (p : OneTermRobinParameters) :
(∀ (i : Fin (qubitDim (oneTermRobinTotalQubits p))),
∃ (j : Fin (qubitDim (oneTermRobinTotalQubits p))),
indicatorOracleMatrix p i j = Coeff.rat 1 ∧
∀ (j' : Fin (qubitDim (oneTermRobinTotalQubits p))),
indicatorOracleMatrix p i j' = Coeff.rat 1 → j' = j) ∧
(∀ (j : Fin (qubitDim (oneTermRobinTotalQubits p))),
∃ (i : Fin (qubitDim (oneTermRobinTotalQubits p))),
indicatorOracleMatrix p i j = Coeff.rat 1 ∧
∀ (i' : Fin (qubitDim (oneTermRobinTotalQubits p))),
indicatorOracleMatrix p i' j = Coeff.rat 1 → i' = i) := byQuantumBlockEncoding.RobinEvolution.warmRobinIndicatorCertificate
theorem warmRobinIndicatorCertificate :
(GHL2025.oneTermRobinGate_U_indic_dagger warmRobinParameters).matrix =
(GHL2025.oneTermRobinGate_U_indic warmRobinParameters).matrix ∧
(∀ j : Nat,
GHL2025.indicatorOracleImage warmRobinParameters
(GHL2025.indicatorOracleImage warmRobinParameters j) = j) ∧
(∀ i : Fin (qubitDim
(GHL2025.oneTermRobinTotalQubits warmRobinParameters)),
∃ j : Fin (qubitDim
(GHL2025.oneTermRobinTotalQubits warmRobinParameters)),
GHL2025.indicatorOracleMatrix warmRobinParameters i j = Coeff.rat 1 ∧Boundary controlled Ry angles
Encode each exceptional Robin-boundary coefficient with a controlled y rotation.
Local declarationsCompiled
Paper-wide routeCompiled
\[\theta_j^s=2\arccos\!\left(D_j^{(s)}/\mathcal N_D\right).\]
What Lean currently establishes
The paper's displayed single-arccos formula is recorded as a typo. With standard RY(theta), Lean proves that the corrected doubled angle produces the requested clean coefficient, and the fixed-N8 Figure-4 route uses that certificate.
Corresponding declarations
QuantumBlockEncoding.GHL2025.RobinBoundaryRotationAngleQuantumBlockEncoding.Robin.warmRobinCorrectedEq27_standardRy_cleanAmplitudeQuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryRyAngleConventionDecision_n3_transcriptQuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryCorrectedCoefficientInterface_n3_transcript
Show the paper-side LaTeX
\theta_j^s=2\arccos\!\left(D_j^{(s)}/\mathcal N_D\right).QuantumBlockEncoding.GHL2025.RobinBoundaryRotationAngle
structure RobinBoundaryRotationAngle where
/-- Row index j (boundary row: j < K1 or j > K2). main.tex:1082 --/
row : Nat
/-- Sparse index s in {0,...,kappa-1}. main.tex:1082 --/
sparseIndex : Nat
/-- The matrix entry D_j^(s) being encoded. main.tex:1082 --/
matrixEntry : Coeff
/-- The argument to arccos: D_j^(s) / N_D (symbolic Coeff).
The caller must ensure this evaluates to a value in [-1, 1].
main.tex:1081-1083 --/
arccosArgument : CoeffQuantumBlockEncoding.Robin.warmRobinCorrectedEq27_standardRy_cleanAmplitude
theorem warmRobinCorrectedEq27_standardRy_cleanAmplitude
(coefficient : Rat)
(lower : (-1 : Real) ≤ (coefficient : Real))
(upper : (coefficient : Real) ≤ 1) :
standardRyMatrix (warmRobinCorrectedEq27BoundaryAngle coefficient) =
ComplexLCU.amplitudeRotation (coefficient : Real) := byQuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryRyAngleConventionDecision_n3_transcript
theorem oneTermRobinGamma3BoundaryRyAngleConventionDecision_n3_transcript :
let p := oneTermParameters 3
let decision := oneTermRobinGamma3BoundaryRyAngleConventionDecision_n3
decision.sourceAnchor =
"GHL2025 Eq. angles for Ry, Eq. ROBIN clarified, Fig. 1-term ROBIN, arXiv:2506.20478" ∧
decision.bridge = oneTermRobinGamma3BoundaryRyCoefficientBridge_n3 ∧
decision.bridge.cosHalfEntry = Coeff.symbol "boundary_cos_half_0_2" ∧
decision.bridge.normalizedCoefficient =
GHL2025.boundaryRotationNormalizedCoefficient p 0 2 ∧
decision.bridge.normalizedCoefficient =
Coeff.mul (GHL2025.robinGlobalSparseAmplitudeValue 3 2 0)QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryCorrectedCoefficientInterface_n3_transcript
theorem oneTermRobinGamma3BoundaryCorrectedCoefficientInterface_n3_transcript :
let interface := oneTermRobinGamma3BoundaryCorrectedCoefficientInterface_n3
interface.decision =
oneTermRobinGamma3BoundaryRyCorrectedAngleSourceDecision_n3 ∧
interface.productEntryFactor = Coeff.symbol "boundary_cos_half_0_2" ∧
interface.normalizedCoefficient =
GHL2025.boundaryRotationNormalizedCoefficient (oneTermParameters 3) 0 2 ∧
interface.normalizedCoefficient =
Coeff.mul (GHL2025.robinGlobalSparseAmplitudeValue 3 2 0)
(Coeff.symbol "N_D_inv") ∧
interface.correctedEntryHypothesis.proved = false ∧One-term block-encoding theorem
The theorem fixes the target operator, normalizer, signal width, zero error, gate scaling, and pure-ancilla count.
Local declarationsCompiled
Paper-wide routePartial route
\[(\mathcal N_D\mathcal N_f\kappa,\;\lceil\log_2n\rceil+\lceil\log_2G_f\rceil+\lceil\log_2\kappa\rceil+4,\;0)\text{-block encoding of }A_k.\]
What Lean currently establishes
The theorem statement and resource/layout equalities compile as typed data. The final projected-block equality is still conditional on the named sparse-access, amplitude-oracle, boundary-rotation, cleanup, and composition contracts.
Corresponding declarations
QuantumBlockEncoding.GHL2025.defaultOneTermRobinTheoremDataQuantumBlockEncoding.GHL2025.defaultOneTermRobinTheoremData_signalQubits_eq_layoutQuantumBlockEncoding.GHL2025.defaultOneTermRobinTheoremData_pureAncillas_eq_resourceQuantumBlockEncoding.RobinEvolution.warmRobinTarget_eq_eval_robinDerivativeMatrix
Show the paper-side LaTeX
(\mathcal N_D\mathcal N_f\kappa,\;\lceil\log_2n\rceil+\lceil\log_2G_f\rceil+\lceil\log_2\kappa\rceil+4,\;0)\text{-block encoding of }A_k.QuantumBlockEncoding.GHL2025.defaultOneTermRobinTheoremData
def defaultOneTermRobinTheoremData (p : OneTermRobinParameters) : OneTermRobinTheoremData where
alpha := oneTermRobinNormalizer
signalQubits := clog2 p.n + clog2 p.functionPieces + clog2 p.kappa + 4
error := Coeff.rat 0
gatesBound := "O(sum_g Q_g n log n + kappa n)"
pureAncillas := 2 * p.n
obligations := {}
/--
A controlled R_y rotation angle for a single boundary row entry.
The paper (Eq. angles for Ry, main.tex:1081-1083) defines:QuantumBlockEncoding.GHL2025.defaultOneTermRobinTheoremData_signalQubits_eq_layout
theorem defaultOneTermRobinTheoremData_signalQubits_eq_layout
(p : OneTermRobinParameters) :
(defaultOneTermRobinTheoremData p).signalQubits =
(oneTermRobinLayout p).signalQubits := rfl
/--
The theorem tuple and the reusable layout record carry the same `2n`
pure-ancilla resource count.
-/QuantumBlockEncoding.GHL2025.defaultOneTermRobinTheoremData_pureAncillas_eq_resource
theorem defaultOneTermRobinTheoremData_pureAncillas_eq_resource
(p : OneTermRobinParameters) :
(defaultOneTermRobinTheoremData p).pureAncillas =
(oneTermRobinResource p).pureAncilla := rfl
/--
The concrete block projection has to project all non-system wires.
Compared with the theorem-level signal parameter, the circuit-level projection
also includes the visible padded `O_D^BS` pure-register qubits and the trailing
one-qubit ancilla in the register partition. This is an arithmetic bridgeQuantumBlockEncoding.RobinEvolution.warmRobinTarget_eq_eval_robinDerivativeMatrix
theorem warmRobinTarget_eq_eval_robinDerivativeMatrix :
warmRobinTarget = fun i j =>
Coeff.evalWith (fun _ => 0)
(Examples.RobinHeat.robinDerivativeMatrix 3 i j) := byEquation ROBIN clarified, gamma_3
After derivative, coefficient, swap, and cleanup operations, the clean branch should contain f(x_i) D_i^(s) divided by the three normalizers.
Local declarationsCompiled
Paper-wide routePartial route
\[\gamma_3\supset(\mathcal N_D\mathcal N_f\kappa)^{-1}\sum_{s,j}f(x_i)D_i^{(s)}\sigma^{(s)}|0\cdots0,s,j,0\rangle.\]
What Lean currently establishes
Lean records the gamma transcript and several finite projection bridges. It also proves that a historical H-free raw-entry equality is false, so that route is retired rather than promoted as the paper theorem.
Corresponding declarations
QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinBlockEncodingProofRoute_robinClarifiedGammaTranscriptQuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundarySourcePreparedProjection_to_backendFold_n3QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3
Show the paper-side LaTeX
\gamma_3\supset(\mathcal N_D\mathcal N_f\kappa)^{-1}\sum_{s,j}f(x_i)D_i^{(s)}\sigma^{(s)}|0\cdots0,s,j,0\rangle.QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinBlockEncodingProofRoute_robinClarifiedGammaTranscript
theorem oneTermRobinBlockEncodingProofRoute_robinClarifiedGammaTranscript
(n : Nat)
(source : Fin
(qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n))))
(hn : 3 <= n)
(hsource : GHL2025.bandedSparseAccessPaperGlobalSlotSource
(oneTermParameters n) source.val = true) :
let gamma := GHL2025.defaultRobinWavefunctionDecomposition
(oneTermParameters n)
∃ (post pre : Fin
(qubitDim (GHL2025.oneTermRobinTotalQubits (oneTermParameters n)))),QuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundarySourcePreparedProjection_to_backendFold_n3
theorem oneTermRobinGamma3BoundarySourcePreparedProjection_to_backendFold_n3
(H : Matrix 8 8 Coeff) (env : String → Rat)
(hUniform :
oneTermRobinGamma3BoundaryHWKappaUniformColumnAllSlotsStatement_n3 H) :
Coeff.evalWith env
(oneTermRobinGamma3BoundarySourcePreparedProjectionTarget_n3
H env).preparedProjectionEntry =
Coeff.evalWith env
(oneTermRobinGamma3BoundarySourcePreparedProjectionTarget_n3
H env).backendBranchFold := byQuantumBlockEncoding.Examples.RobinHeat.oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3
theorem oneTermRobinGamma3BoundaryUnitaryEntry_ne_backendFold_n3 :
oneTermRobinGamma3BoundaryProjectionSummationTarget_n3.signalUnitaryEntry ≠
blockExtractionBranchContributionSum
oneTermRobinGamma3BoundaryBackendBranchContribution_n3 := byFigure 1-term ROBIN
The theorem-facing circuit keeps sparse preparation, the indicator and its inverse, derivative amplitudes, boundary rotations, sparse access, coefficient loading, swap, and cleanup in source order.
Local declarationsCompiled
Paper-wide routePartial route
\[H_W\to U_{\mathrm{indic}}\to(O^S_{D^T},R_y)\to O^{BS}_{D^T}\to U_{\mathrm{indic}}^\dagger\to O_f\to\mathrm{SWAP}\to(O_D^{BS})^\dagger\to H_W^\dagger.\]
What Lean currently establishes
The labeled circuit transcript and the active seven-gate backend order compile. Compiling an ordered list does not establish that every labeled oracle has the paper semantics or that their product satisfies the final block contract.
Corresponding declarations
QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit_gateListQuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout_specQuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit_gateList
Show the paper-side LaTeX
H_W\to U_{\mathrm{indic}}\to(O^S_{D^T},R_y)\to O^{BS}_{D^T}\to U_{\mathrm{indic}}^\dagger\to O_f\to\mathrm{SWAP}\to(O_D^{BS})^\dagger\to H_W^\dagger.QuantumBlockEncoding.RobinEvolution.warmRobinSourceCircuit_gateList
theorem warmRobinSourceCircuit_gateList :
warmRobinSourceCircuit =
[ Gate.oracleCall "H_W^(kappa)"
, Gate.oracleCall "U_indic"
, Gate.oracleCall "O_DT^S"
, Gate.oracleCall "Ry_boundary"
, Gate.oracleCall "O_DT^BS"
, Gate.oracleCall "U_indic^dagger"
, Gate.oracleCall "O_f"
, Gate.oracleCall "SWAP(two n-qubit registers; paper label only)"
, Gate.oracleCall "(O_D^BS)^dagger"QuantumBlockEncoding.RobinEvolution.warmRobinSourceLayout_spec
theorem warmRobinSourceLayout_spec :
warmRobinSourceLayout.systemQubits = 3 ∧
warmRobinSourceLayout.signalQubits = 9 ∧
warmRobinSourceLayout.pureAncillas = 6 := byQuantumBlockEncoding.Robin.warmRobinRegisterSwapCircuit_gateList
theorem warmRobinRegisterSwapCircuit_gateList :
warmRobinRegisterSwapCircuit =
[Gate.swap 0 3, Gate.swap 1 4, Gate.swap 2 5] := byASPBE fixed-N follow-up
Freeze the normalized N=8 matrix, then check independent five-shift and Hadamard-8 weighted-permutation decompositions entry by entry.
Local declarationsCompiled
Paper-wide routeCompiled
\[A/(56/3)=M/224,\qquad M_{ij}=\sum_s\mathbf{1}[\pi_s(j)=i]w_s(j).\]
What Lean currently establishes
For the fixed N=8, homogeneous f=1 benchmark, Lean now closes the true padded-seven sparse source, the paper-seven exact primitive normal form, the standard-RY-corrected Figure-4 realization, and the evolved XOR four-slot circuit. Two same-tier betterThan theorems certify the XOR route under the declared compiler. This remains distinct from the paper's arbitrary-n theorem.
Corresponding declarations
QuantumBlockEncoding.Robin.warmRobin_normalized_eq_integer_div_224QuantumBlockEncoding.Robin.warmRobinFiveShiftDecompositionQuantumBlockEncoding.Robin.warmRobinFiveShiftCleanFormula_eq_targetQuantumBlockEncoding.Robin.warmRobinEightSlotDecompositionQuantumBlockEncoding.Robin.warmRobinHadamard8CleanFormula_eq_targetQuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary_unitaryQuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare_cleanEntryQuantumBlockEncoding.Robin.warmRobinSixSlotCap_sum_eq_maxColumnL1QuantumBlockEncoding.Robin.warmRobinSymmetryPlusFourShiftDecompositionQuantumBlockEncoding.Robin.warmRobinSymmetryMinusFourShiftDecompositionQuantumBlockEncoding.Robin.warmRobinHadamard8VerifiedBlockEncodingQuantumBlockEncoding.Robin.warmRobinFourSlotVerifiedBlockEncodingQuantumBlockEncoding.Robin.warmRobinFourSlotT2Cost_betterThan_hadamard8QuantumBlockEncoding.Robin.warmRobinSplitSeven_duplicate_nonzero_accessQuantumBlockEncoding.Robin.warmRobinSourceSevenSparseDecompositionQuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk_matches_periodicQuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_eval_eq_logicalQuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_cleanBlockQuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveVerifiedBlockEncodingQuantumBlockEncoding.Robin.warmRobinFigure4TransportedPostSwapCleanupQuantumBlockEncoding.Robin.warmRobinFigure4Primitive_eval_eq_logicalQuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCircuit_cleanBlockQuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveVerifiedBlockEncodingQuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitive_eval_eq_flatUnitaryQuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveVerifiedBlockEncodingQuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_paperSevenQuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_figure4QuantumBlockEncoding.Robin.warmRobinBestVerifiedQuantumBlockEncoding.Robin.warmRobinPublicationState_consistent
Show the paper-side LaTeX
A/(56/3)=M/224,\qquad M_{ij}=\sum_s\mathbf{1}[\pi_s(j)=i]w_s(j).QuantumBlockEncoding.Robin.warmRobin_normalized_eq_integer_div_224
theorem warmRobin_normalized_eq_integer_div_224 :
(fun i j => warmRobinTarget i j / warmRobinNormalizer) =
fun i j => warmRobinIntegerTargetRat i j / 224 := byQuantumBlockEncoding.Robin.warmRobinFiveShiftDecomposition
theorem warmRobinFiveShiftDecomposition (row column : Fin 8) :
warmRobinIntegerTarget row column =
∑ slot : Fin 5,
if warmRobinFiveShiftPerm slot column = row then
warmRobinFiveShiftWeight slot column
else 0 := byQuantumBlockEncoding.Robin.warmRobinFiveShiftCleanFormula_eq_target
theorem warmRobinFiveShiftCleanFormula_eq_target (row column : Fin 8) :
warmRobinFiveShiftCleanFormula row column =
RobinEvolution.warmRobinTarget row column /
RobinEvolution.warmRobinNormalizer := byQuantumBlockEncoding.Robin.warmRobinEightSlotDecomposition
theorem warmRobinEightSlotDecomposition (row column : Fin 8) :
warmRobinIntegerTarget row column =
∑ slot : Fin 8,
if warmRobinEightSlotPerm slot column = row then
warmRobinEightSlotWeight slot column
else 0 := byQuantumBlockEncoding.Robin.warmRobinHadamard8CleanFormula_eq_target
theorem warmRobinHadamard8CleanFormula_eq_target (row column : Fin 8) :
warmRobinHadamard8CleanFormula row column =
RobinEvolution.warmRobinTarget row column /
RobinEvolution.warmRobinNormalizer := byQuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary_unitary
theorem warmRobinHadamard8LogicalUnitary_unitary :
warmRobinHadamard8LogicalUnitary ∈
_root_.Matrix.unitaryGroup
(LCUIndex (Fin 2) (Fin 8) (Fin 8)) ℂ := byQuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare_cleanEntry
theorem prepareAmplitudeSelectUnprepare_cleanEntry
{coefficient selector system : Type*}
[Fintype coefficient] [DecidableEq coefficient]
[Fintype selector] [DecidableEq selector]
[Fintype system] [DecidableEq system]
(prepare : _root_.Matrix selector selector ℂ)
(rotation : selector → system →
_root_.Matrix coefficient coefficient ℂ)
(permutation : selector → system ≃ system)
(cleanCoefficient : coefficient) (cleanSelector : selector)
(systemRow systemColumn : system) :QuantumBlockEncoding.Robin.warmRobinSixSlotCap_sum_eq_maxColumnL1
theorem warmRobinSixSlotCap_sum_eq_maxColumnL1 :
(∑ slot : Fin 6, warmRobinSixSlotCap slot) =
warmRobinIntegerColumnL1 1 := byQuantumBlockEncoding.Robin.warmRobinSymmetryPlusFourShiftDecomposition
theorem warmRobinSymmetryPlusFourShiftDecomposition (row column : Fin 4) :
warmRobinSymmetryPlusBlock row column =
∑ slot : Fin 4,
if warmRobinSymmetryFourShiftPerm slot column = row then
warmRobinSymmetryPlusWeight slot column
else 0 := byQuantumBlockEncoding.Robin.warmRobinSymmetryMinusFourShiftDecomposition
theorem warmRobinSymmetryMinusFourShiftDecomposition (row column : Fin 4) :
warmRobinSymmetryMinusBlock row column =
∑ slot : Fin 4,
if warmRobinSymmetryFourShiftPerm slot column = row then
warmRobinSymmetryMinusWeight slot column
else 0 := byQuantumBlockEncoding.Robin.warmRobinHadamard8VerifiedBlockEncoding
noncomputable def warmRobinHadamard8VerifiedBlockEncoding :
VerifiedOperatorBlockEncoding ℂ 3 where
candidate := warmRobinHadamard8OperatorCandidate
unitaryProof := warmRobinHadamard8FlatUnitary_unitary
blockProof := warmRobinHadamard8BlockContainsTarget_proof
/-- Honest boundary: primitive synthesis/refinement is still a separate T3 theorem. -/QuantumBlockEncoding.Robin.warmRobinFourSlotVerifiedBlockEncoding
noncomputable def warmRobinFourSlotVerifiedBlockEncoding :
VerifiedOperatorBlockEncoding ℂ 3 where
candidate := warmRobinFourSlotOperatorCandidate
unitaryProof := warmRobinFourSlotFlatUnitary_unitary
blockProof := warmRobinFourSlotBlockContainsTarget_proof
/-- Under one T2 logical-stage convention, four slots strictly improve the
Hadamard-8 route: gate count and depth tie, while the clean layout uses one
fewer auxiliary qubit. -/QuantumBlockEncoding.Robin.warmRobinFourSlotT2Cost_betterThan_hadamard8
theorem warmRobinFourSlotT2Cost_betterThan_hadamard8 :
warmRobinFourSlotOperatorCandidate.cost.betterThan
warmRobinHadamard8OperatorCandidate.cost := byQuantumBlockEncoding.Robin.warmRobinSplitSeven_duplicate_nonzero_access
theorem warmRobinSplitSeven_duplicate_nonzero_access :
warmRobinSevenSlotPerm (2 : Fin 7) (6 : Fin 8) = 7 ∧
warmRobinSevenSlotPerm (5 : Fin 7) (6 : Fin 8) = 7 ∧
warmRobinSevenSlotWeight (2 : Fin 7) (6 : Fin 8) = 16 ∧
warmRobinSevenSlotWeight (5 : Fin 7) (6 : Fin 8) = 16 := byQuantumBlockEncoding.Robin.warmRobinSourceSevenSparseDecomposition
theorem warmRobinSourceSevenSparseDecomposition (row column : Fin 8) :
warmRobinIntegerTarget row column =
∑ slot : Fin 8,
if slot.val < 7 ∧ warmRobinSourceDTRow slot column = row then
warmRobinSourceSevenWeight slot column
else 0 := byQuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk_matches_periodic
theorem warmRobinFigure4TransposeBulk_matches_periodic
(column : Fin 8) (bulk : warmRobinFigure4TransposeBulk column) :
∀ row, warmRobinIntegerTarget row column =
warmRobinPeriodicIntegerReference row column :=
warmRobinPeriodic_columns_three_and_four column bulkQuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_eval_eq_logical
theorem warmRobinPaperSevenPrimitive_eval_eq_logical :
evalPrimitiveProgram warmRobinPaperSevenPrimitiveProgram =
_root_.Matrix.reindexAlgEquiv ℂ ℂ
warmRobinPaperSevenBitsEquiv.symm
warmRobinPaperSevenWorkspaceLogicalUnitary := byQuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_cleanBlock
theorem warmRobinPaperSevenPrimitive_cleanBlock (row column : Fin 8) :
warmRobinPaperSevenPrimitiveFlatUnitary
(warmRobinPaperSevenPrimitiveCleanIndex row)
(warmRobinPaperSevenPrimitiveCleanIndex column) =
((RobinEvolution.warmRobinTarget row column /
RobinEvolution.warmRobinNormalizer : Rat) : ℂ) := byQuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveVerifiedBlockEncoding
noncomputable def warmRobinPaperSevenPrimitiveVerifiedBlockEncoding :
VerifiedOperatorBlockEncoding ℂ 3 where
candidate := warmRobinPaperSevenPrimitiveOperatorCandidate
unitaryProof := warmRobinPaperSevenPrimitiveFlatUnitary_unitary
blockProof := warmRobinPaperSevenPrimitiveBlockContainsTarget_proofQuantumBlockEncoding.Robin.warmRobinFigure4TransportedPostSwapCleanup
theorem warmRobinFigure4TransportedPostSwapCleanup
(slot column : Fin 8) (coefficient indicator : Fin 2) :
let afterDT := warmRobinFigure4DTSparseAccessBasisEquiv
(warmRobinFigure4TransportInput slot column coefficient indicator)
let afterSwap := warmRobinFigure4RegisterSwapFullBasisEquiv afterDT
let output := warmRobinFigure4DSparseAccessBasisEquiv.symm afterSwap
warmRobinFigure4AddressBits output = slot ∧
warmRobinFigure4SystemBits output =
warmRobinSourceDTRow slot column ∧
output 6 = coefficient ∧ output 7 = indicator ∧ output 8 = 0 := byQuantumBlockEncoding.Robin.warmRobinFigure4Primitive_eval_eq_logical
theorem warmRobinFigure4Primitive_eval_eq_logical :
evalPrimitiveProgram warmRobinFigure4PrimitiveProgram =
_root_.Matrix.reindexAlgEquiv ℂ ℂ
warmRobinFigure4BitsEquiv.symm
(star (ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinFigure4FullSystem)
warmRobinPaperSevenSelectorPrepare) *
warmRobinFigure4LogicalMiddle *
ComplexLCU.selectorLift (coefficient := Fin 2)
(system := WarmRobinFigure4FullSystem)
warmRobinPaperSevenSelectorPrepare) := byQuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCircuit_cleanBlock
theorem warmRobinFigure4PrimitiveCircuit_cleanBlock (row column : Fin 8) :
warmRobinFigure4PrimitiveFlatUnitary
(warmRobinFigure4PrimitiveCleanIndex row)
(warmRobinFigure4PrimitiveCleanIndex column) =
((RobinEvolution.warmRobinTarget row column /
RobinEvolution.warmRobinNormalizer : Rat) : ℂ) := byQuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveVerifiedBlockEncoding
noncomputable def warmRobinFigure4PrimitiveVerifiedBlockEncoding :
VerifiedOperatorBlockEncoding ℂ 3 where
candidate := warmRobinFigure4PrimitiveOperatorCandidate
unitaryProof := warmRobinFigure4PrimitiveCircuit_unitary
blockProof := warmRobinFigure4PrimitiveBlockContainsTarget_proofQuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitive_eval_eq_flatUnitary
theorem warmRobinXorFourSlotPrimitive_eval_eq_flatUnitary :
evalPrimitiveCircuit warmRobinXorFourSlotPrimitiveCircuit =
_root_.Matrix.reindexAlgEquiv ℂ ℂ
(primitiveBasisLEEquiv 6).symm
warmRobinXorFourSlotFlatUnitary := byQuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveVerifiedBlockEncoding
noncomputable def warmRobinXorFourSlotPrimitiveVerifiedBlockEncoding :
VerifiedOperatorBlockEncoding ℂ 3 where
candidate := warmRobinXorFourSlotPrimitiveOperatorCandidate
unitaryProof := warmRobinXorFourSlotFlatUnitary_unitary
blockProof := warmRobinXorFourSlotPrimitiveBlockContainsTarget_proof
/-- Dashboard-compatible names explicitly pointing to the XOR T3 route. -/QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_paperSeven
theorem warmRobinFourSlotT3Cost_betterThan_paperSeven :
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.betterThan
warmRobinPaperSevenPrimitiveOperatorCandidate.cost := byQuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_figure4
theorem warmRobinFourSlotT3Cost_betterThan_figure4 :
warmRobinXorFourSlotPrimitiveOperatorCandidate.cost.betterThan
warmRobinFigure4PrimitiveOperatorCandidate.cost := byQuantumBlockEncoding.Robin.warmRobinBestVerified
noncomputable abbrev warmRobinBestVerified :
VerifiedOperatorBlockEncoding ℂ 3 :=
warmRobinXorFourSlotPrimitiveVerifiedBlockEncoding
/-- Machine-readable publication guard, enabled only after both source-side
same-tier comparisons have compiled. -/QuantumBlockEncoding.Robin.warmRobinPublicationState_consistent
theorem warmRobinPublicationState_consistent :
paperLevelWinnerCertified = true ∧
warmRobinFixedN8SourceOpenContracts = [] ∧
warmRobinFigure4OpenPrimitiveContracts = [] := byEq. (29) and first line of Eq. (30)
Check whether the printed phases really cancel the filler block before accepting the S1 LCU equality.
Local declarationsCompiled
Paper-wide routeCompiled
\[e^{i\pi}=e^{-i\pi}=-1\;\Longrightarrow\;\text{printed filler}=-\mathcal N_A I\neq0,\qquad\text{phase-balanced filler}=0.\]
What Lean currently establishes
This row is a source audit, not a new open problem. ASPBE proves the literal printed full-clean-matrix phase pair does not produce S1 when N_A is nonzero, and proves a phase-balanced correction produces exactly S1.
Corresponding declarations
QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_lowerRightQuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1
Show the paper-side LaTeX
e^{i\pi}=e^{-i\pi}=-1\;\Longrightarrow\;\text{printed filler}=-\mathcal N_A I\neq0,\qquad\text{phase-balanced filler}=0.QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_lowerRight
theorem eq29PrintedClean_lowerRight [DecidableEq ι]
(A B : CMatrix ι ι) (normalizerA : ℂ) (i : ι) :
eq29PrintedClean A B normalizerA (Sum.inr i) (Sum.inr i) = -normalizerA := byQuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1
theorem eq29PrintedClean_ne_S1 [DecidableEq ι]
(A B : CMatrix ι ι) (normalizerA : ℂ) (i : ι)
(hN : normalizerA ≠ 0) :
eq29PrintedClean A B normalizerA ≠ S1 A B := byQuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1
theorem eq29PhaseBalancedClean_eq_S1 [DecidableEq ι]
(A B : CMatrix ι ι) (normalizerA : ℂ)
(hB : IsHermitian B) :
eq29PhaseBalancedClean A B normalizerA = S1 A B := byEq. (29), Eq. (30), Theorem 4
Use verified LCU clean-block algebra to combine A and A-dagger into S1 and S2, then assemble the one-dimensional Hamiltonian; keep the printed phase audit explicit.
Local declarationsCompiled
Paper-wide routeCompiled
\[A=\sum_kA_k,\qquad A^\dagger=\sum_kA_k^\dagger,\qquad S=S_1+iS_2,\qquad H=S_1\otimes x_\xi+S_2\otimes I_\xi.\]
What Lean currently establishes
Theorem 4 is not left open. Lean closes the source-audited LCU route through A/A-dagger, S1/S2, H, and the paper-facing normalization/layout/resource records. The literal printed S1 phase pair is separately refuted as a full clean matrix and replaced by an explicit phase-balanced correction. Uniform primitive compilation of all arbitrary-width Theorem-3 oracles remains a separate implementation frontier.
Corresponding declarations
QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint_sumTermsQuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_lowerRightQuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean_eq_S2QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.Adagger_eq_sum_term_adjointsQuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H_eq_S1_tensor_xXi_add_S2_tensor_IQuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_normalization_closedQuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_layout_closedQuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianResource_pureAncilla_closedQuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed
Show the paper-side LaTeX
A=\sum_kA_k,\qquad A^\dagger=\sum_kA_k^\dagger,\qquad S=S_1+iS_2,\qquad H=S_1\otimes x_\xi+S_2\otimes I_\xi.QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint_sumTerms
theorem adjoint_sumTerms {η : Type*} [Fintype η]
(terms : η → CMatrix ι ι) :
adjoint (sumTerms terms) = sumTerms (fun k => adjoint (terms k)) := byQuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_lowerRight
theorem eq29PrintedClean_lowerRight [DecidableEq ι]
(A B : CMatrix ι ι) (normalizerA : ℂ) (i : ι) :
eq29PrintedClean A B normalizerA (Sum.inr i) (Sum.inr i) = -normalizerA := byQuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1
theorem eq29PrintedClean_ne_S1 [DecidableEq ι]
(A B : CMatrix ι ι) (normalizerA : ℂ) (i : ι)
(hN : normalizerA ≠ 0) :
eq29PrintedClean A B normalizerA ≠ S1 A B := byQuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1
theorem eq29PhaseBalancedClean_eq_S1 [DecidableEq ι]
(A B : CMatrix ι ι) (normalizerA : ℂ)
(hB : IsHermitian B) :
eq29PhaseBalancedClean A B normalizerA = S1 A B := byQuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean_eq_S2
theorem eq30Clean_eq_S2 [DecidableEq ι]
(A B : CMatrix ι ι) (normalizerA : ℂ)
(hB : IsHermitian B) :
eq30Clean A B normalizerA = S2 A B := byQuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.Adagger_eq_sum_term_adjoints
theorem Adagger_eq_sum_term_adjoints
(cert : OneDimCompositionCertificate η ι ξ) :
cert.Adagger = sumTerms (fun k => adjoint (cert.terms k)) := byQuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H_eq_S1_tensor_xXi_add_S2_tensor_I
theorem H_eq_S1_tensor_xXi_add_S2_tensor_I
(cert : OneDimCompositionCertificate η ι ξ) :
cert.H = add (tensor cert.first cert.xXi)
(tensor cert.second (identity ξ)) := byQuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_normalization_closed
theorem oneDimHamiltonianClaim_normalization_closed :
oneDimHamiltonianClaim.normalization = "O(kappa * ||H||_max)" := byQuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_layout_closed
theorem oneDimHamiltonianClaim_layout_closed :
oneDimHamiltonianClaim.layout =
"ceil(log2 n_xi)+ceil(log2 n)+ceil(log2 G)+ceil(log2 kappa)+ceil(log2 eta)+7 signal qubits" := byQuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianResource_pureAncilla_closed
theorem oneDimHamiltonianResource_pureAncilla_closed :
oneDimHamiltonianResourceExpr.pureAncilla =
(2 : CostExpr) * CostExpr.atom "n" + 2 := byQuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed
theorem theorem4_source_lcu_route_closed [DecidableEq ι] [DecidableEq ξ]
{η : Type*} [Fintype η]
(cert : OneDimCompositionCertificate η ι ξ)
(normalizerA : ℂ) :
eq29PhaseBalancedClean cert.A cert.B normalizerA = cert.first ∧
eq30Clean cert.A cert.B normalizerA = cert.second ∧
cert.H = add (tensor cert.first cert.xXi)
(tensor cert.second (identity ξ)) ∧
oneDimHamiltonianClaim.normalization = "O(kappa * ||H||_max)" ∧
oneDimHamiltonianClaim.resource = oneDimHamiltonianResourceExpr := by