we-solve (beta)

Math-2952 · mathematics · Analysis

Uniformly flat real Littlewood polynomials

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every epsilon in (0,1), is there N0 such that for every integer $N>=N0$ one can choose N real coefficients, each +1 or -1, so that the modulus of their polynomial is between (1-epsilon)sqrt(N) and (1+epsilon)sqrt(N) at every point of the unit circle?

Short English statement

For every epsilon in (0,1), is there N0 such that for every integer $N>=N0$ one can choose N real coefficients, each +1 or -1, so that the modulus of their polynomial is between (1-epsilon)sqrt(N) and (1+epsilon)sqrt(N) at every point of the unit circle?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2952-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2952

Uniformly flat real sign polynomials: The primary statement says: For every epsilon>0 and every sufficiently large integer length N, a real sign polynomial has modulus between (1-epsilon)sqrt(N) and (1+epsilon)sqrt(N) everywhere on the circle. The target retains these quantified objects and hypotheses, so its positive assertion is covered.

With the hypotheses and conventions above, the claimed result addresses the whole mathematical assertion on this page.

Uniformly flat real Littlewood polynomials

OpenAI's claim

Uniformly flat real sign polynomials: OpenAI claims that real sign polynomials can have normalized modulus uniformly as close to one as desired once the integer length is large enough. Choices at different lengths are independent of one another.

Mathematical statement of the claimed result

Mathematical claim 1.
For every $0<\epsilon<1$, all sufficiently large integers $N$ admit signs $a_k\in\{-1,1\}$ such that \[(1-\epsilon)\sqrt N\le\left|\sum_{k=0}^{N-1}a_kz^k\right|\le(1+\epsilon)\sqrt N\quad\text{for all }|z|=1.\] The quantifier covers every sufficiently large length, and both inequalities refer to one polynomial.

Outline of the argument

Uniformly flat real sign polynomials: A continuous circle function is built with nearly constant modulus, real coefficients of nearly sign size in the retained frequency range, and a small Fourier tail. Auxiliary-torus waves and phase corrections coordinate the upper and lower modulus bounds. Parseval controls the aggregate coefficient defect, allowing discrepancy rounding to preserve uniform flatness.

Formal verification

Family 076 describes Lean coverage for near-minimal upper maxima and convergence of finite-exponent modulus means; the later uniform lower-envelope conclusions are separate.

Uniformly flat real sign polynomials: No manuscript-specific Comparator is listed in the pinned inventory.

The documented selection does not cover the entire manuscript assertion relevant here.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →