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

For each generation, the dyadic cubes of that generation are pairwise disjoint and cover Rn

Statement

Let n≥1 and let k∈N. Every x∈Rn lies in exactly one dyadic cube of generation k (Dyadic cubes of generation k in Rn); that is, the generation-k dyadic cubes are pairwise disjoint and their union is Rn. Each of them has volume vol⁡(Qk,m)=2−kn (Half-open boxes in Rn and their volume).

Facts & Assumptions

Given: A natural number n≥1, a natural number k, and the dyadic cubes of generation k.

[L1]

Qk,m={ x∈Rn:mi2−k<xi≤(mi+1)2−k for every i<n } (Dyadic cubes of generation k in Rn).

[L2]

For a nonempty box vol⁡(B):=∏i<n(bi−ai) when every ai and every bi is real (Half-open boxes in Rn and their volume).

[F1]

For every real x there is exactly one integer p with p≤x<p+1 (Integer part: for every real x there is exactly one integer m with m≤x<m+1).

[F2]

For a≠0 and m,n∈Z, am+n=aman and (am)n=amn (Laws of integer exponents, claims 1 and 3; Integer powers am).

[F3]

∏k<n(akbk)=(∏k<nak)(∏k<nbk), and finite products are defined by the recursion Π0=1, Πσ(n)=Πn⋅an (Laws of finite sums and finite products, claim 6; Finite sums and finite products, by recursion).

Proof

technique · direct
1.1F1algebra

For a real t there is exactly one integer m with m<t≤m+1: applying [F1] to −t gives the unique integer p with p≤−t<p+1, and m:=−p−1 then satisfies m<t≤m+1, while any integer m′ with m′<t≤m′+1 yields −m′−1≤−t<−m′, so −m′−1=p by the uniqueness in [F1] and m′=m.

1.2L1F2algebra

Since 2−k>0, the condition mi2−k<xi≤(mi+1)2−k is equivalent to mi<2kxi≤mi+1, the powers satisfying 2k2−k=1.

1.3L1L2F2F3

The volume of Qk,m is ∏i<n((mi+1)2−k−mi2−k)=∏i<n2−k=(2−k)n=2−kn, the last two equalities by the recursion for finite products and the power laws.

2.1step 1.1step 1.2L1

Given x∈Rn, step 1.1 applied in each coordinate to the real 2kxi produces exactly one integer mi with mi<2kxi≤mi+1, so by step 1.2 the function m so determined is the unique index of a generation-k dyadic cube containing x; hence the generation-k cubes cover Rn and no two of them share a point.

3.1step 1.3step 2.1∎

Steps 2.1 and 1.3 are the Statement.

Depends on

Used by

Dependency tree · two levels

37 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