%
\label{def:program-linear-calculus}
The \textbf{program monoid as linear calculus}
reinterprets the program monoid
(Definition~\ref{def:program-monoid}, I.D14)
as a linear sequent calculus:
\begin{enumerate}
    \item \textbf{Programs = linear proofs.}
          Each program $P = (i_1, \ldots, i_n)$
          in the program monoid
          is a linear derivation:
          every instruction consumes its input channel
          and produces an output,
          with no instruction reusing a channel
          that has already been consumed.
    \item \textbf{Concatenation = cut rule.}
          The monoid operation
          $P \cdot Q = (i_1, \ldots, i_m, j_1, \ldots, j_n)$
          corresponds to the cut rule of sequent calculus:
          \[
              \frac{\Gamma \vdash A \qquad A, \Delta \vdash B}{%
              \Gamma, \Delta \vdash B}
              \quad\text{(cut)}
          \]
          The conclusion of $P$ (the resource $A$)
          becomes the premise of $Q$.
          The cut connects one proof's output
          to another's input.
    \item \textbf{NF-Confluence = cut-elimination.}
          The NF-Confluence Lemma
          (Lemma~\ref{lem:nf-confluence}, I.L02)
          states: any two reduction paths to normal form
          yield the same result.
          Gentzen's cut-elimination theorem
          (the \emph{Hauptsatz}, 1935) states:
          any proof with cuts
          can be transformed to a cut-free proof,
          and the result is unique
          up to inessential permutations.
          The parallel is exact:
          normal forms in the program monoid
          correspond to cut-free proofs
          in the linear sequent calculus.
    \item \textbf{Four channels = linear context zones.}
          The four orbit rays
          ($\alpha$, $\pi$, $\gamma$, $\eta$)
          partition the linear context
          into four zones,
          each carrying one resource type.
\end{enumerate}