LemmaStatement: 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.

The volume of a half-open box is the sum of the volumes of the cells of any coordinate grid subdividing it

Statement

Let $n \geq 1$ and let $B = B (a, b) \subseteq R^{n}$ be a nonempty half-open box (Half-open boxes in $R^{n}$ and their volume). Suppose that for each $i < n$ a strictly increasing finite list

$a_{i} = c_{i, 0} < c_{i, 1} < \dots < c_{i, N_{i}} = b_{i}, N_{i} \geq 1,$

in $\overline{R}$ is given, and for a multi-index $k$ with $k_{i} < N_{i}$ for every $i < n$ put $Q_{k} : = B ((c_{i, k_{i}})_{i < n}, (c_{i, k_{i} + 1})_{i < n})$ . Then the cells $Q_{k}$ are nonempty half-open boxes, pairwise disjoint, with union $B$ , and

$vol (B) = \sum_{k_{0} < N_{0}} \dots \sum_{k_{n - 1} < N_{n - 1}} vol (Q_{k}),$

where a sum over cells is the iterated recursive sum of Grid partitions of a rectangle in $R^{m}$ , their cells, refinements and mesh, formed here in $[0, + \infty]$ by the recursion of Series in the nonnegative extended real line.

Facts & Assumptions

Given: A natural number $n \geq 1$ , a nonempty box $B = B (a, b)$ , the lists $c_{i, 0} < \dots < c_{i, N_{i}}$ and the cells $Q_{k}$ of the Statement, and the induction principle (The principle of mathematical induction). For $p \leq n$ and a multi-index $k$ with $k_{i} < N_{i}$ for every $i < p$ , let $D_{k}^{p}$ denote the half-open box whose $i$ -th parameter pair is $(c_{i, k_{i}}, c_{i, k_{i} + 1})$ for $i < p$ and $(a_{i}, b_{i})$ for $p \leq i < n$ , so that $D^{0}$ is $B$ itself and $D_{k}^{n} = Q_{k}$ ; and let $S (p)$ be the assertion that $vol (B) = \sum_{k_{0} < N_{0}} \dots \sum_{k_{p - 1} < N_{p - 1}} vol (D_{k}^{p})$ , a sum over no index being read as its single term.

[L1]

A box is nonempty exactly when $a_{i} < b_{i}$ for every $i < n$ , and $B (a, b) : = {x \in R^{n} : a_{i} < x_{i} \leq b_{i} for every i < n}$ (Half-open boxes in $R^{n}$ and their volume).

[L2]

For a nonempty box with parameter pair $(a, b)$ , $vol (B) : = + \infty$ when $a_{i} = - \infty$ or $b_{i} = + \infty$ for some $i < n$ , and $vol (B) : = \prod_{i < n} (b_{i} - a_{i})$ when every $a_{i}$ and every $b_{i}$ is real; and $vol (\emptyset) : = 0$ (Half-open boxes in $R^{n}$ and their volume).

[F1]

For sequences of reals, $\sum_{k < n} λ a_{k} = λ \sum_{k < n} a_{k}$ ; if $m \leq n$ then $\prod_{k < n} a_{k} = (\prod_{k < m} a_{k}) (\prod_{k = m}^{n - 1} a_{k})$ ; $\sum_{k < n} (c_{k + 1} - c_{k}) = c_{n} - c_{0}$ ; and $\prod_{k < n} (a_{k} b_{k}) = (\prod_{k < n} a_{k}) (\prod_{k < n} b_{k})$ (Laws of finite sums and finite products, claims 2, 3, 5 and 6).

[F2]

Finite sums and finite products of a sequence of reals are defined by the recursions $Σ_{0} = 0$ , $Σ_{σ (n)} = Σ_{n} + a_{n}$ and $Π_{0} = 1$ , $Π_{σ (n)} = Π_{n} \cdot a_{n}$ , written $\sum_{k < n} a_{k}$ and $\prod_{k < n} a_{k}$ (Finite sums and finite products, by recursion).

[F3]

For $a, b \in \overline{R}$ , $a + b : = + \infty$ when $a = + \infty$ and $b \neq - \infty$ , or $b = + \infty$ and $a \neq - \infty$ (The extended real line $\overline{R} = R \cup {- \infty, + \infty}$ , its order, and the arithmetic that is left undefined).

[F4]

The partial sums of a sequence in $[0, + \infty]$ are the unique sequence with $s_{0} = 0$ and $s_{n + 1} = s_{n} + a_{n}$ , and finite sums use the same recursion, $\sum_{k < n} a_{k} = s_{n}$ (Series in the nonnegative extended real line).

[F5]

A sum over cells means the iterated recursive sum $\sum_{i_{0} < n_{0}} \dots \sum_{i_{m - 1} < n_{m - 1}}$ of Finite sums and finite products, by recursion (Grid partitions of a rectangle in $R^{m}$ , their cells, refinements and mesh).

Proof

technique · induction

1.1

