Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

A boundary point is regular exactly when it admits a barrier

Statement

Let ΩC be a bounded complex domain and let ζΩ. Then ζ is regular if and only if Ω admits a barrier at ζ.

Facts & Assumptions

Given: A bounded complex domain Ω and a boundary point ζΩ.

[L1]

For every continuous boundary datum, the regularized Perron envelope is harmonic on Ω (The regularized Perron envelope is harmonic).

[L2]

A subharmonic function with a finite interior maximum is constant on the connected domain (A plane subharmonic function with an interior maximum is constant on its component).

[L3]

A barrier at ζ is a negative subharmonic function that tends to 0 at ζ and stays uniformly below a negative constant on the rest of the boundary (Barriers and regular boundary points).

[L4]

The C2 function q(z)=zζ2 is subharmonic because Δq=40 (A C^2 function is subharmonic exactly when its Laplacian is nonnegative).

Proof

technique · direct
1.1

Assume first that b is a barrier at ζ, and let φC(Ω). Put H=Hφ, which is harmonic by [L1]. Fix ε>0. Choose a boundary neighbourhood V of ζ with φ(η)φ(ζ)<ε on VΩ, and choose A>0 so large that the negative boundary bound from [L3] forces both [L3, given, choose] φ(η)φ(ζ)ε+Alim supb(η)0,φ(η)+φ(ζ)ε+Alim supb(η)0 for ηΩV.

L3givenchoose
1.2

Assume conversely that ζ is regular, and define a continuous boundary datum on Ω by ψ(η)=ηζ2. Let B=Hψ, which is harmonic on Ω by [L1]. Regularity gives B(z)ψ(ζ)=0 as zζ. Now let v be any member of the Perron family for ψ. By [L4], the function q(z)=zζ2 is subharmonic on Ω, so v+q is subharmonic there. For every boundary point ηΩ, the defining Perron inequality gives lim supzηzΩ(v(z)+q(z))ψ(η)+ηζ2=0. If v+q were positive somewhere in Ω, then upper semicontinuity and boundedness of Ω would produce a positive interior maximum, contradicting [L2]. Hence v(z)zζ2 on Ω for every lower function v. Taking the supremum over the Perron family and then upper-semicontinuous regularizing yields B(z)zζ2<0(zΩ). Now let V be any neighbourhood of ζ. The compact set ΩV has δV:=minηΩVηζ2>0, so the displayed inequality gives lim supzηzΩB(z)δV(ηΩV). Thus B is negative on Ω, tends to 0 at ζ, and stays uniformly below a negative constant away from ζ. Hence B is a barrier at ζ.

L1L2L4given
2.1

The functions [L2, step 1.1] s+(z)=H(z)φ(ζ)ε+Ab(z),s(z)=H(z)+φ(ζ)ε+Ab(z) are subharmonic on Ω because H and H are harmonic and b is subharmonic. Step 1.1 shows that both have boundary limsup at most 0. If either had a positive value in the interior, upper semicontinuity would produce a positive interior maximum, contradicting [L2]. Hence s±0 on Ω.

L2step 1.1
3.1

Step 2.1 gives [step 2.1, L3] φ(ζ)ε+Ab(z)H(z)φ(ζ)+εAb(z). Letting zζ inside Ω and using b(z)0 gives φ(ζ)εlim infΩzζH(z)lim supΩzζH(z)φ(ζ)+ε. Since ε is arbitrary, H(z)φ(ζ). Thus ζ is regular.

step 2.1L3
4.1

Steps 1.1 through 4.1 prove both directions, so ζ is regular exactly when it admits a barrier.

step 3.1step 1.2

Depends on

Used by

Dependency tree · two levels

13 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