TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

The real Beta--Gamma identity

Statement

For $p, q > 0$ , $B (p, q) = Γ (p) Γ (q) / Γ (p + q)$ .

Facts & Assumptions

Given: Positive reals $p, q$ and the nonnegative function $x^{p - 1} y^{q - 1} e^{- (x + y)}$ on the open first quadrant.

[F1]

If $f : D \to [0, \infty)$ is locally Riemann integrable and $(K_{j})$ is a compact Jordan exhaustion, then $\int_{D} f = \sup_{j} \int_{K_{j}} f$ , independently of the exhaustion (Every Jordan exhaustion computes a nonnegative improper multiple integral).

[F2]

If $g : U \to R^{n}$ is injective and $C^{1}$ with invertible derivative on an open set, $K \subseteq U$ is compact Jordan, and $f$ is bounded on $g (K)$ , then $f$ is integrable exactly when $(f \circ g) ∣ \det D g ∣$ is, and their integrals are equal (Change of variables for an injective $C^{1}$ map on a compact Jordan set).

[F3]

If $A, B$ are nondegenerate closed rectangles, $f$ is integrable on $A \times B$ , and every section in one coordinate order is integrable, then the ordinary iterated integral in that order exists and equals the multiple integral (Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections).

Proof

technique · direct

1.1F1F3

On compact rectangles inside the first quadrant, [F3] factors the integral as a product of one-variable integrals. Passing through rectangular exhaustion by [F1] gives total improper integral $Γ (p) Γ (q)$ .

1.2F2algebra

On compact rectangles inside $(0, \infty) \times (0, 1)$ use $x = r t$ , $y = r (1 - t)$ . The map is injective, its absolute Jacobian is $r$ , and [F2] transforms the integrand times Jacobian into $r^{p + q - 1} e^{- r} t^{p - 1} (1 - t)^{q - 1}$ .

2.1step 1.1step 1.2F1F3

A fixed nested family of such compact rectangles maps to a cofinal exhaustion of the first quadrant. By [F1] the limit is independent of this exhaustion, and by [F3] the transformed integral factors as $Γ (p + q) B (p, q)$ .

3.1step 2.1algebra∎

Gamma is positive on the positive axis, so division of the equality in step 2.1 by $Γ (p + q)$ gives the claimed identity.

The real Beta--Gamma identity

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources