BE Case 2: cubic diagonal family, cold route

% Requires: \usepackage{quantikz}
\paragraph{Construction.}
\[
D_n=\operatorname{diag}_{0\le j<2^n}\!\left(\frac{j}{2^n}\right)^3,\qquad \Pi U_n\Pi^\dagger=D_n.
\]

% Symbolic target
\begin{quantikz}[row sep=.4cm, column sep=.65cm]
\lstick{$\ket{0^3}$} & \gate[wires=2]{U_n\;?} & \meter{} \\
\lstick{$\ket j$}    &                       & \qw
\end{quantikz}

% Rational branch completion
\begin{quantikz}[row sep=.4cm, column sep=.55cm]
\lstick{$\ket{0^3}$} & \gate{\mathrm{complete}(x_j^3)} & \rstick{$\ket{v_j}$} \qw \\
\lstick{$\ket j$}    & \ctrl{-1}                       & \qw
\end{quantikz}

% Householder direct sum
\begin{quantikz}[row sep=.4cm, column sep=.55cm]
\lstick{$\ket{0^3}$} & \gate{H(v_j)} & \rstick{$x_j^3\ket0+\ket{\perp_j}$} \qw \\
\lstick{$\ket j$}    & \ctrl{-1}     & \qw
\end{quantikz}

\paragraph{Proof.}
For arbitrary n, Lean constructs exact rational branch vectors using the four-square theorem, forms a controlled direct sum of Householder matrices, proves rational orthogonality, and proves the clean block equals D_n with alpha=1.
\begin{enumerate}
  \item The target is diag((j/2^n)^3), not one sampled n=2 matrix.
  \item Four-square witnesses close exact normalization for every branch.
  \item The final conjunction proves orthogonality, clean block, alpha, and logical resource record.
\end{enumerate}
Each advertised certificate is the named Lean declaration linked on this page.

import QuantumBlockEncoding

#check QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalRationalCompletion_exists
#check QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_clean_eq_target
#check QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_complete