claimroutineinferred_dep

Excess contact yields auxiliary polynomial

Failure of the curve inequality yields FNF_N of VV-order ≥ (1+3σ)N(1+3\sigma)N at all points
builds the auxiliary polynomial for the contradiction
Claim·§2.2 The curve inequality·inside propCurve inequality for weighted degree

Statement (paper)

If fails, then for every sufficiently large integer NN there exists a nonzero polynomial FNF_N of WW-degree at most NN whose expansions at all the prescribed points have VV-order at least (1+3σ)N(1+3\sigma)N.

In plain English

If the curve inequality deg⁡WC≥(1+σ)∑P↦ajhP\deg_W C\ge(1+\sigma)\sum_{P\mapsto a_j}h_P fails, then for every sufficiently large NN there is a nonzero polynomial FNF_N of WW-degree at most NN whose expansions at all prescribed points have VV-order at least (1+3σ)N(1+3\sigma)N.

Why it's here

This is the interpolation step of the proof by contradiction: a curve violating the bound has too little degree compared with its contact at the prescribed points, which leaves room to construct FNF_N vanishing to high VV-order. The separated weights from the earlier claim make the count of conditions independent of the points and centers, and FNF_N is the auxiliary polynomial used in the later claims, for example to show derivatives vanish along CC and to run the zero-pole count.
Classified routine:
This is an auxiliary-polynomial interpolation step: failure of the degree bound leaves more coefficients than vanishing conditions, so a nonzero polynomial exists by linear algebra. The earlier separated-weights claim supplies the point-independent condition count.

Uses

claimSeparated weights avoid center dependence

Used by

claimLow-cost derivatives vanish along curveclaimSingle-center zero-pole count contradicts excess

Sources

PaperOpen
Section
§2.2 The curve inequality
Page
—
Label
—
Line
sections/interpolation.tex:251
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Excess contact produces auxiliary polynomial" rests on claim-geom-interpolation-1