lemmaroutine

Integral local coordinates for tensor entries

Lemma·lem:tensor-integrality·§D.4.3 A Cauchy deformation and integral local coordinates

Statement (paper)

For every t∈St\in S, the entries of W(t+αz)W(t+\alpha z) belong to O[z]\mathcal O[z], and F(t+αz)F(t+\alpha z) belongs to A[z]\mathcal A[z]. Given the ee coordinates of ζ\zeta modulo 2p2^p, each entry Wxy(t+αζ) mod 2pW_{xy}(t+\alpha\zeta)\bmod 2^p can be computed using polynomially many bit operations in s,ps,p.

In plain English

For every t∈St\in S, the entries of W(t+αz)W(t+\alpha z) lie in O[z]\mathcal O[z] and F(t+αz)F(t+\alpha z) lies in A[z]\mathcal A[z]. Given the ee coordinates of ζ\zeta modulo 2p2^p, each entry Wxy(t+αζ) mod 2pW_{xy}(t+\alpha\zeta)\bmod 2^p can be computed with polynomially many bit operations in s,ps,p.

Why it's here

This lemma says the deformed tensor entries stay integral, so the Cauchy deformation can be carried out in the ring A[z]\mathcal A[z] with arithmetic modulo 2p2^p. 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.

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.