Sheared formal jets preserve homogeneous coefficients through their degree

Proved

OAI.PiExponent.LogarithmicJetIdeals.formalJet_sheared_homogeneous_coeff

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

number-theoryopenai-pi-exponent-017

For any homogeneous polynomial of degree n, the explicit centered and sheared substitution followed by formalJet preserves all coefficients of total degree at most n.

Preamble

import Definitions.Def_OAI_PiExponent_AdmissibleFormalInterpolation

open scoped BigOperators
open OAI.PiExponent.AdmissibleFormalInterpolation

Formal statement

theorem OAI.PiExponent.LogarithmicJetIdeals.formalJet_sheared_homogeneous_coeff
    {m : Nat}
    (center : Fin m -> Complex)
    (n : Nat)
    (Q : MvPolynomial (Fin (m + 1)) Complex)
    (hhom : ∀ a : Finsupp (Fin (m + 1)) Nat,
      a ∈ Q.support -> (∑ k : Fin (m + 1), a k) = n)
    (e : Fin (m + 1) -> Nat)
    (he : (∑ k : Fin (m + 1), e k) <= n) :
    MvPowerSeries.coeff (Finsupp.equivFunOnFinite.symm e)
      (formalJet center (MvPolynomial.aeval
        (Fin.cases (MvPolynomial.X 0 - MvPolynomial.C 1)
          (fun i => MvPolynomial.X i.succ - MvPolynomial.C (center i) -
            (MvPolynomial.X 0 - MvPolynomial.C 1))) Q)) =
      MvPolynomial.coeff (Finsupp.equivFunOnFinite.symm e) Q := by sorry

Source

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

View graph