A bounded worklist for the exact Chan–He recursion

The worklist expands the existing ChanHe.nodes in its existing preorder. Empty triples and zero fuel are popped without emitting an instance. Three children replace one set each by its existing heavy subset, in the order used by the finite reduction.

This is the mathematical invariant for the native traversal, not a native execution contract. In particular, expanding a worklist entry here does not discharge a native modulus or node call. The stack bound counts pending entries, including empty and zero-fuel entries. Those entries still require charged native pop and branch instructions.

Main definitions

• Task: one pending three-set call, including its remaining fuel.
• step: one exact worklist transition and its optional emitted node.
• potential: a natural-valued bound on all remaining transitions, including skipped entries.
• Bounded: a stack-depth invariant giving at most 2f+1 pending entries for root fuel f.

Main results

• output_step: one transition preserves the exact preorder output.
• potential_step: every transition strictly decreases the charged-transition bound.
• bounded_step, Bounded.length_le: the explicit stack has linear capacity in root fuel.

These worklist invariants are original. They reuse the finite recursion of [CH20].

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.Task : Type

One pending call of the existing finite recursion.

• fuel : ℕ

  Remaining recursion levels.

• sets : Fin 3 → Finset ℤ

  The three mathematical sets represented by the native descriptor.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.Task.output (Q : Finset ℕ) (Λ : ℕ) (t : Task) : List ThreeSum.ChanHe.Node

The exact existing preorder associated with one pending call.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.Task.node (Q : Finset ℕ) (Λ : ℕ) (t : Task) : ThreeSum.ChanHe.Node

The exact existing modulus and three sets of a nonempty call.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.Task.empty (t : Task) : Prop

Whether a call is skipped because one of its sets is empty.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.Task.children (Q : Finset ℕ) (Λ f : ℕ) (t : Task) : List Task

The three children, with exactly the mathematical reduction's order and heavy sets.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.output (Q : Finset ℕ) (Λ : ℕ) (ts : List Task) : List ThreeSum.ChanHe.Node

The sequence still to be emitted from a top-first worklist.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.step (Q : Finset ℕ) (Λ : ℕ) (t : Task) (ts : List Task) : List Task × Option ThreeSum.ChanHe.Node

One pop, followed either by a skip or by one emission and three children.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.output_step (Q : Finset ℕ) (Λ : ℕ) (t : Task) (ts : List Task) : output Q Λ (t :: ts) = (step Q Λ t ts).2.toList ++ output Q Λ (step Q Λ t ts).1

One worklist transition preserves the exact output list, including order and skipped calls.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.work : ℕ → ℕ

Number of transitions for the full ternary tree, counting its zero-fuel leaves.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.work_pos (f : ℕ) : 1 ≤ work f

Every pending entry costs at least one pop/skip transition.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.work_eq (f : ℕ) : 2 * work f + 1 = 3 ^ (f + 1)

Closed form without a truncated quotient.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.potential (ts : List Task) : ℕ

The sum of the transition budgets of all pending entries.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.potential_step (Q : Finset ℕ) (Λ : ℕ) (t : Task) (ts : List Task) : potential (step Q Λ t ts).1 + 1 ≤ potential (t :: ts)

One transition spends at least one unit, including the empty and zero-fuel cases.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.Bounded (f : ℕ) : List Task → Prop

Each entry's fuel plus the pending suffix gives a bound measured from the stack bottom.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.bounded_singleton (t : Task) : Bounded t.fuel [t]

A single root of fuel f satisfies the stack invariant.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.Bounded.length_le {f : ℕ} {ts : List Task} (h : Bounded f ts) : ts.length ≤ 2 * f + 1

The explicit stack requires at most 2f+1 entries, even with zero-fuel entries present.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Math.bounded_step {f : ℕ} (Q : Finset ℕ) (Λ : ℕ) (t : Task) (ts : List Task) (h : Bounded f (t :: ts)) : Bounded f (step Q Λ t ts).1

A native pop/skip or three-child push preserves the same fixed stack capacity.