Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26
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.

Harmonic and holomorphic Schwarz reflection across the real axis

Statement

Write

D+:={zC:z<1, Imz>0}.

  1. If u is harmonic on D+, continuous on D+, and u(x)=0 for every x(1,1), then the odd reflection U(z):={u(z),Imz0,u(z),Imz<0, is harmonic on the full unit disc.
  2. If f is holomorphic on D+, continuous on D+, and real-valued on (1,1), then the reflected function F(z):={f(z),Imz0,f(z),Imz<0, is holomorphic on the full unit disc.

Facts & Assumptions

Given: The upper half-disc D+.

[L1]

The Poisson integral gives the unique continuous harmonic extension of continuous boundary data on a closed disc, and uniqueness holds on bounded domains with fixed boundary values (The Poisson integral gives the unique continuous harmonic extension on the closed unit disc, The bounded plane Dirichlet problem has at most one continuous harmonic solution).

[L2]

On a star-shaped domain, every harmonic function has a harmonic conjugate, and a real-valued holomorphic function on a domain is constant (Star-shaped plane domains are homologically simply connected, Harmonic conjugates exist on homologically simply connected plane domains, A real-valued holomorphic function on a domain is constant).

Proof

technique · direct
1.1

For the harmonic statement, let u satisfy the hypotheses, and define continuous boundary data Φ on the unit circle by taking the upper semicircle values of u and extending them oddly across the real axis. By [L1], Φ has a harmonic Poisson extension H to the full unit disc. On the upper half-disc, H and u are continuous harmonic functions with the same boundary values on the upper semicircle and on the diameter (1,1), so [L1] makes them equal there. By the odd construction of Φ, the same harmonic function satisfies H(z)=u(z) on the lower half-disc. Thus H is exactly the reflected function U, so U is harmonic.

L1
2.1

For the holomorphic statement, write f=u+iv on D+. Since f is real-valued on (1,1), one has v=0 there; applying step 1.1 to v gives a harmonic function V on the full disc that equals v above the axis and v(z) below it. Because the disc is star-shaped, [L2] gives a harmonic conjugate W of V, so V+iW is holomorphic. Multiplying by i shows that G:=W+iV is holomorphic and has imaginary part V.

step 1.1L2algebra
3.1

On D+, the holomorphic functions G and f have the same imaginary part v, so their difference is real-valued and holomorphic; [L2] makes Gf a real constant there. Subtracting that constant from G, we may assume G=f on D+.

step 2.1L2
4.1

For Imz<0, the functions G(z) and f(z) have the same imaginary part v(z). Their difference is therefore real-valued and holomorphic on the lower half-disc, hence constant by [L2]; continuity across the diameter, where both functions equal the same real boundary values, forces that constant to be 0. So G(z)=f(z) below the axis, and the reflected function F is holomorphic on the full disc.

step 3.1L2

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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