1\subsection{Axis C: reduced-step SHA-256 (H15--H19)}2\label{sec:results-sha}34\paragraph{Diffusion (H15).} A single-bit difference in $W_0$ flips on average $1.5\%$ of the state bits after one5step and reaches the $0.49$ threshold at step~\shaDiffWzero{} (Table~\ref{tab:sha-diff}, Figure~\ref{fig:sha-diff}); a6difference in $W_5$ or $W_{15}$ is invisible until the word enters the state and then follows the same six-step7profile (full diffusion at steps \shaDiffWfive{} and \shaDiffWfifteen{}); a difference in an IV register needs8\shaDiffIV{} steps. The profile is identical across three seeds of \shaDiffN{} messages. After 64 steps the Hamming9weight of the output difference is $\shaDiffHamming\pm\shaDiffHammingSd$, indistinguishable from the random-oracle10control ($\shaDiffRO$ flip ratio). Classification: known behaviour, reproduced with a precise step count.1112\begin{table}[htbp]13 \centering\footnotesize14 \caption{Mean fraction of flipped state bits after $s$ steps for a single-bit input difference (three seeds $\times$ \shaDiffN{} random messages; identical across seeds to three decimals).}15 \label{tab:sha-diff}16 \input{tables/sha_diffusion}17\end{table}1819\begin{figure}[htbp]20 \centering21 \includegraphics[width=\textwidth]{sha256_diffusion.pdf}22 \caption{Reduced-round diffusion: flip probability of each output bit by step for a one-bit difference in $W_0$ (heat map) and mean flip ratio by step with the random-oracle control. Generated by \code{figures/make\_sha256\_figures.py}.}23 \label{fig:sha-diff}24\end{figure}2526\paragraph{Statistical regularities (H16).} With $N=\shaBiasN{}$ messages per seed the $4\sigma$ thresholds are27$0.014$ for a bit bias and $0.028$ for a correlation, with \shaBiasExpectedPairs{} chance pairs expected among the28$64\times 256$ tested. For $r\le 3$ steps, $64(4-r)$ output bits are untouched IV registers (bias $0.5$,29$\chi^2$ rejections, correlations equal to~1); at $r=4$ the bit biases and byte distributions are already at the30noise floor but 6--13 pairs with $\lvert\mathrm{corr}\rvert=1$ remain (the least significant bit of $e_1$ is an affine31function of the least significant bit of $W_0$ and is still exposed in register~$h$); from $r=\shaBiasFirstClean$32every statistic is at the random-oracle floor and stays there through $r=64$ (Table~\ref{tab:sha-bias},33Figure~\ref{fig:sha-bias}): two isolated $4.1\sigma$ bits in $10\,752$ tests, exactly the number expected by chance.34These are observations, not attacks: the published differential attacks exploit structure far beyond what35first-order statistics on random inputs can see.3637\begin{table}[htbp]38 \centering\footnotesize39 \caption{First-order statistics of the $r$-step compression function on random single-block messages (ranges over three seeds of \shaBiasN{}).}40 \label{tab:sha-bias}41 \input{tables/sha_bias}42\end{table}4344\begin{figure}[htbp]45 \centering46 \includegraphics[width=0.9\textwidth]{sha256_bias.pdf}47 \caption{Bias test: number of biased bits, maximum correlation and significant pairs by step count, with the random-oracle control.}48 \label{fig:sha-bias}49\end{figure}5051\paragraph{SAT and SMT preimage search (H17).} The Tseitin encoding of the full 64-step compression has52\shaPreVars{} variables and \shaPreClauses{} clauses. Over \shaPreCells{} cells ($r\times k\times$ solver $\times$53placement of the $k$ free bits, 2--3 seeds, 300~s) every satisfying assignment was re-hashed with the reference54implementation (\shaPreVerified{} verified). Two regimes appear (Table~\ref{tab:sha-pre}, Figure~\ref{fig:sha-sat}).55For $r\le 16$ the instance is solved in \shaPreRsixteenTime~s with \shaPreRsixteenConf{} conflicts whatever $k$ is:56this is not search but propagation---with at most 16 message words entering the computation, inverting the steps57determines the unknown bits directly (Section~\ref{sec:formal} proves the underlying bijections). As soon as the58message expansion is involved ($r\ge 20$) only the $k=16$ cells are solved: CaDiCaL needs \shaPreRtwentyTime~s at59$r=20$ and \shaPreRsixtyfourTime~s at $r=64$ (\shaPreRsixtyfourSolved{} seeds), Kissat is comparable, and every60$k\ge 24$ cell at $r\ge 20$ times out (the ``spread'' placement of the free bits lets CaDiCaL reach $k=32$ at $r=20$61only). Since $k=16$ free bits is a $2^{16}$ brute-force space, the solvers are \emph{slower} than exhaustive search62once the expansion matters. Z3's bit-vector theory is two to four orders of magnitude slower than the CNF route on63the cells it solves (largest: \shaPreZthreeLargest) and times out on all $r\ge 16$ cells. Peak memory stayed below64302~MB (CNF) and 605~MB (Z3).6566\begin{table}[htbp]67 \centering\footnotesize68 \caption{Preimage search on the $r$-step compression function with $k$ free message bits in $W_0,W_1$ (CaDiCaL~3.0.1, median wall-clock seconds of solved seeds; T($m$) = all $m$ seeds timed out at 300~s; fractions give solved seeds when not all solved).}69 \label{tab:sha-pre}70 \input{tables/sha_preimage_cadical}71\end{table}7273\begin{figure}[htbp]74 \centering75 \includegraphics[width=\textwidth]{sha256_sat_scaling.pdf}76 \caption{SAT/SMT preimage scaling: solver time against step count for each number of free bits, CaDiCaL and Kissat, timeouts censored at 300~s.}77 \label{fig:sha-sat}78\end{figure}7980\paragraph{SAT collision search (H18).} Table~\ref{tab:sha-col} and Figure~\ref{fig:sha-col} give the \shaColCells{}81collision cells (two messages, equal $r$-step output; standard IV or free IV; with or without feed-forward; 600~s;82\shaColVerified{} 119 collisions verified and saved). For $r\in\{4,6,8\}$ both solvers return UNSAT in every variant and83seed (\shaColUnsatCells{} runs, 0.1--4.7~s): there is no collision whose differences lie in the words an 8-step84compression reads, a machine-checked lower bound consistent with the 9-step minimum of the local collision. For85$r=10$--$16$ with the standard IV the solvers find collisions in $0.02$--$0.05$~s with zero conflicts, and every such86collision differs in exactly nine consecutive words---a local collision placed at the end of the computation,87rediscovered by propagation. At $r=18$ all 16 words differ and the cost jumps to \shaColFixedTime~s with the standard88IV (about $10^6$ conflicts) and \shaColFreeTime~s semi-free-start; at $r\ge 20$ every cell times out. The largest89collision found by our generic encoding is therefore \shaColLargestR{} steps, against 24 steps for the 2008 hand90analyses, 28 steps for pure SAT in \citet{alamgir2024sha256}, 31 practical steps for the dedicated tools91\citep{li2024first} and 39 semi-free-start steps \citep{li2024new}. The answer to question~C4 is that unguided92automated search reproduces only the trivial regime; the published records require differential characteristics93that the solver is not given.9495\begin{table}[htbp]96 \centering\footnotesize97 \caption{Collision search on the $r$-step compression function (median seconds of solved seeds; UNSAT with its median time; T($m$) = timeouts at 600~s).}98 \label{tab:sha-col}99 \input{tables/sha_collision}100\end{table}101102\begin{figure}[htbp]103 \centering104 \includegraphics[width=0.9\textwidth]{sha256_collision_scaling.pdf}105 \caption{SAT collision scaling by step count and variant (standard versus free IV, with and without feed-forward), timeouts censored at 600~s.}106 \label{fig:sha-col}107\end{figure}108109\paragraph{The 9-step local collision (H19).} Deriving the correction pattern from the XOR-linearised step gives110$(\delta,\ \SigZ\delta\oplus\SigO\delta,\ \SigO(\SigZ\delta),\ 0,\ \delta,\ \SigZ\delta\oplus\SigO\delta,\ 0,\ 0,\ \delta)$111for $\delta W_i,\dots,\delta W_{i+8}$; a GF(2) matrix computation confirms cancellation for all 32 single-bit112$\delta$ and 20 random multi-bit $\delta$, dropping any one correction leaves a residue, and the statement is113machine-checked for all states and all $\delta$ (Section~\ref{sec:formal}). Applied blindly to the real step114function, the pattern produced \emph{no} collision in \shaLcN{} random samples per bit position (upper bound115$\shaLcBound$ by the rule of three); the difference survives step $i$ with probability \shaLcSurvivalOther{} for116bits 0--30 (two carry conditions) and \shaLcSurvivalMsb{} for the most significant bit (no carry), survives step117$i+1$ with probability $10^{-4}$ to $5\cdot10^{-4}$, and never survives step $i+2$ (Figure~\ref{fig:sha-lc}). That is118the known picture: the linear model is exact, the real step follows it only under conditions on message and state119bits. Given the freedom to choose those bits, CaDiCaL finds a conforming (state, $W_i..W_{i+8}$) pair for all120\shaLcSatBits{} bit positions in \shaLcSatMin--\shaLcSatMax~s (fastest for the high bits, slowest for bit~0), each121re-verified; a second seed reproduces bits 31 and~0. Classification: known result reproduced, with the linear part122formally verified.123124\begin{figure}[htbp]125 \centering126 \includegraphics[width=0.85\textwidth]{sha256_local_collision.pdf}127 \caption{The 9-step local collision in the real step function: survival probability of the difference pattern after steps $i$ and $i+1$ by bit position (\shaLcN{} samples each), and SAT time to find a conforming pair.}128 \label{fig:sha-lc}129\end{figure}130131\paragraph{Answers to C1--C5.} C1: reduced-step regularities exist and are fully characterised by the diffusion132profile and the local-collision structure, both of which disappear within a handful of steps on random inputs.133C2: SAT formulations make the invertibility of the first 16 steps and the 9-step minimum for collisions explicit134and machine-checked; beyond that they measure the cost of unguided search, which grows faster than brute force in135the free bits. C3: the only differential structure that remains meaningful as the step count grows is the local136collision with its message conditions, which is exactly what the dedicated attacks chain together. C4: generic137solvers reproduce 18-step collisions, far below the 31-step record. C5: the ``blind'' XOR pattern is a proposed138simplification ruled out by counterexample ($0/3\,200\,000$).139140\subsection{Axis D: the hypothesis portfolio (H23, H24)}141\label{sec:results-portfolio}142143Table~\ref{tab:hypotheses} is the discovery log in condensed form: every hypothesis with its final classification144and a one-sentence verdict (the full records with evidence files are in \code{hypotheses/}). The tally is sixteen145known results independently reproduced---each now with a measured constant, confidence interval or machine-checked146proof---six empirical observations, three rejected conjectures (two of which we had formulated ourselves as147plausible, \Hname{H05} and \Hname{H22}), no conditional result, no unresolved direction left open by lack of148evidence, and no new verified result in the strict sense of the rubric. The cross-implementation gate149(\Hname{H23}) caught two development errors in the Python reference, one in the CNF encoder (a Boolean fold rule150that silently corrupted $\Ch$ gates) and one in the SAT harness (CaDiCaL's interrupt not honoured through the Python151bindings), and corrected two statements written from memory (the local-collision correction vector and the152singularity of $\sigma_0,\sigma_1$). We discuss what this record says about the methodology in153Section~\ref{sec:implications}.154155{\footnotesize\input{tables/hypotheses}}156