ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

Maximum crossing before a fixed time

Example

Assume the Axiom of Choice and let $B$ be a standard Brownian motion Brownian motion. Use the everywhere-continuous, zero-start representative fixed in Law of the Brownian maximum: replace the path by zero outside a measurable probability-one event of continuity and zero start, retaining the notation $B$ . Let $M_{t} = \sup_{0 \leq s \leq t} B_{s}$ . This is a finite measurable random variable because its continuous-path supremum on $[0, t]$ equals the supremum over $(Q \cap [0, t]) \cup {t}$ . For $a > 0$ and $t > 0$ , $P (M_{t} \geq a) = 2 (1 - Φ ⁣ (\frac{a}{\sqrt{t}})),$ where $Φ$ is the standard normal distribution function Standard normal and normal laws Cumulative distribution function of a real random variable. The value tends to $1$ as $a ↓ 0$ and to $0$ as $a \to \infty$ ; at $t$ fixed, the probability is decreasing in $a$ .

Facts & Assumptions

Given: AC, a standard Brownian motion $B$ in the stated everywhere-continuous zero-start representative, and reals $a > 0$ , $t > 0$ .

[F1]

$P (M_{t} \leq x) = 2 Φ (x / \sqrt{t}) - 1$ for $x \geq 0$ , and the law of $M_{t}$ is atomless; hence $P (M_{t} < a) = P (M_{t} \leq a)$ and $P (M_{t} \geq a) = 1 - P (M_{t} < a)$ . Law of the Brownian maximum

[F2]

$Φ (0) = 1 / 2$ , $\lim_{x \to \infty} Φ (x) = 1$ , and $Φ$ is continuous and nondecreasing. Standard normal and normal laws Cumulative distribution function of a real random variable

[F3]

AC is the standing hypothesis under which the Brownian maximum and normal-law interfaces in [F1]-[F2] are supplied; this example makes no additional selection. The Axiom of Choice

Verification

technique · direct

1.1

By [F1], $P (M_{t} \geq a) = 1 - P (M_{t} < a) = 1 - P (M_{t} \leq a) = 1 - (2 Φ (a / \sqrt{t}) - 1) = 2 (1 - Φ (a / \sqrt{t}))$ for every $a > 0$ and $t > 0$ , which is the displayed value.

F1given

2.1

As $a ↓ 0$ one has $a / \sqrt{t} ↓ 0$ , so continuity of $Φ$ at $0$ with $Φ (0) = 1 / 2$ gives $2 (1 - Φ (a / \sqrt{t})) \to 2 (1 - 1 / 2) = 1$ ; as $a \to \infty$ one has $a / \sqrt{t} \to \infty$ and $Φ \to 1$ , so the value tends to $0$ . Since $Φ$ is nondecreasing, the value is nonincreasing in $a$ .

F2step 1.1

3.1

The boundary cases are consistent: at $a = 0$ the formula would give $1$ , while the stated range is $a > 0$ ; the case $t > 0$ is essential because the normalization $a / \sqrt{t}$ uses a positive square root. AC is used only through [F3].

F1F3givenstep 2.1∎

Source notes

Durrett, Section 7.4, records the crossing probability as the reflection consequence; the example adds the two limiting checks explicitly.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

Rick Durrett, Probability: Theory and Examples, fifth edition, Section 7.4 (standard reference, not scraped)