Extracting a finite gradient certificate from tangent inclusion

The formal-divisor construction already produces a projective power-series arc and a row annihilating its explicit tangent columns. The remaining local commutative-algebra condition is that the equation-defined Zariski tangent space at the dehomogenized Laurent point be contained in the span of those columns. Under exactly that condition, finite-dimensional annihilator duality places the affine tail of the row in the span of equation differentials. A finitely supported expansion can then be reindexed by a finite type, producing the finite-gradient boundary certificate used by the canonical asymptotic consumer.

Thus no separate finite-generation theorem for the ideal is needed. The global normalization argument has only to establish the displayed tangent inclusion for the completed boundary chart (and separately handle any residue-field transport).

Finite reindexing of an equation-differential expansion

theorem Stafford38.Geometry.FiniteGradientFromTangentInclusion.exists_fin_gradient_identity_of_mem_affineConormalSpace {k : Type u} [Field k] {m : ℕ} (I : Ideal (MvPolynomial (Fin m) k)) (y xi : Fin m → k) (hxi : AffineConormalSpan.coordinateCovector xi ∈ AffineConormalSpan.affineConormalSpace y I) : ∃ (r : ℕ) (equations : Fin r → ↥I) (coefficients : Fin r → k), ∀ (i : Fin m), xi i = ∑ j : Fin r, coefficients j * CoisotropicTranslation.differentialAt y (↑(equations j)) i

Membership of a coordinate covector in the equation conormal space gives an honest Fin r-indexed gradient identity. This is the finite-support content of Submodule.span; it does not require the whole ideal to be finitely generated.

Completed formal chart to finite-gradient certificate

theorem Stafford38.Geometry.FiniteGradientFromTangentInclusion.exists_finiteGradientBoundaryCertificate_of_zariski_le_formalSpan {k : Type u} [Field k] {m : ℕ} (hm : 0 < m) (I : Ideal (MvPolynomial (Fin m) k)) {κ : Type u_1} [Finite κ] (q ell : Fin (m + 1) → PowerSeries k) (Z : Matrix (Fin (m + 1)) κ (PowerSeries k)) (tau : Fin (m + 1) → PowerSeries k) (hq0 : q 0 ≠ 0) (hrow : GeometryRetractionSpecialization.rowMul ell (GeometryFormalDivisorTangent.formalTangentMatrix q Z tau) = 0) (hbase : ∀ f ∈ Ideal.map (ScalarExtensionPoints.scalarPolynomialMap (Fin m)) I, (MvPolynomial.eval (ProjectiveConormalDehomogenization.dehomogenizedPoint (FormalDivisorLaurentConormal.laurentColumn q))) f = 0) (htangent : AffineConormalSpan.zariskiTangentSpace (ProjectiveConormalDehomogenization.dehomogenizedPoint (FormalDivisorLaurentConormal.laurentColumn q)) (Ideal.map (ScalarExtensionPoints.scalarPolynomialMap (Fin m)) I) ≤ ProjectiveConormalDehomogenization.dehomogenizedTangentSpan (FormalDivisorLaurentConormal.laurentColumn q) (FormalDivisorLaurentConormal.laurentNonpositionTangentMatrix Z tau)) (hresidue : (GeometryRetractionSpecialization.residueColumn fun (i : Fin m) => ell i.succ) = fun (i : Fin m) => if i = ⟨0, hm⟩ then 1 else 0) : Nonempty (FiniteGradientBoundaryProducer.FiniteGradientBoundaryCertificate k m hm I)

A formal projective row plus the standard tangent-inclusion condition constructs the complete finite-gradient boundary certificate.

This theorem identifies the exact higher-dimensional local bridge left to the normalization argument: prove the Zariski tangent space of the scalar-extended ambient ideal is contained in the dehomogenized span of the formal divisor and normalized transverse columns. Once that inclusion is available, Mathlib's finite-dimensional annihilator and finite-support span machinery supplies the finite equations and coefficients automatically.