ch:soft-linear-logic: ch:soft-linear-logic

Use two identities $A⊢A$, combine their disjoint contexts with tensor introduction to obtain $A,A⊢A\otimes A$, and apply rank-$2$ multiplexing to conclude $!A⊢A\otimes A$. For the additive formula, apply rank-$1$ multiplexing separately to two copies of the identity derivation, obtaining two derivations of $!A⊢A$; additive conjunction introduction reuses that same context and concludes . Rank $0$ exposes no copy and therefore acts as weakening.

First . Boxing gives , which evaluates to $17$ at rank $2$. Its degree is one more than the larger degree of $u$ and $v$.

At rank $2$, the family has bounds $k_m{2}^m$. Since the exponent $m$ grows with the encoded net, no fixed-degree polynomial covers the family by the corollary. The changed hypothesis is that $u$, and hence its degree, was fixed.

The degrees are $2$ and $3$, so the representation sequent is ${\mathsf{S}}^{(6)}⊢\mathsf{B}$: it has six string assumptions. Coefficients change how many fixed transition components are composed; the number of antecedent copies records polynomial degrees, not coefficients.

Licensed: a fixed rank-$n$ net $u$ normalizes in at most $W_u(n)$ external steps. Not licensed: a source function on a numeric input $x$ runs in at most $3x+2$ steps because its type carries that potential. The first quantity is proof-net weight at rank; the second would be input-indexed operational cost.

Under the mutated equation, $$W_{!v}^{\mathsf{m}}(3)=W_v(3)+1=4,W_{!!v}^{\mathsf{m}}(3)=W_{!v}^{\mathsf{m}}(3)+1=5.$$ Opening the outer box may create three copies of $!v$, whose combined mutated weight is . The missing factor of $X$ was the charge for multiplexing.

Rank $0$ exposes no copy of $A$, rank $1$ exposes one, and rank $2$ exposes two, giving weakening, dereliction, and binary contraction behavior. Each rule removes one $!A$ on the left; none derives $!!A$ from $!A$, which would be digging.

A principal multiplicative interaction removes at least one right-logical cell of weight $1$, while left cells have weight $0$. For an exponential cut against rank $q\le n$, the redex charge is $n{W}_w(n)+1$ and the copies cost at most $q{W}_w(n)$; the decrease is at least one. Commuting independent cells does not change either calculation.

A fixed degree-$3$ net has bound $k{n}^3$ as rank $n$ varies. A family with degree equal to input length has a bound of the form $k_n{n}^n$, with changing coefficient and exponent; the fixed-program hypothesis needed for one polynomial is absent.

Linear time has degree $1$ and constant space degree $0$, so the theorem gives ${\mathsf{S}}^{(2)}⊢\mathsf{B}$. The construction needs a string encoding, length iterator, fixed transition net, constant-size tape/state encoding, iteration composition, and accepting-state Boolean observation.