Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

On a regular bounded plane domain, Perron's method solves the Dirichlet problem

Statement

Let ΩC be a bounded complex domain such that every boundary point is regular. For every continuous boundary datum φ:ΩR, the regularized Perron envelope Hφ is harmonic on Ω, extends continuously to Ω, agrees with φ on Ω, and is the unique function with those properties.

Facts & Assumptions

Given: A bounded complex domain Ω whose every boundary point is regular, and a continuous boundary datum φ:ΩR.

[L1]

The regularized Perron envelope is harmonic on Ω (The regularized Perron envelope is harmonic).

[L2]

Regularity at a boundary point means that the Perron envelope tends to the prescribed boundary datum there; barriers characterize regular points (A boundary point is regular exactly when it admits a barrier).

[L3]

A bounded-domain harmonic extension of fixed continuous boundary data is unique (The bounded plane Dirichlet problem has at most one continuous harmonic solution).

Proof

technique · direct
1.1

By [L1], Hφ is harmonic on Ω. By the hypothesis that every boundary point is regular and the definition packaged in [L2], for every ζΩ one has [L1, L2, given] limzζzΩHφ(z)=φ(ζ).

L1L2given
2.1

Step 1.1 gives the boundary limits pointwise on Ω, and the continuity of φ turns those limits into a continuous extension of Hφ to Ω by setting the boundary values equal to φ.

step 1.1given
3.1

If u is any other continuous harmonic function on Ω with u=φ on Ω, then [L3] applied to u and the extension from step 2.1 gives u=Hφ on Ω. Thus Perron's method solves the Dirichlet problem uniquely on regular bounded plane domains.

step 2.1L3

Depends on

Used by

Dependency tree · two levels

14 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