Exact emissions from the complete native traversal visit

This packages the executed modulus and node calls into the worklist's semantic entry format. The heavy lists are witnesses to actual native memory, not program inputs or advice. The old prefix survives before the single output-pointer store, and every new packed cell equals the existing finite node array.

Main definitions

• Emission: exact metadata, old-prefix frame and heavy/packed readback of an actual live visit.

Main results

• emit_entry: the complete native visit produces an exact emission with its charged bound.

These native composition proofs are original.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Emission (Q : Finset ℕ) (Λ : ℕ) (e : Entry) (x y : WordRAM.Data 128) : Type

Semantic readback of one completed actual native visit.

• M : ℕ

  The actual selected unsigned modulus.

• exactModulus : self.M = (Math.Task.node Q Λ e.task).M

  Selection agrees with the existing finite node.

• positive : 1 ≤ self.M

  The native fallback is positive.

• upper : self.M ≤ x.regs limit ^ 2

  Both selected candidates lie within the supplied bound.

• lists : Fin 3 → List ℤ

  Actual native compact heavy enumerations.

• nodup (j : Fin 3) : (self.lists j).Nodup

  Each enumeration is duplicate-free.

• sets (j : Fin 3) : (self.lists j).toFinset = ThreeSum.ChanHe.heavy (e.task.sets j) self.M

  The enumerated sets are exactly the existing heavy subsets.

• length_le (j : Fin 3) : (self.lists j).length ≤ (e.data j).length

  A heavy enumeration never exceeds its parent column.

• lengths (j : Fin 3) : y.regs (heavyLength j) = (self.lists j).length

  The delivered unsigned lengths describe these actual lists.

• bases (j : Fin 3) : y.regs (heavyBase j) = (recordLayout x self.M).heavy j

  The delivered unsigned bases are the concrete heavy-array bases.

• heavy (j : Fin 3) : { base := (recordLayout x self.M).heavy j, length := (self.lists j).length }.Realizes y.mem fun (i : Fin { base := (recordLayout x self.M).heavy j, length := (self.lists j).length }.length) => WordRAM.Signed.encode (self.lists j)[↑i]

  Exact signed-encoded heavy-array readback.

• packed : { base := (recordLayout x self.M).packed, length := 4 * x.regs groups }.Realizes y.mem fun (i : Fin { base := (recordLayout x self.M).packed, length := 4 * x.regs groups }.length) => WordRAM.Signed.encode ((Math.Task.node Q Λ e.task).oneArray (x.regs magnitude) ↑i)

  Exact signed-encoded packed-node readback.

• count : y.regs outputCount = x.regs outputCount + 1

  The actual count increment.

• heap_eq : y.regs heap = (recordLayout x self.M).endpoint

  The actual advanced allocation frontier.

• before : ℕ → ℕ

  The complete node output before its single external pointer-table store.

• prefixMemory (p : ℕ) : p < x.regs heap → self.before p = x.mem p

  The two actual modulus searches and the node call preserve every old prefix cell.

• memory : y.mem = Function.update self.before (x.regs outputs + x.regs outputCount) (recordLayout x self.M).packed

  The sole pointer-table store is an actual native memory update.

• registers (i : Fin 128) : 64 ≤ ↑i → i ≠ selected → i ≠ heap → i ≠ outputCount → i ≠ temporary → ↑i < 88 ∨ 96 ≤ ↑i → y.regs i = x.regs i

  The current record, persistent controller parameters and stack dispatcher survive.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.emit_entry {w n : ℕ} (x : WordRAM.Data 128) (e : Entry) (hl : e.Loaded x) (hv : e.Valid n (x.regs magnitude)) (hs : e.Stored x.mem) (hm : 2 ≤ x.regs limit) (hmod : GenericRAM.Signed.Fits w ↑(x.regs limit ^ 2)) (hbudget : WordRAM.Fits (w + 2) (Modulus.budget (WordRAM.Data.comap kernel (modulusState x)))) (hnode : ∀ (M : ℕ), 1 ≤ M → M ≤ x.regs limit ^ 2 → GenericRAM.Signed.Fits w ↑(recordLayout x M).budget) (hN : 2 * x.regs limit ^ 2 ≤ x.regs groups) (hcard : x.regs primeCount = (x.regs limit).primesLE.card) (hbefore : x.regs bitmap + x.regs limit < x.regs heap) (hbitmap : ∀ q ≤ x.regs limit, x.mem (x.regs bitmap + q) = if Nat.Prime q then 1 else 0) (hvalues : ∀ (j : Fin 3), ∀ i < (e.data j).length, GenericRAM.Signed.Fits w (e.read j i)) (hsrc : ∀ (j : Fin 3), e.source j + (e.data j).length ≤ x.regs heap) (hone : x.regs one = 1) (htable : x.regs outputs + x.regs outputCount < x.regs heap) : ∃ (y : WordRAM.Data 128), WordRAM.ExecWithin (w + 2) visit x y (visitTime n (x.regs limit) (x.regs groups)) ∧ Nonempty (Emission (x.regs limit).primesLE (x.regs digits) e x y)

Execute both complete searches and the complete node construction for an actual loaded entry. All heavy witnesses come from the executed memory and all control work is charged.