ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

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.

Green kernel of a slit plane via the square-root map

Example

Let $Ω = C ∖ (- \infty, 0]$ be the slit plane, let $a, z \in Ω$ with $z \neq a$ , and let $\sqrt{}$ be the principal square root of Complex powers defined from a holomorphic logarithm branch, so that $Re \sqrt{w} > 0$ for $w \in Ω$ . Then the canonical Green kernel of The canonical Green kernel of a plane domain is $g_{Ω} (z, a) = \log ∣ \frac{\sqrt{z} + \overline{\sqrt{a}}}{\sqrt{z} - \sqrt{a}} ∣ .$ The kernel tends to zero at every point of the slit and at infinity. This is an unbounded domain, and no general Euclidean boundary map is used: the boundary value at the slit is read off directly from the explicit formula.

Facts & Assumptions

Given: The slit plane $Ω = C ∖ (- \infty, 0]$ , points $a, z \in Ω$ with $z \neq a$ , and the right half-plane $H = {w \in C : Re w > 0}$ . Conjugates and moduli are those of Real and imaginary parts, complex conjugation, and modulus, complex domains are those of A complex domain is a nonempty connected open subset of $C$ , and the canonical Green kernel is that of The canonical Green kernel of a plane domain.

[F1]

For a proper plane domain $D$ and $b \in D$ the canonical Green function $g_{D} (\cdot, b)$ , when it exists, is the pointwise least nonnegative function that is harmonic on $D ∖ {b}$ and satisfies: $g_{D} (\cdot, b) + \log ∣ \cdot - b ∣$ extends harmonically across $b$ (The canonical Green kernel of a plane domain).

[F2]

For every integer $n \geq 1$ , the map $R_{n} (z) = \exp (Log z / n)$ is a biholomorphism from the slit plane onto the sector $V_{n} = {r e^{i θ} : r > 0, ∣ θ ∣ < π / n}$ , with inverse $w \mapsto w^{n}$ ; for $n = 2$ this is a biholomorphism $\sqrt{} : Ω \to H$ with inverse $w \mapsto w^{2}$ , and both $Ω$ and $H$ are complex domains (A slit-plane root branch biholomorphically parametrizes a sector, Biholomorphic maps between complex domains, Complex powers defined from a holomorphic logarithm branch).

[F3]

The function $\log ∣ \cdot ∣$ is harmonic on $C ∖ {0}$ (Logarithmic modulus is harmonic off its centre), and the composition of a harmonic function with a holomorphic map is harmonic (Plane harmonicity is preserved by holomorphic and antiholomorphic changes of coordinate).

[F4]

If $u$ is continuous on the closure of a bounded complex domain and harmonic inside, then $\sup_{\overline{D}} u = \sup_{\partial D} u$ and $\inf_{\overline{D}} u = \inf_{\partial D} u$ (Maximum and minimum principles for plane harmonic functions).

Verification

technique · direct

1.1F1F2F3givenalgebra

Put $β : = \sqrt{a}$ , so that $β \in H$ by [F2] and $Re β > 0$ . Define $q (w) : = \log ∣ w + \overline{β} ∣ - \log ∣ w - β ∣ (w \in H ∖ {β}) .$ The translations $w \mapsto w + \overline{β}$ and $w \mapsto w - β$ are holomorphic and are nonzero on $H$ and $H ∖ {β}$ , respectively; by [F3], their logarithmic moduli are harmonic on those sets. (The real part of $w - β$ may vanish away from $β$ , but the complex number $w - β$ is still nonzero there.) Hence $q$ is harmonic on $H ∖ {β}$ . Writing $w = u + i v$ with $u = Re w$ and $β = α + i γ$ , $α > 0$ , gives $∣ w + \overline{β} ∣^{2} - ∣ w - β ∣^{2} = (u + α)^{2} - (u - α)^{2} = 4 u α$ , so $∣ w + \overline{β} ∣ \geq ∣ w - β ∣$ with equality exactly on the imaginary axis; thus $q \geq 0$ on $H$ . Finally $q (w) + \log ∣ w - β ∣ = \log ∣ w + \overline{β} ∣$ is harmonic across $w = β$ , since $β + \overline{β} = 2 α \neq 0$ makes $w + \overline{β}$ nonvanishing near $β$ . So $q$ is a nonnegative logarithmic-pole candidate at $β$ in the sense of [F1].

