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

Two dyadic cubes are either disjoint or one contains the other

Statement

Let $n \geq 1$ and let $Q$ and $Q^{'}$ be dyadic cubes in $R^{n}$ (Dyadic cubes of generation $k$ in $R^{n}$ ) of generations $k$ and $k^{'}$ with $k \leq k^{'}$ . If $Q \cap Q^{'} \neq \emptyset$ then $Q^{'} \subseteq Q$ . Consequently any two dyadic cubes are either disjoint or one of them contains the other, and two dyadic cubes of the same generation are either equal or disjoint.

Facts & Assumptions

Given: A natural number $n \geq 1$ and dyadic cubes $Q = Q_{k, m}$ and $Q^{'} = Q_{k^{'}, m^{'}}$ with $k \leq k^{'}$ .

[L1]

$Q_{k, m} = {x \in R^{n} : m_{i} 2^{- k} < x_{i} \leq (m_{i} + 1) 2^{- k} for every i < n}$ , and every dyadic cube is nonempty (Dyadic cubes of generation $k$ in $R^{n}$ ).

[L2]

$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).

[F1]

For $a \neq 0$ and $m, n \in Z$ , $a^{m + n} = a^{m} a^{n}$ (Laws of integer exponents, claim 3; Integer powers $a^{m}$ ).

[F2]

The order relation on $Z$ is a total order compatible with addition: $x \leq y$ implies $x + z \leq y + z$ (The integers form a totally ordered ring).

[F3]

The canonical embedding of $N$ into $Z$ is injective and preserves addition, multiplication and order, and its image is exactly the set of nonnegative integers, so every $x \geq 0$ in $Z$ is the image of a unique natural number (The naturals embed in the integers, The integers as equivalence classes of pairs of naturals).

[F4]

For all $m, n \in N$ : $m < n$ if and only if $σ (m) \leq n$ (Discreteness: $σ (n)$ is the immediate successor).

Proof

technique · direct

1.1

Put $d : = k^{'} - k \geq 0$ and $M_{i} : = m_{i} 2^{d}$ , an integer; then $m_{i} 2^{- k} = M_{i} 2^{- k^{'}}$ and $(m_{i} + 1) 2^{- k} = (M_{i} + 2^{d}) 2^{- k^{'}}$ , so in coordinate $i$ the cube $Q$ is cut out by $M_{i} 2^{- k^{'}} < x_{i} \leq (M_{i} + 2^{d}) 2^{- k^{'}}$ and the cube $Q^{'}$ by $m_{i}^{'} 2^{- k^{'}} < x_{i} \leq (m_{i}^{'} + 1) 2^{- k^{'}}$ .

L1L2F1

1.2

For integers $u < v$ one has $u + 1 \leq v$ , since $v - u > 0$ is the image of a unique natural number, that natural is not $0$ , hence it is at least $1$ and $v - u \geq 1$ ; consequently, for integers $A < B$ and $C$ , if the real conditions $A < t \leq B$ and $C < t \leq C + 1$ hold for some real $t$ , then $A \leq C$ and $C + 1 \leq B$ , because $C < A$ would give $C + 1 \leq A$ and $t \leq C + 1 \leq A$ , contradicting $A < t$ , while $B < C + 1$ would give $B \leq C$ and $t \leq B \leq C$ , contradicting $C < t$ .

F2F3F4

2.1

If $x \in Q \cap Q^{'}$ then step 1.2, applied in each coordinate with $A : = M_{i}$ , $B : = M_{i} + 2^{d}$ , $C : = m_{i}^{'}$ and $t : = 2^{k^{'}} x_{i}$ , gives $M_{i} \leq m_{i}^{'}$ and $m_{i}^{'} + 1 \leq M_{i} + 2^{d}$ , so the parameter interval of $Q^{'}$ in coordinate $i$ is contained in that of $Q$ , and hence $Q^{'} \subseteq Q$ .

step 1.1step 1.2L1L2

3.1

For arbitrary dyadic cubes, relabel so that the generation of the first is the smaller, and step 2.1 gives the dichotomy; when the generations are equal, $Q^{'} \subseteq Q$ and the symmetric conclusion $Q \subseteq Q^{'}$ both hold, so $Q = Q^{'}$ .

step 2.1L1∎

Depends on

Used by

Every open subset of ℝⁿ is the union of a countable pairwise disjoint family of dyadic cubes Theorem

Dependency tree · two levels

41 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

T. Tao, An Introduction to Measure Theory (GSM 126), Exercise 1.1.14 (standard reference, not scraped)