We study the behaviour of the cut elimination in differential linear logic proof nets (without exponential boxes).

Sometimes, we want to consider parallel reduction, that fires as much cuts as wanted in the net, but doing so, we are not able to bound the loss of size in one step of reduction. We propose a method (adapted from a Lionel Vaux technique in lambda calculus) where, recovering a kind of geometric invariant in proof nets, allows us to manage this loss of size. We are then able, with well-chosen informations, to bound the size of all possible antireducts of a given net.

This result leads to others, since the notion of invariance we're dealing with can be applied to infinite sets of structures, like the Taylor expansions of nets. In this setting, we deduce from the geometrical considerations above, an interesting finiteness result having at least two nice applications : one concerning the simulation of the exponential cut-elimination in MELL; one concerning a normalization by evaluation method in connected MELL proof-nets.