2.1F1step 1.1

Let $k$ be any nonnegative logarithmic-pole candidate at $β$ on $H$ and put $u : = k - q$ . On $H ∖ {β}$ the function $u$ is harmonic as a difference of harmonic functions, and it extends harmonically across $β$ : by the defining property in [F1] both $k (w) + \log ∣ w - β ∣$ and $q (w) + \log ∣ w - β ∣ = \log ∣ w + \overline{β} ∣$ are harmonic in a neighbourhood of $β$ , and $u$ is their difference off $β$ .

2.2F2F3step 1.1

Define $G (z) : = q (\sqrt{z}) = \log ∣ (\sqrt{z} + \overline{β}) / (\sqrt{z} - β) ∣$ for $z \in Ω ∖ {a}$ . Then $G \geq 0$ by step 1.1, and $G$ is harmonic on $Ω ∖ {a}$ by [F3], because $\sqrt{} : Ω \to H$ is holomorphic by [F2] and $\sqrt{z} = β$ holds exactly for $z = a$ , by the inverse property in [F2].

3.1F1F4step 1.1step 2.1algebra

Fix $R > ∣ β ∣$ and $δ \in (0, α / 2)$ , where $α = Re β$ , and set $D : = {w : Re w > δ, ∣ w ∣ < R}$ , a bounded complex domain with $\overline{D} \subseteq H$ . By step 2.1 the function $- u$ is harmonic on $D$ and continuous on $\overline{D}$ , so its supremum on $\overline{D}$ is attained on $\partial D$ by [F4]. On the circular arc ${∣ w ∣ = R, Re w \geq δ}$ one has $∣ w + \overline{β} ∣ \leq R + ∣ β ∣$ and $∣ w - β ∣ \geq R - ∣ β ∣ > 0$ , hence $- u = q - k \leq q \leq \log \frac{R + ∣ β ∣}{R - ∣ β ∣} = : c_{R},$ because $k \geq 0$ and $q \geq 0$ . On the vertical segment ${Re w = δ, ∣ w ∣ \leq R}$ one has $- u \leq q$ and, since $∣ w - β ∣ \geq α / 2$ there, $∣ w + \overline{β} ∣ - ∣ w - β ∣ = \frac{∣ w + \overline{β} ∣^{2} - ∣ w - β ∣^{2}}{∣ w + \overline{β} ∣ + ∣ w - β ∣} = \frac{4 δ α}{∣ w + \overline{β} ∣ + ∣ w - β ∣} \leq \frac{4 δ α}{α / 2} = 8 δ,$ so $q = \log (1 + \frac{∣ w + \overline{β} ∣ - ∣ w - β ∣}{∣ w - β ∣}) \leq \frac{8 δ}{α / 2} = \frac{16 δ}{α}$ . Therefore $- u \leq \max {c_{R}, 16 δ / α}$ on $D$ . Letting $δ ↓ 0$ for fixed $w \in H$ with $R > ∣ w ∣$ gives $- u (w) \leq c_{R}$ , and letting $R \to \infty$ gives $- u (w) \leq 0$ , since $c_{R} = \log (1 + \frac{2 ∣ β ∣}{R - ∣ β ∣}) \to 0$ . Hence $k \geq q$ on $H$ , and $q$ is the canonical Green kernel $g_{H} (\cdot, β)$ of the half-plane by [F1].

3.2F1F2F3step 2.2algebra

The function $G$ has the logarithmic pole at $a$ . For $z \in Ω ∖ {a}$ the factorization $z - a = (\sqrt{z} - β) (\sqrt{z} + β)$ of [F2] gives $\log ∣ \sqrt{z} - β ∣ = \log ∣ z - a ∣ - \log ∣ \sqrt{z} + β ∣$ , hence $G (z) + \log ∣ z - a ∣ = \log ∣ \sqrt{z} + \overline{β} ∣ + \log ∣ \sqrt{z} + β ∣ = \log ∣ z + 2 (Re β) \sqrt{z} + ∣ β ∣^{2} ∣,$ and the holomorphic function $h (z) : = z + 2 (Re β) \sqrt{z} + ∣ β ∣^{2}$ on $Ω$ satisfies $h (a) = 4 β Re β \neq 0$ . So $z \mapsto \log ∣ h (z) ∣$ is harmonic on a neighbourhood of $a$ by [F3], and $G + \log ∣ \cdot - a ∣$ extends harmonically across $a$ . Together with steps 1.1 and 2.2 this shows that $G$ is a nonnegative logarithmic-pole candidate at $a$ on $Ω$ .

