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

Brownian bridge from Brownian motion

Example

Assume the Axiom of Choice. Let B be a standard Brownian motion and, for 0t1, define

βt=BttB1.

Then β is a centered Gaussian process with one almost-surely continuous path event,

Cov(βs,βt)=min(s,t)st(0s,t1),

and β0=0 almost surely while β1=0 identically. This is the standard Brownian bridge from 0 to 0 over [0,1].

Facts & Assumptions

Given: AC and a standard Brownian motion B.

[F1]

Brownian motion is a centered Gaussian process with covariance Cov(Bs,Bt)=min(s,t) and has one probability-one continuity event. Brownian motion, Gaussian process.

[F2]

Covariance is symmetric and bilinear in finite linear combinations. Covariance is symmetric and bilinear in finite linear combinations.

[F3]

The Lebesgue integral, hence expectation on an arbitrary probability space, is linear on finite linear combinations of integrable random variables. The Lebesgue integral is linear on L1(μ).

[F5]

A finite intersection of probability-one events has probability one. Basic identities for a probability measure.

[F6]

AC is inherited through the Brownian and Gaussian-law interfaces. The Axiom of Choice.

Verification

technique · direct
1.1

Fix n1, times t1,,tn[0,1], and coefficients a1,,an. Then j=1najβtj=j=1najBtj(j=1najtj)B1. This is a finite linear combination of Brownian values, with time 1 appended if necessary, so [F1] makes it normal; repeated occurrences of time 1, repeated tj, and zero coefficients are allowed. Its mean is zero by finite linearity because all Brownian values are centered. Hence β is a centered Gaussian process.

F1F3algebra
1.2

For s,t[0,1], covariance bilinearity gives Cov(βs,βt)=min(s,t)tmin(s,1)smin(1,t)+stVar(B1). Since s,t1 and Var(B1)=1, this is min(s,t)tsst+st=min(s,t)st.

F1F2algebra
1.3

Let A be the probability-one event on which tBt(ω) is continuous on [0,), and let A0={B0=0}. Their intersection has probability one by [F5]. For ωAA0, the map ttB1(ω) is continuous and [F4] makes tβt(ω) continuous on [0,1]. On this event β0=B0=0, while for every ω one has β1=B1B1=0.

F1F4F5algebra
2.1

Steps 1.1--1.3 establish Gaussianity, centering, the covariance, path continuity, and both endpoints. The cases s=0, t=0, s=t, and s=t=1 follow directly from the same covariance formula, including its zero endpoint variances. The empty finite-dimensional list, if admitted, has the unique empty-tuple law. AC is used only through [F1]; the deterministic linear transformation and continuity argument make no new choice.

step 1.1step 1.2step 1.3F1F6

Source notes

Yoshida, Exercise 6.1.10, printed p. 180, defines a Brownian bridge from a to b over duration s as Bt(t/s)Bs+(1t/s)a+(t/s)b. Durrett, Section 8.4, printed pp. 412--413, specializes this to BttB1 and computes the covariance s(1t) for s<t. The proof above supplies all finite-dimensional and endpoint details.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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