Each cell is a nonempty box contained in $B$ , since $a_{i} = c_{i, 0} \leq c_{i, k_{i}} < c_{i, k_{i} + 1} \leq c_{i, N_{i}} = b_{i}$ for every $i < n$ , so that $(c_{i, k_{i}}, c_{i, k_{i} + 1}] \subseteq (a_{i}, b_{i}]$ in every coordinate.

1.2

The cells are pairwise disjoint with union $B$ : distinct multi-indices differ at some $i$ with, say, $k_{i} < k_{i}^{'}$ , whence $c_{i, k_{i} + 1} \leq c_{i, k_{i}^{'}}$ and no point can satisfy $x_{i} \leq c_{i, k_{i} + 1}$ and $c_{i, k_{i}^{'}} < x_{i}$ at once; and for $x \in B$ and $i < n$ the set ${r \leq N_{i} : c_{i, r} < x_{i}}$ contains $0$ and omits $N_{i}$ , so its greatest member $k_{i}$ satisfies $k_{i} < N_{i}$ and $c_{i, k_{i}} < x_{i} \leq c_{i, k_{i} + 1}$ .

1.3

A finite sum in $[0, + \infty]$ equals $+ \infty$ exactly when one of its terms does, and when every term is real it is the finite sum of those reals: the recursion $s_{q + 1} = s_{q} + u_{q}$ produces $+ \infty$ once a term is $+ \infty$ and never leaves $[0, + \infty)$ otherwise.

F3F4

1.4

Let $D = B (d, f)$ be a nonempty box all of whose parameters are real, let $p < n$ , let $d_{p} = t_{0} < \dots < t_{N} = f_{p}$ be reals, and write $D^{(r)}$ for the box obtained from $D$ by replacing its $p$ -th parameter pair by $(t_{r}, t_{r + 1})$ ; putting $u_{i} : = f_{i} - d_{i}$ for $i \neq p$ and $u_{p} : = 1$ , and $Π : = \prod_{i < n} u_{i}$ , the product and splitting laws give $vol (D) = Π (f_{p} - d_{p})$ and $vol (D^{(r)}) = Π (t_{r + 1} - t_{r})$ , so scaling and telescoping give $\sum_{r < N} vol (D^{(r)}) = Π \sum_{r < N} (t_{r + 1} - t_{r}) = Π (t_{N} - t_{0}) = vol (D)$ .

L2F1F2algebra

1.5

At $p = 0$ the iterated sum carries no summation index, so its value is its single term $vol (D^{0}) = vol (B)$ and $S (0)$ holds.

F5base

1.6

Let $p < n$ and assume $S (p)$ as the induction hypothesis.

2.1

Let $D = B (d, f)$ be a nonempty box, let $p < n$ , and let $d_{p} = t_{0} < \dots < t_{N} = f_{p}$ in $\overline{R}$ with the boxes $D^{(r)}$ as in step 1.4; if some parameter of $D$ is infinite then $vol (D) = + \infty$ , and the sum $\sum_{r < N} vol (D^{(r)})$ is $+ \infty$ as well, because an infinite parameter in a coordinate $i \neq p$ is shared by every nonempty $D^{(r)}$ , while $d_{p} = - \infty$ makes $vol (D^{(0)}) = + \infty$ and $f_{p} = + \infty$ makes $vol (D^{(N - 1)}) = + \infty$ .

step 1.3L2F3

3.1

Combining the two cases, for every nonempty box $D$ , every $p < n$ and every strictly increasing list $d_{p} = t_{0} < \dots < t_{N} = f_{p}$ in $\overline{R}$ one has $vol (D) = \sum_{r < N} vol (D^{(r)})$ , since either all parameters of $D$ are real, and then so are all the $t_{r}$ , or some parameter is infinite.

step 1.4step 2.1L2

4.1

Each box $D_{k}^{p}$ is nonempty, by the inequalities of step 1.1 applied in coordinates $i < p$ and $a_{i} < b_{i}$ in the others, and its $p$ -th parameter pair is $(a_{p}, b_{p})$ with the list $a_{p} = c_{p, 0} < \dots < c_{p, N_{p}} = b_{p}$ available, so step 3.1 gives $vol (D_{k}^{p}) = \sum_{k_{p} < N_{p}} vol (D_{k}^{p + 1})$ ; substituting this into the identity of step 1.6 termwise yields $S (p + 1)$ .

step 1.1step 1.6step 3.1

5.1

By induction $S (p)$ holds for every $p \leq n$ , and $S (n)$ is the displayed identity because $D_{k}^{n} = Q_{k}$ ; together with steps 1.1 and 1.2 this is the Statement.

step 1.1step 1.2step 4.1discharge-induction: step 4.1∎

Depends on

Used by

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

Dependency tree · two levels

34 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

John K. Hunter, Measure Theory (UC Davis lecture notes), Chapter 2 (standard reference, not scraped)
T. Tao, An Introduction to Measure Theory (GSM 126), Section 1.1 (standard reference, not scraped)