Complete live transitions of the native Chan–He worklist

One transition executes the seven pops, both complete modulus searches, all three actual histogram/packing calls, output delivery and the three reversed child pushes. Its invariant preserves exact existing-node output, live arrays, the actual prime bitmap, and the space reservations paid for by the strictly decreasing work measure.

Main results

• live_transition: complete actual native body execution and full invariant preservation.

These native composition and invariant proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.live_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) (hw : a.Ready w) (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) (hf : e.fuel ≠ 0) (hn : ∀ (j : Fin 3), (e.data j).length ≠ 0) : ∃ (s : Cursor) (y : WordRAM.Data 128), WordRAM.ExecWithin (w + 2) body x y (visitTime a.n a.m a.N + 314) ∧ Cursor.Invariant a w target s y ∧ s.work < { pending := e :: es, emitted := ns }.work

Execute and verify the whole live native worklist transition.