ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

Exit side from an interval

Example

Assume the Axiom of Choice and fix the everywhere-continuous zero-start representative $B$ used for the law $P_{0}$ in Brownian motion started at x (hence a standard Brownian motion in the sense of Brownian motion). Define $T_{c}$ from this fixed representative. For the interval with endpoints $- 2$ and $3$ , $P (T_{3} < T_{- 2}) = \frac{2}{5}, P (T_{- 2} < T_{3}) = \frac{3}{5},$ where $T_{c}$ denotes the first hitting time of the level $c$ . The two values sum to $1$ , as they must.

Facts & Assumptions

Given: AC and the fixed everywhere-continuous representative of standard Brownian motion started at $0$ under $P_{0}$ .

[F1]

Two-sided exit probability: for $a < x < b$ and the shifted law $P_{x}$ , $P_{x} (T_{b} < T_{a}) = \frac{x - a}{b - a}$ . Two-sided Brownian exit probability

[F2]

The unshifted law is $P_{0}$ , and the hitting times in the Example are defined from the same fixed everywhere-continuous zero-start representative, so $P (T_{3} < T_{- 2}) = P_{0} (T_{3} < T_{- 2})$ . Brownian motion started at x Brownian motion

[F3]

AC is the ambient assumption of the Brownian construction. The Axiom of Choice

[F4]

For this fixed everywhere-continuous zero-start representative, one-dimensional Brownian motion hits every level almost surely, so both $T_{3}$ and $T_{- 2}$ are finite almost surely, and the process cannot be at the two levels at the same time. One-dimensional Brownian motion hits every point almost surely Brownian motion started at x

Verification

technique · direct

1.1F1F2given

Apply [F1] with $a = - 2$ , $x = 0$ , $b = 3$ : $P_{0} (T_{3} < T_{- 2}) = \frac{0 - (- 2)}{3 - (- 2)} = \frac{2}{5}$ .

2.1F4step 1.1

The events ${T_{3} < T_{- 2}}$ and ${T_{- 2} < T_{3}}$ are disjoint, and their union has probability one because both hitting times are finite almost surely by [F4] and the process cannot be at both levels at once; hence $P (T_{- 2} < T_{3}) = 1 - \frac{2}{5} = \frac{3}{5}$ .

3.1F3givenstep 2.1∎

The values $\frac{2}{5} + \frac{3}{5} = 1$ sum to one, the starting point $0$ lies strictly between the endpoints, and the common denominator $b - a = 5$ is nonzero. AC is used only through [F3].

Source notes

Durrett, Theorem 7.5.3, states the two-sided exit probability used here; the example substitutes the pair of endpoints and checks the complementary probability.

Remarks

The number line shows the starting point and the two first-exit alternatives. The arrows indicate which boundary is hit first, not sample paths or a process stopped at a boundary. The two events partition a probability-one set, as verified in step 2.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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, Theorem 7.5.3 (standard reference, not scraped)