claimroutineinferred_dep

Leaf cost and total running time bound

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

Statement (paper)

Each leaf, which uses direct summation over at most 2H2^H assignments with polynomially many entry evaluations per assignment, costs at most a polynomial in s+Ls+\mathcal L times exp⁡(OC(H)+OC,A(s9/10))=exp⁡(OC,A(s/λ))\exp(O_C(H)+O_{C,A}(s^{9/10}))=\exp(O_{C,A}(s/\sqrt\lambda)). Since the total number of calls is at most exp⁡(OC(s/λ))\exp(O_C(s/\sqrt\lambda)) independently of L\mathcal L, and the work per call, including local arithmetic, packing, descriptions, recovery and entry computations, is bounded by a fixed polynomial in s+Ls+\mathcal L times the leaf factor, the total running time is at most (s+L)O(1)exp⁡(OC,A(s/λ))(s+\mathcal L)^{O(1)}\exp(O_{C,A}(s/\sqrt\lambda)).

In plain English

Each leaf of the recursion is computed by direct summation over at most 2H2^H assignments and costs a polynomial in s+Ls+\mathcal L times exp⁡(OC,A(s/λ))\exp(O_{C,A}(s/\sqrt\lambda)). Combined with the bound on the number of recursive calls, the total running time is (s+L)O(1)exp⁡(OC,A(s/λ))(s+\mathcal L)^{O(1)}\exp(O_{C,A}(s/\sqrt\lambda)).

Why it's here

This finishes the time analysis of the theorem. The leaf work (at most 2H2^H assignments, each needing polynomially many entry evaluations at cost 2O(s9/10)2^{O(s^{9/10})}) is subexponential at the scale s/λs/\sqrt\lambda, and the call-count bound from the previous claim is independent of L\mathcal L. Multiplying the number of calls by the per-call cost, which is polynomial in s+Ls+\mathcal L times the leaf factor, gives the stated bound.
Classified routine:
Direct bookkeeping: multiplies the call-count bound from claim-thm-tensor-contraction-2 by the per-call cost of brute-force summation over at most 2^H leaf assignments, a standard running-time analysis of a recursive algorithm.

Uses

claimTotal number of recursive calls

Used by

Nothing in the paper

Sources

PaperOpen
Section
§D.4.7 Time and space bounds
Page
—
Label
—
Line
quantitative-contraction.tex:589
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Leaf cost and overall time bound" rests on claim-thm-tensor-contraction-2