Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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.

Assuming countable choice, L(Rn) is a sigma-algebra containing every elementary set and λn is a complete measure extending elementary volume

Statement

Let n1 and assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Then:

  1. L(Rn) is a sigma-algebra on Rn and λn is a measure on it (Measures on sigma-algebras);
  2. the measure space (Rn,L(Rn),λn) is complete (Complete measure spaces), and every SRn with λn(S)=0 is Lebesgue measurable with λn(S)=0;
  3. every elementary set is Lebesgue measurable and λn(A)=μ0(A) for every AEn; in particular λn(B)=vol(B) for every half-open box B, λn()=0 and λn(Rn)=+.

Facts & Assumptions

Given: A natural number n1, the Axiom of Countable Choice, Lebesgue outer measure λn, and the family L(Rn) of sets Carathéodory measurable for it.

[L1]

A set ERn is Lebesgue measurable when it is Carathéodory measurable for λn, the family of these is L(Rn), and λn:=λn ⁣L(Rn) (Lebesgue measurable sets, the family L(Rn), and the restricted set function λn).

[L2]

Assuming countable choice, λn is an outer measure on Rn, and λn(A)=μ0(A) for every elementary set A (Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume).

[L3]

λn is the outer set function induced by the premeasure μ0 on the algebra En of elementary sets (Lebesgue outer measure on Rn).

[F1]

For an outer measure μ on X, the Carathéodory measurable subsets form a sigma-algebra, and the restriction of the outer measure to it is a complete measure (Carathéodory's theorem: measurable sets form a sigma-algebra carrying a complete measure).

[F2]

Assume the Axiom of Countable Choice. Every member of the source algebra is Carathéodory measurable for the induced outer measure (Assuming countable choice, every source-algebra set is measurable for the induced outer measure).

[F3]

Assume the Axiom of Countable Choice. If μ0 is a premeasure on an algebra A0 of subsets of X and μ is its induced outer set function, then A0Mμ and μA0=μ0 (Assuming countable choice, a premeasure extends through its induced outer measure).

[F4]

Every set of outer measure zero, and every subset of it, is Carathéodory measurable and has outer measure zero (Every outer-null set is Carathéodory measurable).

[F5]

A measure space (X,A,μ) is complete if every subset of every measurable μ-null set is measurable (Complete measure spaces); and a measure on (X,A) is a function μ:A[0,+] with μ()=0 that is countably additive on pairwise disjoint sequences (Measures on sigma-algebras).

[F6]

The Axiom of Countable Choice says that for every family (Xn)nN of nonempty sets indexed by N there is a function f with domain N such that f(n)Xn for every nN (The Axiom of Countable Choice (ACω)).

Proof

technique · direct
1.1

Under countable choice λn is an outer measure on Rn, so [F1] applies to it: its Carathéodory measurable sets, which are by definition the members of L(Rn), form a sigma-algebra, and the restriction λn of λn to it is a complete measure.

L1L2F1F5F6
1.2

Since λn is the outer set function induced by the premeasure μ0 on En, the extension theorem and the source-algebra lemma give EnL(Rn) and λn(A)=μ0(A) there; a half-open box and and Rn are elementary, so λn(B)=vol(B), λn()=0 and λn(Rn)=+.

L1L3L4F2F3F6
1.3

A set S with λn(S)=0 is Carathéodory measurable for λn, hence Lebesgue measurable, and its measure is its outer measure, namely 0.

L1F4
2.1

Claim 1 and the completeness half of claim 2 are step 1.1, the null-set half of claim 2 is step 1.3, and claim 3 is step 1.2.

step 1.1step 1.2step 1.3

Depends on

Used by

Cited to discharge well-definedness by Lebesgue measurable sets, the family L(ℝⁿ), and the restricted set function λₙ.

Dependency tree · two levels

51 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