Alphabeta Math
LemmaStatement: 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 local strict subharmonic peak function globalizes

Statement

Let ΩC be a bounded complex domain and let ζΩ. Suppose there are a neighbourhood U of ζ and a subharmonic function q on ΩU such that:

  1. q(z)<0 for every zΩU;
  2. q(z)0 as zζ with zΩ;
  3. for some smaller neighbourhood WU of ζ, one has sup{q(z):zΩW}<0.

Then Ω has a global barrier at ζ.

Facts & Assumptions

Given: A bounded complex domain Ω, a boundary point ζ, and local data U, W, and q as in the Statement.

[L1]

Positive scalar multiples and finite maxima of subharmonic functions are subharmonic (Positive linear combinations and finite maxima preserve subharmonicity).

[L2]

Subharmonic pieces glue across a disc boundary under the limsup inequality (Subharmonic pieces glue across a boundary under the limsup inequality).

Proof

technique · direct
1.1

Choose η>0 with qη on ΩW, and then choose a constant c>0 so large that cq1 on ΩW. The function cq is still subharmonic on ΩW by [L1], remains negative there, and still tends to 0 at ζ.

L1givenchoose
2.1

Define [L1, L2, step 1.1] b(z)={max{cq(z),1},zΩW,1,zΩW. Inside ΩW the function is subharmonic by [L1]. On the seam W one has cq1, so the inside limsup is at most the outside value 1; [L2] therefore glues the inside and outside pieces into a global subharmonic function on Ω.

L1L2step 1.1
3.1

The function b is negative on Ω, tends to 0 at ζ because near ζ the maximum chooses the cq branch, and is identically 1 outside W, so it stays uniformly below a negative constant away from ζ. Thus b is a global barrier at ζ.

step 2.1

Depends on

Used by

Dependency tree · two levels

6 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