ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated

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.

Gamma-Poisson updating with a zero exposure

Statement

Assume Countable Choice. Take $λ \sim Gamma (2, 1)$ and two independent counts with exposures $(e_{1}, e_{2}) = (2, 0)$ . For observed counts $(y_{1}, y_{2}) = (3, 0)$ , the evidence is $32 / 243$ and the posterior is $Gamma (5, 3)$ . If the zero-exposure count were instead $y_{2} = 1$ , its evidence would be zero and no posterior quotient would be defined.

Facts & Assumptions

Given: Countable Choice, shape $a = 2$ , rate $b = 1$ , exposures $(2, 0)$ , and counts $(3, 0)$ .

[A1]

Countable Choice is assumed by the Gamma density normalization used by the update theorem. The Axiom of Countable Choice ( ${A C}_{ω}$ ).

[F1]

For compatible zero-exposure data, the evidence is $c b^{a} Γ (a + S) / [Γ (a) (b + E)^{a + S}]$ and the posterior is Gamma $(a + S, b + E)$ ; an impossible zero-exposure count has zero evidence. Exposure-adjusted Gamma-Poisson conjugate update.

[F2]

For positive integers, $Γ (r + 1) = r!$ . $Γ (n + 1) = n!$ for every natural number $n$ .

Proof

Given: Countable Choice, the stated prior, exposures, and counts.

1.1A1F1F2algebra

Here $S = 3$ , $E = 2$ , and $c = 2^{3} / 3! = 4 / 3$ because the zero-exposure observation contributes factor one. By [F2], $Γ (5) = 24$ and $Γ (2) = 1$ . Substitution in [F1] gives $m (3, 0) = \frac{4}{3} \frac{Γ (5)}{Γ (2) 3^{5}} = \frac{4}{3} \frac{24}{243} = \frac{32}{243} .$

1.2A1F1givenalgebra

The updated shape is $2 + 3 = 5$ and the updated rate is $1 + 2 + 0 = 3$ , so [F1] gives $Gamma (5, 3)$ .

2.1A1F1cases∎

If $y_{2} = 1$ at exposure $e_{2} = 0$ , that observation is impossible under every $λ$ by [F1]. The likelihood is identically zero, its evidence is zero, and the finite-positive condition for a quotient fails.

Depends on

Used by

Nothing in the library uses this result yet.

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

Gelman et al., Bayesian Data Analysis, 3rd ed., §2.4 (standard reference, not scraped)
Johnson, Ott & Dogucu, Bayes Rules!, Chapter 5, §5.2.2 (standard reference, not scraped)