Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition

Statement

Let n1 and let ARn be an elementary set (Elementary sets: the finite unions of half-open boxes in Rn). If

A  =  j<mBj  =  l<pCl

for finite lists of pairwise disjoint half-open boxes (Half-open boxes in Rn and their volume), then

j<mvol(Bj)  =  l<pvol(Cl)

in [0,+]. Consequently there is exactly one function μ0:En[0,+], the elementary volume, 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.

Facts & Assumptions

Given: A natural number n1, an elementary set A, and two presentations A=j<mBj=l<pCl by finite lists of pairwise disjoint half-open boxes.

[L1]

Every elementary set has a presentation as a finite pairwise disjoint union of half-open boxes. Applied to the concatenated list B0,,Bm1,C0,,Cp1, the generated grid has pairwise disjoint cells whose union is Rn; for every member of the list, a cell that meets it is contained in it, and that member is the union of the cells contained in it (Every elementary set is a finite disjoint union of half-open boxes, and any finitely many boxes admit a common grid refinement).

[L2]

For a nonempty box B=B(a,b) and strictly increasing lists ai=ci,0<<ci,Ni=bi with Ni1, the cells Qk are nonempty pairwise disjoint boxes with union B and vol(B)=k0<N0kn1<Nn1vol(Qk) (The volume of a half-open box is the sum of the volumes of the cells of any coordinate grid subdividing it).

[L3]

vol():=0, and a box is nonempty exactly when ai<bi for every i<n (Half-open boxes in Rn and their volume).

[L4]

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]

For sequences of reals, k<n(ak+bk)=k<nak+k<nbk, and if mn then k<nak=k<mak+k=mn1ak (Laws of finite sums and finite products, claims 1 and 3).

[F2]

Finite sums of a sequence of reals are defined by the recursion Σ0=0, Σσ(n)=Σn+an, written k<nak (Finite sums and finite products, by recursion).

Proof

technique · direct
1.1

Let (Qk) be the cells of the grid generated by the concatenated list, indexed by the multi-indices k with ki<Ni for i<n; they are nonempty, pairwise disjoint, cover Rn, and each of them is either contained in or disjoint from each Bj and each Cl.

L1L3
1.2

If one of the boxes in either decomposition has infinite volume, then both sums are + and there is nothing left to prove. Indeed, by [L3] a nonempty box has infinite volume exactly when some endpoint is infinite, and such a box is unbounded. Conversely, a finite union of boxes all of whose endpoints are real is bounded: for each such box B(a,b) every coordinate of every point of B lies between the real endpoints ai and bi, so choosing one real bound for each box and then taking the maximum over the finite list bounds the whole union. Therefore, if A contains an unbounded box from one decomposition, the other decomposition cannot consist entirely of finite-volume boxes, since that would make A bounded. So it remains only to treat the case in which every Bj and every Cl has finite volume; from now on all the volumes that appear are real numbers and the finite-sum laws of [F1] apply to them.

L3F1F2
2.1

For each j<m let wkj:=vol(Qk) when QkBj and wkj:=0 otherwise; then vol(Bj)=k0<N0kn1<Nn1wkj, because for Bj= no cell is contained in it and both sides are 0, while for Bj=B(aj,bj) nonempty the parameters aij and bij occur among the grid points, say aij=ci,αi and bij=ci,βi with αi<βi, the cells contained in Bj are exactly those with αiki<βi in every coordinate, the lists ci,αi<<ci,βi subdivide Bj so that [L2] applies, and widening each summation range from αiki<βi to ki<Ni only inserts zero terms.

step 1.1step 1.2L2L3F1
2.2

A cell is contained in A exactly when it is contained in exactly one Bj, since a cell contained in A meets A, hence meets some Bj and is contained in it, while a cell contained in two of the pairwise disjoint boxes would be empty; so, writing vk:=vol(Qk) when QkA and vk:=0 otherwise, one has j<mwkj=vk for every k.

step 1.1L3L4
3.1

Summing the identities of step 2.1 over j<m and regrouping the resulting finite real sums by repeated use of the additivity law in [F1] gives j<mvol(Bj)=k0<N0kn1<Nn1j<mwkj. Since step 2.2 identifies the inner sum with vk, this is k0<N0kn1<Nn1vk.

step 1.2step 2.1step 2.2F1
4.1

The right-hand side of step 3.1 is built from A and the grid alone, and the same computation applied to the list C0,,Cp1, whose parameters also generate the same grid, gives l<pvol(Cl) for the same value; hence the two sums agree, and since every elementary set has at least one presentation by a finite list of pairwise disjoint half-open boxes, the assignment μ0 is a well-defined function on En with μ0()=0 and μ0(B)=vol(B) for a single box.

step 3.1L1L3L4

Depends on

Used by

Dependency tree · two levels

30 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