% Source excerpts used by the QuantumComputinglib Robin correspondence page.
% Source: Guseynov--Huang--Liu (2025), arXiv:2506.20478.
% These statements are paper inputs, not Lean certificates.

\subsection*{Banded sparse access}
Robin Lemma~2 invokes Lemma~1 of arXiv:2405.12855 for this primitive:
\[
\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.
\]

\subsection*{Bulk indicator}
\[
\begin{aligned}
U_{\mathrm{indic}}(K_1,K_2)
  \sum_{i=0}^{2^n-1}\sigma_i\ket{i}^n\ket{0}
={}&
\sum_{i=0}^{K_1-1}\sigma_i\ket{i}^n\ket{0}\\
&+\sum_{i=K_1}^{K_2}\sigma_i\ket{i}^n\ket{1}
+\sum_{i=K_2+1}^{2^n-1}\sigma_i\ket{i}^n\ket{0}.
\end{aligned}
\]

\subsection*{Boundary rotations}
Equation~(27) prints a single \(\arccos\), which is missing a factor of two
under the standard \(R_y(\theta)\) convention.  The corrected executable and
formal contract is
\[
\theta_j^s =
2\arccos\left(\frac{D_j^{(s)}}{\mathcal{N}_D}\right),
\quad
s=0,\ldots,\kappa-1,
\quad
j\in[0,K_1)\cup(K_2,2^n).
\]
The paper-literal single-\(\arccos\) expression is retained in the source-audit
record only; it is not used as a standard-\(R_y\) amplitude loader.

\subsection*{One-term theorem}
For a piecewise-continuous \(f\) and a discretized \(\kappa\)-sparse Robin
derivative matrix \(D\), the paper states a
\[
\left(
  \mathcal{N}_D\mathcal{N}_f\kappa,\;
  \left\lceil\log_2 n\right\rceil+
  \left\lceil\log_2 G_f\right\rceil+
  \left\lceil\log_2\kappa\right\rceil+4,\;
  0
\right)
\]
block encoding of
\[
A_k\sim f(x)\frac{\partial^m}{\partial x^m},
\]
with gate complexity
\[
\mathcal{O}\left(\sum_{g=1}^{G}Q_g n\log n+\kappa n\right)
\]
and \(2n\) pure ancillas.

\subsection*{The clean gamma-three coefficient}
\[
\ket{\gamma_3}
=
\frac{1}{\mathcal{N}_D\mathcal{N}_f\kappa}
\sum_{\substack{s=0,\ldots,\kappa-1\\
0\le j<K_1\ \cup\ K_2<j<2^n}}
f(x_i)D_i^{(s)}\sigma^{(s)}
\ket{0}^{m_f+1}\ket{s}
\ket{0}^{n-\lceil\log_2\kappa\rceil}\ket{j}\ket{0}
+\cdots.
\]


% ASPBE-THEOREM4-COMPOSITION
% Source audit note for Eq. (18), Eqs. (29)-(30), and Theorem 4.
% The paper combines the one-term A_k and A_k^\dagger encodings into A and
% A^\dagger, defines the Hermitian pieces S_1 and S_2 of the homogenized
% system, and then forms
%   H = S_1 \otimes x_\xi + S_2 \otimes I_\xi.
% The corresponding Lean source-level composition roots live in
% QuantumBlockEncoding/GHLHamiltonian.lean.


% ASPBE-THEOREM4-PHASE-AUDIT
% Eq. (29) defines both L_1(phi) and L_2(phi) with the filler I exp(i phi).
% The first line of Eq. (30) then uses phases pi and -pi.  Since both phases
% equal -1, a literal full-clean-matrix addition leaves the lower-right filler
% -N_A I rather than the displayed zero block.  ASPBE records this as the
% theorem eq29PrintedClean_ne_S1 (for nonzero N_A), and separately certifies a
% phase-balanced correction with filler phases +1 and -1 via
% eq29PhaseBalancedClean_eq_S1.  The S_2 line closes with the printed zero
% phases, and theorem4_source_lcu_route_closed packages the corrected S_1,
% printed S_2, final H formula, and paper-facing metadata.
