claimroutine

Persistent derivatives force large local length

Lower-bounds local length by (εN)k/(2k!∏κb)(\varepsilon N)^k/(2k!\prod\kappa_b) on a slice
lower bound on intersection multiplicity
Claim·§2.1 A local multiplicity comparison·inside lemLocal multiplicity comparison of weights and costs

Statement (paper)

Let SS be the affine coordinate slice through the chosen smooth point xx of ZZ, obtained by fixing the coordinates outside AA. Then the zero set of the restricted equations fℓ∣Sf_\ell|_S is isolated at xx, and the local quotient of the analytic local ring of SS at xx by the ideal generated by the restricted equations has length at least #{α∈Z≥0k:∑b∈Bκbαb<εN}≥(εN)k2k!∏b∈Bκb\#\{\alpha\in\NN^k:\sum_{b\in B}\kappa_b\alpha_b<\varepsilon N\}\ge \frac{(\varepsilon N)^k}{2k!\prod_{b\in B}\kappa_b}, for every N>0N>0.

In plain English

On the coordinate slice SS through a smooth point xx of ZZ (fixing coordinates outside AA), the restricted equations fℓ∣Sf_\ell|_S have an isolated zero at xx. The local quotient ring of SS at xx by these equations has length at least #{α∈Z≥0k:∑b∈Bκbαb<εN}\#\{\alpha\in\NN^k:\sum_{b\in B}\kappa_b\alpha_b<\varepsilon N\}, which is at least (εN)k/(2k!∏b∈Bκb)(\varepsilon N)^k/(2k!\prod_{b\in B}\kappa_b) for every N>0N>0.

Why it's here

This gives the lower bound on local intersection multiplicity in the proof of the multiplicity comparison. The vanishing of the derivatives DγfℓD^\gamma f_\ell on ZZ for small cost puts many monomials in the DD-field normal coordinates into the quotient, so it must be large. The next claim pairs this with a weighted Bezout upper bound, and the two bounds together give the comparison of ∏ρa\prod\rho_a with ∏κb\prod\kappa_b.
Classified routine:
This adapts the standard local-algebra argument that vanishing derivatives leave corresponding monomial classes independent in the local quotient. The numerical bound is an elementary lattice-point estimate.

Uses

Nothing else in the paper

Used by

claimWeighted Bezout caps slice intersection length

Sources

PaperOpen
Section
§2.1 A local multiplicity comparison
Page
—
Label
—
Line
sections/interpolation.tex:100
Leannot aligned

Phase 2 aligns this node to a Lean declaration.