Alphabeta Math
Pipeline-generated
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.

Function-space pCN and invariant posterior kernels — Examples and Counterexamples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Infinite-dimensional Gaussian random-walk reverse flow is singular

Statement refuted

Assume the Axiom of Choice and fix β∈(0,1]. Let H=ℓ2(N,R) with its complete coordinate basis positively indexed as (ej)j≥1, where ej has its nonzero coordinate at j−1. Write uj=⟨u,ej⟩ for coefficients in this basis throughout. Take mutually independent standard normal variables (Xj,Yj)j≥1 and set U=∑j≥12−j/2Xjej,ξ=∑j≥12−j/2Yjej. These series converge almost surely in H and define independent centered Borel Gaussian random elements with the same law μ0. Define the Gaussian random-walk proposal V=U+βξ, its probability kernel Qβ(u,B)=μ0({z∈H:u+βz∈B}), its forward flow η(du,dv)=μ0(du)Qβ(u,dv), and its transpose η⊤(C)=η({(u,v):(v,u)∈C}). Then η and η⊤ are mutually singular: a Borel set Aβ⊆H×H satisfies η(Aβ)=1,η⊤(Aβ)=0. For the same reference law and scale, the pCN proposal flow is symmetric.

Facts & Assumptions

Given: AC, β∈(0,1], and the Gaussian sequence and Hilbert-space notation of the Statement.

[A1]

AC implies both Dependent Choice and Countable Choice. The Axiom of Choice AC implies DC implies countable choice

[F2]

After the explicit reindexing j↦j−1 for j≥1, the coordinate vectors form a complete orthonormal basis of H, and the norm squared is the sum of coordinate squares. Coordinate vectors form the Hilbert basis of real ell-two

[F3]

For independent standard normal coordinates and weights λj=2−j, the series ∑jλjXjej converges almost surely in H and defines a centered Borel Gaussian random element. Its coordinates are 2−j/2Xj. Weighted Hilbert Gaussian series and prior regularity Coordinate vectors form the Hilbert basis of real ell-two

[F4]

Disjoint subfamilies of an independent family generate independent sigma-algebras, and measurable functions of independent random elements remain independent. Independent random elements Disjoint groups of an independent sigma-algebra family remain independent Measurable coordinatewise functions preserve independence

[F5]

A N(0,1) variable has mean zero, second moment one, and fourth moment three. Location-scale normal laws have their stated mean and variance A normal variable has finite fourth moment

[F6]

Expectations of integrable products of independent variables factor. Expectations factor over finite products of independent random variables

[F7]

IID square-integrable real variables satisfy the strong law of large numbers. Identical distribution and IID families Iid finite variance strong law

[F8]

For a probability measure and a probability kernel, the associated joint flow is a probability measure with the iterated-integral identity. Measure kernel and probability kernel A prior and model kernel define a joint law

[F9]

Integrating a Borel function against a random-element law equals its expectation; independent random elements have product joint law. Law or distribution of a random element Change of variables for expectation Independent random elements have product joint law

[F10]

The Borel sigma-algebra of a topological space is generated by its open sets; Borel measurable functions are closed under finite arithmetic operations. The Borel sigma-algebra of a topological space Arithmetic and lattice operations preserve measurability whenever they are defined

[F11]

The finite-support vectors with rational coordinates form a countable dense subset of H=ℓ2: for each N the rational vectors supported in the first N coordinates are countable by the rational countability and finite product facts, their union is countable by Countable Choice, and density follows from finite truncation convergence and rational approximation of each finite coordinate list. The positive rational-radius norm balls are open in the induced metric topology and give a countable base: given x∈U with U open, choose r>0 with B(x,r)⊆U, then d in the dense set with ∥d−x∥<r/3 and a positive rational s with ∥d−x∥<s<r−∥d−x∥; the triangle inequality gives x∈B(d,s)⊆U. Thus H is second-countable, the Borel sigma-algebra on H×H is the product sigma-algebra, and integration of a nonnegative product-measurable function against a probability kernel gives a measurable function of its source point. The Axiom of Choice AC implies DC implies countable choice The Axiom of Countable Choice (ACω) Coordinate vectors form the Hilbert basis of real ell-two Q is countably infinite A product of two at most countable sets is at most countable Every subset of an at most countable set is at most countable Countable unions of at most countable sets, assuming ACω The rationals embed densely in the reals Separability: the existence of an at most countable dense subset Second countability: an at most countable basis for the topology A norm on a real vector space, the induced metric, and the dictionary with the metric axioms Open ball, closed ball and sphere in a metric space The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed Borel sigma-algebra of a product of second-countable spaces Measurability of integration against a kernel A continuous map has Borel preimages of Borel sets

