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.

Characteristics of a monomial, an exponential and a tangent

Example

For each integer $d \geq 1$ , $T (r, z^{d}) = d \log r + O (1), T (r, \exp z) = \frac{r}{π} + O (1), T (r, \tan z) = \frac{2 r}{π} + O (1)$ as $r \to \infty$ , using the normalized chordal characteristic. Here $\tan z$ means the meromorphic quotient of complex sine by complex cosine. Their Nevanlinna orders are respectively $0, 1, 1$ .

Verification

Given: The characteristic and order conventions, the fixed-rational composition law, complex sine and cosine defined from the complex exponential, the exponential modulus formula, and the stated real trigonometric facts.

[F1] For a meromorphic $h$ , $T (r, h) = m (r, \infty; h) + N (r, \infty; h)$ , where the chordal proximity is the circular mean of $\log (1 / δ (h, \infty))$ (Counting, chordal proximity and characteristic).

[F2] If $R$ is a fixed rational map of degree $q \geq 1$ and $h$ is nonconstant meromorphic, then $T (r, R (h)) = q T (r, h) + O_{R, h} (1)$ (Elementary characteristic laws and fixed rational composition).

[F3] For a nonconstant meromorphic $h$ , its order and lower order are the limsup and liminf of $\log T (r, h) / \log r$ on the eventual domain $r > 1$ , $T (r, h) > 1$ (Order and lower order from the Nevanlinna characteristic).

[F4] $\exp (u + v) = \exp u \exp v$ for all complex $u, v$ , and $\exp x = e^{x}$ for real $x$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[F5] For complex $z$ , $\sin z = \frac{\exp (i z) - \exp (- i z)}{2 i}, \cos z = \frac{\exp (i z) + \exp (- i z)}{2}$ (Complex sine, cosine, hyperbolic sine, and hyperbolic cosine from the complex exponential).

[F6] For real $x, y$ , $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ and $∣ \exp (x + i y) ∣ = e^{x}$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[F7] Sine is strictly increasing on $[- π / 2 + 2 m π, π / 2 + 2 m π]$ and strictly decreasing on $[π / 2 + 2 m π, 3 π / 2 + 2 m π]$ ; cosine is strictly decreasing on $[2 m π, (2 m + 1) π]$ and strictly increasing on $[(2 m + 1) π, (2 m + 2) π]$ (Signs, monotonicity intervals, and ranges of sine and cosine).

[F8] For real $x$ , $\sin (x + π / 2) = \cos x$ , $\cos (x + π / 2) = - \sin x$ , $\sin (x + π) = - \sin x$ , and $\cos (x + π) = - \cos x$ ; in particular $\sin (π / 2) = 1$ , $\cos (π / 2) = 0$ , $\sin π = 0$ , and $\cos π = - 1$ (Quarter-turn values and shifts by pi/2 and pi).

[F9] $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ , $\sin 0 = 0$ , and $\cos 0 = 1$ (The derivatives of sine and cosine are cosine and minus sine).

