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.

Reciprocal Gamma has order one and characteristic of size $r \log r$

Example

Let $g (z) = 1 / Γ (z)$ be the reciprocal Gamma function. Its zeros are simple and are exactly $0, - 1, - 2, \dots$ , and it has no poles. For every sufficiently large $r$ , $T (r, g) = Θ (r \log r) .$ Consequently its Nevanlinna order and lower order are both one.

Verification

Given: The characteristic and order conventions for meromorphic functions, the reciprocal-Gamma product, Gamma's meromorphic continuation, and the sectorial Stirling formula.

[F1] $T (r, h) = m (r, \infty; h) + N (r, \infty; h)$ , where $m (r, \infty; h)$ is the circular mean of $\frac{1}{2} \log (1 + ∣ h ∣^{2})$ (Counting, chordal proximity and characteristic).

[F2] The order and lower order are the limsup and liminf of $\log T (r, h) / \log r$ for all sufficiently large $r$ with $T (r, h) > 1$ (Order and lower order from the Nevanlinna characteristic).

[F3] The reciprocal Gamma product $\frac{1}{Γ (z)} = z e^{γ z} \prod_{n \geq 1} (1 + \frac{z}{n}) e^{- z / n}$ converges locally uniformly on $C$ (The Weierstrass product for reciprocal Gamma).

[F4] For fixed $0 < δ < π$ , on the closed sector $∣ \arg z ∣ \leq π - δ$ , with the principal logarithm in $z^{z - 1 / 2} = \exp ((z - \frac{1}{2}) Log z)$ , $Γ (z) = \sqrt{2 π} z^{z - 1 / 2} e^{- z} (1 + O_{δ} (∣ z ∣^{- 1}))$ as $∣ z ∣ \to \infty$ (Stirling's formula for Gamma).

[F5] Gamma is meromorphic on $C$ with simple poles exactly at the nonpositive integers (Meromorphic continuation of Gamma).

1.1F3F5algebra

By [F3], the product defines an entire function $g$ . On every compact $K$ , for all large $n$ the series for $Log (1 + z / n) - z / n$ is bounded by $C_{K} n^{- 2}$ uniformly on $K$ , so the product tail is the exponential of a locally uniformly convergent sum and is nowhere zero. The finitely many factors then give simple zeros exactly at $0, - 1, - 2, \dots$ ; [F5] identifies these with the simple poles of the meromorphic continuation of $Γ$ , and $g$ has no poles.

1.2F3algebra

Fix $r \geq 2$ and $∣ z ∣ = r$ . At a product zero the upper bound is immediate; otherwise $\log ∣ g (z) ∣ = \log r + ℜ (γ z) + \sum_{n \geq 1} (\log ∣ 1 + z / n ∣ - ℜ z / n)$ . For $n \leq 2 r$ , the summands are at most $\log (1 + r / n) + r / n$ , with total $O (r \log r)$ . For $n > 2 r$ , $w = z / n$ satisfies $∣ w ∣ < 1 / 2$ , so $\log ∣ 1 + w ∣ - ℜ w = ℜ (Log (1 + w) - w) \leq \sum_{k \geq 2} ∣ w ∣^{k} / k \leq C ∣ w ∣^{2}$ ; the tail is at most $C r^{2} \sum_{n > 2 r} n^{- 2} = O (r)$ . Since $∣ ℜ (γ z) ∣ \leq ∣ γ ∣ r$ , this gives $\log^{+} ∣ g (z) ∣ \leq C r \log r$ uniformly on the circle, and hence $m_{0} (r, g) = O (r \log r)$ .

1.3F3F4algebra

Set $δ = π / 4$ and $I = [2 π / 3, 3 π / 4]$ , a fixed arc in the closed sector $∣ \arg z ∣ \leq 3 π / 4$ . For $z = r e^{i t}$ with $t \in I$ , [F3] identifies $g$ with $1 / Γ$ and [F4] applies uniformly: writing its error as $E (z) = O (r^{- 1})$ , $\log ∣ g (r e^{i t}) ∣ = - r \cos t \log r + r t \sin t + r \cos t + \frac{1}{2} \log r - \frac{1}{2} \log (2 π) + O (r^{- 1})$ . Since $- \cos t \geq 1 / 2$ , $t \sin t \geq 0$ , and $\cos t \geq - 1$ , this is at least $\frac{1}{4} r \log r > 0$ for all sufficiently large $r$ , uniformly on $I$ . This closed arc meets the exact sector hypotheses in [F4].

2.1step 1.3algebra

Integrating the lower bound of step 1.3 over the arc of length $π / 12$ gives $m_{0} (r, g) : = (2 π)^{- 1} \int_{0}^{2 π} \log^{+} ∣ g (r e^{i t}) ∣ d t \geq (1 / 96) r \log r$ for all sufficiently large $r$ .

3.1F1F2step 1.2step 2.1algebra∎

Since $g$ is entire, [F1] gives $T (r, g) = m (r, \infty; g)$ . The pointwise inequality $\log^{+} ∣ w ∣ \leq \frac{1}{2} \log (1 + ∣ w ∣^{2}) \leq \log^{+} ∣ w ∣ + \frac{1}{2} \log 2$ gives $m_{0} (r, g) \leq T (r, g) \leq m_{0} (r, g) + \frac{1}{2} \log 2$ . Steps 1.2 and 2.1 prove $T (r, g) = Θ (r \log r)$ , so $T > 1$ eventually. By [F2], $\log T (r, g) / \log r = (\log r + \log \log r + O (1)) / \log r \to 1$ , proving both order assertions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

Goldberg–Ostrovskii, Value Distribution of Meromorphic Functions, Ch. 2 §5, reciprocal-Gamma exercise, printed pp. 80–81 (standard reference, not scraped)
K. Chandrasekharan, Lectures on the Riemann Zeta-Function, Lecture 7 §6, Stirling formula, printed pp. 60–62 (standard reference, not scraped)

Reciprocal Gamma has order one and characteristic of size rlog⁡rrlogr