Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30
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.

The Laplace fundamental solution is harmonic off its pole

Statement

Assume Countable Choice and n≥2. The displayed Φ is smooth on Rn∖{0} and satisfies ΔΦ=0 there; for every pole y, x↦Φ(x−y) is harmonic on Rn∖{y}.

Facts & Assumptions

Given: ACω, n≥2, and the kernel Φ with the normalization fixed in Fundamental solution for the positive operator minus Laplacian.

[A1]

Countable Choice, written ACω, is the assumption retained from the kernel convention (The Axiom of Countable Choice (ACω)). The differentiation argument below does not use choice.

[F1]

For n≥3, Φ(x)=∣x∣2−n/((n−2)ωn−1) away from zero; for n=2, Φ(x)=−(2π)−1log⁡∣x∣ (Fundamental solution for the positive operator minus Laplacian).

[F2]

A scalar function is Ck when all iterated coordinate derivatives through order k exist and are continuous (Ck maps and multi-index derivative notation in Euclidean space).

[F3]

A Euclidean map is Ck when each component is Ck (Ck Euclidean maps and diffeomorphisms).

[F4]

Finite sums and products and compositions of Ck Euclidean maps are Ck (Ck Euclidean maps are closed under componentwise algebra and composition).

[F5]

The total chain rule gives D(g∘f)=Dg(f)∘Df (The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a)).

[F6]

A total derivative's matrix gives the coordinate partial derivatives (A total derivative computes every directional derivative, and its matrix is the Jacobian).

[F7]

For t>0, (tα)′=αtα−1 for every real α (Continuity and derivatives of positive-base real powers).

[F10]

The Laplacian is the sum of the pure second coordinate partials (The Laplacian of a C2 function and of a C2 vector field).

[F11]

A C2 function whose Laplacian vanishes is harmonic (The Laplacian of a C2 function and of a C2 vector field).

[F12]

Induction on the natural numbers proves a property once its base case and successor step hold (The principle of mathematical induction).

Proof

technique · direct
1.1F2F7F8F9F12inductionalgebra

For any real α, induction on j using [F12] and [F7] gives (tα)(j)=cjtα−j on (0,∞), where c0=1 and cj+1=cj(α−j). Each derivative is continuous by the real-power continuity in [F7], so tα is smooth under [F2]. Also log⁡′(t)=t−1 by [F8]; applying the same derivative calculation to t−1 shows every higher derivative of log⁡t exists and is continuous. Thus both radial profiles used in [F1] are smooth for t>0.

2.1F1F2F3F4F7step 1.1algebra

On U=Rn∖{0}, put s(x)=∑i=1nxi2. Its coordinate functions and their finite sums and products are smooth by direct coordinate differentiation and [F2]–[F4]. Since s(x)>0 on U, the radius r(x)=s(x)1/2 is smooth there by [F7], step 1.1, and closure under composition [F4]. Composing r with the power profile for n≥3 or the logarithm profile for n=2 proves that Φ is smooth on U.

3.1F2F5F6F7F9F10step 1.1step 2.1algebra

For a smooth radial profile q(r) and r=∣x∣>0, the chain rule [F5] and partial-derivative formula [F6] give ∂iq(r)=q′(r)xi/r. Differentiating again by the chain and product rules [F5], [F7] and [F9] gives ∂i2q(r)=q′′(r)xi2/r2+q′(r)(1/r−xi2/r3). Summing over i and using ∑ixi2=r2 and the Laplacian definition [F10] yields Δq(r)=q′′(r)+(n−1)q′(r)/r. The calculation is on r>0, where all derivatives used exist by steps 1.1 and 2.1.

4.1F1F7F8F9step 3.1casesalgebra

If n≥3, set q(r)=r2−n/((n−2)ωn−1). Then q′(r)=−r1−n/ωn−1 and q′′(r)=(n−1)r−n/ωn−1 by [F7] and [F9], so step 3.1 gives ΔΦ=0. If n=2, set q(r)=−(2π)−1log⁡r. Then q′(r)=−(2πr)−1 by [F8]–[F9] and q′′(r)=(2πr2)−1 by applying [F7] to r−1; hence q′′+q′/r=0. These cases exhaust n≥2.

5.1A1F4F5F11step 2.1step 4.1algebra∎

For fixed y, translation x↦x−y has affine coordinate functions, so direct differentiation gives its identity derivative and zero higher derivatives. The chain rule [F5] therefore gives Δx(Φ(x−y))=(ΔΦ)(x−y)=0 whenever x≠y. The translated function is smooth there by [F4], hence is harmonic by [F11]. The assumption ACω in [A1] is carried from the kernel convention but is not used in these pointwise derivative calculations.

Depends on

Used by

Dependency tree · two levels

62 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