Short answer

Not in the purely syntactic way you are doing it. If you insist on (i) local, constant‑time “incremental” copying that can pull a λ out across the duplicator and (ii) the usual lexical notion of scope (a binder’s variable never occurs outside its body), then the two requirements conflict. To keep closed scopes, crossing a λ must bring along its whole body at once; to keep copying incremental, you let pieces of the body remain behind and then some bound occurrences must temporarily sit outside the λ’s scope. So, with your rules as stated, you cannot have both.

What you can have instead are well‑known alternatives that keep scopes closed but change what “incremental copying” means:

• Use boxes/environments (closures), i.e., add an extra level of structure that is duplicated as a unit (linear‑logic “!” boxes, Lamping’s brackets, explicit substitutions/environments). Copying remains incremental at the level of boxes/closures, but you are not allowed to “slice through” a binder without also moving its whole body.

Why the conflict arises

Consider duplicating a term of the form λy.u where y actually occurs in u. Your incremental step wants to commute the duplicator with the λ, exposing λ twice while leaving u to be copied gradually. If you keep standard scoping as an invariant:

• Either you keep a single binder y for both copies. Then y has multiple occurrences across the two copies, violating your linearity/“O(1) substitution” premise.

• Or you split y into y0 and y1, one for each copy. Then all occurrences of y inside u must be renamed accordingly. If you do this gradually, there will be an intermediate state where some y0 or y1 occurs outside its λ, i.e., scope is broken. To avoid that, you would need one global step that simultaneously updates all occurrences of y in u, which is not constant time unless you hide u behind an indirection (a box/environment).

This is the core, representation‑independent reason: with standard lexical scope, a λ’s body is the syntactic region that must remain under the binder. If you let copying commute past the binder locally, you are forced either to extrude scope temporarily (your y0 & y1 trick) or to duplicate the entire body at once (non‑incremental).

How people keep both efficiency and scopes

Two long‑established families of solutions preserve scopes and still allow efficient, fine‑grained copying—but they do so by never slicing through a scope boundary without carrying the scope with it.

1. Boxes (linear logic) and sharing graphs. In Lamping’s algorithm and its descendants (interaction nets, optimal reduction), duplication is mediated by fans/duplicators that copy entire “!”‑boxes. The boxes delimit scopes; duplicators never push across a binder unless they copy the whole box that contains all occurrences of the bound variable. This prevents scope extrusion by construction. Copying is still incremental in the graph sense (you duplicate pointers and small nodes locally), but you cannot expose a λ outside its box without paying for moving its body with it. References: Lamping (1990), Lafont (interaction nets), Asperti–Guerrini “The Optimal Implementation of Functional Programming Languages.”

2. Explicit substitutions and closures (environments). Calculi like the λσ‑calculus, Curien’s calculus of closures, or the linear substitution calculus keep binders closed by representing “the rest” of the binding as an explicit environment. Duplicating a term duplicates a pointer to a closure/environment (constant time), and λ can be “pulled” out in the syntax while the bound occurrences remain captured by the environment. No variable ever occurs outside its scope because scope is represented by the environment object. Eventually realizing the duplication inside the closure may take time proportional to the body, but the local steps are constant time.

What this means for your calculus

• If you keep your local rule that commutes copying with λ by renaming the bound variable into y0 & y1, then during the incremental process you will have bound names occurring outside their original λ. That is exactly the “loss of scopes” you observed, and there’s no way around it with those rules.

• If you want closed scopes as an invariant, you need a mechanism that prevents slicing through binders: either forbid that commuting step (only duplicate at scope boundaries), or wrap the λ’s body in a box/environment so that any duplication that crosses the λ carries the body with it.

• You can still get O(1) local steps and incremental duplication at the level of boxes/environments, but you cannot both (a) expose a λ earlier than its body and (b) maintain lexical scoping, without an additional indirection.

In short: with the usual, purely syntactic notion of scope, local constant‑time “incremental copying” that pulls a λ out past a duplicator forces scope extrusion. To have both efficient incremental behavior and closed scopes, you need to adopt boxes/environments (interaction‑net boxes, explicit substitutions/closures) and restrict duplication to respect those scope boundaries.