The plain jet maps the rectangular ideal into the coordinate-power ideal

Proved

OAI.PiExponent.LogarithmicJetIdeals.plainJet_mem_span_X_pow_of_mem_rectangularJetIdeal

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

number-theoryopenai-pi-exponent-017

Under the plain affine jet substitution, every polynomial in the rectangular jet ideal maps into the ideal generated by the coordinate powers $X_k^{degree(k)+1}$ .

Preamble

import Definitions.Def_OAI_PiExponent_LogarithmicJetIdeals_PlainJet
import Definitions.Def_OAI_PiExponent_LogarithmicJetIdeals_RectangularJetIdeal
import Mathlib.RingTheory.Ideal.Operations

open OAI.PiExponent.AdmissibleFormalInterpolation

Formal statement

theorem OAI.PiExponent.LogarithmicJetIdeals.plainJet_mem_span_X_pow_of_mem_rectangularJetIdeal
    {m : Nat} (c : Fin m -> Complex) (degree : Fin (m + 1) -> Nat)
    (R : MvPolynomial (Fin (m + 1)) Complex)
    (h : R ∈ OAI.PiExponent.LogarithmicJetIdeals.rectangularJetIdeal c degree) :
    OAI.PiExponent.LogarithmicJetIdeals.plainJet c R ∈
      Ideal.span (Set.range (fun k : Fin (m + 1) =>
        (MvPowerSeries.X k : MvPowerSeries (Fin (m + 1)) Complex) ^ (degree k + 1))) := by sorry

Source

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

View graph