\subsection{Machine-checked statements}
\label{sec:formal-checked}

The formal layer is a Lean~4.35 project (\code{formal/}, core library only, no Mathlib) that builds from a clean
state in 32~s on the laptop with no \code{sorry} and no user axiom other than the explicit fields of the abstract
group structure. Bit-vector goals are closed by \code{bv\_decide}, which bit-blasts to an and-inverter graph, calls
the CaDiCaL solver bundled with Lean, and re-checks the returned LRAT certificate with Lean's verified checker
\citep{boving2025interactive,demoura2021lean}; a static test (\code{tests/test\_formal\_lean.py}) enforces the absence of
\code{sorry}, \code{axiom}, \code{native\_decide} and Mathlib, and optionally re-runs the build. Table~\ref{tab:formal}
lists the headline theorems; \code{formal/README.md} lists all 80-odd lemmas with the size of each SAT instance,
the exact build output and a record of the attempts that timed out.

\begin{table}[htbp]
  \centering\footnotesize
  \begin{threeparttable}
    \caption{Machine-checked statements (Lean 4.35, \code{bv\_decide} with LRAT certificates unless stated). AIG = nodes of the bit-blasted instance.}
    \label{tab:formal}
    \begin{tabular}{@{}>{\raggedright\arraybackslash}p{4.1cm}>{\raggedright\arraybackslash}p{8.0cm}>{\raggedright\arraybackslash}p{3.4cm}@{}}
      \toprule
      Theorem(s) & Statement & Method (AIG) \\
      \midrule
      \code{Ch\_\allowbreak{}opt}, \code{Maj\_\allowbreak{}opt\_\allowbreak{}or}, \code{Maj\_\allowbreak{}opt\_\allowbreak{}xor} & $\Ch(x,y,z)=((y\oplus z)\wedge x)\oplus z$; $\Maj=(x\wedge(y\vee z))\vee(y\wedge z)=((x\oplus y)\wedge(y\oplus z))\oplus y$ & SAT (608--768) \\
      \code{Sigma0\_\allowbreak{}xor}, \ldots, \code{sigma1\_\allowbreak{}xor} & $\F_2$-linearity of $\SigZ,\SigO,\sigz,\sigo$ & SAT (870--960) \\
      \code{Sigma0\_\allowbreak{}injective}, \code{Sigma1\_\allowbreak{}injective}, \code{sigma0\_\allowbreak{}injective}, \code{sigma1\_\allowbreak{}injective} & all four maps are injective on 32 bits & SAT, UNSAT certificates (644--704) \\
      \code{*\_\allowbreak{}bijective} (4) & explicit inverses: $\SigZ^{-1}$ = XOR of 17 rotations, $\sigz^{-1},\sigo^{-1}$ as $32\times32$ $\F_2$ matrices; both compositions are the identity & byte-split SAT (33--4\,817) + rewriting \\
      \code{shr3\_\allowbreak{}not\_\allowbreak{}injective}, \code{sigma0\_\allowbreak{}rotations\_\allowbreak{}not\_\allowbreak{}injective} & controls: each summand of $\sigz$ is singular & \code{decide} \\
      \code{stepInv\_\allowbreak{}step}, \code{step\_\allowbreak{}stepInv}, \code{step\_\allowbreak{}bijective}, \code{steps\_\allowbreak{}bijective} & the SHA-256 step is a bijection of the 256-bit state for fixed $(K_t,W_t)$, and so is any sequence of steps & two 160-bit SAT lemmas (2\,048, 2\,420) + rewriting; direct 320-bit SAT timed out \\
      \code{scheduleStep\_\allowbreak{}inv}, \code{schedule\_\allowbreak{}backward} & $W_{t-16}=W_t\ominus\sigo(W_{t-2})\ominus W_{t-7}\ominus\sigz(W_{t-15})$; \newline any 16 consecutive schedule words determine all 64 & SAT (1\,921) + recursion \\
      \code{localCollision\_\allowbreak{}absorb}, \code{localCollision\_\allowbreak{}xor3} & in the XOR-linearised step (with $\Ch=\Maj=0$, resp.\ $\Ch=\Maj=x\oplus y\oplus z$), for all states, constants, messages and $\delta$: \newline the correction pattern $(\delta,\ \SigO\delta\oplus\SigZ\delta,\ \SigO(\SigZ\delta),\ 0,\ \delta,\ \SigZ\delta\oplus\SigO\delta,\ 0,\ 0,\ \delta)$ cancels after 9 steps & difference version by byte-split SAT (5\,049 / 8\,769), lifted by proven linearity of the 9-step map \\
      \code{absorb\_\allowbreak{}corrections\_\allowbreak{}not\_\allowbreak{}real\_\allowbreak{}collision} & control: the same corrections do \emph{not} give a collision of the real (modular) 9-step map on a concrete input & \code{decide} \\
      \code{schnorr\_\allowbreak{}correct}, \code{ecdsa\_\allowbreak{}correct}, \code{ecdsa\_\allowbreak{}malleable} & in an axiomatised cyclic group with $x(-P)=x(P)$: $s\equiv k+ed\Rightarrow [s]G=R+[e]P$; ECDSA verification is correct; $(r,s)$ valid $\Rightarrow(r,n-s)$ valid & rewriting from the structure fields (no SAT) \\
      \bottomrule
    \end{tabular}
    \begin{tablenotes}\footnotesize
      \item Every \code{bv\_decide} theorem depends on the per-theorem axiom Lean~4.35 records for the natively executed LRAT check (same trust base as \code{Lean.ofReduceBool}); the group-theoretic theorems depend only on \code{propext} and \code{Quot.sound}. Full \code{\#print axioms} output in \code{formal/build.log}.
    \end{tablenotes}
  \end{threeparttable}
\end{table}

Three points deserve comment. First, the formal layer corrected a belief we held when writing the hypothesis
portfolio: we expected $\sigz$ and $\sigo$ to be non-injective because they contain a logical shift, and the SAT
solver returned UNSAT for the injectivity goal---both are bijections (hypothesis~\Hname{H22}, rejected), which
matters for any analysis that inverts the message schedule. Second, the 9-step local collision required a correction
vector slightly different from the one we had first written down from memory ($\delta W_{i+1}$ must cancel both
$\SigO\delta$ from the $e$-register and $\SigZ\delta$ from the $a$-register); the formal derivation is in the file
header and the Python simulation of Axis~C agrees. Third, what is \emph{not} formalised is as important as what
is: curve arithmetic, the random-mapping analysis, the probability of the real local collision and every timing claim
remain informal, and no conjecture appears as a theorem.