ExampleConstruction: Literature-sourcedVerification: 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 unit sphere checks both layer jump signs

Example

On the unit sphere $S_{1}$ with outward normal, let both layer densities be the constant $1$ . The single layer has boundary trace $1$ and conormal jump $\partial_{n}^{-} S 1 - \partial_{n}^{+} S 1 = 1$ . The double-layer kernel $\partial_{n_{y}} G_{3}$ has potential $- 1$ in the unit ball and $0$ outside; hence $γ^{-} D 1 - γ^{+} D 1 = - 1$ . Its common normal derivative is zero. Thus these conventions agree with $γ^{-} D - γ^{+} D = - ϕ$ and $\partial_{n}^{-} S - \partial_{n}^{+} S = λ$ .

Facts & Assumptions

Given: The Newton kernel and its fundamental-solution identity, a unit sphere with outward normal, and constant density $1$ .

[F1]

The kernel is $G_{3} = (4 π ∣ x - y ∣)^{- 1}$ (The three-dimensional Laplace Newton kernel).

[F2]

For density one on a radius- $R$ sphere, $U_{R} (x) = R$ for $∣ x ∣ \leq R$ and $U_{R} (x) = R^{2} / ∣ x ∣$ for $∣ x ∣ \geq R$ ; at $R = 1$ the trace is $1$ and the interior/exterior normal derivatives are $0$ and $- 1$ (A constant density on the sphere gives a constant trace).

[F3]

Differentiation under a compact parameter integral is valid when the integrand and its parameter derivative are continuous on a compact rectangle. Use it successively in the two sphere parameters with area density $R^{2} \sin θ$ ; for fixed $x \notin S_{1}$ , choose $R$ in a small interval around one avoiding $∣ x ∣$ , so all kernel derivatives there are uniformly continuous and bounded. (Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral, Surface area and scalar surface integrals on a regular patch)

Proof

1.1F1F2F3givenalgebra

The single-layer trace and conormal sign are exactly [F2]. For the double layer put $U_{R} (x) = \int_{S_{R}} G_{3} (x, y) d S_{y}$ and $D_{R} 1 (x) = \int_{S_{R}} \partial_{n_{y}} G_{3} (x, y) d S_{y}$ . In sphere parameters $y = R ω$ , differentiating $R^{2} G_{3} (x, R ω)$ by [F3] gives $\partial_{R} U_{R} = D_{R} 1 + (2 / R) U_{R}$ : the kernel derivative is the outward source-normal derivative, and the second term differentiates area density.

2.1F2step 1.1givenalgebra∎

For fixed $∣ x ∣ < 1$ and $R$ sufficiently near one, [F2] gives $U_{R} (x) = R$ , so $D_{R} 1 = 1 - 2 = - 1$ . For fixed $∣ x ∣ > 1$ it gives $U_{R} (x) = R^{2} / ∣ x ∣$ , so $D_{R} 1 = 2 R / ∣ x ∣ - (2 / R) (R^{2} / ∣ x ∣) = 0$ . At $R = 1$ the two potentials are constant on their respective sides; therefore their trace jump is $- 1$ and both normal derivatives are zero. This proves both signs without adding a divergence-theorem axiom to the classical example.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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

Francisco-Javier Sayas, First Steps in the Boundary Element Method (2015 lecture notes) (standard reference, not scraped)
Martin Costabel, Boundary Integral Operators on Lipschitz Domains: Elementary Results (1988) (standard reference, not scraped)