claimstandardinferred_dep

Weighted Bezout caps slice intersection length

Weighted Bezout caps the local intersection length by

N^k/\prod\rho_a

upper bound paired with the lower bound to compare products

Claim·§2.1 A local multiplicity comparison·inside lemLocal multiplicity comparison of weights and costs

Statement (paper)

The

k

general constant linear combinations of the restricted equations, each of weighted degree at most

N

in the variables indexed by

A

, have local intersection length at the isolated common zero

x

at most

\frac{N^k}{\prod_{a\in A}\rho_a}

In plain English

On the coordinate slice indexed by

A

k

general constant linear combinations of the restricted equations, each of weighted degree at most

N

, meet at the isolated point

x

with local intersection length at most

N^k/\prod_{a\in A}\rho_a

Why it's here

This is the upper bound that pairs with the previous claim's lower bound on local length,

(\varepsilon N)^k/(2k!\prod_{b\in B}\kappa_b)

. Weighted Bezout bounds the total intersection number by the product of degrees divided by the product of weights, and the local length at the isolated point

x

cannot exceed it. Combining the two bounds and cancelling

N^k

gives the comparison of

\prod\rho_a

with

\prod\kappa_b

Classified standard:

Weighted Bézout bounds the total intersection number of k equations of weighted degrees at most N by N^k/∏_{a∈A}ρ_a. The local intersection length at an isolated zero is at most that total.

Uses

claimPersistent derivatives force large local length

Used by

Nothing in the paper

Sources

PaperOpen

Section: §2.1 A local multiplicity comparison
Page: —
Label: —
Line: sections/interpolation.tex:137

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Weighted Bezout caps slice intersection length" rests on claim-geom-multiplicity-1