[F12]

For the same Gaussian reference law and β∈[0,1], the pCN proposal pair law is symmetric. The pCN Gaussian reference pair law is symmetric

[F13]

Under Countable Choice, Borel probability laws on a separable Hilbert space with the same finite coordinate laws in a complete orthonormal basis are equal. The Axiom of Countable Choice (ACω) AC implies DC implies countable choice Borel laws on a separable Hilbert space are determined by basis coordinates

Proof

Given: The hypotheses and notation in the Statement.

1.1A1F1F2F3F4F5F9F13givenconstruct

By [A1] and [F1], take a countable independent sequence (Zn)n≥1 with law N(0,1) and put Xj=Z2j−1, Yj=Z2j. Each subsequence is again IID standard normal. The odd and even coordinate sigma-algebras are independent by [F4]. Apply [F3] with H0=H1=H, wj=1, and λj=2−j to each subsequence. Since ∑j2−j=1, both series converge almost surely in H and define centered Borel Gaussian random elements. Their finite coordinate laws agree: by [F3], each finite coordinate vector is obtained by multiplying independent standard normals by the same coefficients 2−j/2, so each vector has the same product normal law by [F5] and [F9]. AC implies Countable Choice by [A1], so [F13] identifies their Borel laws. Each limit is measurable with respect to its own coordinate sigma-algebra: its partial sums are block-measurable, the event that they are Cauchy is a countable combination of measurable norm inequalities, and the limit, set to zero on the null complement, is therefore block-measurable. In detail, for a proper open O⊂H with closed complement C, on the convergence event the preimage of O is the condition lim inf⁡Ndist⁡(SN,C)>0; the distance function is 1-Lipschitz, and the zero value assigned off that event is included exactly when 0∈O. This is a measurable condition on the block. The odd and even coordinate sigma-algebras are independent by [F4], hence U and ξ are independent. Denote their common law by μ0.

1.2F2F10F11givenconstruct

For (u,v)∈H×H, set fn(u,v):=1n∑j=1n2j(vj2−uj2),Aβ:={(u,v):fn(u,v)→β2}. Each coordinate map is continuous since ∣uj−vj∣≤∥u−v∥2 by [F2]; finite arithmetic operations make fn Borel by [F10]. Explicitly, Aβ=⋂k=1∞⋃N=1∞⋂n=N∞{∣fn−β2∣<1/k}, so Aβ is Borel by [F10]. The limit criterion follows because for every ε>0 one can choose k with 1/k<ε.

2.1F8F9F11step 1.1givenconstruct

For each u∈H, Qβ(u,⋅) is the pushforward of μ0 under the continuous map z↦u+βz, hence is a probability measure. By [F11], H is second-countable and the product Borel sigma-algebra is B(H)⊗B(H). For Borel B⊆H, addition and scalar multiplication make (u,z)↦u+βz continuous, so (u,z)↦1B(u+βz) is product-measurable. Integrating it against the constant kernel u↦μ0 is measurable by [F11], so Qβ is a probability kernel. Its joint flow η exists by [F8]. By the product joint law [F9] and the proposal pushforward, η is the law of (U,U+βξ).

2.2F4F5F6F7F9F10step 1.1givenalgebra

