Alphabeta Math
Pipeline-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.

✓ 3 results · all verified · 2 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Radial basis and kernel interpolation — Examples

1 · Prerequisites

2 · Summary

The examples apply the Matérn fill-distance theorem to a smooth Gaussian graph on a cube, show that duplicate sites make the Gram matrix singular, and construct near-duplicate sites whose exact condition numbers diverge even as fill distance tends to zero. The last example isolates separation from fill distance; it makes no floating-point solver or stabilization claim.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Duplicate sites make the kernel Gram matrix singular

Example

Let K(x,y)=ϕ(∣x−y∣) be any radial kernel, and let a site list contain x1=x2.

Facts & Assumptions

Given: A radial kernel and a finite site list with x1=x2.

[F1]

A radial kernel has Gram entries Kij=ϕ(∣xi−xj∣), and ordinary RBF interpolation is defined on distinct sites. (Radial kernels, polynomial augmentation, and site geometry)

Verification

1.1F1givenalgebra

For every row index i, the equal sites give Ki1=ϕ(∣xi−x1∣)=ϕ(∣xi−x2∣)=Ki2. Thus the first two columns, and by symmetry the first two rows, coincide.

2.1step 1.1F1algebra∎

The nonzero vector e1−e2 is therefore in the nullspace of the Gram matrix, so the matrix is singular. This example violates the distinct-site hypothesis in [F1] and is not a counterexample to the interpolation theorem.

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passOpen item page →

A small fill distance can coexist with poor separation and conditioning

Example

Assume Countable Choice. For fixed d≥1, ν>0, and a>0, let Xm be the midpoint grid in Ω=(0,1)d for each odd m≥3. There are 0<δm<1/(4m2) such that the augmented sets Zm=Xm∪{x0+δme1}, with x0=(1/2,…,1/2), satisfy hZm→0, ρZm→∞, and κ2(KZm)→∞ for the normalized Matérn kernel.

Facts & Assumptions

Given: Countable Choice, odd integers m≥3, the midpoint grid Xm={(i1+1/2m,…,id+1/2m):0≤ij<m}, its central site x0=(1/2,…,1/2), and the normalized Matérn kernel k.

[F1]

An admitted domain is nonempty, bounded and Lipschitz and has the uniform cone condition; hX=sup⁡x∈Ωmin⁡y∈X∣x−y∣, qX=12min⁡i≠j∣xi−xj∣, and ρX=hX/qX. (Radial kernels, polynomial augmentation, and site geometry)

[F2]

The normalized Matérn kernel is continuous and satisfies k(0)=1. (The Matérn spectral integral, normalization, and radial formula)

[F3]

For distinct sites with qX≤1, the exact Gram matrix is positive definite; its smallest eigenvalue is the minimum Rayleigh quotient, and a real symmetric matrix has an orthonormal eigenbasis. (Separated Matérn sites have a positive Gram lower bound, The smallest and largest eigenvalues of a self-adjoint endomorphism are the minimum and maximum Rayleigh quotients, Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis)

[F4]

The condition number is κ2(K)=∥K∥2∥K−1∥2, and the induced 2-norm is the supremum of ∥Kv∥2 over unit vectors. (The condition number kappa_p(A) = ||A||_p ||A^{-1}||_p of a nonsingular linear system, The matrix norm induced by a published vector p-norm)

Verification

technique · add a near-duplicate and test its normalized difference vector

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 (pj=0 or 1), with inward signs σj=1 at 0 and −1 at 1. Put uj=σj/∣I∣ for j∈I and uj=0 otherwise. In the orthogonal coordinates x=p+y+tu with y⊥u, a sufficiently small neighborhood has no constraints from inactive coordinates, and the active inequalities reduce to t>max⁡j∈I(−∣I∣ σjyj). 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∈[0,1]d, choose signs σj=1 if xj≤1/2 and −1 otherwise, and put u=(σ1,…,σd)/d. If u=e1 take Qx=I; otherwise put v=(e1−u)/∣e1−u∣ and Qx=I−2vvT, which is orthogonal and sends e1 to u. Choose 0<θ<π/2 with cos⁡θ/d−sin⁡θ>0, and set r0=1/2. For any cone vector z, z1>∣z∣cos⁡θ and ∣z−z1e1∣<∣z∣sin⁡θ. Hence σj(Qxz)j≥z1/d−∣z−z1e1∣>∣z∣(cos⁡θ/d−sin⁡θ)>0 for each coordinate. Each coordinate moves toward the cube's interior by less than r0, so x+Qxz∈(0,1)d.

1.2F1F2F3givenchoosealgebra

