Constant fibre forces zero ideal contact at an affine place

Proved

OAI.PiExponent.FormalInterpolation.constant_fibre_contact_zero_at_place

by Eyal1990 · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

At a place where every coordinate has nonnegative valuation, the logarithmic center ideal has contact zero if the i0 coordinate is the constant a and no center has that coordinate. The proof constructs the product of the i0-coordinate generators, shows it lies in the product ideal, and evaluates it to a nonzero constant. Its valuation is zero, which bounds the contact infimum by zero; contact is a natural number.

Preamble

import Definitions.Def_OAI_PiExponent_TruncatedPolynomialJets
import Definitions.Def_OAI_PiExponent_LogarithmicInterpolationNumerics
import Definitions.Def_OAI_PiExponent_WeightedIdealCurveCriterion
import Mathlib.RingTheory.Algebraic.Defs

open scoped BigOperators
open OAI.PiExponent OAI.PiExponent.DeterminantContradiction OAI.PiExponent.FormalInterpolation

Formal statement

theorem OAI.PiExponent.FormalInterpolation.constant_fibre_contact_zero_at_place
    {m K : Nat} (c : Fin K → Fin m → Complex)
    (T : Fin m → Nat) (e : Fin (m + 1) → Nat)
    (E : Type) [Field E] [Algebra Complex E] [Algebra.EssFiniteType Complex E]
    (x : Fin (m + 1) → E) (hfibre : x 0 = 1)
    (i0 : Fin m) (a : Complex) (ha : x i0.succ = algebraMap Complex E a)
    (hn : ∀ j : Fin K, c j i0 ≠ a)
    (nu : PolynomialCurvePlace E)
    (h_aff : ∀ i, (0 : WithTop Int) ≤ nu.1 (x i)) :
    polynomialCurveIdealContact nu x (logarithmicCentersIdeal c T e) = 0 := by sorry

View graph