Exact memory output of native Chan–He traversal

The pointer table is an unsigned word list. Each pointed-to block contains the existing Node.oneArray, encoded with the signed integer encoding, at the common finite length 4N. This reuses the generic block/list realization API and introduces no alternative convolution predicate or execution model.

Main definitions

• StoredNodes: exact pointer-table and packed-array readback for the emitted preorder.

Main results

• StoredNodes.congr: transfer exact readback along a frame on its live cells.
• StoredNodes.append: one actual pointer-table store appends a represented native node.

The concrete output invariant and proofs are original.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.StoredNodes (U N table : ℕ) (ns : List (ℕ × ThreeSum.ChanHe.Node)) (mem : ℕ → ℕ) : Prop

The exact finite output table and its signed-encoded packed node arrays.

• pointers : WordRAM.Block.HoldsList table (List.map Prod.fst ns) mem

  The table contains exactly the native base pointers in emitted order.

• cells (i : Fin ns.length) : { base := ns[↑i].1, length := 4 * N }.Realizes mem fun (u : Fin { base := ns[↑i].1, length := 4 * N }.length) => WordRAM.Signed.encode (ns[↑i].2.oneArray U ↑u)

  Every pointed-to word equals the existing mathematical packed array cell.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.storedNodes_nil (U N table : ℕ) (mem : ℕ → ℕ) : StoredNodes U N table [] mem

Empty traversal output imposes no pointed-to array obligations.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.StoredNodes.congr {U N table : ℕ} {ns : List (ℕ × ThreeSum.ChanHe.Node)} {before after : ℕ → ℕ} (h : StoredNodes U N table ns before) (ht : ∀ (a : ℕ), table ≤ a → a < table + ns.length → after a = before a) (hc : ∀ (i : Fin ns.length), ∀ u < 4 * N, after (ns[↑i].1 + u) = before (ns[↑i].1 + u)) : StoredNodes U N table ns after

Pointer-table and packed-array readback survive a frame on all their live cells.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.StoredNodes.append {U N table p : ℕ} {ν : ThreeSum.ChanHe.Node} {ns : List (ℕ × ThreeSum.ChanHe.Node)} {mem : ℕ → ℕ} (h : StoredNodes U N table ns mem) (hnew : { base := p, length := 4 * N }.Realizes mem fun (u : Fin { base := p, length := 4 * N }.length) => WordRAM.Signed.encode (ν.oneArray U ↑u)) (hold : ∀ (i : Fin ns.length), table + ns.length < ns[↑i].1) (hp : table + ns.length < p) : StoredNodes U N table (ns ++ [(p, ν)]) (Function.update mem (table + ns.length) p)

Appending one native pointer preserves all packed readback. The stored pointer lies below both the old arrays and the fresh array, so the actual store cannot overwrite array data.