4.1F1F2F3step 3.1step 2.2step 3.2algebra

Leastness on $Ω$ : let $k$ be any nonnegative logarithmic-pole candidate at $a$ on $Ω$ and define $K (w) : = k (w^{2})$ for $w \in H$ . Then $K \geq 0$ , and $K$ is harmonic on $H ∖ {β}$ by [F3], since $w \mapsto w^{2}$ is holomorphic by [F2] and $w^{2} = a$ holds exactly for $w = β$ . Moreover, for $w \neq β$ the identity $w^{2} - a = (w - β) (w + β)$ gives $K (w) + \log ∣ w - β ∣ = (k (w^{2}) + \log ∣ w^{2} - a ∣) - \log ∣ w + β ∣,$ where $k (\cdot) + \log ∣ \cdot - a ∣$ is harmonic near $a$ by [F1], so its composition with $w \mapsto w^{2}$ is harmonic near $β$ , and $\log ∣ w + β ∣$ is harmonic near $β$ because $2 β \neq 0$ . Thus $K$ is a nonnegative logarithmic-pole candidate at $β$ on $H$ , and step 3.1 gives $K \geq q$ on $H$ . For $z \in Ω$ , writing $z = w^{2}$ with $w = \sqrt{z} \in H$ by [F2], we obtain $k (z) = K (w) \geq q (w) = G (z)$ . Hence every candidate dominates $G$ , so $G$ is the pointwise least candidate and $g_{Ω} (z, a) = G (z) = \log ∣ (\sqrt{z} + \overline{\sqrt{a}}) / (\sqrt{z} - \sqrt{a}) ∣$ by [F1].

5.1F2step 1.1step 4.1algebra

Boundary limits on the slit. Let $ζ \leq 0$ and let $z_{n} \in Ω$ with $z_{n} \to ζ$ ; put $w_{n} : = \sqrt{z_{n}} \in H$ . Since $w_{n}^{2} = z_{n}$ , the identity $2 (Re w_{n})^{2} = ∣ w_{n} ∣^{2} + Re (w_{n}^{2}) = ∣ z_{n} ∣ + Re z_{n}$ gives $Re w_{n} \to 0$ because $∣ z_{n} ∣ + Re z_{n} \to ∣ ζ ∣ + ζ = 0$ for $ζ \leq 0$ . Consequently $∣ w_{n} + \overline{β} ∣^{2} - ∣ w_{n} - β ∣^{2} = 4 (Re w_{n}) (Re β) \to 0$ by step 1.1, while $∣ w_{n} - β ∣ \geq Re β - Re w_{n} \geq Re β / 2$ for all large $n$ ; hence the quotient $∣ w_{n} + \overline{β} ∣ / ∣ w_{n} - β ∣$ tends to $1$ and $g_{Ω} (z_{n}, a) = q (w_{n}) \to 0$ . So the kernel has limit $0$ at every point of the slit $(- \infty, 0] = \partial Ω$ .

6.1givenstep 1.1step 4.1algebra∎

Limit at infinity. For $∣ z ∣ > 4 ∣ β ∣^{2}$ one has $∣ w ∣ = ∣ \sqrt{z} ∣ > 2 ∣ β ∣$ , so $0 \leq g_{Ω} (z, a) = q (w) \leq \log \frac{∣ w ∣ + ∣ β ∣}{∣ w ∣ - ∣ β ∣} = \log (1 + \frac{2 ∣ β ∣}{∣ w ∣ - ∣ β ∣}) \leq \frac{2 ∣ β ∣}{∣ w ∣ - ∣ β ∣},$ which tends to $0$ as $∣ z ∣ \to \infty$ . Thus the kernel vanishes at the slit and at infinity, as claimed; all of the above is an explicit choice-free calculation, the boundary behaviour being read off from the formula $z \mapsto q (\sqrt{z})$ rather than from any Euclidean boundary correspondence.

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

Mikhail Lyubich, Dynamics of Quadratic Polynomials, Vol. I, Appendix 1, Sections 10.1-10.9 (standard reference, not scraped)
E. B. Saff, Logarithmic Potential Theory with Applications to Approximation Theory, Section 3 (standard reference, not scraped)