ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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.

A one-frequency Fourier layer on the circle

Example

On the one-dimensional torus, let $v (x) = \sin (2 π x)$ and use a Fourier cutoff $K \geq 1$ . If the spectral matrices satisfy $R_{1} = R_{- 1} = 1$ and all other retained matrices vanish, then the spectral part of the layer returns $v$ exactly. If the cutoff is $K = 0$ , its spectral part is zero because $\hat{v} (0) = 0$ . These finite-mode computations illustrate the layer definition and make no approximation or universality claim for the full Fourier neural-operator architecture.

Example references

Kovachki et al., §4.4, equation (26): finite Fourier-mode parameterization

Kovachki et al., §4.4, equation (26): Fourier-layer convention

Facts & Assumptions

Given: $v (x) = \sin (2 π x)$ on $T = R / Z$ and the Fourier coefficient convention in the Fourier neural-operator layer definition.

[F1]

The Fourier coefficient of $e^{2 π i k x}$ at index $j$ is $1$ if $j = k$ and $0$ otherwise, by integrating the exponential over one period.

Verification

Proof strategy: compute the two nonzero Fourier coefficients.

1.1givenF1algebra

Using $\sin (2 π x) = (e^{2 π i x} - e^{- 2 π i x}) / (2 i)$ and [F1], $\hat{v} (1) = 1 / (2 i)$ , $\hat{v} (- 1) = - 1 / (2 i)$ , and every other coefficient is zero.

2.1step 1.1algebra∎

With $R_{1} = R_{- 1} = 1$ , the retained sum is $e^{2 π i x} / (2 i) - e^{- 2 π i x} / (2 i) = v (x)$ . At cutoff zero, the sum has only the $k = 0$ term, which vanishes because $\hat{v} (0) = 0$ .

Depends on

Fourier neural-operator layer

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

Kovachki et al., Neural Operator: Learning Maps Between Function Spaces With Applications to PDEs (standard reference, not scraped)