claimroutineinferred_dep

Persistent component constrains normal bases

Finds a persistent component

Z

with

\prod_A w_a\le C_*\prod_B v_b

for normal bases

applies the multiplicity lemma to restrict normal bases

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

Statement (paper)

There is an irreducible component

Z

of the common zero set in

Y\ne0

of the derivatives of cost at most

r\delta

(where

\delta=\sigma N/L_0

0\le r\le L_0

), containing

C^\circ

and of dimension between

1

and

m

, which persists on two adjacent levels, with

k=\operatorname{codim}Z

. Moreover, for every coordinate normal basis

A

and every frame normal basis

B

Z

one has

\prod_{a\in A}w_a\le C_*\prod_{b\in B}v_b,

where

C_*

is the uniform constant of Lemma , independent of

N

and of the choice of equations and

Z

In plain English

Under the failure of the curve inequality, there is an irreducible component

Z

of the common zeros (in

Y\ne0

) of the low-cost derivatives, of cost at most

r\delta

, containing

C^\circ

, of dimension between

1

and

m

, and persisting on two adjacent levels. For

k=\operatorname{codim}Z

, every coordinate normal basis

A

and frame normal basis

B

Z

satisfy

\prod_{a\in A}w_a\le C_*\prod_{b\in B}v_b

, with

C_*

uniform.

Why it's here

The vanishing of low-cost derivatives along

C

from the previous claim yields a common zero set containing

C^\circ

, and a pigeonhole over the levels

0\le r\le L_0

gives a component that persists on two adjacent levels. Applying the multiplicity comparison lemma to that component then bounds the weight product of coordinate normal bases by the cost product of frame bases. Combined with the separated-weights choice, this limits which index sets can occur as normal bases, which the next claim uses to show

Y

is constant on

Z

Classified routine:

This follows by applying a pigeonhole argument to the low-cost derivative zero sets from claim-geom-curve-inequality-2, then applying geom-multiplicity to the persistent component.

Uses

lemLocal multiplicity comparison of weights and costsclaimLow-cost derivatives vanish along curveclaimSeparated weights avoid center dependence

Used by

claimLogarithmic residues force constant Y

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Persistent component constrains normal bases" rests on claim-geom-curve-inequality-2
info
inferred_dep
outline: "Persistent component constrains normal bases" rests on claim-geom-interpolation-1