Pipeline-generated

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.

✓ 3 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 3 also cleared it.

Nonuniform fast fourier transforms — Examples

1 · Prerequisites

2 · Summary

These examples compute exact samples for a finite two-point MRI object, show how near-canceling clustered sources keep their input l1 norm fixed as one Fourier coefficient becomes small, and verify a finite-format branch where a positive Gaussian multiplier cannot receive a positive dyadic lower bound. The MRI example is a point-source Fourier model only; none of the examples asserts an acquisition or reconstruction result.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Exact MRI Fourier samples from a two-point object

Statement

Consider a two-point object in $T^{2} = [0, 1)^{2}$ with locations $x_{0} = (1 / 4, 0), x_{1} = (1 / 2, 1 / 4),$ and weights $c_{0} = 1, c_{1} = 2$ . At the two type-3 frequency samples $ξ_{0} = (0, 0), ξ_{1} = (1 / 3, 1 / 5),$ the exact nonuniform Fourier samples are $G_{0} = 3, G_{1} = e^{- 2 π i / 12} + 2 e^{- 2 π i (13 / 60)} .$ These are finite Fourier samples of a point-source model of an MRI object; no acquisition or reconstruction claim is made.

Facts & Assumptions

Given: The two locations, weights and frequency samples stated above.

[F1]

Type-1, type-2, and type-3 nonuniform Fourier transforms: a type-3 sample is $G_{ℓ} = \sum_{j} c_{j} e^{- 2 π i ξ_{ℓ} \cdot x_{j}}$ for finite real source and frequency lists.

[F2]

The complex exponential by its power series: its power series defines every displayed value, and substituting $z = 0$ gives $e^{0} = 1$ .

Proof

1.1F1F2givenalgebra

For $ξ_{0} = (0, 0)$ , both dot products are zero, so [F1] gives $G_{0} = 1 \cdot e^{0} + 2 \cdot e^{0} = 3$ .

2.1F1F2givenalgebra∎

For $ξ_{1} = (1 / 3, 1 / 5)$ , the dot products are $ξ_{1} \cdot x_{0} = 1 / 12$ and $ξ_{1} \cdot x_{1} = 1 / 6 + 1 / 20 = 13 / 60$ . Substituting these and the weights in [F1] yields $G_{1} = e^{- 2 π i / 12} + 2 e^{- 2 π i (13 / 60)}$ , as claimed.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A positive mode multiplier too small to certify

Statement

Use the dyadic interval format with precision $p = 5$ and exponent limits $e_{\min} = - 2$ , $e_{\max} = 8$ , and select the matching operationwise model with a valid unit-roundoff bound $u = 1 / 32$ . Set the common range truncation index to $J = 64$ , twiddle bound to $ϵ_{t w} = 1 / 32$ , phase tolerance to $δ_{ϕ} = 1 / 32$ , phase precisions to $p_{ϕ, 0} = 5$ and $p_{ϕ, \max} = 8$ , and the FFT recursion cap to $d_{F F T} = 4$ . Give the algorithm one type-1 source $x_{0} = 0, c_{0} = 1$ , mode bound $K = 7$ , one candidate $τ = 1 / 40$ , $M = 16$ , $w = L = 1$ , and requested positive absolute tolerance $ε_{r e q} = 1$ . Its least positive subnormal is $η = 2^{- 6} = 1 / 64$ . The exact smallest deconvolution multiplier $d_{\min} = \sqrt{1 / 40} e^{- 49 π / 40}$ is positive but less than $η$ . Therefore a finite outward dyadic lower endpoint for this multiplier cannot be positive, and the algorithm must reject the candidate as inconclusive at its positive-lower-bound check (or at an earlier range check); it cannot return a certified result using this candidate.

Facts & Assumptions

Given: The displayed one-dimensional candidate and dyadic format, with $p = 5$ , $e_{\min} = - 2$ , $e_{\max} = 8$ , and $u = 1 / 32$ .

[F1]

Dyadic floating-point format and directed rounding: the least positive subnormal is $2^{e_{\min} - p + 1}$ , and every positive finite representable number is at least that value.

[F2]

Real elementary functions and their domains: $e^{x} = \sum_{n = 0}^{\infty} x^{n} / n!$ .

[F3]

The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ and The exponential function is strictly increasing: $e^{x} > 0$ , $e^{- x} = 1 / e^{x}$ , and the real exponential is strictly increasing.

[F4]

Certified Gaussian gridding for type 1 and type 2: the candidate requires a positive certified lower endpoint for $d_{\min}$ and rejects it if the lower endpoint is nonpositive; a non-finite elementary-range result is also inconclusive.

[F5]

Nonnegative real square roots exist uniquely: the nonnegative square root of a positive number is positive and order comparisons follow from squaring nonnegative quantities.

[F6]

Real elementary functions and their domains: $π = 4 \int_{0}^{1} (1 + t^{2})^{- 1} d t \geq 2 > 0$ , since the integrand is at least $1 / 2$ on $[0, 1]$ .

Proof

1.1givenF1F2F3F5F6algebra

The format's subnormal spacing is $η = 2^{- 2 - 5 + 1} = 2^{- 6} = 1 / 64$ by [F1], and the exact multiplier is positive by [F3], [F5] and $τ = 1 / 40 > 0$ . Since $1 / 40 < 1 / 36 = (1 / 6)^{2}$ , [F5] gives $\sqrt{1 / 40} < 1 / 6$ ; also $π \geq 2$ by [F6]. Thus $d_{\min} = \sqrt{1 / 40} e^{- 49 π / 40} < \frac{1}{6} e^{- 49 / 20} .$ For $x = 49 / 20 > 0$ , the positive exponential series gives $e^{x} > \sum_{n = 0}^{5} \frac{x^{n}}{n!} = \frac{4,277,427,349}{384,000,000} > \frac{32}{3} .$ Taking positive reciprocals therefore yields $d_{\min} < \frac{1}{6} \cdot \frac{3}{32} = 1 / 64 = η$ .

2.1F1F4step 1.1algebra∎

By [F1], any positive finite dyadic endpoint is at least $η$ . A sound lower endpoint for the exact multiplier must be at most $d_{\min} < η$ by step 1.1, so it cannot be positive. The algorithm's explicit check [F4] consequently rejects this candidate as inconclusive if its finite multiplier enclosure is reached; if an earlier range operation is non-finite, [F4] gives the same inconclusive outcome. Thus this candidate cannot yield a certified transform result.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

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.

Sources

Leslie Greengard and June-Yub Lee, Accelerating the Nonuniform Fast Fourier Transform