GHL Eq. (9) benchmark at N=8 (A1=B1=0)

% Requires: \usepackage{quantikz}
\paragraph{Construction.}
\[
A_{\mathrm{GHL}}^{(9)}=\Delta x^{-2}\,\widetilde A(A_1\Delta x,B_1\Delta x),\qquad \widetilde A_0:=\widetilde A(0,0)=\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{\widetilde A_0}{56/3}=\frac{M}{224},\quad M=12\widetilde A_0.
\]

% Sparse-source correction
\begin{quantikz}[column sep=.45cm]
\lstick{$(s,j)$} & \gate{\mathrm{audit\;address}} & \gate{\mathrm{deduplicate}} & \rstick{$7\;padded\;slots$} \qw
\end{quantikz}

% Fixed-N8 Figure-4 realization
\begin{quantikz}[row sep=.35cm, column sep=.24cm]
\lstick{$\ket{0^3}_s$} & \gate{H_W} & \ctrl{2} & \qw & \gate{O_{D^T}^{BS}} & \qw & \gate{(O_D^{BS})^\dagger} & \gate{H_W^\dagger} & \qw \\
\lstick{$\ket0_c$}     & \qw        & \qw      & \gate{R_y(2\arccos(D/N_D))} & \qw & \qw & \qw & \qw & \qw \\
\lstick{$\ket j$}      & \qw        & \gate{U_{\rm indic}} & \qw & \qw & \gate{\mathrm{SWAP}} & \qw & \qw & \qw
\end{quantikz}

% Paper-seven normal form
\begin{quantikz}[row sep=.35cm, column sep=.35cm]
\lstick{$\ket{0^3}_s$} & \gate{\mathrm{PREPARE}_7} & \ctrl{1} & \ctrl{2} & \gate{\mathrm{PREPARE}_7^\dagger} & \qw \\
\lstick{$\ket0_c$}     & \qw & \gate{R_y(2\arccos w_s)} & \qw & \qw & \qw \\
\lstick{$\ket j$}      & \qw & \qw & \gate{\mathrm{SELECT}_{+\delta_s}} & \qw & \qw
\end{quantikz}

% XOR four-slot primitive
\begin{quantikz}[row sep=.35cm, column sep=.32cm]
\lstick{$\ket{0^2}_s$} & \gate{\mathrm{PREPARE}_4} & \ctrl{1} & \ctrl{2} & \gate{\mathrm{PREPARE}_4^\dagger} & \qw \\
\lstick{$\ket0_c$}     & \qw & \gate{\mathrm{UCRY}(w_{s,j})} & \qw & \qw & \qw \\
\lstick{$\ket j$}      & \gate{\mathrm{pair\;basis}} & \qw & \gate{\mathrm{XOR\!\ SELECT}} & \gate{\mathrm{uncompute}} & \qw
\end{quantikz}

\paragraph{Proof.}
The displayed and Lean-certified target is not the full symbolic Eq. (9) matrix. It is the dimensionless N=8 stencil A_tilde_0 obtained after setting A1=B1=0; for the homogeneous benchmark A2=B2=0 as well, and those two constants affect only the source vector. Lean proves three exact primitive block encodings of A_tilde_0 under one frozen convention: the padded paper-seven normal form, a fixed-N8 and f=1 standard-RY-corrected realization of Figure 4, and the evolved XOR four-slot candidate. The normalizer 56/3 belongs to A_tilde_0. Restoring the paper's physical Delta x^{-2} factor gives normalizer 56/(3 Delta x^2).
\begin{enumerate}
  \item Lean detects duplicate nonzero accesses in the historical split-seven LCU and replaces it with a true padded-seven sparse enumeration.
  \item The full source order uses the corrected D-transpose bulk window, standard-RY doubled angles, transported cleanup, and f=1 constant folding.
  \item The equivalent sparse source contract compiles directly as PREPARE, amplitude loading, modular-add SELECT, and unprepare.
  \item Two compiled betterThan theorems establish the strict gate-count improvement over both source realizations.
\end{enumerate}
Each advertised certificate is the named Lean declaration linked on this page.

import QuantumBlockEncoding

#check QuantumBlockEncoding.Robin.warmRobin_normalized_eq_integer_div_224
#check QuantumBlockEncoding.RobinEvolution.warmRobinTarget_eq_paperEq9_dimensionless_A1_B1_zero
#check QuantumBlockEncoding.Robin.warmRobinSplitSeven_duplicate_nonzero_access
#check QuantumBlockEncoding.Robin.warmRobinSourceSevenSparseDecomposition
#check QuantumBlockEncoding.Robin.warmRobinFigure4TransposeBulk_matches_periodic
#check QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_eval_eq_logical
#check QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_cleanBlock
#check QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveVerifiedBlockEncoding
#check QuantumBlockEncoding.Robin.warmRobinFigure4TransportedPostSwapCleanup
#check QuantumBlockEncoding.Robin.warmRobinFigure4Primitive_eval_eq_logical
#check QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveCircuit_cleanBlock
#check QuantumBlockEncoding.Robin.warmRobinFigure4PrimitiveVerifiedBlockEncoding
#check QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitive_eval_eq_flatUnitary
#check QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitive_cleanBlock
#check QuantumBlockEncoding.Robin.warmRobinXorFourSlotPrimitiveVerifiedBlockEncoding
#check QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_paperSeven
#check QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_betterThan_figure4
#check QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_componentwise_paperSeven
#check QuantumBlockEncoding.Robin.warmRobinFourSlotT3Cost_componentwise_figure4
#check QuantumBlockEncoding.Robin.warmRobinBestVerified
#check QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint_sumTerms
#check QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.Adagger_eq_sum_term_adjoints
#check QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H_isHermitian
#check QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H_eq_S1_tensor_xXi_add_S2_tensor_I
#check QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_lowerRight
#check QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1
#check QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1
#check QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean_eq_S2
#check QuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed