ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 smooth scattered surface inherits the Matérn fill-distance rate

Example

Assume the Axiom of Choice and Countable Choice as required by the Fourier-space and interpolation suppliers. Fix $d \geq 1$ , $ν > 0$ , $a > 0$ , and let $Ω = (0, 1)^{d}$ . The smooth graph ${(x, f (x)) : x \in \overline{Ω}}$ with $f (x) = e^{- π ∣ x ∣^{2}}$ is interpolated from midpoint-grid samples by the normalized Matérn kernel of smoothness $ν$ .

Facts & Assumptions

Given: Full AC, Countable Choice, the fixed $d, ν, a$ , the cube, the function $f$ , and midpoint grids $X_{m} = {(\frac{i_{1} + 1 / 2}{m}, \dots, \frac{i_{d} + 1 / 2}{m}) : 0 \leq i_{j} < m}, m \in N, m \geq 1.$

[F1]

An admitted domain is nonempty, bounded and Lipschitz and has a single cone radius and aperture at every point of the closure; the fill distance is $h_{X} = \sup_{x \in Ω} \min_{y \in X} ∣ x - y ∣$ . (Radial kernels, polynomial augmentation, and site geometry)

[F2]

Every Schwartz function is in the Fourier Bessel-potential space $H^{s} (R^{d})$ for every $s > d / 2$ , and $H^{s} (Ω)$ consists of restrictions of whole-space members. (Schwartz functions are dense in the Fourier Bessel-potential norm, Fourier Bessel-potential and restriction-quotient Sobolev spaces)

[F3]

The real exponential is smooth with derivative itself; repeated coordinatewise chain and product rules show every partial derivative of $f$ is a finite sum of polynomial multiples of $e^{- π ∣ x ∣^{2}}$ . (The exponential function is smooth and $(\exp)^{'} = \exp$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ )

[F4]

The Schwartz seminorms require polynomially weighted derivatives to be bounded. For any degree $M \geq 0$ , take an integer $n \geq 1$ with $2 n \geq M$ ; for $r \geq 1$ , $r^{M} \leq r^{2 n}$ and exponential domination applied with $x = r^{2}$ gives $r^{2 n} e^{- π r^{2}} \to 0$ . On $∣ x ∣ \leq 1$ , each polynomial is bounded by the sum of the absolute values of its finitely many coefficients. (Schwartz space and its seminorms, The exponential dominates every fixed nonnegative integer power at $+ \infty$ )

[F5]

The Matérn interpolation error and power function are bounded by $C h_{X}^{ν}$ on an admitted cone domain for small fill distance. (Matérn interpolation and its power function converge at rate h^ν)

Proof technique: verify the domain, regularity, and grid radius, then apply the fill-distance theorem.

Verification

technique · verify the domain, regularity, and grid radius, then apply the fill-distance theorem

Given: The data above.

1.1F1givenconstructalgebra

The cube is bounded and Lipschitz. At a boundary point $p$ , let $I$ be the nonempty set of active coordinates ( $p_{j} = 0$ or $1$ ), with inward signs $σ_{j} = 1$ at $0$ and $- 1$ at $1$ . Put $u_{j} = σ_{j} / \sqrt{∣ I ∣}$ for $j \in I$ and $u_{j} = 0$ otherwise. In the orthogonal coordinates $x = p + y + t u$ with $y ⊥ u$ , a sufficiently small neighborhood has no constraints from inactive coordinates, and the active inequalities reduce to $t > \max_{j \in I} (- \sqrt{∣ I ∣} σ_{j} y_{j}) .$ This is the epigraph of a finite maximum of linear functions, hence a local Lipschitz graph with the cube on one side. The cube also satisfies the uniform cone condition: for $x \in [0, 1]^{d}$ , let $σ_{j} = 1$ if $x_{j} \leq 1 / 2$ and $σ_{j} = - 1$ otherwise, and put $u = (σ_{1}, \dots, σ_{d}) / \sqrt{d}$ . If $u = e_{1}$ let $Q_{x} = I$ ; otherwise put $v = (e_{1} - u) / ∣ e_{1} - u ∣$ and $Q_{x} = I - 2 v v^{T}$ , which is orthogonal and sends $e_{1}$ to $u$ . Choose $0 < θ < π / 2$ with $\cos θ / \sqrt{d} - \sin θ > 0$ , and set $r_{0} = 1 / 2$ . For any cone vector $z$ , $z_{1} > ∣ z ∣ \cos θ$ and $∣ z - z_{1} e_{1} ∣ < ∣ z ∣ \sin θ$ . Hence for every coordinate, $σ_{j} (Q_{x} z)_{j} \geq z_{1} / \sqrt{d} - ∣ z - z_{1} e_{1} ∣ > ∣ z ∣ (\cos θ / \sqrt{d} - \sin θ) > 0$ . Each coordinate moves toward the cube's interior by less than $r_{0}$ , so $x + Q_{x} z \in (0, 1)^{d}$ .

2.1F2F3F4step 1.1algebra

The sites in $X_{m}$ are distinct. Each $x \in (0, 1)^{d}$ is at coordinatewise distance at most $1 / (2 m)$ from a midpoint in each grid interval, so $h_{X_{m}} \leq \sqrt{d} / (2 m) \to 0$ . By [F3], every partial derivative of $f$ is a finite sum of polynomial multiples of $e^{- π ∣ x ∣^{2}}$ ; [F4] makes every polynomially weighted derivative bounded, so $f$ is Schwartz. Then [F2] gives $f ∣_{Ω} \in H^{s} (Ω)$ for $s = ν + d / 2$ .

3.1F5step 2.1algebra∎

For all sufficiently large $m$ , step 2.1 gives $h_{X_{m}} \leq h_{0}$ from [F5]. The Matérn interpolation theorem therefore yields $∥ f - s_{X_{m}} f ∥_{L^{\infty} (Ω)} \leq C h_{X_{m}}^{ν} ∥ f ∥_{H^{s} (Ω)} \leq C {(\frac{\sqrt{d}}{2 m})}^{ν} ∥ f ∥_{H^{s} (Ω)}, \sup_{x \in Ω} P_{X_{m}} (x) \leq C {(\frac{\sqrt{d}}{2 m})}^{ν} .$ The graph samples are the scattered surface data, and the bound uses fill distance alone; no mesh-ratio condition is needed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

63 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

Narcowich, Ward, and Wendland, Sobolev bounds on functions with scattered zeros, Math. Comp. 74 (2005), Theorem 1.1 (standard reference, not scraped)
Gregory E. Fasshauer, MATH 590: Meshfree Methods, Chapter 13, pp. 34–36 (standard reference, not scraped)