Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

Hadamard-lacunary sets are Sidon

Statement

Every subset E of a positive q-Hadamard-lacunary sequence is a Sidon set in the sense of Sidon sets in the integer dual. More precisely, one may take CE=2r for any positive integer r such that qr≥3,1qr−1<1−1q. Such an r exists for every q>1.

Facts & Assumptions

Given: A finite polynomial F=∑λ∈Λaλeλ, with Λ⊂E, and r as in the Statement. The original sequence consists of positive integers indexed by j≥1, with λj+1≥qλj. Integrals are over the period-one circle with normalized measure.

[L1]

A finite ratio-three frequency class has a nonnegative Riesz product of integral one and prescribed coefficient P^(−λ)=ελ‾/2 at its own frequencies (Riesz-product witnesses for a Hadamard-lacunary set).

[L2]

The real-valued endpoint Holder inequality bounds ∫∣h∣g by ∥h∥∞∥g∥1 for real measurable h and nonnegative integrable g (Holder's inequality for integrals, including the endpoint cases).

Proof

technique · separate each residue-class product from the other original frequencies, then pair and sum
1.1givenL1construct

Set Q=qr and split the original indices of Λ into r residue classes Λν. Each class has successive ratios at least Q≥3. Set ελ=aλ/∣aλ∣ when aλ≠0, and set it to 1 otherwise. By [L1], the product Pν=∏λ∈Λν(1+Re⁡(ελeλ)) is nonnegative, has integral one, and has the prescribed coefficients on its class. Empty classes use the product 1.

2.1step 1.1givenalgebra

Every nonzero frequency m in the product expansion is a signed sum of distinct frequencies of Λν. If L is its largest contributing frequency, the sum of the smaller frequencies is less than L/(Q−1), so ∣∣m∣−L∣<LQ−1<(1−1q)L. Every other frequency of the original sequence is at most L/q or at least qL; in the latter case its distance from L is at least (q−1)L>(1−1/q)L. Thus if ∣m∣ belongs to the original sequence it must equal L, which lies in this class. In particular P^ν(−λ)=0 for λ∈Λ∖Λν.

3.1step 1.1step 2.1L1L2

Finite character integration, [L1], and this vanishing give ∫01FPν=12∑λ∈Λν∣aλ∣. For completeness, if z=∫FPν≠0, multiplication by z‾/∣z∣ and taking real parts gives ∣z∣≤∫∣F∣Pν; the same inequality is immediate if z=0. Apply [L2] to the real functions ∣F∣ and Pν to obtain 12∑λ∈Λν∣aλ∣≤∫01∣F∣Pν≤∥F∥∞.

4.1step 3.1algebra∎

Summing over the r classes yields ∑λ∈Λ∣aλ∣≤2r∥F∥∞. The constant depends only on q and r, not on the finite support or coefficients, so this is the Sidon inequality.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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