Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedaudited 2026-09-06
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.

An i.i.d. sequence with a prescribed law

Example

Assume countable choice and dependent choice. Given any probability law ν on (S,Σ), equip SN with its cylinder sigma-algebra and the canonical product probability and set Xn(x)=xn. Then (Xn) is an i.i.d. S-valued sequence with common law ν.

Facts & Assumptions

Given: Countable choice, dependent choice, and a probability space (S,Σ,ν), repeated at every index n∈N.

[F1]

The stated choice principles give the canonical countable product probability. (Assuming countable and dependent choice, countable products of arbitrary probability spaces)

[F2]

Its coordinate maps are independent copies with the prescribed law. (Coordinate random elements of a countable product are independent)

Verification

1.1

Apply [F1] with (En,En,μn)=(S,Σ,ν) for every n∈N. It gives the canonical probability on the cylinder sigma-algebra of SN. By [F2], its coordinate maps Xn(x)=xn are independent and each has law ν.

givenF1F2
2.1

Its finite-family conclusion is independence, while its one-coordinate conclusion is the common marginal; together these are the definition of i.i.d.

step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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