  We introduce $\mathsf{LEM}$, a type-assignment system for the linear $
\lambda $-calculus that extends second-order $\mathsf{IMLL}_2$, i.e.,
intuitionistic multiplicative Linear Logic, by means of logical rules that
weaken and contract assumptions, but in a purely linear setting. $\mathsf{LEM}$
enjoys both a mildly weakened cut-elimination, whose computational cost is
cubic, and Subject reduction. A translation of $\mathsf{LEM}$ into
$\mathsf{IMLL}_2$ exists such that the derivations of the former can
exponentially compress the dimension of the derivations in the latter.
$\mathsf{LEM}$ allows for a modular and compact representation of boolean
circuits, directly encoding the fan-out nodes, by contraction, and disposing
garbage, by weakening. It can also represent natural numbers with terms very
close to standard Church numerals which, moreover, apply to Hereditarily Finite
Permutations, i.e. a group structure that exists inside the linear $ \lambda
$-calculus.
