%
\label{def:diagonal-linear}
The \textbf{diagonal--linear correspondence}
is the structural isomorphism between $\KAxiom{5}$'s
diagonal discipline and the $!$-free fragment
of Girard's linear logic, given by the following map:
\begin{enumerate}
    \item \textbf{K5.1 $\longleftrightarrow$ no free contraction.}
          ``No unearned diagonals'' (K5.1) states that
          the diagonal map $\Delta : A \to A \otimes A$
          is not available without explicit construction.
          In linear logic, the contraction rule
          \[
              \frac{\Gamma, A, A \vdash B}{\Gamma, A \vdash B}
              \quad\text{(contraction)}
          \]
          is absent in the $!$-free fragment.
          Both express the same constraint:
          a resource cannot be duplicated without cost.
    \item \textbf{K5.2 $\longleftrightarrow$ linear resource tracking.}
          ``Each overflow consumes one channel'' (K5.2) states
          that using a channel in a construction
          removes it from the available context.
          In linear sequent calculus,
          using a formula $A$ in a derivation
          \emph{consumes} $A$ from the context $\Gamma$:
          the formula is no longer available
          for subsequent steps.
          Both express the same discipline:
          resources are tracked, not ambient.
    \item \textbf{K5.3 $\longleftrightarrow$ finite resource budget.}
          ``Saturation at four channels'' (K5.3) bounds
          the total linear context.
          The four orbit rays
          ($\alpha$, $\pi$, $\gamma$, $\eta$)
          define a finite resource pool.
          In the linear reading,
          the sequent $\Gamma \vdash C$
          has $|\Gamma| \leq 4$:
          the context is bounded.
\end{enumerate}