This question is about Girard's system LU, presented in his paper On the unity of logic. Girard starts by giving a "modal" sequent calculus with two zones of both hypotheses and consequents, $\Gamma;\Gamma'\vdash \Delta';\Delta$, of which $\Gamma'$ and $\Delta'$ are treated classically (with contraction and weakening) and $\Gamma$ and $\Delta$ are treated linearly (without contraction and weakening). He gives rules in this calculus for the usual connectives $\otimes,\oplus,\&,⅋,\neg,\multimap,!,?,\bigwedge,\bigvee$ of classical linear logic, and explains how the result is bi-interpretable with ordinary classical linear logic. At this point it seems clear that he has just given a different presentation of the "same" classical linear logic.

Then he introduces new "chimeric" connectives $\wedge,\vee,\Rightarrow,\supset,\forall,\exists$. It appears as though each of these connectives is *defined* in terms of the linear ones, although not by a uniform definition but rather by a case analysis on whether the input formulas are "positive, negative, or neutral". For instance, $A\wedge B$ is $A\otimes B$ if $A$ and $B$ are both positive, but it is $A\& B$ if $A$ and $B$ are both negative, while if $A$ is positive and $B$ is negative then $A\wedge B$ is $A\otimes !B$, and so on. He gives explicit rules for these new connectives as well, but a brief perusal of these rules suggests to me that they are derived from the definitions of the new connectives in terms of the linear ones. Finally he considers several fragments of the resulting system that embed classical and intuitionistic nonlinear logics: classical logic uses $\wedge,\vee,\neg,\Rightarrow,\forall,\exists$ while intuitionistic logic uses $\wedge,\vee,\supset,\bigvee,\exists$.

It seems to me, therefore that LU is just a rephrasing of linear logic together with new embeddings of classical and intuitionistic logic into it that are defined by case analysis on the polarity of formulas rather than "uniformly" as the more common embeddings are. (This "just" is not meant to be disparaging; I find LU very interesting, I'm just trying to understand it better.) But Girard doesn't seem to view it this way; and moreover in Vauzeilles's proof of cut-elimination for LU it takes $3\frac12$ extra pages to extend the result to the chimeric connectives, which doesn't seem like it would be the case if they were simply defined in terms of the linear ones. So I must be missing something; what is it?