TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-10-02

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.

Nevanlinna five-value uniqueness theorem

Statement

Assume Countable Choice. Let $f$ and $g$ be nonconstant meromorphic functions on $C$ . Suppose that $f$ and $g$ share five distinct sphere values ignoring multiplicity: there are distinct $a_{1}, \dots, a_{5} \in \hat{C}$ such that for each $j$ the preimage sets ${z : f (z) = a_{j}}$ and ${z : g (z) = a_{j}}$ agree. Then $f = g$ identically.

Facts & Assumptions

Given: Nonconstant meromorphic functions $f, g$ on $C$ sharing the distinct sphere values $a_{1}, \dots, a_{5}$ ; Countable Choice is assumed (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F1]

First Main Theorem: for nonconstant meromorphic $h$ and $a \in \hat{C}$ , $m (r, a; h) + N (r, a; h) = T (r, h) + C (h, a)$ with $C (h, a)$ independent of $r$ ; in particular $N (r, a; h) \leq T (r, h) + C (h, a)$ (Nevanlinna’s First Main Theorem with exact centre constant).

[F2]

Characteristic laws: $T (r, h_{1} + h_{2}) \leq T (r, h_{1}) + T (r, h_{2}) + O (1)$ , $T (r, 1 / h) = T (r, h) + O_{h} (1)$ for $h \equiv̸ 0$ , and for a fixed rational map $R = P / Q$ of degree $d = \max (\deg P, \deg Q) \geq 1$ and nonconstant meromorphic $h$ , $T (r, R (h)) = d T (r, h) + O_{R, h} (1)$ ; a Möbius transformation is such an $R$ with $d = 1$ (Elementary characteristic laws and fixed rational composition).

[F3]

Truncated Second Main Theorem: for nonconstant meromorphic $h$ on $C$ and distinct sphere targets $b_{1}, \dots, b_{q}$ with $q \geq 3$ , $(q - 2) T (r, h) \leq \sum_{j = 1}^{q} \overset{ˉ}{N} (r, b_{j}; h) + S (r, h)$ outside a set of finite linear measure, where $S (r, h) \leq C (\log^{+} T (r, h) + \log r)$ off that set; when $h$ is rational the error is $O_{h} (1)$ , and for $h$ of finite order it is $O_{h} (\log r)$ , in both cases at every sufficiently large radius (Nevanlinna Second Main Theorem with ramification and truncation).

[F4]

Truncated counts: $\overset{ˉ}{N} (r, b; h)$ counts the distinct $b$ -points of $h$ once, and $N (r, a; h) = \overset{ˉ}{N} (r, a; h) + N_{1} (r, a; h)$ with $N_{1} (r, a; h) \geq 0$ for $r \geq 1$ ; each zero of $h$ contributes its multiplicity to $N (r, 0; h)$ (Truncated value and ramification counts).

[F5]

Growth: every nonconstant meromorphic $h$ on $C$ has $T (r, h) \to \infty$ ; $T (r, h) / \log r \to \infty$ when $h$ is transcendental, and $T (r, h) = d \log r + O (1)$ when $h$ is rational of degree $d$ (Transcendental characteristic dominates logarithmic growth).

Proof

technique · normalise the five values to finite values by a Möbius map, compare the common value counts with the zeros of $F-G$, apply the truncated Second Main Theorem to both normalised functions, and use the characteristic growth to reach a contradiction unless $F-G\equiv0$

1.1F2construct

(Möbius normalisation) Pick $b \in C ∖ {a_{1}, \dots, a_{5}}$ and put $R (z) : = 1 / (z - b)$ , a Möbius transformation with $R (b) = \infty$ ; set $F : = R \circ f$ , $G : = R \circ g$ and $c_{j} : = R (a_{j})$ . Then each $c_{j}$ is finite (it is $0$ when $a_{j} = \infty$ ) and the $c_{j}$ are distinct; $F$ and $G$ are nonconstant meromorphic, their preimage sets of $c_{j}$ agree for every $j$ , and [F2] gives $T (r, F) = T (r, f) + O (1)$ and $T (r, G) = T (r, g) + O (1)$ as $r \to \infty$ .

2.1F1F2F4step 1.1

