claimroutine

Recursive contraction algorithm is correct

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

Statement (paper)

The recursive algorithm, run on the original entries embedded into

\mathcal A_{P_0}

, is correct: at every call (active call or leaf) it returns the contraction of the tensor network assigned to that call, and in particular the top-level call returns the contraction of the original network. This holds by induction from the leaves, using Lemma , the recursion identity , and the recovery lemma (Lemma ).

In plain English

Run on the original entries embedded into

\mathcal A_{P_0}

, the recursive algorithm returns, at every call (active or leaf), the contraction of the tensor network assigned to that call. In particular the top-level call returns the contraction of the original network.

Why it's here

This is the correctness half of the proof of the tensor contraction theorem, shown by induction from the leaves. At each active call, Lemma D.4 makes the deformed entries integral so the sub-calls are legitimate, the recursion identity expresses the contraction through them, and the tapered Hermite recovery lemma extracts

F(0)

from the returned values at the points of

S

Classified routine:

A direct induction from the leaves that combines the paper's earlier lemmas: integrality (Lemma D.4), the recursion identity, and tapered Hermite recovery. It is bookkeeping for the correctness half of the theorem's proof and adds no new idea.

Uses

lemTapered Hermite recovery of F(0)lemIntegral local coordinates for tensor entries

Used by

Nothing in the paper

Sources

PaperOpen

Section: §D.4.7 Time and space bounds
Page: —
Label: —
Line: quantitative-contraction.tex:561

Leannot aligned

Phase 2 aligns this node to a Lean declaration.