ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Clustered sources and absolute l1 error

Statement

Let $0 < δ < 1 / 4$ , take the one-dimensional type-1 data $x_{0} = 1 / 4, x_{1} = 1 / 4 + δ, c_{0} = 1, c_{1} = - 1,$ and include mode $k = 1$ . For every real $δ$ in this range, $∥ c ∥_{1} = 2$ while $F_{1} = e^{- π i / 2} (1 - e^{- 2 π i δ}), ∣ F_{1} ∣ \leq 2 π δ .$ Thus this exact Fourier coefficient tends to zero as the source points cluster, although the coefficient l1 norm remains $2$ . The dyadic subfamily, for example $δ = 2^{- n}$ with $n \geq 3$ , consists of admissible exact input coordinates and also tends to zero. For any such dyadic datum for which the algorithm has a successful run, the theorem gives an absolute l1-scaled error certificate; the exact family has no positive lower bound on $∣ F_{1} ∣$ from which that certificate alone yields a relative-error guarantee.

Facts & Assumptions

Given: $0 < δ < 1 / 4$ , the displayed two-source type-1 data, and a mode box with $K_{1} \geq 1$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): the successful-run error theorem assumes Countable Choice through the Gaussian Poisson-summation supplier.

[F1]

Type-1, type-2, and type-3 nonuniform Fourier transforms: $F_{1} = \sum_{j} c_{j} e^{- 2 π i x_{j}}$ .

[F2]

Certified type-1 Gaussian gridding error and type-2 adjoint bound: for any successful type-1 run on admissible finite dyadic data, the error is bounded absolutely by $ϵ_{a n a} ∥ c ∥_{1} + B_{r o u n d}$ ; success is conditional on the supplied candidate and arithmetic controls.

[F3]

$\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , and The derivatives of sine and cosine are cosine and minus sine: the complex exponential is additive-to-multiplicative, $e^{i t} = \cos t + i \sin t$ , $∣ e^{i t} ∣ = 1$ , and $(\sin t)^{'} = \cos t$ .

[F4]

Pythagorean and parity identities for all six trigonometric functions on their natural domains: $∣ \cos t ∣ \leq 1$ for real $t$ .

[F5]

Elementary factorial and geometric series converge uniformly, Real elementary functions and their domains, and The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : cosine is continuous and integrable on each compact interval, the integral obeys $∣ \int_{a}^{b} h ∣ \leq ∣ b - a ∣ \max ∣ h ∣$ , and integrating the derivative of sine gives $\sin t = \int_{0}^{t} \cos s d s$ .

[F6]

Real elementary functions and their domains: $π = 4 \int_{0}^{1} (1 + s^{2})^{- 1} d s \geq 2 > 0$ .

[F7]

Finite complex-array norms used by the NUFFT certificates: $∥ c ∥_{1} = \sum_{j} ∣ c_{j} ∣$ for the displayed two-entry array.

[F8]

Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive and Real and imaginary parts, complex conjugation, and modulus: $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ , $∣ i ∣ = 1$ , and $∣ a ∣ = a$ for $a \geq 0$ .

Proof

1.1givenF1F7algebra

Since $c_{0} = 1$ and $c_{1} = - 1$ , [F7] gives $∥ c ∥_{1} = ∣ 1 ∣ + ∣ - 1 ∣ = 2$ . For mode $1$ , substitute the source locations into [F1] to obtain $F_{1} = e^{- 2 π i / 4} - e^{- 2 π i (1 / 4 + δ)} = e^{- π i / 2} (1 - e^{- 2 π i δ}) .$ This is a direct factorization of the exact two-term sum.

2.1A1F2F3F4F5F6F7F8step 1.1algebra∎

Put $t = π δ$ . By the complex exponential addition law and [F3], $1 - e^{- 2 i t} = e^{- i t} (e^{i t} - e^{- i t}) = e^{- i t} (2 i \sin t),$ so $∣ 1 - e^{- 2 i t} ∣ = 2 ∣ \sin t ∣$ by [F3] and [F8]. From [F3]–[F5], for $t \geq 0$ we have $∣ \sin t ∣ = ∣ \int_{0}^{t} \cos s d s ∣ \leq t \max_{0 \leq s \leq t} ∣ \cos s ∣ \leq t .$ Since $t = π δ > 0$ by [F6] and $∣ e^{- π i / 2} ∣ = 1$ , step 1.1 yields $∣ F_{1} ∣ \leq 2 t = 2 π δ$ . Taking the dyadic sequence $δ = 2^{- n}$ with $n \geq 3$ shows that admissible exact input coefficients can have $∣ F_{1} ∣$ arbitrarily small while step 1.1 keeps $∥ c ∥_{1} = 2$ by [F7]. Whenever a successful run is available for one of these inputs, [F2] gives an absolute bound without division by $∣ F_{1} ∣$ ; thus the certificate alone supplies no uniform relative-error estimate without an additional lower bound on the exact output.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

76 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.