claimroutineinferred_dep
Total number of recursive calls
Statement (paper)
The recursive algorithm makes at most calls in total, where each active call at depth has at most children, and the number of interpolation nodes, values, and groups at a call is polynomial in , independently of .
In plain English
The recursive contraction algorithm makes at most calls in total, since an active call at depth has at most children. The number of interpolation nodes, values, and groups at each call is polynomial in , independent of .
Why it's here
This bounds the size of the recursion tree, which the leaf-cost and overall time bound builds on. The packet layout from the tensor-packets lemma and the tapered Hermite recovery of keep the per-call fan-out and the number of interpolation data polynomial. The geometric factor makes the total over depths a single , and the term is absorbed into it.
Classified routine:
This counts the calls in the recursion tree. The per-call fan-out bounds come from the earlier tensor-packets and tapered-Hermite lemmas, and the geometric sum over depths with ratio is standard bookkeeping.
Uses
Used by
Sources
PaperOpen
- Section
- §D.4.7 Time and space bounds
- Page
- —
- Label
—- Line
quantitative-contraction.tex:571
Leannot aligned
Phase 2 aligns this node to a Lean declaration.
Friction
- infoinferred_depoutline: "Total number of recursive calls" rests on lem:tensor-packets
- infoinferred_depoutline: "Total number of recursive calls" rests on lem:tapered-hermite