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 constant density on the sphere gives a constant trace

Example

For $R > 0$ , let $S_{R} = {y \in R^{3} : ∣ y ∣ = R}$ and take density $λ = 1$ . The classical Newton single-layer potential is $S 1 (x) = \int_{S_{R}} \frac{1}{4 π ∣ x - y ∣} d S_{y} = {\begin{cases} R, & ∣ x ∣ \leq R, \\ R^{2} / ∣ x ∣, & ∣ x ∣ \geq R . \end{cases}$ It is continuous on $S_{R}$ with trace $R$ . With outward radial normal, the interior and exterior normal derivatives at the sphere are $0$ and $- 1$ , respectively, so their difference is $1$ , the density.

Facts & Assumptions

Given: The Newton kernel $G_{3} (x, y) = (4 π ∣ x - y ∣)^{- 1}$ of The three-dimensional Laplace Newton kernel, a radius $R > 0$ , and the sphere $S_{R}$ .

[F1]

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

[F2]

The usual radius- $R$ sphere parametrization has area density $R^{2} \sin θ$ on $0 < θ < π$ , $0 < φ < 2 π$ ; its omitted poles and meridian have zero parameter contribution. Taking $t = \cos θ$ gives $d S = R^{2} d φ (- d t)$ in the axisymmetric integral. (Surface area and scalar surface integrals on a regular patch, The derivatives of sine and cosine are cosine and minus sine, The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ )

Proof

1.1F1F2givenalgebra

For $r = ∣ x ∣ > 0$ , spherical coordinates centered on the axis through $x$ give $S 1 (x) = \frac{R^{2}}{2} \int_{- 1}^{1} (r^{2} + R^{2} - 2 r R t)^{- 1 / 2} d t = \frac{R}{2 r} (r + R - ∣ r - R ∣) .$ If $r < R$ this equals $R$ , and if $r > R$ it equals $R^{2} / r$ ; at $r = R$ the same convergent improper integral gives $R$ , and at $r = 0$ the constant kernel $1 / (4 π R)$ times the parametrized area $4 π R^{2}$ gives $R$ .

2.1step 1.1givenalgebra∎

Differentiating the two radial formulas gives $\partial_{r} S 1 = 0$ for $r < R$ and $\partial_{r} S 1 = - R^{2} / r^{2}$ for $r > R$ . Their boundary limits are $0$ and $- 1$ , so $\partial_{n}^{-} S 1 - \partial_{n}^{+} S 1 = 1 = λ$ . This direct smooth-sphere calculation checks the kernel normalization and jump orientation independently of the polyhedral theorem.

Depends on

Used by

A unit sphere checks both layer jump signs Example

Dependency tree · two levels

23 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)