Fresh pushes for copy-on-write overlays

A productive unary push allocates a singleton private block above the existing adjacent overlay. The protected base remains shared, and its exact parking witness is transported through head normalization, head rotation, and fresh owner allocation.

theorem IndexedGrammar.Aho.overlayScheduleRun_pushFresh {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A B : g.nt} {f : g.flag} {stack : List g.flag} {w : List T} {r : IRule T g.nt g.flag} (hr : r ∈ g.rules) (hlhs : r.lhs = A) (hc : r.consume = none) (hrhs : r.rhs = [IRhsSymbol.nonterminal B (some f)]) (rest : g.NFParse B (f :: stack) w) (hone : 1 ∈ rest.eventDepths) (restOverlay : OverlayScheduleRun rest) : OverlayScheduleRun (NFParse.push hr hlhs hc hrhs rest)

Start a fresh private singleton above a nonempty adjacent overlay.