claimroutineinferred_dep

Projective degree equals weighted curve degree

Shows deg⁡L∣C=Rdeg⁡WC\deg L|_C=R\deg_W C for curves meeting the chart
converts projective degree into weighted degree for nefness
Claim·§2.3 From the curve inequality to all coefficient packets·inside thmInterpolation with separated weights

Statement (paper)

For any curve CC meeting the chart of the constant monomial, deg⁡(L∣C)=Rdeg⁡WC\deg(L|_C)=R\deg_W C.

In plain English

For any curve CC meeting the chart of the constant monomial, the degree of the line bundle LL restricted to CC equals RR times the weighted degree deg⁡WC\deg_W C.

Why it's here

This claim converts the projective degree of LL on a curve into the weighted degree measured by the weights WW. Later claims, such as the nefness of A−(1+σ)EA-(1+\sigma)E and the vanishing and jet generation step, can then reduce curve inequalities to weighted-degree estimates for deg⁡WC\deg_W C.
Classified routine:
This is the standard degree calculation for the monomial embedding: its line bundle has degree equal to the embedding scale R times the corresponding weighted curve degree. The claim applies that calculation to the paper’s weights and notation.

Uses

claimSeparated weights avoid center dependence

Used by

claimCurve inequality makes blowup class nefclaimVanishing and projective sections generate jets

Sources

PaperOpen
Section
§2.3 From the curve inequality to all coefficient packets
Page
—
Label
—
Line
sections/interpolation.tex:429
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Projective degree matches weighted curve degree" rests on claim-geom-interpolation-1