ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-10-02

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.

Poisson extension fixes coordinate functions

Example

Assume Countable Choice and $n \geq 3$ . Use one-based coordinate labels $x_{j} : = x_{j - 1}^{c a n}$ and $y_{j} : = y_{j - 1}^{c a n}$ for $1 \leq j \leq n$ . For every ball $B_{R} (a)$ , every coordinate index $j \in {1, \dots, n}$ and the boundary datum $g (y) = y_{j}$ , the ball Poisson integral is $U_{g} (x) = \int_{\partial B_{R} (a)} P_{R, a} (x, y) y_{j} d S_{y} = x_{j} (x \in B_{R} (a)) .$

Facts & Assumptions

Given: Countable Choice, an integer $n \geq 3$ , a centre $a \in R^{n}$ , a radius $R > 0$ , a coordinate index $j$ and the datum $g (y) = y_{j}$ on $\partial B_{R} (a)$ .

[F1]

$U_{g}$ is the unique function in $C^{2} (B_{R} (a)) \cap C (\overline{B_{R} (a)})$ that is harmonic on $B_{R} (a)$ and equals $g$ on $\partial B_{R} (a)$ (Continuous Dirichlet problem on a ball).

[F2]

With the one-based coordinate labels of the Example and canonical derivative indices $0 \leq i < n$ , the line identity $u (x + t e_{i}^{c a n}) = x_{j} + t δ_{i, j - 1}$ gives $\partial_{i} x_{j} = δ_{i, j - 1}$ . These derivatives are constant, so all second partials vanish and $Δ x_{j} = \sum_{i < n} \partial_{i} \partial_{i} x_{j} = 0$ ; thus $u (x) : = x_{j}$ is smooth and harmonic (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ , The Laplacian of a $C^{2}$ function and of a $C^{2}$ vector field).

[F3]

At the centre the kernel is constant, $P_{R, a} (a, y) = R^{2} / (R ω_{n - 1} ∣ a - y ∣^{n}) = 1 / (ω_{n - 1} R^{n - 1})$ , and $∣ \partial B_{R} (a) ∣ = ω_{n - 1} R^{n - 1}$ (Poisson kernel of a Euclidean ball, Sphere and ball measures scale in Rn).

[F4]

Countable Choice ${A C}_{ω}$ is the standing hypothesis (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Verification

technique · direct

1.1givenF2F4

Work under [F4] and put $u (x) : = x_{j}$ . By [F2] the function $u$ is smooth with $Δ u = 0$ on $R^{n}$ , hence on $B_{R} (a)$ , and it lies in $C^{2} (B_{R} (a)) \cap C (\overline{B_{R} (a)})$ ; its restriction to the sphere is $u (y) = y_{j} = g (y)$ .

2.1step 1.1F1

By [F1] the Poisson integral $U_{g}$ lies in the same class, is harmonic on $B_{R} (a)$ and has the same boundary trace $g$ . Applying the uniqueness clause of [F1] to the two admissible functions $u$ and $U_{g}$ gives $U_{g} (x) = u (x) = x_{j}$ for every $x \in B_{R} (a)$ .

3.1step 2.1F3algebra

Evaluating at the centre checks the spherical first moment: step 2.1 gives $\int_{\partial B_{R} (a)} P_{R, a} (a, y) y_{j} d S_{y} = a_{j}$ , and by [F3] the kernel there is the constant $1 / ∣ \partial B_{R} (a) ∣$ , so $\frac{1}{∣ \partial B_{R} (a) ∣} \int_{\partial B_{R} (a)} y_{j} d S_{y} = a_{j}$ .

4.1step 2.1step 3.1∎

Steps 2.1 and 3.1 prove the displayed identity and its central specialization; the argument uses only the uniqueness clause of the ball Dirichlet theorem together with the elementary harmonicity of $x_{j}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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

Thomas Schmidt, Partial Differential Equations I (2026) (standard reference, not scraped)