ExampleConstruction: AI-adaptedVerification: 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.

LIL rules out a square-root-time bound

Example

Let $B$ be a standard Brownian motion. Almost surely there is no finite random constant $C$ and no random $δ > 0$ such that $∣ B_{t} ∣ \leq C \sqrt{t} for all 0 < t < δ .$ Thus the square-root bound that holds in expectation for a single time is false as a pathwise statement near the origin.

Facts & Assumptions

Given: AC and a standard Brownian motion $B$ .

[F1]

Almost surely ${lim sup}_{t ↓ 0} B_{t} / \sqrt{2 t \log \log (1 / t)} = 1$ and the corresponding limit inferior is $- 1$ . Brownian law of the iterated logarithm at zero

[F2]

AC is assumed explicitly in this example. The Axiom of Choice

Verification

technique · direct

1.1

On the probability-one event of [F1], combining the two limit statements gives ${lim sup}_{t ↓ 0} ∣ B_{t} ∣ / \sqrt{2 t \log \log (1 / t)} = 1$ , so there are $t_{n} ↓ 0$ with $\sqrt{2 \log \log (1 / t_{n})} ∣ B_{t_{n}} ∣ / \sqrt{2 t_{n} \log \log (1 / t_{n})} \to \infty$ .

givenF1

2.1

For such a sequence $∣ B_{t_{n}} ∣ / \sqrt{t_{n}} = \sqrt{2 \log \log (1 / t_{n})} \cdot \frac{∣ B_{t_{n}} ∣}{\sqrt{2 t_{n} \log \log (1 / t_{n})}} \to \infty$ ; hence for every finite constant $c$ there exist $t \in (0, δ)$ with $∣ B_{t} ∣ > c \sqrt{t}$ , whatever $δ > 0$ is prescribed, which is exactly the failure of the displayed bound for a finite random $C$ and random $δ > 0$ .

step 1.1

3.1

The cases are covered: only $t > 0$ is quantified, so the normalizer $\log \log (1 / t)$ is defined and positive for small $t$ ; the constant $C$ is allowed to be random and finite, and the argument produces, on the given outcome, arbitrarily small times violating any fixed finite value; and AC enters only through [F2].

step 2.1F2given∎

Source notes

The law of the iterated logarithm at zero does more than fail to provide a one-half modulus: it exhibits a sequence of times along which $∣ B_{t} ∣ / \sqrt{t}$ diverges. Durrett's Theorem 8.5.1, transported to zero, is the source of that sequence.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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 8.5.1 (standard reference, not scraped)