CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The integers are not a Sidon set

Statement refuted

“The set $Z$ is a Sidon set.”

Facts & Assumptions

Given: $z = e_{1} (x)$ , and polynomials $P_{0} = Q_{0} = 1$ defined recursively by $P_{m + 1} = P_{m} + z^{2^{m}} Q_{m}, Q_{m + 1} = P_{m} - z^{2^{m}} Q_{m} .$

Counterexample

technique · Rudin--Shapiro recursion

1.1

Inductively, $P_{m}$ and $Q_{m}$ have $2^{m}$ coefficients, all $\pm 1$ , on [given, algebra] the frequencies $0, \dots, 2^{m} - 1$ . The two supports in each recursion are disjoint, so this is immediate from the displayed construction.

givenalgebra

2.1

On $∣ z ∣ = 1$ , the parallelogram identity gives [step 1.1, algebra] $∣ P_{m + 1} ∣^{2} + ∣ Q_{m + 1} ∣^{2} = 2 ∣ P_{m} ∣^{2} + 2 ∣ Q_{m} ∣^{2} .$ Starting from $∣ P_{0} ∣^{2} + ∣ Q_{0} ∣^{2} = 2$ , induction yields $∣ P_{m} ∣^{2} + ∣ Q_{m} ∣^{2} = 2^{m + 1}$ , hence $∥ P_{m} ∥_{\infty} \leq 2^{(m + 1) / 2}$ .

step 1.1algebra

3.1

The coefficient $ℓ^{1}$ mass of $P_{m}$ is $2^{m}$ . If the defining [step 2.1, algebra] inequality of Sidon sets in the integer dual held for $Z$ with one constant $C$ , it would give $2^{m} \leq C 2^{(m + 1) / 2}$ for every $m$ , which is impossible. Hence $Z$ is not Sidon.

step 2.1algebra∎

Depends on

Sidon sets in the integer dual

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

2 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Loukas Grafakos, Classical Fourier Analysis, 3rd ed., Example 3.6.11 (standard reference, not scraped)