ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)

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.

Sinc-square integral from Plancherel

Statement

Assume countable choice. With the quotient at zero defined as one, $\int_{R} {(\frac{\sin (π ξ)}{π ξ})}^{2} d ξ = 1.$

Facts & Assumptions

Given: The Axiom of Countable Choice ( ${A C}_{ω}$ ) and the integral transform Fourier transform on complex L1 classes. The sine/cosine derivative and Euler formulas give the complex exponential antiderivative (The derivatives of sine and cosine are cosine and minus sine, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[F1]

The complex interval FTC integrates derivatives to endpoint differences (Complex integration by parts on intervals and decaying lines).

[F2]

The integral transform represents the norm transform on $L^{1} \cap L^{2}$ (Agreement of the integral and L2 transforms).

[F3]

Plancherel preserves the square norm (Plancherel theorem).

Verification

1.1

Set $f = 1_{[- 1 / 2, 1 / 2]}$ . Then $∥ f ∥_{1} = ∥ f ∥_{2}^{2} = 1$ , so $f \in L^{1} \cap L^{2}$ . For $ξ \neq 0$ , [F1] gives $\hat{f} (ξ) = [e^{- 2 π i x ξ} / (- 2 π i ξ)]_{- 1 / 2}^{1 / 2} = (e^{- π i ξ} - e^{π i ξ}) / (- 2 π i ξ) = \sin (π ξ) / (π ξ)$ . For $ξ = 0$ the defining integral is the interval length, one.

F1givenalgebra

2.1

By [F2] and [F3], the square modulus of this explicitly computed transform has integral $∥ F_{2} f ∥_{2}^{2} = ∥ f ∥_{2}^{2} = 1$ . The sinc quotient is real, so its squared modulus is its square, yielding the statement. This supplies integrability of the square as well as its value.

step 1.1F2F3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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

Gerald Teschl, Topics in Real and Functional Analysis (2017) (standard reference, not scraped)