Distinct midpoint sites have fill distance at most d/(2m). Since m is odd, x0∈Xm. By continuity in [F2], choose ϵm>0 so that ∣1−k(δe1)∣<1/m whenever 0<δ<ϵm, then choose 0<δm<min⁡{ϵm,1/(4m2)}. Strict positive definiteness for x0 and x0+δme1 makes 1−k(δme1)>0, so 0<1−k(δme1)<1/m. Put Zm=Xm∪{x0+δme1}. The new site is inside the cube because δm<1/(4m2)<1/2. Every other grid site is at distance at least 1/m from x0, while δm<1/(4m2)<1/(2m), so the new site is distinct from all grid sites. At the boundary corner 0, the nearest grid point is (1/(2m),…,1/(2m)), at distance d/(2m); the new site has squared distance d/4+δm+δm2>d/(4m2), so min⁡z∈Zm∣z∣=d/(2m). For Dm(x)=min⁡z∈Zm∣x−z∣, the triangle inequality gives ∣Dm(x)−Dm(y)∣≤∣x−y∣. Since xn=(1/n,…,1/n)∈Ω for n≥2 and xn→0, Dm(xn)→Dm(0); the fill-distance supremum therefore satisfies hZm≥d/(2m)≥1/(2m). Adding a site cannot increase fill distance, so also hZm≤d/(2m)→0. The separation radius satisfies 0<qZm≤δm/2<1/(8m2); consequently ρZm=hZm/qZm>4m→∞.

2.1F2F3F4step 1.2algebra∎

Let u be the unit vector with entries 1/2 and −1/2 at the new site and x0, and zero elsewhere. The corresponding Rayleigh quotient is uTKZmu=12(1+1−2k(δme1))=1−k(δme1). Hence [F3] gives 0<λmin⁡(KZm)≤1−k(δme1)<1/m. By [F3] choose an orthonormal eigenbasis Q and write KZm=QΛQT. Since every diagonal entry is 1, tr⁡KZm=∣Zm∣=∑i,jqij2λj=∑jλj, so λmax⁡(KZm) is at least the average eigenvalue, namely 1. For a unit vector v=Qc, orthogonality gives ∥KZmv∥22=∑jλj2cj2≤λmax⁡(KZm)2, with equality at a top eigenvector; the same calculation for KZm−1 gives induced 2-norm 1/λmin⁡(KZm). Thus [F4] gives κ2(KZm)=λmax⁡(KZm)/λmin⁡(KZm)>m. Together with step 1.2, this gives hZm→0, ρZm→∞, and condition number tending to infinity.

ExampleConstruction: AI-generatedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

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≥1, ν>0, a>0, and let Ω=(0,1)d. The smooth graph {(x,f(x)):x∈Ω‾} 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 Xm={(i1+1/2m,…,id+1/2m):0≤ij<m},m∈N,m≥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 hX=sup⁡x∈Ωmin⁡y∈X∣x−y∣. (Radial kernels, polynomial augmentation, and site geometry)

[F2]

Every Schwartz function is in the Fourier Bessel-potential space Hs(Rd) for every s>d/2, and Hs(Ω) 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)

[F4]

The Schwartz seminorms require polynomially weighted derivatives to be bounded. For any degree M≥0, take an integer n≥1 with 2n≥M; for r≥1, rM≤r2n and exponential domination applied with x=r2 gives r2ne−πr2→0. On ∣x∣≤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 +∞)

[F5]

The Matérn interpolation error and power function are bounded by ChXν 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 (pj=0 or 1), with inward signs σj=1 at 0 and −1 at 1. Put uj=σj/∣I∣ for j∈I and uj=0 otherwise. In the orthogonal coordinates x=p+y+tu with y⊥u, a sufficiently small neighborhood has no constraints from inactive coordinates, and the active inequalities reduce to t>max⁡j∈I(−∣I∣ σjyj). 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∈[0,1]d, let σj=1 if xj≤1/2 and σj=−1 otherwise, and put u=(σ1,…,σd)/d. If u=e1 let Qx=I; otherwise put v=(e1−u)/∣e1−u∣ and Qx=I−2vvT, which is orthogonal and sends e1 to u. Choose 0<θ<π/2 with cos⁡θ/d−sin⁡θ>0, and set r0=1/2. For any cone vector z, z1>∣z∣cos⁡θ and ∣z−z1e1∣<∣z∣sin⁡θ. Hence for every coordinate, σj(Qxz)j≥z1/d−∣z−z1e1∣>∣z∣(cos⁡θ/d−sin⁡θ)>0. Each coordinate moves toward the cube's interior by less than r0, so x+Qxz∈(0,1)d.

2.1F2F3F4step 1.1algebra

The sites in Xm are distinct. Each x∈(0,1)d is at coordinatewise distance at most 1/(2m) from a midpoint in each grid interval, so hXm≤d/(2m)→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∣Ω∈Hs(Ω) for s=ν+d/2.

3.1F5step 2.1algebra∎

For all sufficiently large m, step 2.1 gives hXm≤h0 from [F5]. The Matérn interpolation theorem therefore yields ∥f−sXmf∥L∞(Ω)≤ChXmν∥f∥Hs(Ω)≤C(d2m)ν∥f∥Hs(Ω),sup⁡x∈ΩPXm(x)≤C(d2m)ν. The graph samples are the scattered surface data, and the bound uses fill distance alone; no mesh-ratio condition is needed.

Sources