lemmaroutinestructure_uncertain
Tensor network edges packed into packets
Lemma·
lem:tensor-packets·§D.4.2 Parameters and collision packingStatement (paper)
Under , label the vertices on
each side of the network by elements of . There is a
deterministically constructible labeling and an embedding of the
edges into packets of slots with the following properties.
\begin{enumerate}
\item There are at most packets. Each edge occupies the same
slot at its row and column ends. Unused slots have no ports.
\item In every packet and every coordinate, the unordered pair of
row and column symbols is fixed. When these symbols differ,
bit of the slot number specifies their orientation in
coordinate , for .
\item For every coordinate and every symbol, at most real
ports on each side belong to vertices with that symbol.
\end{enumerate}
The construction uses polynomial time and space in .
In plain English
Under the tensor-packing conditions, vertices on each side are labeled by elements of , and the edges can be embedded deterministically into at most packets of slots. Each edge uses the same slot at both ends, and in each packet and coordinate the row/column symbol pair is fixed, with slot bit giving the orientation when the symbols differ. For each coordinate and symbol, at most real ports on each side belong to vertices carrying that symbol.
Why it's here
This lemma gives the network a regular, packet-based layout whose slot numbers encode the orientation of each coordinate, so the later recursive contraction can handle many edges at once. The balanced port bound per symbol keeps the load even across coordinates, and the polynomial-time construction is what the recursion-count claim relies on.
Classified routine:
A technical combinatorial packing and labeling construction in an appendix, built from balanced-partition and counting arguments of the kind used for packing bipartite edges into structured blocks. It supports the paper's recursive tensor contraction rather than being one of its headline ideas.
Uses
Nothing else in the paper
Used by
Sources
PaperOpen
- Section
- §D.4.2 Parameters and collision packing
- Page
- —
- Label
lem:tensor-packets- Line
quantitative-contraction.tex:114
Leannot aligned
Phase 2 aligns this node to a Lean declaration.
Friction
- infostructure_uncertainUsed in prose (child edge bound at quantitative-contraction.tex:525) outside any proof environment; the skeleton records no ref edge to it.