claimroutineinferred_dep

Logarithmic residues force constant Y

Shows

Y

is constant on

Z

, so

Y=1

C

puts the curve in the fiber

Y=1

Claim·§2.2 The curve inequality·inside propCurve inequality for weighted degree

Statement (paper)

On the persistent component

Z

, the function

Y

is constant. In particular

Y=1

C^\circ

, and hence on

C

by density. When some positive coordinate direction is nontangent to

Z

, one has

dX_i=dY/Y

Z

for the largest such index

i

, and this forces

Y

(and

X_i

) to be constant on

Z

In plain English

On the persistent component

Z

the function

Y

is constant, so

Y=1

C^\circ

and hence on

C

by density. If some positive coordinate direction is nontangent to

Z

, then

dX_i=dY/Y

Z

for the largest such index

i

, which forces

Y

and

X_i

to be constant on

Z

Why it's here

This shows that the persistent component lies inside the affine fiber

Y=1

, which lets the next claim work with a fiber polynomial there. The idea is to use the normal-basis weight bound from the persistent-component claim together with the separated-weights choice. These rule out every index pattern except the one where the largest nontangent direction gives

dX_i=dY/Y

, and that relation forces

Y

to be constant.

Classified routine:

The index-pattern reduction follows from the earlier persistent-component normal-basis bound and separated-weights choice. The final step uses the standard residue obstruction: an exact differential cannot equal dY/Y for a nonconstant rational function Y on an algebraic curve.

Uses

claimPersistent component constrains normal basesclaimSeparated weights avoid center dependence

Used by

claimFiber polynomial retains derivative vanishing

Sources

PaperOpen

Section: §2.2 The curve inequality
Page: —
Label: —
Line: sections/interpolation.tex:327

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Logarithmic residues force constant Y" rests on claim-geom-curve-inequality-3
info
inferred_dep
outline: "Logarithmic residues force constant Y" rests on claim-geom-interpolation-1