ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Wald's equation for a bounded stopping time

Statement

Let $N \in N$ with $N \geq 1$ , let $X_{k}$ be iid Bernoulli $(p)$ , $0 < p \leq 1$ , and use the natural filtration $F_{n} = σ (X_{1}, \dots, X_{n})$ (with $F_{0}$ trivial). Set $τ = \min (\inf {k \geq 1 : X_{k} = 1}, N) .$ Then $E τ = \frac{1 - (1 - p)^{N}}{p}, E \sum_{k = 1}^{τ} X_{k} = 1 - (1 - p)^{N} = p E τ .$

Facts & Assumptions

Given: The hypotheses, objects, and conventions in the Statement.

[F1]

Wald first equation under integrable stopping applies because $τ$ is a stopping time for the natural filtration and $τ \leq N$ .

Proof

1.1

For every $n$ , the event ${τ \leq n}$ is determined by $X_{1}, \dots, X_{n}$ , so $τ$ is a stopping time for the stated filtration; it is bounded by $N$ . The event ${τ \geq k}$ for $1 \leq k \leq N$ says the first $k - 1$ trials failed, so it has probability $(1 - p)^{k - 1}$ . The tail sum therefore gives $E τ = \sum_{k = 1}^{N} (1 - p)^{k - 1} = \frac{1 - (1 - p)^{N}}{p},$ including $p = 1$ , when the geometric sum is $1$ .

2.1

The stopped sum is exactly the indicator that at least one of the first $N$ trials succeeds: after the first success the sum stops, while if all fail it is zero. Its expectation is $1 - (1 - p)^{N}$ . Since $E X_{1} = p$ , F1 also gives it as $p E τ$ , agreeing with step 1.1. The argument is choice-free.

F1step 1.1∎

Depends on

Wald first equation under integrable stopping

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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

Durrett, Probability: Theory and Examples, 5th ed., Wald's equation in §4.8 (standard reference, not scraped)