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.

Elementary volume is a sigma-finite premeasure on the algebra of elementary sets

Statement

Let n1, let En be the algebra of elementary subsets of Rn (The elementary sets form an algebra of subsets of Rn containing every half-open box) and let μ0 be elementary volume (The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition). Then μ0 is a sigma-finite premeasure on En (Premeasures on algebras of sets): μ0()=0; whenever (Ak)kN is a pairwise disjoint sequence in En whose union A again lies in En,

μ0(A)  =  k=0μ0(Ak);

and Rn=kN(k,k]n with μ0((k,k]n)<+ for every k.

No choice principle is used. The one place where a textbook proof selects countably many objects is the enlargement of each Ak, and here the enlarged set is the canonical Ak+1/(m+1) of Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it with m the least natural number that works, which is a definition rather than a selection. The compact inner set and the finite subcover are each a single instantiation of an existential statement.

Facts & Assumptions

Given: A natural number n1, the algebra En with elementary volume μ0, and a pairwise disjoint sequence (Ak)kN in En whose union A lies in En.

[L1]

En is an algebra of subsets of Rn, it contains every half-open box, and it is closed under intersection of two members and under difference (The elementary sets form an algebra of subsets of Rn containing every half-open box).

[L2]

For every n1, there is exactly one function μ0:En[0,+] whose value at A is the sum of the volumes of the members of any presentation of A by a finite list of pairwise disjoint half-open boxes; it satisfies μ0()=0 and μ0(B)=vol(B) for every half-open box B (The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition).

[L3]

Elementary volume is finitely additive on pairwise disjoint elementary sets, monotone, and finitely subadditive (Elementary volume is finitely additive, monotone and finitely subadditive on the elementary algebra).

[L4]

A+δ is an elementary set, it is determined by A and δ alone, it contains A, and every point of A is an interior point of A+δ in (Rn,d2) (Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it, claim 1).

[L5]

For every real ε>0 there is mN with μ0(A+1/(m+1))μ0(A)+ε (Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it, claim 2).

[L6]

If μ0(A)<+, then for every real ε>0 there are an elementary set A and a compact set KRn with AKA and μ0(A)μ0(A)+ε (Every elementary set is squeezed in volume between a compact subset and an elementary set whose interior contains it, claim 3).

[L7]

For a nonempty box vol(B):=+ when ai= or bi=+ for some i<n, and vol(B):=i<n(biai) when every ai and every bi is real; B(a,b):={xRn:ai<xibi  for every i<n}; and (u,v]n:=B(u,v) (Half-open boxes in Rn and their volume).

[L8]

A subset ERn is an elementary set when there are a natural number m and a list B0,,Bm1 of half-open boxes with E=j<mBj (Elementary sets: the finite unions of half-open boxes in Rn).

[F1]

A premeasure on an algebra A0 vanishes at the empty set and is countably additive whenever a disjoint sequence in A0 has its union in A0; it is sigma-finite if there is a sequence (Pn) in A0 with X=nPn and μ0(Pn)<+ for every n (Premeasures on algebras of sets).

[F2]

The nonnegative extended sum of a sequence in [0,+] is k=0ak:=supnNsn, the supremum of its nondecreasing partial sums (Series in the nonnegative extended real line).

[F3]

A is a compact subset of X if and only if for every set I and every family (Ui)iI of open subsets of X with AiIUi there are nN and indices i0,,inI with AUi0Uin, or else A= (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, claim 3; Open cover, subcover, compact metric space, and compact subset of a metric space).

[F5]

Every nonempty subset SN has a least element (The well-ordering principle).

[F6]

If r<1 then k=0rk=1/(1r); in particular k=02k=2 (For r<1, k0rk=1/(1r), and for r1 the series diverges).

[F7]

Every complete ordered field F is Archimedean: for every xF there is a natural number n1 with x<n1F (Every complete ordered field is Archimedean).

[F8]

