BE Case 2: cubic diagonal family, hinted route

% Requires: \usepackage{quantikz}
\paragraph{Construction.}
\[
O_0=\sum_{j=0}^{2^n-1}x_j|j\rangle\!\langle j|,\quad x_j=\frac{j}{2^n},\qquad D_n=O_0^3=\sum_jx_j^3|j\rangle\!\langle j|.
\]

% Hint parsed
\begin{quantikz}[column sep=.45cm]
\lstick{$\ket j$} & \gate{O_0:\,x_j} & \gate{p(z)=z^3} & \rstick{$x_j^3$} \qw
\end{quantikz}

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

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

\paragraph{Proof.}
Lean closes two named endpoints: an exact linear-diagonal Householder input block and an exact cubic-diagonal Householder output block. The algebraic hint chooses a route; each unitary and clean block is still proved independently.
\begin{enumerate}
  \item The prose suggestion is converted into two formal operator contracts.
  \item The input diagonal block has exact unitarity, projection, alpha, and resource fields.
  \item The desired cubic family is closed independently; the differing branch widths are not ranked here.
\end{enumerate}
Each advertised certificate is the named Lean declaration linked on this page.

import QuantumBlockEncoding

#check QuantumBlockEncoding.CubicDiagonalOracle.linearDiagonalHouseholderInputBEContract_complete
#check QuantumBlockEncoding.CubicDiagonalOracle.cubicDiagonalHouseholderExactBEContract_complete