Expansion of a single-coordinate polynomial

Proved

OAI.PiExponent.FinitePeriodCollision.single_coordinate_support_as_sum

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

irrationality-measurenumber-theoryopenai-pi-exponent-017

A polynomial supported only on coordinate i equals the finite sum of its singleton-coordinate monomials, indexed by the coordinate values appearing in its support.

Preamble

import Mathlib.Algebra.MvPolynomial.Basic
open scoped BigOperators

Formal statement

theorem OAI.PiExponent.FinitePeriodCollision.single_coordinate_support_as_sum
    {σ : Type} [DecidableEq σ] {R : Type} [CommSemiring R]
    (p : MvPolynomial σ R) (i : σ)
    (hsupport : ∀ (s : σ →₀ ℕ), p.coeff s ≠ 0 →
      ∀ j : σ, s j ≠ 0 → j = i) :
    p = ∑ n ∈ p.support.image (fun s => s i),
      MvPolynomial.monomial (Finsupp.single i n)
        (p.coeff (Finsupp.single i n)) := by sorry

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/Collision.lean, formal_period_collision_bound; https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/DeterminantAnalyticBound.lean, translated_summand_bound and log_norm_sum_le; https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/NumberTheory/PiExponent/Analysis/TranslationCountLimit.lean, translationTermCount. Synthesized explicit actual-matrix bridge obligation for Approximation/DeterminantContradiction.lean, AnalyticAggregateStatement; not claimed to be proved by those source lemmas.

View graph