claimroutineinferred_dep

Fiber polynomial retains derivative vanishing

Restricts to the fiber Y=1Y=1: gives GNG_N with high order and vanishing derivatives
fiber polynomial for isolating a single center
Claim·§2.2 The curve inequality·inside propCurve inequality for weighted degree

Statement (paper)

In the affine fiber Y=1Y=1, with degree weights wiw_i, order weights vi=wi/θv_i=w_i/\theta and hP=min⁡iord⁡P(Xi−cji)/vih_P=\min_i\operatorname{ord}_P(X_i-c_{ji})/v_i, for all sufficiently large NN there is a nonzero polynomial GN(X1,…,Xm)G_N(X_1,\ldots,X_m) of weighted degree at most NN and order at least (1+3σ)N(1+3\sigma)N at every center, and it satisfies ∂XγGN∣C=0\partial_X^\gamma G_N\big|_C=0 for all multi-indices γ\gamma with ∑i=1mviγi≤σN\sum_{i=1}^m v_i\gamma_i\le\sigma N.

In plain English

On the fiber Y=1Y=1, for all large NN there is a nonzero polynomial GN(X1,…,Xm)G_N(X_1,\ldots,X_m) of weighted degree at most NN with order at least (1+3σ)N(1+3\sigma)N at every center, such that ∂XγGN\partial_X^\gamma G_N vanishes on CC for all γ\gamma with ∑iviγi≤σN\sum_i v_i\gamma_i\le\sigma N.

Why it's here

Since Y=1Y=1 on CC (previous claim), the auxiliary polynomial can be restricted to the fiber, giving a polynomial in X1,…,XmX_1,\ldots,X_m alone. The restriction keeps the high vanishing order at the centers and the vanishing of low-cost derivatives along CC from the earlier claim. The next claims use GNG_N to analyze the persistent component inside the fiber and isolate a single center.
Classified routine:
This is a restriction-to-a-fiber step: the earlier claims establish that Y=1 on C and that the auxiliary polynomial has the required vanishing. The nonzero restriction needs a separate justification if it is not supplied by the earlier construction.

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Fiber polynomial retains derivative vanishing" rests on claim-geom-curve-inequality-2
  • info
    inferred_dep
    outline: "Fiber polynomial retains derivative vanishing" rests on claim-geom-curve-inequality-4
  • info
    inferred_dep
    outline: "Fiber polynomial retains derivative vanishing" rests on claim-geom-interpolation-1