Successor jet generator coefficient support

Proved

OAI.PiExponent.LogarithmicJetIdeals.local_jet_ideal_generator_coeff_support_succ

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

number-theoryopenai-pi-exponent-017

If a coefficient of the formal image of a successor jet generator is nonzero, its exponent vector is either the unit exponent at that successor coordinate, or is supported only at coordinate zero with exponent at least the truncation cutoff.

Preamble

import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation
import Definitions.Def_OAI_PiExponent_LogarithmicJetIdeals
open OAI.PiExponent
open OAI.PiExponent.AdmissibleFormalInterpolation
open OAI.PiExponent.LogarithmicJetIdeals
open scoped BigOperators

Formal statement

theorem OAI.PiExponent.LogarithmicJetIdeals.local_jet_ideal_generator_coeff_support_succ
    {m : ℕ} (c : Fin m → ℂ) (T : Fin m → ℕ)
    (b : Fin (m + 1) → ℕ) (i : Fin m) :
    MvPowerSeries.coeff (InterpolationMatrix.exponentVector b)
      (AdmissibleFormalInterpolation.formalJet c
        (jetCoordinate c T i.succ)) ≠ 0 →
      (∀ j : Fin (m + 1), b j = if j = i.succ then 1 else 0) ∨
        (T i ≤ b 0 ∧ ∀ j : Fin m, b j.succ = 0) := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Approximation/AdmissibleMatrixGeometry.lean#L41-L44

View graph