papers/hanzo-harness-hacking/sections/13-proof-of-proposition-ref-prop-gate-mono.tex

\section{Proof of Proposition~\ref{prop:gate-mono}
}
\label{app:proof-gate}

\begin{proof}[Full Proof]
We show each implication:

$\Gamma_4 \Rightarrow \Gamma_3$: CI ($\Gamma_4$) includes all automated checks.
When CI passes, the diff is syntactically and semantically valid code, which is
the minimum requirement for agent review ($\Gamma_3$). Human approval additionally
requires the content to be judged appropriate, which is strictly stronger than
agent review. Therefore $\Gamma_4 \Rightarrow \Gamma_3$.

$\Gamma_3 \Rightarrow \Gamma_2$: Agent review ($\Gamma_3$) requires the
modification to have passed the agent's quality check. The agent's review
process verifies logical consistency, which subsumes syntactic correctness and
test passage ($\Gamma_2$). Therefore $\Gamma_3 \Rightarrow \Gamma_2$.

$\Gamma_2 \Rightarrow \Gamma_1$: \texttt{AllTests}($\xi.\mathcal{S}$) in
$\Gamma_2$ includes tests over the triggering failure cases $\mathcal{C}$.
Therefore $\Gamma_2 \Rightarrow \Gamma_1$.

Composing: $\Gamma_4 \Rightarrow \Gamma_3 \Rightarrow \Gamma_2 \Rightarrow \Gamma_1$. \qed
\end{proof}