[F10] If $G^{'} = f$ on a compact interval and $f$ is integrable there, then $\int_{a}^{b} f = G (b) - G (a)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ).

[F11] A differentiable real function is continuous at each point where it is differentiable (A function differentiable at $c$ is continuous at $c$ ).

[F12] A continuous real function on a compact interval is Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[F13] The complex exponential is defined by $\exp z = \sum_{n \geq 0} z^{n} / n!$ , so $\exp 0 = 1$ (The complex exponential by its power series).

[F14] The complex exponential is entire and its derivative is itself (The complex exponential is entire and its complex derivative is itself).

[F15] A composite of holomorphic maps is holomorphic, and its derivative is the product of the derivatives (The composite of holomorphic maps is holomorphic and its complex Jacobian is the product).

[F16] A complex polynomial is entire (Complex polynomials are entire with the power-rule derivative, and rational functions are holomorphic wherever their denominator is nonzero).

[F17] A nonzero holomorphic function has isolated zeros (Zeros of a nonzero holomorphic function are isolated).

[F18] A finite-order zero has a local factorization $f (z) = (z - a)^{m} g (z)$ with $g (a) \neq 0$ (The order of a zero is the exponent in its local holomorphic factorization).

1.1F3F14step 1.2step 2.1step 1.3step 4.1algebra∎

Put $m_{0} (r, h) = (2 π)^{- 1} \int_{0}^{2 π} \log^{+} ∣ h (r e^{i t}) ∣ d t$ for an entire $h$ . Since such $h$ has no poles, [F1] gives $T (r, h) = m (r, \infty; h)$ . For every finite $w$ , $\log^{+} ∣ w ∣ \leq \frac{1}{2} \log (1 + ∣ w ∣^{2}) \leq \log^{+} ∣ w ∣ + \frac{1}{2} \log 2.$ Thus $m_{0} (r, h) \leq T (r, h) \leq m_{0} (r, h) + \frac{1}{2} \log 2$ . [F1, algebra] 1.2 For $h (z) = z^{d}$ , the pole count is zero and $∣ h (r e^{i t}) ∣ = r^{d}$ at every angle. Hence $T (r, z^{d}) = \frac{1}{2} \log (1 + r^{2 d}) = d \log r + \frac{1}{2} \log (1 + r^{- 2 d}) = d \log r + O (1) .$ [F1, algebra] 1.3 Set $E (z) = \exp (2 i z)$ . The linear polynomial $z \mapsto 2 i z$ is entire by [F16], the complex exponential is entire by [F14], and [F15] shows $E$ is entire with $E^{'} (0) = \exp^{'} (0) 2 i = 2 i \exp 0 = 2 i \neq 0$ , using [F13]. Thus $E$ is nonconstant. [F13, F14, F15, F16, algebra] 2.1 On $∣ z ∣ = r$ , Euler's formula in [F6] gives $z = r e^{i t} = r (\cos t + i \sin t)$ , so $∣ \exp (λ r e^{i t}) ∣ = e^{λ r \cos t} (λ > 0) .$ The logarithmic positive part is therefore $(λ r \cos t)^{+}$ . From [F7], cosine is strictly decreasing on $[0, π]$ and strictly increasing on $[π, 2 π]$ . By [F8] and [F9], it has values $1, 0, - 1, 0, 1$ at $0, π / 2, π, 3 π / 2, 2 π$ , respectively. These facts show cosine is positive on $[0, π / 2) \cup (3 π / 2, 2 π]$ and negative on $(π / 2, 3 π / 2)$ . By [F11], [F12], and [F10], the cosine integrals below exist and are evaluated using the primitive $\sin t$ : $\int_{0}^{2 π} (\cos t)^{+} d t = \int_{0}^{π / 2} \cos t d t + \int_{3 π / 2}^{2 π} \cos t d t = (\sin \frac{π}{2} - \sin 0) + (\sin 2 π - \sin \frac{3 π}{2}) = 2.$ Consequently $m_{0} (r, \exp (λ z)) = λ r / π$ . Step 1.1 now gives $T (r, \exp (λ z)) = λ r / π + O (1)$ , in particular the asserted formula for $\exp z$ . [F6, F7, F8, F9, F10, F11, F12, step 1.1, algebra] 2.2 Let $R (w) = - i (w - 1) / (w + 1)$ . This is a degree-one rational map. By [F2], $R (E)$ is the meromorphic composition to which the characteristic law applies. The definitions in [F5] and the addition law [F4] give, wherever $\cos z \neq 0$ , $\frac{\sin z}{\cos z} = - i \frac{\exp (2 i z) - 1}{\exp (2 i z) + 1} = - i \frac{E (z) - 1}{E (z) + 1} .$ Indeed [F4] and [F13] give $\exp (i z) \exp (- i z) = 1$ , so multiplying the numerator and denominator in [F5] by $\exp (i z)$ is legitimate. They give $\cos z = \frac{\exp (- i z) (E (z) + 1)}{2}, \sin z = \frac{\exp (- i z) (E (z) - 1)}{2 i} .$ Thus $\cos z = 0$ exactly when $E (z) = - 1$ . Since $E$ is nonconstant by step 1.3, [F17] makes each zero of $E + 1$ isolated, and [F18] factors it with a finite positive order there. At such a point $E - 1 = - 2$ , so $R (E)$ has a pole of that order, while the quotient has the same pole because its numerator is nonzero. At every other point the quotient equals $R (E)$ . Hence $R (E)$ is precisely the meromorphic continuation of $\sin z / \cos z$ , the complex tangent used here. [F2, F4, F5, F13, F17, F18, step 1.3, algebra] 3.1 For $z = r e^{i t}$ , [F6] and the decomposition in step 2.1 give $\log^{+} ∣ E (r e^{i t}) ∣ = (- 2 r \sin t)^{+} .$ By [F7], [F8], and [F9], sine increases from $0$ to $1$ on $[0, π / 2]$ , decreases to $0$ on $[π / 2, π]$ , and its shift by $π$ changes sign. Thus it is positive on $(0, π)$ and negative on $(π, 2 π)$ . By [F11], [F12], and [F10], $- \sin t$ is integrable and has primitive $\cos t$ . Hence $\int_{0}^{2 π} (- \sin t)^{+} d t = \int_{π}^{2 π} - \sin t d t = \cos 2 π - \cos π = 2,$ and $m_{0} (r, E) = 2 r / π$ . Step 1.1 gives $T (r, E) = 2 r / π + O (1)$ . [F6, F7, F8, F9, F10, F11, F12, step 1.1, step 2.1, algebra] 4.1 The numerator and denominator of $R$ are coprime linear polynomials, so $R$ has degree one. By [F2], step 1.3, step 2.2, and step 3.1, $T (r, \tan z) = T (r, R (E (z))) = T (r, E) + O (1) = \frac{2 r}{π} + O (1) .$ [F2, step 1.3, step 2.2, step 3.1, algebra] 5.1 For each $d \geq 1$ , step 1.2 has $T (r, z^{d}) = d \log r + O (1) > 1$ eventually, so $\log T (r, z^{d}) / \log r \to 0$ . Steps 2.1 and 4.1 give positive linear growth for $\exp z$ and $\tan z$ , so for either function $\log T (r, h) = \log r + O (1)$ and the ratio tends to $1$ . The three functions are nonconstant (the monomial has $d \geq 1$ , $\exp z$ has derivative $1$ at zero by [F14], and step 1.3 shows $E$ is nonconstant; the positive linear growth of $R (E)$ in step 4.1 also rules out a constant tangent). Thus [F3] applies; in each case the limsup and liminf agree with the computed limit.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

101 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, §2, Exercise 2* (standard reference, not scraped)
Goldberg–Ostrovskii, Value Distribution of Meromorphic Functions, Ch. 1 §6, Theorems 6.1–6.2 and Corollary (6.26) (standard reference, not scraped)