Support of a powered coordinate factor

Proved

OAI.PiExponent.FinitePeriodCollision.coordinate_factor_support

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

irrationality-measurenumber-theoryopenai-pi-exponent-017

Every monomial with nonzero coefficient in the factor (C (b i) + X i) ^ a i uses only variable i. This includes exponent zero and the zero-power case.

Preamble

import Definitions.Def_OAI_PiExponent_FinitePeriodAnalytic
open OAI.PiExponent
open OAI.PiExponent.FinitePeriodCollision

Formal statement

theorem OAI.PiExponent.FinitePeriodCollision.coordinate_factor_support
    {m : ℕ} (a : Fin m → ℕ) (b : Fin m → PowerSeries ℂ) :
    ∀ (i : Fin m) (s : Fin m →₀ ℕ),
      ((MvPolynomial.C (b i) + MvPolynomial.X i) ^ a i).coeff s ≠ 0 →
        ∀ j : Fin m, s j ≠ 0 → j = i := 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