propositionnovelunresolved_ref

Curve inequality for weighted degree

Every curve has weighted degree at least (1+σ)(1+\sigma) times its total contact height
gives the nefness the interpolation theorem needs
Proposition·geom:curve-inequality·§2.2 The curve inequality

Statement (paper)

With the weights chosen above, every such curve satisfies deg⁡WC≥(1+σ)∑P↦ajhP, \deg_W C\ge(1+\sigma)\sum_{P\mapsto a_j}h_P, where the sum includes all branches through the prescribed points.

In plain English

With the chosen weights, every curve CC of the type under consideration has weighted degree at least (1+σ)(1+\sigma) times the sum of the contact heights hPh_P over all branches PP mapping to the prescribed points aja_j.

Why it's here

This is the geometric input that the interpolation theorem uses, and it is what makes the blown-up class nef. The proof is by contradiction: failure of the bound yields an auxiliary polynomial with many vanishing derivatives along CC, and the multiplicity comparison lemma together with the separated weights forces Y=1Y=1, then a single center. The final zero-pole count at that center contradicts the assumed failure.
Classified novel:
This is the paper’s central geometric input: it converts local multiplicity comparisons into a global weighted degree bound for all relevant curves. The separated-weights argument and final zero–pole count go beyond the local multiplicity comparison lemma it uses.

Uses

lemLocal multiplicity comparison of weights and costs

Used by

thmInterpolation with separated weightsclaimCurve inequality makes blowup class nef

Inside the proof

claimExcess contact yields auxiliary polynomialclaimLow-cost derivatives vanish along curveclaimPersistent component constrains normal basesclaimLogarithmic residues force constant YclaimFiber polynomial retains derivative vanishingclaimSeparated normals isolate one centerclaimSingle-center zero-pole count contradicts excess

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • warn
    unresolved_ref
    The normal-basis contradictions use the crucial weight-separation inequality established in unlabeled setup at interpolation.tex:195–214.