Atomic pop for copy-on-write overlays

An event-free private head is erased by the existing adjacent pop certificate. If another private block is exposed, execution stays in overlay mode; only an empty private tail returns to the marker-aware protected/plain modes.

theorem IndexedGrammar.Aho.overlayScheduleRun_atomicPop {T : Type} {g : IndexedGrammar T} [Fintype g.nt] {A : g.nt} {stack : List g.flag} {w : List T} (parse : g.NFParse A stack w) (hpositive : ∀ d ∈ parse.eventDepths, 0 < d) (ordinaryIH : ∀ {B : g.nt} {residualStack : List g.flag} (residual : g.NFParse B residualStack w), residual.nodeCount < parse.nodeCount → OrdinaryScheduleRuns residual) (overlayIH : ∀ {B : g.nt} {residualStack : List g.flag} (residual : g.NFParse B residualStack w), residual.nodeCount < parse.nodeCount → OverlayScheduleRun residual) : OverlayScheduleRun parse

Execute and erase the first private overlay block when it contains no productive event.

The marker-aware ordinary mutual hypothesis handles the singleton/base case. The overlay hypothesis is used only after a pop exposes another branch-local block.