Cauchy row tests depend only on the circle values

Proved

OAI.PiExponent.FinitePeriodCollision.rowTest_congr_sphere

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

irrationality-measurenumber-theoryopenai-pi-exponent-017

If two functions agree on the radius-1/2 circle, their row tests agree. This removes the integral congruence step from the parent. It follows directly by unfolding rowTest to cauchyPowerSeries and applying congruence to the circle integral; no analyticity assumption is needed for this equality.

Preamble

import Definitions.Def_OAI_PiExponent_FinitePeriodAnalytic
open scoped BigOperators
open OAI.PiExponent
open OAI.PiExponent.DeterminantContradiction.FiniteTranslation
open OAI.PiExponent.FinitePeriodCollision

Formal statement

theorem OAI.PiExponent.FinitePeriodCollision.rowTest_congr_sphere
    {f g : ℂ → ℂ} (ell : ℕ)
    (hfg : ∀ z ∈ Metric.sphere (0 : ℂ) (1 / 2), f z = g z) :
    rowTest ell f = rowTest ell g := 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