For sequences of reals, k<n(ak+bk)=k<nak+k<nbk; if akbk for all k<n then k<nakk<nbk; and if ak0 for all k<n then k<nak0, with k<nak>0 when every ak>0 (Laws of finite sums and finite products, claims 1, 4 and 6).

[F9]

Finite sums and finite products of a sequence of reals are defined by the recursions Σ0=0, Σσ(n)=Σn+an and Π0=1, Πσ(n)=Πnan (Finite sums and finite products, by recursion).

[F10]

For a,bR, a+b:=+ when a=+ and b, or b=+ and a (The extended real line R=R{,+}, its order, and the arithmetic that is left undefined).

Proof

technique · direct
1.1

μ0 is a function on the algebra En with values in [0,+] and μ0()=0, which is the first premeasure clause.

L1L2F1
1.2

Each cube (k,k]n is a half-open box, hence elementary, with μ0((k,k]n)=(2k)n<+ for k1 and μ0((0,0]n)=0; and kN(k,k]n=Rn, because for xRn the Archimedean property supplies a natural k1 above each of the finitely many reals xi.

L1L2L7L8F7
1.3

For every N, finite additivity gives k<Nμ0(Ak)=μ0(k<NAk) and monotonicity gives μ0(k<NAk)μ0(A), so every partial sum is at most μ0(A) and therefore k=0μ0(Ak)μ0(A), that supremum being the nonnegative extended sum.

L3F2
1.4

Suppose μ0(A)<+ and let ε>0 be real. Fix an elementary A and a compact K with AKA and μ0(A)μ0(A)+ε; for each k let mk be the least natural number with μ0(Ak+1/(mk+1))μ0(Ak)+ε2k, which exists because the set of such naturals is nonempty and N is well ordered, and put Uk:=int(Ak+1/(mk+1)), an open set containing Ak. Since KA=kAkkUk, compactness yields finitely many indices covering K, hence a natural N with Kk<NUk, so that Ak<NAk+1/(mk+1); monotonicity, finite subadditivity and the geometric series then give μ0(A)k<Nμ0(Ak+1/(mk+1))k<Nμ0(Ak)+εk<N2kk=0μ0(Ak)+2ε, whence μ0(A)k=0μ0(Ak)+3ε; as ε was an arbitrary positive real and μ0(A) is finite, μ0(A)k=0μ0(Ak).

L2L3L4L5L6F2F3F4F5F6F8
2.1

Suppose instead μ0(A)=+ and put T:=k=0μ0(Ak); if T=+ then μ0(A)T holds, and if T<+ a contradiction follows. Fix a disjoint box presentation A=j<qBj; some Bj0=B(a,b) has infinite volume, hence is nonempty with ai0= or bi0=+ for some i0<n. Take yBj0 and put αi:=yi1 when ai= and αi:=(ai+yi)/2 otherwise, so that ai<αi<yi and c:=i<nui>0, where ui:=yiαi for ii0 and ui0:=1. For a real R exceeding every αi and every yi, the box DR with parameter pairs (αi,yi] for ii0 and (αi0,R], respectively (R,yi0], in coordinate i0 according as bi0=+ or ai0=, satisfies DRBj0(R,R]nA(R,R]n and has volume at least (Rαi0yi0)c. On the other hand A(R,R]n is elementary of finite volume and is the disjoint union of the elementary sets Ak(R,R]n, so step 1.4 and monotonicity give μ0(A(R,R]n)k=0μ0(Ak(R,R]n)T; taking R above (T/c)+αi0+yi0+1 by the Archimedean property contradicts this.

step 1.4L1L2L3L7L8F2F7F8F9F10
3.1

Steps 1.3, 1.4 and 2.1 give μ0(A)=k=0μ0(Ak) in every case, which with steps 1.1 and 1.2 makes μ0 a sigma-finite premeasure on En.

step 1.1step 1.2step 1.3step 1.4step 2.1F1

Depends on

Used by

Dependency tree · two levels

73 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