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.

Characteristic under a target Möbius change

Example

Let $f$ be a nonconstant meromorphic function on $C$ and let $a \in C$ . Define the degree-one map $M_{a} (w) = \frac{1 + \overline{a} w}{w - a}, M_{a} (\infty) = \overline{a} .$ Then $δ (M_{a} (w), \infty) = δ (w, a) (w \in \hat{C}),$ and $T (r, M_{a} \circ f) = T (r, f) + O_{f, a} (1) (r \to \infty) .$

Verification

Given: The normalized chordal distance and Nevanlinna characteristic, the First Main Theorem, the fixed-rational composition law, and the local zero/pole order facts for meromorphic functions.

[F1] For finite $w, a$ , $δ (w, a) = ∣ w - a ∣ / (\sqrt{1 + ∣ w ∣^{2}} \sqrt{1 + ∣ a ∣^{2}})$ ; $δ (w, \infty) = δ (\infty, w) = 1 / \sqrt{1 + ∣ w ∣^{2}}$ and $δ (\infty, \infty) = 0$ (Counting, chordal proximity and characteristic).

[F2] For nonconstant meromorphic $f$ and finite $a$ , $m (r, a; f) + N (r, a; f) = T (r, f) + C (f, a)$ for every $r > 0$ (Nevanlinna’s First Main Theorem with exact centre constant).

[F3] For a fixed rational map $R$ of degree $d \geq 1$ and nonconstant meromorphic $f$ , $T (r, R (f)) = d T (r, f) + O_{R, f} (1)$ as $r \to \infty$ (Elementary characteristic laws and fixed rational composition).

[F4] A holomorphic function of finite order $m$ at $b$ factors locally as $(z - b)^{m} h (z)$ with $h (b) \neq 0$ (The order of a zero is the exponent in its local holomorphic factorization).

[F5] At a pole of order $m$ , the reciprocal extends holomorphically across the pole and has a zero of order $m$ (Characterizations of poles).

1.1givenalgebra

The numerator and denominator of $M_{a}$ have determinant $- (1 + ∣ a ∣^{2}) \neq 0$ , so $M_{a}$ is a degree-one Möbius map; also $M_{a} (a) = \infty$ and the limit at $w = \infty$ is $\overline{a}$ . The identity $M_{a} (w) = \overline{a} + (1 + ∣ a ∣^{2}) / (w - a)$ holds for finite $w \neq a$ .

2.1F1step 1.1algebra

For finite $w \neq a$ , $∣ 1 + \overline{a} w ∣^{2} + ∣ w - a ∣^{2} = (1 + ∣ a ∣^{2}) (1 + ∣ w ∣^{2})$ , so [F1] gives $δ (M_{a} (w), \infty) = ∣ w - a ∣ / \sqrt{(1 + ∣ a ∣^{2}) (1 + ∣ w ∣^{2})} = δ (w, a)$ . At $w = a$ , both sides are zero since $M_{a} (a) = \infty$ ; at $w = \infty$ , $δ (M_{a} (\infty), \infty) = 1 / \sqrt{1 + ∣ a ∣^{2}} = δ (\infty, a)$ . Thus the pointwise identity holds on the whole sphere, including both endpoints.

2.2F4F5step 1.1algebra

Let $F = M_{a} \circ f$ . At a finite point $b$ with $f (b) = a$ of order $m$ , [F4] gives $f (z) - a = (z - b)^{m} h (z)$ with $h (b) \neq 0$ ; the numerator $1 + \overline{a} f (z)$ equals $1 + ∣ a ∣^{2} \neq 0$ at $b$ , so $F$ has a pole of order $m$ . At a pole $b$ of $f$ of order $m$ , [F5] says $1 / f$ has a zero of order $m$ ; since $1 / (f - a) = (1 / f) / (1 - a / f)$ and $1 - a / f$ is nonzero at $b$ , step 1.1 shows $F = \overline{a} + (1 + ∣ a ∣^{2}) / (f - a)$ extends holomorphically and finitely there. At every other point $f$ is finite and different from $a$ , so $F$ is finite and holomorphic. Hence the poles of $F$ are exactly the $a$ -points of $f$ with the same multiplicities; the closed-disc counts and their integrated versions satisfy $N (r, \infty; F) = N (r, a; f)$ for every $r > 0$ .

3.1F1step 2.1algebra

By step 2.1, the integrands defining $m (r, \infty; F)$ and $m (r, a; f)$ are equal at every point of the circle, with the same logarithmic singularity at an $a$ -point and the same finite value at a pole of $f$ . Therefore $m (r, \infty; F) = m (r, a; f)$ for every $r > 0$ .

4.1F2F3step 2.2step 3.1algebra∎

The map $M_{a}$ has degree one and is invertible, so $F$ is nonconstant; [F3] gives $T (r, F) = T (r, f) + O_{f, a} (1)$ . Steps 2.2–3.1 also give $T (r, F) = m (r, a; f) + N (r, a; f)$ , and [F2] identifies this sum exactly as $T (r, f) + C (f, a)$ . This proves the asserted characteristic estimate and confirms the target count/proximity relation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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–3 (standard reference, not scraped)
Goldberg–Ostrovskii, Value Distribution of Meromorphic Functions, Ch. 1 §6, equation (6.8) (standard reference, not scraped)