ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 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.

A repeated zero contributes its Green kernel twice

Example

Fix $b, R \in C \times (0, \infty)$ with $0 < ∣ b ∣ < R$ , and let $f (z) = (z - b)^{2}$ on a neighborhood of $∣ z ∣ \leq R$ . The Poisson–Jensen formula contains the zero term $- 2 G_{R} (z, b)$ . At the centre its Jensen correction is $2 \log (R / ∣ b ∣)$ .

Verification

Given: $0 < ∣ b ∣ < R$ and $f (z) = (z - b)^{2}$ .

[F1] In the meromorphic Poisson–Jensen formula each zero contributes its multiplicity times $- G_{R} (z, b)$ (Poisson–Jensen formula for a meromorphic function on a disc).

1.1givenalgebra

The only zero in the radius- $R$ disc is $b$ , with multiplicity two; there are no poles or boundary divisor points, and $f (0) = b^{2} \neq 0$ .

2.1F1step 1.1algebra

By [F1], Poisson–Jensen therefore reads $2 \log ∣ z - b ∣ = \frac{1}{2 π} \int_{0}^{2 π} \frac{R^{2} - ∣ z ∣^{2}}{∣ R e^{i t} - z ∣^{2}} 2 \log ∣ R e^{i t} - b ∣ d t - 2 G_{R} (z, b)$ for $∣ z ∣ < R$ with $z \neq b$ . The coefficient is exactly two because the local factor is squared.

3.1F1step 2.1algebra∎

At $z = 0$ , $G_{R} (0, b) = \log (R / ∣ b ∣)$ . Also $R e^{i t} - b = R e^{i t} (1 - (b / R) e^{- i t})$ , and the convergent logarithm series has zero angular mean, so the boundary mean of $\log ∣ f ∣$ is $2 \log R$ . The formula becomes $2 \log ∣ b ∣ = 2 \log R - 2 \log (R / ∣ b ∣)$ , displaying the stated centre correction.

Depends on

Poisson–Jensen formula for a meromorphic function on a disc

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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

Alexandre Eremenko, Lectures on Nevanlinna Theory, §1 (standard reference, not scraped)