%
\label{thm:diagonal-linear}
The diagonal discipline
(Definition~\ref{def:diagonal-discipline}, I.D03)
and the structural fragment of $!$-free linear logic
are structurally isomorphic in the following sense:
\begin{enumerate}
    \item[\textup{(i)}]
          $\KAxiom{5}$'s refusal of self-products
          within a channel corresponds to the absence
          of the contraction rule:
          \[
              \frac{\Gamma, A, A \vdash B}{\Gamma, A \vdash B}
              \quad\text{is not available.}
          \]
    \item[\textup{(ii)}]
          $\KAxiom{5}$'s channel consumption
          corresponds to the linear sequent calculus's
          one-use-per-formula rule:
          each formula in $\Gamma$ is consumed
          exactly once in any derivation.
    \item[\textup{(iii)}]
          $\KAxiom{5}$'s saturation at four channels
          corresponds to a finite linear context:
          $|\Gamma| \leq 4$.
    \item[\textup{(iv)}]
          $\KAxiom{5}$'s controlled overflow
          (three rewiring levels:
          addition $\to$ multiplication
          $\to$ exponentiation $\to$ tetration)
          corresponds to controlled introduction
          of $!$-like reuse,
          bounded by the solenoidal count
          ($\KAxiom{6}$: three solenoidal channels,
          since four channels minus one scaffold
          yields three).
\end{enumerate}

[Proof sketch]
We verify each clause by structural comparison.

\textbf{(i) Contraction.}
In $\tau$, the diagonal map
$\Delta_A : A \to A \times A$
would require sending an object to two copies of itself.
$\KAxiom{5}$.1 refuses this:
the object occupies one orbit position
and cannot appear in two positions simultaneously
without an explicit $\rho$-construction
that earns the second copy.
In linear logic, contraction
$\Gamma, A, A \vdash B \,/\, \Gamma, A \vdash B$
would allow using one copy of $A$
as though it were two.
Both constraints express the same principle:
duplication requires work.

\textbf{(ii) Consumption.}
In $\tau$, using a channel for a construction
(e.g., forming a product $A \times B$)
consumes both input channels:
$A$ and $B$ are no longer independently available
in the resulting object.
In linear sequent calculus,
the $\otimes$-right rule
\[
    \frac{\Gamma_1 \vdash A \qquad \Gamma_2 \vdash B}{%
    \Gamma_1, \Gamma_2 \vdash A \otimes B}
\]
splits the context:
$\Gamma_1$ is consumed for $A$
and $\Gamma_2$ for $B$,
with no sharing between them.
The context split in linear logic
mirrors the channel consumption in $\tau$.

\textbf{(iii) Finite context.}
The four orbit rays
$\alpha$, $\pi$, $\gamma$, $\eta$
bound the number of independent channels.
In the linear reading,
this is a context of size at most $4$:
any sequent in the $\tau$-linear calculus
has the form
$A_\alpha, A_\pi, A_\gamma, A_\eta \vdash C$
with at most four resources.

\textbf{(iv) Controlled reuse.}
The three rewiring levels of $\KAxiom{5}$
(Chapter~\ref{ch:diagonal-discipline})
allow controlled diagonal operations:
addition permits combining resources
within a channel,
multiplication permits iterated combination,
exponentiation permits iterated multiplication,
and tetration (the fourth level)
is capped by $\KAxiom{6}$.
Each level introduces one more layer
of structural iteration ---
analogous to nested applications of $!$
that progressively reintroduce contraction
in a controlled, bounded manner.
The solenoidal bound (three active channels,
since $4 - 1 = 3$)
ensures that the total reuse is finite.
This is a bounded $!$: not the unrestricted
exponential modality of full linear logic,
but a modality with three levels of nesting.