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 kernel integral has a mesh-refinement limit while a fixed-grid map needs a separate interface

Example

On the open domain $D = (0, 1)$ , use the continuous representatives $a \in C ([0, 1])$ and $G (a) \in C ([0, 1])$ , and define $G (a) (x) = \int_{0}^{1} a (y) d y$ for every $x \in [0, 1]$ . Its midpoint-mesh realization with $n$ cells is the constant output $G_{n} (a) (x) = \frac{1}{n} \sum_{j = 1}^{n} a ((j - \frac{1}{2}) / n)$ . For a fixed continuous input $a$ , these outputs converge uniformly in $x$ to $G (a)$ . By contrast, the identity map $F_{n} : R^{n} \to R^{n}$ on a length- $n$ vector is defined on a different input and output space at each $n$ ; without an additional reconstruction rule it is not a single function-space operator that accepts arbitrary meshes and can be queried at arbitrary output points.

Example references

Kovachki et al., Definition 4, Theorem 8, and §1.2: continuum operators versus fixed-grid maps

Kovachki et al., Appendix E: uniform Riemann-sum convergence for operator layers

Facts & Assumptions

Given: A continuous function $a : [0, 1] \to R$ , the integral operator $G$ , and the midpoint quadrature rule in the Example.

[F1]

A continuous function on the compact interval $[0, 1]$ is uniformly continuous.

Verification

Proof strategy: estimate each midpoint cell error by the modulus of continuity.

1.1givenalgebra

Let $I_{j} = [(j - 1) / n, j / n]$ and define $ω_{a} (δ) = \sup {∣ a (x) - a (y) ∣ : x, y \in [0, 1], ∣ x - y ∣ \leq δ}$ . For each $y \in I_{j}$ , $∣ y - (j - \frac{1}{2}) / n ∣ \leq 1 / (2 n)$ , so $∣ \int_{I_{j}} a (y) d y - \frac{1}{n} a ((j - \frac{1}{2}) / n) ∣ \leq \frac{1}{n} ω_{a} (1 / (2 n)) .$ Summing over $j$ gives $∣ G (a) (x) - G_{n} (a) (x) ∣ \leq ω_{a} (1 / (2 n))$ for every $x$ .

2.1step 1.1F1algebra∎

By [F1], $ω_{a} (δ) \to 0$ as $δ ↓ 0$ . The bound in step 1.1 is independent of $x$ , so $G_{n} (a) \to G (a)$ in $C ([0, 1])$ . The dimension of $F_{n}$ changes with $n$ and its definition returns only a length- $n$ vector, so no arbitrary-point output or common function-space domain follows from $F_{n}$ alone.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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