ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27

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.

A rectangle contour evaluates the Gaussian cosine integral

Example

For every real $b$ , $\int_{0}^{\infty} e^{- x^{2}} \cos (2 b x) d x = \frac{\sqrt{π}}{2} e^{- b^{2}} .$

Facts & Assumptions

Given: A real number $b$ and the entire function $F (z) = e^{- z^{2}} e^{2 i b z}$ .

[L1]

An entire function has zero integral on every rectangle contour (The residue theorem for a null-homologous cycle).

[L2]

The Gaussian integral is $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ (The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ ).

Verification

technique · computation

1.1L1

Integrate $F$ around the rectangle with vertices [given, L1] $- T, T, T + i b, - T + i b$ . Since $F$ is entire, makes the total integral $0$ . The vertical sides vanish as $T \to \infty$ because $∣ F (x + i y) ∣ = e^{- x^{2} + y^{2} - 2 b y}$ and therefore decays like $e^{- T^{2}}$ there.

2.1step 1.1algebra

The top horizontal side is traversed from $T + i b$ to $- T + i b$ and therefore contributes $- e^{- b^{2}} \int_{- T}^{T} e^{- x^{2}} d x .$ Hence step 1.1 gives $\int_{- T}^{T} e^{- x^{2}} e^{2 i b x} d x = e^{- b^{2}} \int_{- T}^{T} e^{- x^{2}} d x + o (1) .$

3.1step 2.1L2∎

Letting $T \to \infty$ and using [L2] yields $\int_{- \infty}^{\infty} e^{- x^{2}} e^{2 i b x} d x = e^{- b^{2}} \sqrt{π} .$ Taking real parts and then using the evenness of $e^{- x^{2}} \cos (2 b x)$ gives the half-line formula.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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

L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4 §5.3 (standard reference, not scraped)