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 plane subharmonic function with an interior maximum is constant on its component

Statement

Let u be subharmonic on a complex domain Ω. If u attains a finite maximum at an interior point of Ω, then u is constant on Ω.

Facts & Assumptions

Given: A subharmonic function u on a complex domain Ω and a point aΩ with u(a)=M=supΩu<.

[L1]

Subharmonicity means that every sufficiently small circle average is at least the center value (Subharmonic functions on plane domains).

Proof

technique · direct
1.1

Let [given] S={zΩ:u(z)=M}. Because u is upper semicontinuous, S is closed in Ω, and it is nonempty because aS.

given
1.2

Choose r>0 with D(a,r)Ω. For every 0<ρ<r, [L1] gives [L1, given] M=u(a)12π02πu(a+ρeit)dtM, so the average equals M. Since the integrand never exceeds M, it equals M almost everywhere on the circle za=ρ. If some point of that circle had value <M, upper semicontinuity would make the value <M on a short arc, forcing the average below M. Hence uM on every circle za=ρ with 0<ρ<r.

L1given
2.1

Step 1.2 shows that every point of D(a,r) lies in S, so S is open in Ω. Since Ω is connected and S is nonempty, closed, and open, one has S=Ω. Therefore uM on Ω.

step 1.1step 1.2

Depends on

Used by

Dependency tree · one level

1 result within one dependency step 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