claimroutineinferred_dep

Separated normals isolate one center

Shows separated normals force a constant coordinate, so

C

has one prescribed point

reduces the proof to the single-center case

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

Statement (paper)

Suppose

m\ge2

. Then the component

Z'

, of codimension

k

with

1\le k\le m-1

in the fiber, has a unique normal-basis index set, and for some index

i

in it the coordinate

X_i

is constant on

Z'

. Consequently

Z'

, and hence

C

, meets at most one prescribed point; every prescribed point of

C

lies in

C^\circ\subseteq Z'

, so all of them coincide with a single point

a_j

In plain English

m\ge2

, the persistent component

Z'

of codimension

k

(with

1\le k\le m-1

) in the fiber has a unique normal-basis index set, and some coordinate

X_i

in it is constant on

Z'

. Hence

Z'

and

C

meet at most one prescribed point, and all prescribed points of

C

coincide with a single

a_j

Why it's here

The polynomial

G_N

from the previous claim has the derivative vanishing needed to apply the multiplicity lemma on

Z'

. The separated weight choice then makes the inequality from that lemma single out one dominant index set, which forces a constant coordinate. Since a constant coordinate fixes a value,

Z'

can contain only one center, and this reduces the problem to the single-center count in the next claim.

Classified routine:

This follows from the earlier local multiplicity lemma and the separated-weight choice: their inequality isolates one normal-basis index set and forces a coordinate to be constant on the component. The conclusion about prescribed points then follows directly.

Uses

lemLocal multiplicity comparison of weights and costsclaimFiber polynomial retains derivative vanishingclaimSeparated weights avoid center dependence

Used by

claimSingle-center zero-pole count contradicts excess

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Separated normals isolate one center" rests on claim-geom-curve-inequality-5
info
inferred_dep
outline: "Separated normals isolate one center" rests on claim-geom-interpolation-1