(Common value count versus zeros of the difference) Put $h : = F - G$ , a meromorphic function, and $C (r) : = \sum_{j = 1}^{5} \overset{ˉ}{N} (r, c_{j}; F)$ . The sets ${F = c_{j}}$ are pairwise disjoint because the $c_{j}$ are distinct, and each is contained in ${h = 0}$ , since $F (z) = c_{j}$ forces $G (z) = c_{j}$ by the sharing hypothesis. If $h \equiv 0$ there is nothing to prove. If $h$ is a nonzero constant, then $C (r) = 0$ , since no common $c_{j}$ -point can be a zero of $h$ . Otherwise $h$ is nonconstant, so for $r \geq 1$ the distinct common zeros have nonnegative integrated weights and [F1] applied at target $0$ , together with [F2], gives $C (r) \leq N (r, 0; h) \leq T (r, h) + O (1) \leq T (r, F) + T (r, G) + O (1) = T (r, f) + T (r, g) + O (1)$ . Thus the count bound holds for all large $r$ when $h \equiv̸ 0$ , which is the range used below; from here on assume $h \equiv̸ 0$ .

3.1F3step 1.1step 2.1algebra

(Second Main Theorem bounds) Apply [F3] with $q = 5$ to the nonconstant functions $F$ and $G$ and the distinct finite targets $c_{1}, \dots, c_{5}$ : outside sets $E_{F}$ and $E_{G}$ of finite linear measure, $3 T (r, F) \leq \sum_{j = 1}^{5} \overset{ˉ}{N} (r, c_{j}; F) + S (r, F)$ and $3 T (r, G) \leq \sum_{j = 1}^{5} \overset{ˉ}{N} (r, c_{j}; G) + S (r, G)$ ; by the shared preimage sets, $\sum_{j} \overset{ˉ}{N} (r, c_{j}; F) = \sum_{j} \overset{ˉ}{N} (r, c_{j}; G) = C (r)$ , so adding gives $3 (T (r, F) + T (r, G)) \leq 2 C (r) + S (r, F) + S (r, G)$ outside $E : = E_{F} \cup E_{G}$ .

4.1F3F5step 3.1algebra

(Growth separation) Off $E$ , both errors are negligible compared with $T (r, F) + T (r, G)$ : if $F$ is transcendental then $S (r, F) = O (\log^{+} T (r, F) + \log r) = o (T (r, F))$ because $T (r, F) / \log r \to \infty$ and $T (r, F) \to \infty$ by [F5], while if $F$ is rational then $S (r, F) = O (1) = o (T (r, F))$ ; in either case $S (r, F) = o (T (r, F) + T (r, G))$ , and the same argument applies to $G$ , so $S (r, F) + S (r, G) = o (T (r, F) + T (r, G))$ along $r \notin E$ , large $r$ .

5.1F5step 2.1step 3.1step 4.1algebra

(Contradiction unless the difference vanishes) Substituting the count bound of step 2.1 into step 3.1 and using step 4.1 gives $3 (T (r, F) + T (r, G)) \leq 2 (T (r, F) + T (r, G)) + o (T (r, F) + T (r, G)) + O (1)$ , hence $T (r, F) + T (r, G) \leq o (T (r, F) + T (r, G)) + O (1)$ for all large $r \notin E$ . Since $E$ has finite measure its complement is unbounded, and along it $T (r, F) + T (r, G) \to \infty$ by [F5] because $F$ and $G$ are nonconstant; choosing $r \notin E$ so large that the $o (1)$ term is below $\frac{1}{2}$ makes the inequality impossible. Hence $h \equiv 0$ , that is, $F \equiv G$ .

6.1step 1.1step 5.1algebra∎

(Conclusion) From $F \equiv G$ and $F = R \circ f$ , $G = R \circ g$ with $R$ injective on the sphere, $f = R^{- 1} \circ F = R^{- 1} \circ G = g$ identically.

Depends on

Used by

Four shared values do not force equality Example

Dependency tree · two levels

25 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

I. Laine, Complex Analysis III lecture notes (standard reference, not scraped)
A. Goldberg and I. Ostrovskii, Value Distribution of Meromorphic Functions (standard reference, not scraped)