Prove2Me

Local jet ideals at distinct centers are comaximal

Proved
OAI.PiExponent.LogarithmicJetIdeals.localJetIdeals_comaximal_of_ne

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

number-theoryopenai-pi-exponent-017

For two center maps differing at any coordinate, their local jet ideals with the same truncation and exponents are comaximal.

Preamble
import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation
import Definitions.Def_OAI_PiExponent_LogarithmicJetIdeals
import Mathlib.RingTheory.Ideal.Operations

open OAI.PiExponent
open OAI.PiExponent.AdmissibleFormalInterpolation
open OAI.PiExponent.LogarithmicJetIdeals
Formal statement
theorem OAI.PiExponent.LogarithmicJetIdeals.localJetIdeals_comaximal_of_ne
    {m : ℕ} (c d : Fin m → ℂ) (T : Fin m → ℕ)
    (e : Fin (m + 1) → ℕ)
    (h : ∃ i : Fin m, c i ≠ d i) :
    localJetIdeal c T e ⊔ localJetIdeal d T e = ⊤ := by sorry
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Approximation/AdmissibleMatrixGeometry.lean#L41-L44

View graph