Prove2Me

Local-coordinate polynomial embeds as evaluation at truncated-log coordinates

Proved
OAI.PiExponent.LogarithmicJetIdeals.localCoordinatePolynomial_eq_truncatedCoordinate_aeval

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

number-theoryopenai-pi-exponent-017

The polynomial defining the local coordinates, when embedded into multivariate power series, is evaluation at the same truncated-log coordinates.

Preamble
import Definitions.Def_OAI_PiExponent_LogarithmicJetIdeals_LocalCoordinates
import Mathlib.RingTheory.MvPowerSeries.Substitution

open OAI.PiExponent
open OAI.PiExponent.AdmissibleFormalInterpolation
open OAI.PiExponent.LogarithmicJetIdeals
Formal statement
theorem OAI.PiExponent.LogarithmicJetIdeals.localCoordinatePolynomial_eq_truncatedCoordinate_aeval
    {m : ℕ} (c : Fin m → ℂ) (T : Fin m → ℕ)
    (P : MvPolynomial (Fin (m + 1)) ℂ) :
    (localCoordinatePolynomial c T P : MvPowerSeries (Fin (m + 1)) ℂ) =
      MvPolynomial.aeval
        (Fin.cases (1 + MvPowerSeries.X 0)
          (fun i : Fin m => MvPowerSeries.C (c i) + MvPowerSeries.X i.succ +
            liftLogSeries m (InterpolationMatrix.truncatedLog (T i) : PowerSeries ℂ))) P := by sorry
Source
https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Approximation/AdmissibleMatrixGeometry.lean#L41-L44

View graph