For each j, define Dj:=2j((U+βξ)j2−Uj2)=(Xj+βYj)2−Xj2=2βXjYj+β2Yj2. The pairs (Xj,Yj) are independent by grouping the independent coordinates, and have the same product standard-normal law by [F9]. Applying the same polynomial map to each pair therefore makes (Dj) IID by [F4] and [F9]. By [F5]–[F6], E[XjYj]=E[Xj]E[Yj]=0, E[Yj2]=1, and E[Dj]=β2. They are square-integrable: using (a+b)2≤2a2+2b2, E[Dj2]≤8β2E[Xj2Yj2]+2β4E[Yj4]=8β2+6β4<∞, where independence gives E[Xj2Yj2]=1 and [F5] gives E[Yj4]=3. By [F7], 1n∑j=1nDj⟶β2almost surely.

3.1F9step 2.1step 2.2step 1.2givenalgebra

Under the forward flow η, the pair has the law of (U,V) from step 2.1, and fn(U,V)=n−1∑j=1nDj. Step 2.2 therefore gives η(Aβ)=1. Under the transpose η⊤, the pair has the law of (V,U), and fn(V,U)=−fn(U,V)→−β2. Since β>0, −β2≠β2, hence η⊤(Aβ)=0.

4.1F12step 3.1given∎

Thus Aβ and its complement are disjoint Borel sets with η(Aβ)=1 and η⊤(Aβc)=1. This is mutual singularity of the two probability measures, and in particular neither is absolutely continuous with respect to the other. By [F12], the pCN reference proposal flow at this same scale equals its transpose.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

A Gaussian pCN kernel leaves a normal posterior invariant

Example

Assume the Axiom of Choice. Let H=R, give the unknown parameter u the prior law μ0=N(0,1), and observe one datum Y=0 from the model Y∣u∼N(u,1). The Gaussian conjugate update gives posterior μ=N(0,1/2). Use the potential Φ(u)=u2/2 in the pCN algorithm. For β∈[0,1], write ρ=1−β2, propose v=ρu+βξ with ξ∼N(0,1) independent of the current state, and accept with probability α(u,v)=min⁡{1,exp⁡((u2−v2)/2)}. The resulting pCN probability kernel leaves N(0,1/2) invariant for every β∈[0,1].

Facts & Assumptions

Given: The Axiom of Choice, the one-observation normal model and pCN rule in the Example.

[F1]

For prior N(μ0,τ02) and one observation from N(u,σ2), the posterior mean is (τ0−2+σ−2)−1(μ0/τ02+y/σ2) and the posterior variance is (τ0−2+σ−2)−1; evidence is finite and positive. Known-variance Normal-Normal conjugate update

[F2]

The law N(m,1) has density (2π)−1/2exp⁡(−(y−m)2/2) with respect to Lebesgue measure. Standard normal and normal laws A positive-variance normal law has its location-scale density

[F3]

The pCN rule proposes v=ρu+βξ and accepts with probability min⁡{1,exp⁡(Φ(u)−Φ(v))} for finite potential values. Prior-preserving Crank–Nicolson sampler

[F4]

The pCN accept-reject probability kernel leaves its normalized posterior target invariant. The pCN accept-reject kernel preserves the posterior

Proof

Given: The Axiom of Choice, prior N(0,1), observation variance 1, datum y=0, and potential Φ(u)=u2/2.

1.1F1givenalgebra

Apply [F1] with μ0=0, τ02=1, σ2=1, n=1, and y=0. The posterior variance is (1+1)−1=1/2, and its mean is (1+1)−1(0+0)=0. The evidence is finite and positive, so the posterior is the proper law N(0,1/2).

2.1F2step 1.1givenalgebra

By [F2], the likelihood density at y=0 is (2π)−1/2e−u2/2. Its constant factor cancels when the likelihood is normalized against the prior, so the potential Φ(u)=u2/2 gives exactly the posterior from step 1.1. It is finite on D=H=R, and the pCN target assumptions are satisfied.

3.1F3step 2.1givenalgebra

For the proposal in [F3], Φ(u)−Φ(v)=u2−v22, so the stated acceptance probability is precisely the algorithm's pCN acceptance rule for this target.

4.1F4step 1.1step 3.1given∎

Step 1.1 identifies the normalized target, and step 3.1 identifies the kernel as the pCN accept-reject kernel for that target. Applying [F4] proves that N(0,1/2) is invariant for every β∈[0,1].

Sources