Polylogarithmic traversal overhead on charged native instructions

The full ternary transition budget includes skipped calls. At the existing Chan–He recursion fuel it is polylogarithmic, just as the emitted-node bound is. Combining it with the actual native visit cost gives a cubic candidate-bound term and a linear-times-candidate input term. This is a charged instruction estimate, not the finite reduction's candidate/element pair count.

Main results

• work_fuel_le: polylogarithmically many charged transitions, including zero-fuel leaves.
• visitTime_square_le: the actual visit bound is controlled by n*m + m³ up to constants.
• rootTime_fuel_square_le: the complete native root bound has polylogarithmic tree overhead.

These native resource estimates are original. Substituting the actual parameter bound and composing all frontend roots remain obligations of initialized-input preprocessing.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.work_fuel_le (n : ℕ) : Math.work (ThreeSum.ChanHe.fuel n) ≤ 3 * (2 * Nat.log 2 n + 2) ^ 5

Full-tree work counts all native pops, not just emitted mathematical instances.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.visitTime_square_le (n m : ℕ) : visitTime n m (2 * m ^ 2) ≤ 1024 * ((n + 1) * (m + 1) + (m + 1) ^ 3)

The concrete N=2m² visit cost has the desired input-times-candidate and cubic terms.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.rootTime_fuel_square_le (n card m : ℕ) : rootTime (ThreeSum.ChanHe.fuel n) card m (2 * m ^ 2) ≤ 70 + 6144 * (2 * Nat.log 2 n + 2) ^ 5 * ((card + 1) * (m + 1) + (m + 1) ^ 3)

The complete native root cost, including setup, all skipped calls and all stack/loop work, has only a polylogarithmic factor beyond card*m + m³.