Complete skipped transitions of the native worklist

Zero-fuel and empty entries still execute the seven native pops and their actual branch paths. The remaining arrays, bitmap and previously emitted packed output retain exact readback. Both space reservations improve because the transition measure decreases without allocation.

Main results

• skip_transition: the actual native body preserves the full worklist invariant on every skipped entry and strictly decreases its remaining charged-transition measure.

These native composition and invariant proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.skip_transition {a : Arena} {w : ℕ} {target : List ThreeSum.ChanHe.Node} (e : Entry) (es : List Entry) (ns : List (ℕ × ThreeSum.ChanHe.Node)) (x : WordRAM.Data 128) (ha : a.Separated) (h2 : WordRAM.Fits (w + 2) 2) (hcap : WordRAM.Fits (w + 2) (a.stack + a.capacity)) (h : Cursor.Invariant a w target { pending := e :: es, emitted := ns } x) (hskip : e.fuel = 0 ∨ (e.data 0).length = 0 ∨ (e.data 1).length = 0 ∨ (e.data 2).length = 0) : ∃ (y : WordRAM.Data 128), WordRAM.ExecWithin (w + 2) body x y 107 ∧ Cursor.Invariant a w target { pending := es, emitted := ns } y ∧ { pending := es, emitted := ns }.work < { pending := e :: es, emitted := ns }.work

Popping a skipped entry executes the complete native body and preserves every part of the worklist invariant, including exact output, all live memory and concrete space reservations.