lemmaroutine

Polynomial rows vanish on off-block vectors

Lemma·lem:swaps-forms·§4.3 The polynomial rows

Statement (paper)

The rows in have degree at most R−1R-1 and satisfy P⃗u(0)=δu\vec{P}_u(0)=\delta_u for every u∈Bu\in\mathcal B. For t∈[Q]t\in[Q] and g∈[r]g\in[r], let Ct,gBC^{\mathcal B}_{t,g} be the restriction of CBC^{\mathcal B} to the columns St,gBS^{\mathcal B}_{t,g}. For every u,t,gu,t,g with g≠du(t)g\ne d_u(t) and every ξ∈QSt,gB\xi\in\mathbb Q^{S^{\mathcal B}_{t,g}}, its extension ξ~\widetilde\xi by zero to B\mathcal B satisfies Ct,gBξ=0⃗⟹⟨P⃗u(t),ξ~⟩=0. C^{\mathcal B}_{t,g}\xi=\vec{0} \quad\Longrightarrow\quad \langle \vec{P}_u(t), \widetilde\xi\rangle=0. More generally, ⟨P⃗u(t),ζ⟩\langle \vec{P}_u(t), \zeta\rangle is determined by ζ∣St,du(t)B\zeta|_{S^{\mathcal B}_{t,d_u(t)}} and CBζC^{\mathcal B}\zeta.

In plain English

The polynomial rows P⃗u\vec{P}_u have degree at most R−1R-1 and satisfy P⃗u(0)=δu\vec{P}_u(0)=\delta_u. For g≠du(t)g\ne d_u(t), any ξ\xi supported on the columns St,gBS^{\mathcal B}_{t,g} with Ct,gBξ=0C^{\mathcal B}_{t,g}\xi=0 satisfies ⟨P⃗u(t),ξ~⟩=0\langle \vec{P}_u(t),\widetilde\xi\rangle=0. More generally, ⟨P⃗u(t),ζ⟩\langle \vec{P}_u(t),\zeta\rangle depends only on ζ\zeta restricted to St,du(t)BS^{\mathcal B}_{t,d_u(t)} and on CBζC^{\mathcal B}\zeta.

Why it's here

This gives the structural properties of the rows that the later steps rely on: low degree, the correct value at 00, and the fact that at point tt a row sees only the block du(t)d_u(t) plus the constraint values from CBC^{\mathcal B}. This is what lets the constraint matrix from Lemma 4.1 control the evaluations of the rows, with the kernel condition on CBC^{\mathcal B} serving as the only information needed from the other blocks.
Classified routine:
This lemma checks properties of the explicitly defined rows in eq:swaps-row: degree bounds, the value at 0, and that each evaluation sees only one block plus the constraint values. These follow directly from the construction together with the swap matrix of Lemma 4.1, so it is bookkeeping rather than a new idea.

Uses

lemSwap matrix with few rows fixes M_0

Used by

lemLayout data is efficiently constructible

Sources

PaperOpen
Section
§4.3 The polynomial rows
Page
—
Label
lem:swaps-forms
Line
main_full_version.tex:2333
Leannot aligned

Phase 2 aligns this node to a Lean declaration.