lemmaroutine

Row coefficients are bounded and constructible

Lemma·lem:row-coefficients·§4.6 Coefficient bounds and the completed construction

Statement (paper)

Let dden=(R−1)!Q!d_{\mathrm{den}}=(R-1)!Q!. Then ddenP⃗u(T)∈Z[T]1×Dd_{\mathrm{den}}\vec{P}_u(T)\in\mathbb Z[T]^{1\times D} for every u∈Bu\in\mathcal B. The sum of the absolute values of all coefficients in each row ddenP⃗u(T)d_{\mathrm{den}}\vec{P}_u(T) is at most 2O(Qlog⁡Q)2^{O(Q\log Q)}. The same bound holds for ddenP⃗f,v(T)d_{\mathrm{den}}\vec{P}_{f,v}(T). The matrices M0,CBM_0,C^{\mathcal B} and the rows P⃗u(T)\vec{P}_u(T) can be constructed in poly⁡(D,Q,r)\poly(D,Q,r) bit operations.

In plain English

With dden=(R−1)!Q!d_{\mathrm{den}}=(R-1)!Q!, the scaled rows ddenP⃗u(T)d_{\mathrm{den}}\vec{P}_u(T) (and ddenP⃗f,v(T)d_{\mathrm{den}}\vec{P}_{f,v}(T)) have integer polynomial entries whose coefficients have absolute sum at most 2O(Qlog⁡Q)2^{O(Q\log Q)} in each row. The matrices M0M_0, CBC^{\mathcal B} and the rows P⃗u(T)\vec{P}_u(T) can be built in poly⁡(D,Q,r)\poly(D,Q,r) bit operations.

Why it's here

This lemma clears denominators with a single factor ddend_{\mathrm{den}} and shows the resulting integer coefficients stay of size 2O(Qlog⁡Q)2^{O(Q\log Q)}, so the rows can be used as bounded-weight integer constraints in the completed construction. It also certifies that the construction, including the swap matrix CBC^{\mathcal B} from the swaps-matrix lemma, is efficiently computable, which later layout and counting results rely on.
Classified routine:
The proof clears denominators with a single factorial factor and bounds the coefficient sizes by direct bookkeeping on factorial and binomial magnitudes. Constructibility follows from explicit polynomial-time linear algebra over the rows, given the earlier swap-matrix lemma.

Uses

lemSwap matrix with few rows fixes M_0

Used by

lemLayout data is efficiently constructiblepropCost of counting solutions via factor evaluation

Sources

PaperOpen
Section
§4.6 Coefficient bounds and the completed construction
Page
—
Label
lem:row-coefficients
Line
main_full_version.tex:2635
Leannot aligned

Phase 2 aligns this node to a Lean declaration.