claimroutineinferred_dep

Single-center zero-pole count contradicts excess

A zero-pole count for Xl−cjlX_l-c_{jl} gives deg⁡WC>(1+σ)∑hP\deg_W C>(1+\sigma)\sum h_P at one center
closes the contradiction in the single-center case
Claim·§2.2 The curve inequality·inside propCurve inequality for weighted degree

Statement (paper)

Suppose the prescribed points on CC reduce to the single point aja_j, and let XlX_l be a coordinate nonconstant on CC. Then the nonzero rational function Xl−cjlX_l-c_{jl} has total pole degree at most wldeg⁡WCw_l\deg_W C and order at least (wl/θ)hP(w_l/\theta)h_P at each branch P↦ajP\mapsto a_j, so that deg⁡WC≥θ−1∑P↦ajhP>(1+σ)∑P↦ajhP\deg_W C\ge\theta^{-1}\sum_{P\mapsto a_j}h_P>(1+\sigma)\sum_{P\mapsto a_j}h_P, by the last inequality in ; this contradicts the assumption that fails.

In plain English

If all prescribed points on CC reduce to a single point aja_j, then the curve inequality cannot fail: a nonconstant coordinate XlX_l gives a function Xl−cjlX_l-c_{jl} whose zero and pole counts force deg⁡WC≥θ−1∑P↦ajhP>(1+σ)∑P↦ajhP\deg_W C\ge\theta^{-1}\sum_{P\mapsto a_j}h_P>(1+\sigma)\sum_{P\mapsto a_j}h_P.

Why it's here

This finishes the proof by contradiction in the single-center case reached by the previous claim. The nonzero function Xl−cjlX_l-c_{jl} has at most wldeg⁡WCw_l\deg_W C poles but vanishes to order at least (wl/θ)hP(w_l/\theta)h_P at each branch over aja_j, and comparing these counts together with the last inequality in the σ\sigma condition contradicts the assumed failure of the bound.Thus the curve inequality holds in this case.
Classified routine:
This follows by the standard zero–pole degree count for a nonzero rational function on a curve, applied to the coordinate function with the stated weighted-degree pole bound. The final contradiction uses the earlier single-center reduction and the inequality in .

Uses

claimSeparated normals isolate one centerclaimExcess contact yields auxiliary polynomialclaimSeparated weights avoid center dependence

Used by

Nothing in the paper

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Single-center zero-pole count contradicts excess" rests on claim-geom-curve-inequality-6
  • info
    inferred_dep
    outline: "Single-center zero-pole count contradicts excess" rests on claim-geom-curve-inequality-1
  • info
    inferred_dep
    outline: "Single-center zero-pole count contradicts excess" rests on claim-geom-interpolation-1