claimroutine

Numerical checks with exhaustive fallback

Claim·§5.5 Constructing the forms and completing the proof·inside thmCounting zeros of sparse polynomials faster

Statement (paper)

The algorithm can verify, using exact integer arithmetic, all numerical hypotheses required by the construction (the preliminary guards, 2(b+w)D2⩽M′2(b+w)D^2\le M', 2Qr2⩽n′2Qr^2\le n', the endpoints of I\mathcal I, R⩾32R\ge32, 6R⩽Q6R\le Q, and the binomial tail bound ), and if any check fails it counts the common zeros by checking the original equations on all 2n2^n assignments. For fixed k,ck,c, a failure can occur only for finitely many nn, so this fallback is absorbed in the theorem's constants.

In plain English

All numerical conditions needed by the construction can be checked exactly with integer arithmetic. If any check fails, the algorithm just counts common zeros by brute force over all 2n2^n assignments, and for fixed k,ck,c this happens only for finitely many nn.

Why it's here

This claim makes the construction rigorous by separating the finitely many small nn where the parameter conditions might fail from the large-nn regime. The explicit parameter lemma shows the checks hold for large nn and run in polylogarithmic time, and the incidence-labeling lemma then applies whenever they pass. The brute-force fallback costs only a constant for the theorem's bound.
Classified routine:
Standard bookkeeping: exact verification of the parameter conditions plus a brute-force fallback over all 2^n assignments, justified by the explicit parameter lemma (lem-incidence-parameters) showing the checks hold for all large n, so failures cost only a constant.

Uses

lemDeterministic balanced incidence labelinglemExplicit parameter choice satisfies layout hypotheses

Used by

Nothing in the paper

Sources

PaperOpen
Section
§5.5 Constructing the forms and completing the proof
Page
—
Label
—
Line
main_full_version.tex:3185
Leannot aligned

Phase 2 aligns this node to a Lean declaration.