LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Shifted log-Gamma branch is independent of the shift

Statement

For every $z \in Ω = C ∖ (- \infty, 0]$ , the value $ℓ (z)$ in Log-Gamma branch on the slit plane is independent of the integer $m \geq 0$ with $Re (z + m) > 0$ , is holomorphic on $Ω$ , and satisfies $e^{ℓ (z)} = Γ (z)$ .

Facts & Assumptions

Given: $z \in Ω$ and the branch definitions Log-Gamma branch on the right half-plane and Log-Gamma branch on the slit plane.

[F1]

Weierstrass log-Gamma series converges to a Gamma branch: $e^{ℓ_{+} (w)} = Γ (w)$ and $ℓ_{+}$ is holomorphic for $Re w > 0$ .

[F2]

The Gamma functional equation: if $Re w > 0$ , then $Γ (w + 1) = w Γ (w)$ .

[F3]

Gamma functional equation away from the poles: the same functional equation holds when $w$ is not a nonpositive integer.

[F4]

The principal logarithm is the normalised holomorphic branch on the slit plane: $Log$ is holomorphic on the slit plane and ${Log}^{'} (w) = 1 / w$ . Complex logarithms, the principal logarithm, and principal and multivalued complex powers and Every nonzero complex number has a unique polar form $r (\cos θ + i \sin θ)$ with $r > 0$ and $- π < θ \leq π$ give $Log w = \log w \in R$ for positive real $w$ .

[F5]

The complex exponential is entire and its complex derivative is itself and The chain rule for complex derivatives: $(e^{H})^{'} = e^{H} H^{'}$ for holomorphic $H$ .

[F6]

A differentiable map on a connected open Euclidean set has zero derivative exactly when it is constant: a holomorphic function with zero derivative on a connected open domain is constant.

[F7]

$\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential and The complex exponential by its power series: $\exp (u + v) = \exp (u) \exp (v)$ and $\exp (0) = 1$ . In particular, $\exp (- v)$ is the reciprocal of $\exp (v)$ .

[F8]

The natural logarithm as the inverse of the exponential function and Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: on the positive reals, $\log$ is the inverse of $\exp$ and $\log 1 = 0$ .

[F9]

Real and imaginary parts, complex conjugation, and modulus, Real and complex modulus product and triangle inequalities, and Every path-connected space is connected, and every path component lies inside a component: the right half-plane is open, since if $x = Re w_{0} > 0$ and $∣ w - w_{0} ∣ < x$ , then $Re w \geq x - ∣ Re (w - w_{0}) ∣ \geq x - ∣ w - w_{0} ∣ > 0$ . For $w_{0}, w_{1}$ in it, $γ (t) = (1 - t) w_{0} + t w_{1}$ has positive real part and $∣ γ (t) - γ (s) ∣ = ∣ t - s ∣ ∣ w_{1} - w_{0} ∣$ , which proves continuity by the metric definition. The half-plane contains $1$ and is open and connected.

[F10]

Complex differentiability is equivalent to real total differentiability together with a complex-linear derivative, with $\partial_{\overset{ˉ}{z}} f = 0$ , or with the Cauchy–Riemann equations: under $C ≅ R^{2}$ , a complex-differentiable function is totally differentiable and its real derivative is multiplication by its complex derivative; in particular, $H^{'} = 0$ implies $D H = 0$ .

Proof

1.1F1F2F4F5F6F7F8F9F10algebra

For $Re w > 0$ , the function $H (w) = ℓ_{+} (w + 1) - ℓ_{+} (w) - Log w$ is holomorphic by [F1]. The functional equation [F2], branch identity [F1], and $\exp (Log w) = w$ from [F4] give $\exp (ℓ_{+} (w + 1)) = \exp (ℓ_{+} (w) + Log w)$ . By [F7], $\exp (H (w)) = 1$ . Differentiating this identity by [F5] gives $\exp (H (w)) H^{'} (w) = 0$ , hence $H^{'} (w) = 0$ . By [F10], the real derivative of $H$ vanishes; the right half-plane is nonempty, open, and connected by [F9], so [F6] makes $H$ constant there. For positive real $w$ , all three terms are real by the defining series for $ℓ_{+}$ and the real logarithm, so [F8] and $\exp (H (w)) = 1$ imply $H (w) = \log 1 = 0$ . Therefore $ℓ_{+} (w + 1) = ℓ_{+} (w) + Log w$ throughout the right half-plane.

2.1givenstep 1.1algebra

If $m_{2} > m_{1}$ are both admissible shifts, then $w = z + m_{1}$ has positive real part, as do $w, w + 1, \dots, w + (m_{2} - m_{1} - 1)$ . Iterating step 1.1 gives $ℓ_{+} (z + m_{2}) - \sum_{j = 0}^{m_{2} - 1} Log (z + j) = ℓ_{+} (z + m_{1}) - \sum_{j = 0}^{m_{1} - 1} Log (z + j),$ so the definition is independent of $m$ . Locally $m$ can be fixed, making the formula holomorphic; independence makes these local formulas agree.

3.1F1F3step 2.1algebra∎

Exponentiating the formula with any admissible $m$ gives $e^{ℓ (z)} = Γ (z + m) / \prod_{j = 0}^{m - 1} (z + j)$ by [F1]. None of the factors vanishes because $z \in Ω$ . Iterating [F3] downward therefore identifies this quotient with $Γ (z)$ .

Depends on

Used by

Cited to discharge well-definedness by Log-Gamma branch on the slit plane.

Dependency tree · two levels

104 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

DLMF, §5.11, asymptotic expansions (standard reference, not scraped)
DLMF, §5.5, functional relations (standard reference, not scraped)
DLMF, §§5.5, 5.8, and 5.11 (standard reference, not scraped)
N. M. Temme, “Numerical aspects of special functions,” Acta Numerica 17 (2008), §§2 and 3 (standard reference, not scraped)