lemmaroutine
Integral local coordinates for tensor entries
Lemma·
lem:tensor-integrality·§D.4.3 A Cauchy deformation and integral local coordinatesStatement (paper)
For every , the entries of belong to
, and belongs to .
Given the coordinates of modulo , each entry
can be computed using polynomially
many bit operations in .
In plain English
For every , the entries of lie in and lies in . Given the coordinates of modulo , each entry can be computed with polynomially many bit operations in .
Why it's here
This lemma says the deformed tensor entries stay integral, so the Cauchy deformation can be carried out in the ring with arithmetic modulo . It also bounds the cost of evaluating those entries, which the Boolean tensor contraction theorem and its recursion-correctness claim need to keep the algorithm's running time under control.
Classified routine:
A technical integrality and bit-complexity check for the Cauchy-deformed tensor entries. It follows by direct computation in the ring of integers and polynomial arithmetic modulo 2^p, and it supports the paper's tensor contraction machinery without being a new idea in itself.
Uses
Nothing else in the paper
Used by
Sources
PaperOpen
- Section
- §D.4.3 A Cauchy deformation and integral local coordinates
- Page
- —
- Label
lem:tensor-integrality- Line
quantitative-contraction.tex:206
Leannot aligned
Phase 2 aligns this node to a Lean declaration.