ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-27

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.

The Perron solution on an annulus with constant radial boundary data is logarithmic

Example

Let $A_{r, R} = {z \in C : r < ∣ z ∣ < R}$ with $0 < r < R$ , and prescribe the constant boundary values $u = α on ∣ z ∣ = r, u = β on ∣ z ∣ = R .$ Then the Perron solution is $u (z) = α + \frac{β - α}{\log (R / r)} \log \frac{∣ z ∣}{r} .$

Facts & Assumptions

Given: Radii $0 < r < R$ , real constants $α, β$ , and the annulus $A_{r, R}$ .

[L1]

Exterior-disc points are regular, so a bounded domain with that property at every boundary point has a unique Perron Dirichlet solution (Exterior disc points and exterior cone points are regular, On a regular bounded plane domain, Perron's method solves the Dirichlet problem).

[L2]

Continuous harmonic extensions on a bounded domain are unique (The bounded plane Dirichlet problem has at most one continuous harmonic solution).

Verification

technique · direct

1.1

Every point of the two boundary circles of $A_{r, R}$ admits an exterior disc, so [L1] makes the annulus regular and hence ensures existence of a Perron solution.

L1given

1.2

The function [given, algebra] $h (z) = α + \frac{β - α}{\log (R / r)} \log \frac{∣ z ∣}{r}$ is harmonic on $A_{r, R}$ because $\log ∣ z ∣$ is harmonic away from $0$ , and it satisfies $h = α$ on $∣ z ∣ = r$ and $h = β$ on $∣ z ∣ = R$ .

givenalgebra

2.1

By step 1.1, the Perron solution exists; by step 1.2, $h$ is a continuous harmonic function on the closure of the annulus with the required boundary data. The uniqueness statement [L2] therefore forces the Perron solution to equal $h$ .

L2step 1.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

Boris Khoruzhenko, Potential Theory lecture notes (standard reference, not scraped)