%
\label{def:ladder-checker}
The \textbf{Ladder Checker} is a quadruple of decision procedures:
\begin{enumerate}
    \item \texttt{existence\_checker}$(k)$:
          Given $k \in \{0, 1, 2, 3\}$,
          certifies that $E_k$ is non-empty
          by producing an explicit object $x_k \in \Obj(E_k)$
          together with a non-identity endomorphism $f_k : x_k \to x_k$.
    \item \texttt{stability\_checker}$(k)$:
          Given $k \in \{0, 1, 2, 3\}$,
          certifies that $E_k$ is closed
          under morphism composition:
          for all composable pairs $(g, f)$ in~$E_k$,
          the composite $g \circ f$ remains in~$E_k$.
    \item \texttt{strictness\_checker}$(k)$:
          Given $k \in \{1, 2, 3\}$,
          certifies that $E_k \setminus E_{k-1} \neq \varnothing$
          by exhibiting a \emph{strictness witness}:
          an object $w_k \in E_k$
          together with a proof that $w_k \notin E_{k-1}$.
    \item \texttt{saturation\_checker}$(k_{\max})$:
          Given $k_{\max} = 3$,
          certifies that $\mathcal{F}_E(E_{k_{\max}}) = E_{k_{\max}}$
          by showing that the functor category
          $[E_3^{\mathrm{op}}, E_3]$ introduces no
          object outside~$E_3$.
\end{enumerate}