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

Random-mapping representation for a finite transition matrix

Statement

Assume Choice. Let S be finite and ordered and let p be a transition matrix. There is a measurable F:S×[0,1]→S such that, for uniform U, F(x,U) has law p(x,⋅). If X0 is an S-valued random element and U1,U2,… are fresh IID uniforms, independent of X0, then Xn+1=F(Xn,Un+1) is the p-chain.

Facts & Assumptions

Given: Choice, the finite ordered state space, transition matrix, and, for the chain assertion, the S-valued random element and fresh uniforms in the statement.

[F1]

Disjoint blocks of an independent family generate independent sigma-algebras. (Disjoint groups of an independent sigma-algebra family remain independent)

[F2]

The bounded-function conditional identity characterizes a Markov chain. (Bounded-function form of the Markov property)

Verification

1.1given

Suppose first that S={s1,…,sd} with d≥1. For each row put [given] c0(x)=0,cj(x)=∑k=1jp(x,sk),1≤j≤d. Then cd(x)=1. Define F(x,u)=sjwhen{cj−1(x)≤u<cj(x),j<d,cd−1(x)≤u≤1,j=d. These intervals partition [0,1] with a fixed endpoint convention, even when some row entries vanish. Since S is finite, every inverse image is a finite union of measurable slices, so F is measurable.

2.1step 1.1

Uniform interval lengths give [step 1.1] P(F(x,U)=sj)=cj(x)−cj−1(x)=p(x,sj). The possible singleton endpoint at 1 has probability zero, so the last closed endpoint does not change this calculation. It covers row probabilities zero and one and the one-state case d=1.

3.1F1F2step 1.1step 2.1

Let Hn=σ(X0,U1,…,Un); then Xn is [F1, F2, step 1.1, step 2.1] Hn-measurable and [F1] makes Un+1 independent of Hn. For each sj, 1{F(Xn,Un+1)=sj}=∑i=1d1{Xn=si}1{Un+1∈Iij}, where Iij is the row interval from step 1.1. Conditioning term by term and using step 2.1 gives p(Xn,sj). Summing over sj∈A proves the transition identity for every A⊆S, hence [F2] gives the p-chain. Empty/full A and time zero are included. Choice is used only for conditional expectations and, if a canonical realization is requested, by its path-law supplier.

4.1givenstep 1.1step 2.1step 3.1∎

Together with steps 1.1--3.1, consider S=∅: the unique map [given, step 1.1, step 2.1, step 3.1] ∅×[0,1]→∅ satisfies the row-law assertion vacuously, but no probability initial law—and hence no chain—exists on S.

Remarks

For a concrete illustration, take S={s1,s2} and transition matrix p=(1/32/33/41/4). The two bars show the row intervals from step 1.1. At the illustrated input u=1/2, the first row gives F(s1,u)=s2, while the second gives F(s2,u)=s1. Each internal boundary belongs to the interval on its right; the endpoint 1 belongs to the final interval.

x=s1x=s2s1s2s1s201=3103=41u=1=2

The bars illustrate alternative evaluations of F, not two simultaneous chain updates. At time n, only the row x=Xn is used, with the fresh input Un+1. The rigorous verification above is independent of the illustration.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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