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

Adding an entire harmonic function preserves a Laplace fundamental solution

Statement

If $- Δ E = δ_{0}$ in distributions on $R^{n}$ and $h$ is an entire classical harmonic function, then $- Δ (E + h) = δ_{0}$ . Thus the fundamental solution is not unique without an extra growth or normalization condition.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ , let $n \geq 1$ , let $E \in D^{'} (R^{n})$ satisfy $- Δ E = δ_{0}$ , and let $h \in C^{2} (R^{n}; C)$ satisfy $Δ h = 0$ componentwise. In $E + h$ , the function $h$ denotes its regular distribution.

[A1]

Countable Choice, written ${A C}_{ω}$ , says every sequence of nonempty sets has a choice function. (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

For locally integrable $f$ , the regular functional is $⟨ u_{f}, φ ⟩ = \int f φ$ . (Regular distribution from a locally integrable function).

[F2]

Assuming Countable Choice, each locally integrable function defines a distribution via the regular functional. (Locally integrable functions embed in distributions).

[F3]

Under Countable Choice, if $f \in C^{k} (Ω; C)$ then $\partial^{α} u_{f} = u_{\partial^{α} f}$ for $∣ α ∣ \leq k$ . (Distributional differentiation is continuous and commutes).

[F4]

The Laplacian is $Δ f = \sum_{i} \partial_{i}^{2} f$ , and a $C^{2}$ function with $Δ f = 0$ is harmonic. (The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

[F5]

Distributional derivatives are signed transposes of test derivatives. (Distributional derivative).

[F6]

Distributions are a complex vector space of continuous complex-linear functionals, with a bilinear pairing and no conjugation. (Distribution).

[F7]

A distribution is a fundamental solution for $L$ when $L E = δ_{0}$ . (Fundamental solution of a constant-coefficient operator).

[F8]

For a compact $K \subseteq Ω$ with $Ω$ open, there is $χ \in C_{c}^{\infty} (Ω)$ with $0 \leq χ \leq 1$ equal to one near $K$ . (Test function cutoffs and euclidean localization).

[F9]

Every Euclidean ball of positive radius has positive finite Lebesgue measure under Countable Choice. (Euclidean balls have positive finite Lebesgue measure).

Proof

technique · direct

1.1givenA1F1F2F9

The continuous function $h$ is bounded on each compact set; under [F9] this makes it locally integrable. Define its regular functional $u_{h}$ by [F1]. By [F2] and the stated assumption [A1], $u_{h} \in D^{'} (R^{n})$ .

2.1step 1.1A1F3F4

Apply the classical-to-distributional derivative identity [F3] to every second partial derivative of $h$ , separately to its real and imaginary parts if needed. Summing by [F4] gives $Δ u_{h} = u_{Δ h} = 0$ , since $Δ h = 0$ .

3.1givenstep 2.1F5F6F7algebra

By linearity in [F5] and [F6], $- Δ (E + u_{h}) = (- Δ E) + (- Δ u_{h})$ . The premise in the Statement and step 2.1 make this $δ_{0} + 0 = δ_{0}$ , so [F7] says $E + u_{h}$ is again a fundamental solution.

4.1step 3.1A1F1F4F8F9

To witness actual nonuniqueness, take $h \equiv 1$ . It is entire and harmonic by [F4]. Apply [F8] to the closed unit ball to obtain $χ \in C_{c}^{\infty} (R^{n})$ , $0 \leq χ \leq 1$ , with $χ = 1$ on a neighborhood of that ball. By [F9], $\int χ \geq λ_{n} (B_{1}) > 0$ ; compact support and $χ \leq 1$ make this integral finite. Thus $⟨ u_{1}, χ ⟩ = \int χ > 0$ by [F1], so $u_{1} \neq 0$ and $E + u_{1} \neq E$ . Step 3.1 shows this distinct distribution still has point source $δ_{0}$ .

5.1step 1.1step 2.1step 3.1step 4.1A1F2F3F9cases∎

The zero correction $h = 0$ leaves $E$ unchanged, while the constant correction in step 4.1 proves nonuniqueness. The argument includes dimension one because [F3] applies for every $n \geq 1$ ; dimension zero is outside the Laplacian definition [F4]. Countable Choice enters only through the regular-distribution embedding, the smooth-derivative compatibility, and ball measure [F2, F3, F9]; no full Axiom of Choice is used.

Source notes

Hunter §§2.5–2.7, printed pp. 32–42. The addition identity follows from the linearity of distributional differentiation and the classical harmonic equation. The constant correction is an explicit nonzero witness, established by testing its regular distribution against a compactly supported cutoff of positive integral.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 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

John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)