%
\label{thm:k5-structural-exclusion}
$\KAxiom{5}$'s diagonal discipline
(Definition~\ref{def:diagonal-discipline}, I.D03),
which maps onto the $!$-free fragment of linear logic
via the Diagonal--Linear Correspondence
(Theorem~\ref{thm:diagonal-linear}, I.T37),
structurally excludes the diagonal morphisms
$\Delta_A : A \to A \otimes A$
that Lawvere's fixed-point theorem requires.
Specifically:
\begin{enumerate}[\normalfont(i)]
    \item $\KAxiom{5}$.1
          (``no unearned diagonals'')
          directly refuses $\Delta_A$ for general $A$.
          The diagonal map would require
          an object to occupy two orbit positions
          simultaneously without an explicit
          $\rho$-construction earning the second copy.
          Under the Diagonal--Linear Correspondence,
          this is the absence of the contraction rule
          in the $!$-free fragment.
    \item $\KAxiom{5}$.2
          (``each overflow consumes one channel'')
          enforces linear resource tracking:
          using a channel in a construction
          removes it from availability.
          Under the correspondence,
          this is the one-use-per-formula discipline
          of linear sequent calculus.
    \item $\KAxiom{5}$.3
          (``saturation at four channels'')
          bounds the total resource budget
          at four orbit rays
          ($\alpha$, $\pi$, $\gamma$, $\eta$).
          Under the correspondence,
          this is a finite linear context
          $|\Gamma| \leq 4$.
\end{enumerate}
The Diagonal--Linear Correspondence
(Definition~\ref{def:diagonal-linear}, I.D78;
Theorem~\ref{thm:diagonal-linear}, I.T37)
places $\tau$'s structural discipline
in the $*$-autonomous regime.
Since Lawvere's fixed-point theorem requires
the diagonal morphism $\Delta_A$ that
$*$-autonomous categories do not possess,
the standard categorical proof of incompleteness
does not apply to $\tau$'s internal proof theory.

[Proof sketch]
The argument has three components.

\textbf{Step 1: K5 maps to the $!$-free fragment.}
The Diagonal--Linear Correspondence
(Theorem~\ref{thm:diagonal-linear}, I.T37)
establishes that $\KAxiom{5}$'s three constraints
are structurally isomorphic
to the structural rules of the $!$-free fragment
of Girard's linear logic:
K5.1 corresponds to the absence of contraction,
K5.2 to linear resource consumption,
K5.3 to a bounded context.
This was verified clause-by-clause
in Chapter~\ref{ch:diagonal-linear-correspondence}.

\textbf{Step 2: The $!$-free fragment models in $*$-autonomous categories.}
$*$-Autonomous categories
(Remark~\ref{rem:barr-star-autonomous})
are the categorical semantics
of the multiplicative fragment of linear logic.
In these categories,
the tensor $\otimes$ is not cartesian:
no general diagonal $\Delta_A : A \to A \otimes A$ exists.
This is a standard result in categorical proof theory
--- the correspondence between
$*$-autonomous categories
and multiplicative linear logic
was established by Seely (1989)
and refined by subsequent work.

\textbf{Step 3: Lawvere's theorem requires the diagonal.}
Lawvere's fixed-point theorem
(Remark~\ref{rem:lawvere-fpt})
requires the diagonal $\Delta_A$
to construct the self-referential morphism $g$
that produces a fixed point.
Without $\Delta_A$, the morphism $g(a) = f(e(a)(a))$
cannot be formed ---
the double use of $a$
(once as argument to $e$, once as argument to $e(a)$)
is the operational content of the diagonal.
In the $*$-autonomous regime,
this double use is structurally unavailable.

Combining: $\KAxiom{5}$ places $\tau$
in the $!$-free fragment (Step~1),
which models in $*$-autonomous categories (Step~2),
where Lawvere's theorem does not apply (Step~3).