ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Bayes' theorem for choosing one of two urns and observing a colour

Example

Choose urn $U_{1}$ with probability $1 / 3$ and urn $U_{2}$ with probability $2 / 3$ , independently choose a uniform auxiliary value $r \in {1, 2, 3, 4}$ , and declare the observation red when $U_{1}$ was chosen and $r \leq 3$ , or when $U_{2}$ was chosen and $r = 1$ . Thus the red likelihoods are $3 / 4$ and $1 / 4$ , respectively. The posterior probability of $U_{1}$ after observing red is $3 / 5$ .

Facts & Assumptions

Given: The finite two-stage experiment in the Example.

[L1]

Bayes' theorem over a positive-probability finite partition gives posterior probability as prior times likelihood divided by total likelihood (Bayes' theorem over a finite partition).

[L2]

A finite product experiment assigns product weights to its branches (The finite product of finite probability spaces).

[L3]

Conditional probability is the probability of an intersection divided by the positive probability of the conditioning event (Conditional probability $P (A ∣ B)$ for $P (B) > 0$ ).

Verification

technique · direct

1.1

In the product space, the three red branches over $U_{1}$ have total weight $(1 / 3) (3 / 4) = 1 / 4$ , and the one red branch over $U_{2}$ has weight $(2 / 3) (1 / 4) = 1 / 6$ . Hence $P (r e d) = 5 / 12 > 0$ .

L2algebra

2.1

Directly, $P (U_{1} ∣ r e d) = (1 / 4) / (5 / 12) = 3 / 5$ .

step 1.1L3algebra

3.1

Bayes' formula [L1] has the same numerator $1 / 4$ and denominator $1 / 4 + 1 / 6 = 5 / 12$ , so it also gives $3 / 5$ .

step 1.1step 2.1L1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 25 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

C. M. Grinstead and J. L. Snell, Introduction to Probability, 2nd ed., Section 4.1 (standard reference, not scraped)