Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

Distributional laplacian of the newtonian kernel

Example

Assume Countable Choice for Lebesgue integration. Set N(x)=−1/(4π∣x∣) for x∈R3∖{0} and assign any finite value at zero. Then N∈Lloc1(R3) and ΔuN=δ0.

Facts & Assumptions

[F1]

Regular distributions integrate locally integrable functions; second distribution derivatives transpose with positive sign, and Dirac evaluates at zero (Regular distribution from a locally integrable function, Distributional derivative, Dirac delta and its derivatives).

[F2]

Green's second identity applies to two real C2 functions on a neighborhood of an elementary solid; complex tests are handled by real and imaginary parts (Green's second identity on a glued elementary solid region).

[F4]

Under Countable Choice, bounded Borel Riemann integrands on boxes have the same Lebesgue integral (Riemann–Lebesgue comparison for distribution test integrands). Apply this to zero extensions from balls, whose boundary has Jordan content zero by the simple descriptions in F3.

[F5]

Dominated convergence applies to integrable complex functions (Dominated convergence).

Proof

Given: N and Countable Choice. We use smooth radial regularization so Green's identity is applied only on the proved elementary ball, without assuming a presentation of a punctured solid.

1.1givenF1F6

For a>0, divide 0<∣x∣≤a into shells 2−j−1a<∣x∣≤2−ja, j≥0. Each lies in a box of side 21−ja, and 1/∣x∣≤2j+1/a there. F6 bounds the integral of 1/∣x∣ by ∑j≥016a22−2j<∞. A singleton is null since it lies in boxes of arbitrarily small volume. Thus N is locally integrable and its value at zero is immaterial. Direct differentiation gives ∂iN=xi/(4π∣x∣3) and ΔN=(3∣x∣−3−3∣x∣2∣x∣−5)/(4π)=0 off zero.

2.1step 1.1F2F3F4

For ε>0 put Nε(x)=−(4π)−1(∣x∣2+ε2)−1/2. This is smooth everywhere, and coordinate differentiation gives [step 1.1, algebra] hε(x):=ΔNε(x)=3ε24π(∣x∣2+ε2)5/2≥0. For R>0 we supply the ball presentation required by F3. In each coordinate direction its base is the closed radius-R disc and its lower and upper functions are −R2−∣t∣2 and R2−∣t∣2, continuous and strictly ordered on the interior. These descriptions also prove that the ball is Jordan measurable. Use the parametrization P(ϕ,θ)=R(sin⁡ϕcos⁡θ,sin⁡ϕsin⁡θ,cos⁡ϕ) on the eight rectangles cut at ϕ=π/2 and θ=π/2,π,3π/2. It is smooth on neighborhoods of the rectangles and Pϕ×Pθ=Rsin⁡ϕ P, nonzero on each interior. An interior image has three nonzero coordinates; its third coordinate uniquely determines ϕ∈(0,π) and its first two uniquely determine the azimuth in its quadrant, so it shares its image with no other point of that closed rectangle. Distinct patches overlap only over rectangle edges, whose preimages have content zero. For each direction sort the four octants with positive coordinate as upper and the four with negative coordinate as lower, with no lateral patches. The corresponding area-vector coordinate has the required strict sign, and projected interiors are the four disjoint open quarter discs. Their omissions are the two diameters and boundary circle, all content zero: diameters admit arbitrarily thin rectangle covers; the circle lies in annuli of content π((R+h)2−(R−h)2)→0 by F3. Thus all adaptation clauses hold for the same eight-patch list. This proves the ball is elementary using only the definitions, not a B-page supplier. F2 on this ball BR with functions 1,Nε gives ∫BRhε=∫∂BR∂nNε. The supplied parametrization R(sin⁡ϕcos⁡θ,sin⁡ϕsin⁡θ,cos⁡ϕ) has area density R2sin⁡ϕ, by direct cross product. Its total area is R2∫02π∫0πsin⁡ϕ dϕ dθ=4πR2, and its outward normal is x/R. Thus [step 1.1, F2, F3, F4] ∫BRhε=R3(R2+ε2)3/2⟶1. F4 identifies these compact-region Riemann integrals with Lebesgue integrals. All Green functions are C2 on a neighborhood of the entire closed ball.

3.1step 2.1step 1.1F2F4F5

Fix a test ψ supported in the interior of BR. F2 for Nε,ψ has zero boundary terms since ψ and its derivatives vanish near the sphere. Hence ∫NεΔψ=∫BRhεψ. On the left, ∣Nε∣≤1/(4π∣x∣) off zero, an integrable bound on BR by step 1.1, and Nε→N almost everywhere. F5 gives convergence to ∫NΔψ.

4.1step 3.1step 2.1F1F6

For 0<δ<R, the difference between ∫BRhεψ and ψ(0)∫BRhε is bounded by sup⁡∣x∣≤δ∣ψ(x)−ψ(0)∣ times a mass at most one, plus 2∥ψ∥∞∫BR∖Bδhε. On the latter region, hε≤3ε2/(4πδ5), so the second term tends to zero by finite box volume. First choose δ using continuity, then let ε→0. Together with step 2.1 this proves ∫BRhεψ→ψ(0). Step 3.1 and F1 now give (ΔuN)(ψ)=∫NΔψ=ψ(0). This proves the identity with its positive sign. The zero test gives zero, and no value of the singular formula at zero is used. □

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

74 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