claimroutineinferred_dep

Total number of recursive calls

Claim·§D.4.7 Time and space bounds·inside thmSubexponential Boolean tensor network contraction

Statement (paper)

The recursive algorithm makes at most exp⁡(OC(s/λ)+OC(λlog⁡λ))=exp⁡(OC(s/λ))\exp\left(O_C(s/\sqrt\lambda)+O_C(\lambda\log\lambda)\right)=\exp\left(O_C(s/\sqrt\lambda)\right) calls in total, where each active call at depth dd has at most sO(1)exp⁡(OC(sλ(28)d))s^{O(1)}\exp\left(O_C\left(\frac{s}{\sqrt\lambda}\left(\frac{\sqrt2}{8}\right)^d\right)\right) children, and the number of interpolation nodes, values, and groups at a call is polynomial in ss, independently of L\mathcal L.

In plain English

The recursive contraction algorithm makes at most exp⁡(OC(s/λ))\exp(O_C(s/\sqrt\lambda)) calls in total, since an active call at depth dd has at most sO(1)exp⁡(OC((s/λ)(2/8)d))s^{O(1)}\exp(O_C((s/\sqrt\lambda)(\sqrt2/8)^d)) children. The number of interpolation nodes, values, and groups at each call is polynomial in ss, independent of L\mathcal L.

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 F(0)F(0) keep the per-call fan-out and the number of interpolation data polynomial. The geometric factor (2/8)d(\sqrt2/8)^d makes the total over depths a single exp⁡(OC(s/λ))\exp(O_C(s/\sqrt\lambda)), and the OC(λlog⁡λ)O_C(\lambda\log\lambda) 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 (2/8)d(\sqrt2/8)^d is standard bookkeeping.

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

  • info
    inferred_dep
    outline: "Total number of recursive calls" rests on lem:tensor-packets
  • info
    inferred_dep
    outline: "Total number of recursive calls" rests on lem:tapered-hermite