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.

Triangle function and squared sinc

Example

Assume countable choice. The triangle $T (x) = \max (1 - ∣ x ∣, 0)$ on $R$ has $\hat{T} (ξ) = (\sin (π ξ) / (π ξ))^{2}$ , with value one at zero.

Facts & Assumptions

Given: The Axiom of Countable Choice ( ${A C}_{ω}$ ) and $I = 1_{[- 1 / 2, 1 / 2]}$ .

[F1]

The interval indicator I has sinc transform, with value one at zero (Transform of an interval indicator).

[F2]

Fourier turns integrable convolution into multiplication (Fourier transform turns L1 convolution into multiplication).

Verification

1.1

The integral $(I * I) (x)$ is the length of $[- 1 / 2, 1 / 2] \cap [x - 1 / 2, x + 1 / 2]$ . For $0 \leq x \leq 1$ this length is $1 - x$ ; for $- 1 \leq x \leq 0$ it is $1 + x$ ; for $∣ x ∣ > 1$ the intervals are disjoint. At $∣ x ∣ = 1$ the intersection is a null singleton. Thus $I * I = T$ everywhere.

given

2.1

By F1 and F2, $\hat{T} = {\hat{I}}^{2}$ gives the displayed squared sinc. At zero the value is one, also equal to $\int_{- 1}^{1} (1 - ∣ x ∣) d x = 2 [x - x^{2} / 2]_{0}^{1} = 1$ . Countable choice is inherited from the indicator and convolution suppliers.

F1F2step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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)