Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)
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.

Probability algebras, arbitrary joins and the countable chain condition

Statement

Assume AC. Let (X,Σ,μ) be a probability space, so μ(X)=1. Identify A,BΣ when μ(AB)=0, and write B for the set of equivalence classes. Set operations induce Boolean operations on B, and m([A])=μ(A) is a well-defined strictly positive probability on it. The order is [A][B] exactly when μ(AB)=0.

The Boolean algebra B is complete. Every subset DB has a countable subset D0D with D=D0, allowing D0=. Every antichain of nonzero elements is countable. For arbitrary DB and cB,

cD={cd:dD}.

Countable joins are represented by countable unions of measurable representatives. No assertion that an arbitrary union of representatives is measurable or represents its Boolean join is made.

Facts & Assumptions

Given: A probability space and AC. All families below are sets.

[F1]

Measures are countably additive on disjoint measurable sequences. (Measures on sigma-algebras)

[F2]

Countable unions of measurable null sets are null, by countable subadditivity. (Finite and countable subadditivity of measures)

[F3]

The measure of an increasing measurable union is the supremum of the measures. (Continuity from below for measures)

[F4]

Boolean algebras have the bounded distributive lattice laws, with order given by meet. (Boolean algebras and their order)

[F5]

Completeness means existence of every set supremum, including the empty supremum zero. (Completeness, regular opens, and order continuity)

[F6]

AC selects measurable representatives, countably many finite approximants to a supremum, and enumerations of countably many finite antichain pieces. (The Axiom of Choice)

Proof

1.1

Symmetric difference is symmetric, AA=, and AC(AB)(BC). F1 and F2 therefore give an equivalence relation. Its classes form a set quotient of Σ. Replacing either input of a union or intersection by an equivalent set changes the result only inside the union of the input symmetric differences; complement preserves symmetric difference. Hence the operations are well-defined and inherit all F4 identities from set operations. Splitting sets into disjoint differences shows that equivalent sets have equal measure, so m is well-defined. It vanishes exactly on the zero class, and m(1)=1, making the algebra nontrivial. The equation [A][B]=[A] is equivalent to μ(AB)=0.

F1F2F4
2.1

For a sequence (an) choose representatives An by F6 and put a=[nAn]. This bounds every an. If b=[B] is another upper bound, each AnB is null; F2 makes their union null, so ab. Thus a is the supremum. Another sequence of representatives gives the same class, again by F2. For a disjoint sequence of Boolean elements, remove from An all earlier Aj to obtain literally disjoint representatives: the removed part is a finite union of null intersections. F1 then proves m(nan)=nm(an). An empty sequence has supremum zero.

F1F2F6step 1.1
3.1

Given DB, let s be the supremum supplied by F7 in [0,1] of m(F) over finite FD, including F=. Choose finite FnD with m(Fn)>s2n; when s=0 all Fn may be empty. Put D0=nFn, which is countable by F6, and let c=D0 using step 2.1. The finite joins over F0Fn increase to c. Measurable representatives can be chosen increasing by taking successive finite unions, so F3 gives m(c)=s.

F3F6F7step 2.1
3.2

Let A be an antichain of nonzero elements. For each positive integer n put An={aA:m(a)1/n}. Any n+1 distinct members of An would have disjoint join of measure at least (n+1)/n>1, contrary to step 2.1. Thus An has at most n elements. Strict positivity gives A=n1An, and F6 makes this union countable. The empty antichain and singleton antichains satisfy the same bound.

F6step 1.1step 2.1
4.1

For any dD, the finite joins in step 3.1 with d adjoined still have measure at most s. F3 gives m(cd)s=m(c). Disjoint additivity then gives m(d¬c)=m(cd)m(c)=0, hence dc by strict positivity. Any upper bound of D bounds D0 and thus bounds c by step 2.1. Therefore c=D, proving completeness and the countable-subfamily assertion. If D is empty the construction gives c=0; if it is a singleton its supremum is that element.

F1F3F5step 1.1step 2.1step 3.1
5.1

Put u=D and v={cd:dD}. Each joined term lies below cu, so vcu. Conversely cdv implies d=(cd)(¬cd)v¬c. Hence uv¬c, and finite distributivity gives cuc(v¬c)v. This proves the identity, including c=0, c=1 and D=. Only the established Boolean supremum is used, not the possibly nonmeasurable union of an arbitrary family of representatives.

F4step 4.1

Depends on

Used by

Dependency tree · two levels

19 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