BE Case 1: isolated cold reconstruction

% Requires: \usepackage{quantikz}
\paragraph{Construction.}
\[
E_1=|0\rangle\!\langle1|_{\mathrm{time}}\otimes|0\rangle\!\langle1|_{\mathrm{type}}\otimes I_2,\qquad \langle0|_aU_{\mathrm{cold}}|0\rangle_a=E_1.
\]

% Target fixed
\begin{quantikz}[row sep=.4cm, column sep=.65cm]
\lstick{$a:\ket0$} & \gate[wires=2]{U_{\rm cold}\;?} & \meter{} \\
\lstick{$t,y,s$}    &                                  & \qw
\end{quantikz}

% Cold permutation
\begin{quantikz}[row sep=.4cm, column sep=.55cm]
\lstick{$a:\ket0$} & \gate[wires=2]{P_{\rm cold}} & \rstick{$\ket0$ or garbage} \qw \\
\lstick{$t,y,s$}    &                               & \rstick{$E_1\ket{t,y,s}$ on clean branch} \qw
\end{quantikz}

\paragraph{Proof.}
Lean separately proves that the cold image table is bijective, that its clean projection is E_1, and that the packaged candidate has score (5,5,1,0). This page does not call replay a new rediscovery.
\begin{enumerate}
  \item Register order, alpha=1, and the clean block are fixed before construction.
  \item The exact finite candidate closes bijectivity, projection, and resource fields.
\end{enumerate}
Each advertised certificate is the named Lean declaration linked on this page.

import QuantumBlockEncoding

#check QuantumBlockEncoding.mainCaseColdPartialPermImage_bijective
#check QuantumBlockEncoding.mainCaseColdPartialPerm_clean_eq_target
#check QuantumBlockEncoding.mainCaseColdPartialPermVerified
#check QuantumBlockEncoding.mainCaseColdPartialPermCandidate_cost