claimroutineinferred_dep

Low-cost derivatives vanish along curve

Shows derivatives of FNF_N of cost ≤ σN\sigma N vanish identically along CC
converts high order at points into vanishing along the curve
Claim·§2.2 The curve inequality·inside propCurve inequality for weighted degree

Statement (paper)

Assume that fails. Then for every sufficiently large integer NN the nonzero polynomial FNF_N satisfies DγFN∣C=0D^\gamma F_N\big|_C=0 for all multi-indices γ\gamma with ∑avaγa≤σN\sum_a v_a\gamma_a\le\sigma N, where D0,…,DmD_0,\dots,D_m is the commuting frame on Y≠0Y\ne0.

In plain English

If the curve inequality fails, then for all large NN the nonzero auxiliary polynomial FNF_N has DγFND^\gamma F_N vanishing identically on CC for every multi-index γ\gamma with ∑avaγa≤σN\sum_a v_a\gamma_a\le\sigma N, where D0,…,DmD_0,\dots,D_m is the commuting frame on Y≠0Y\ne0.

Why it's here

This is the step of the contradiction argument that turns the high VV-order of FNF_N at the prescribed points (from the previous claim) into vanishing of many derivatives along the whole curve CC. The failure of the curve inequality leaves more contact with CC than the degree of CC can accommodate, so each derivative of cost at most σN\sigma N must vanish on CC. The later claims use this vanishing to find a persistent component constraining normal bases and to build the fiber polynomial.
Classified routine:
This follows from the preceding auxiliary-polynomial claim by a standard zero-counting argument on a curve: after a low-cost derivative, the remaining prescribed vanishing would exceed the degree bound unless that derivative vanished identically on C.

Uses

claimExcess contact yields auxiliary polynomial

Used by

claimPersistent component constrains normal basesclaimFiber polynomial retains derivative vanishing

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Low-cost derivatives vanish along curve" rests on claim-geom-curve-inequality-1