LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Fundamental parallelotopes of a lattice tile Euclidean space with covolume volume

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $A$ be an invertible real $n \times n$ matrix, $Λ = A Z^{n}$ a full-rank lattice, and $F : = A ((0, 1]^{n}) = {\sum_{i = 1}^{n} t_{i} a_{i} : 0 < t_{i} \leq 1},$ where $a_{1}, \dots, a_{n}$ are the columns of $A$ , the fundamental parallelotope of $Λ$ . Then every $x \in R^{n}$ has a unique representation $x = λ + p$ with $λ \in Λ$ and $p \in F$ ; consequently the translates $F + λ$ ( $λ \in Λ$ ) are pairwise disjoint and cover $R^{n}$ . Moreover $F$ is Lebesgue measurable and $λ_{n} (F) = ∣ \det A ∣ = covol (Λ)$ . Countable Choice is inherited by the box-measure and linear change-of-variables suppliers in the volume computation; the unique representation is choice-free.

Facts & Assumptions

Given: Countable Choice and an invertible real $n \times n$ matrix $A$ with columns $a_{1}, \dots, a_{n}$ and the full-rank lattice $Λ = A Z^{n}$ of Full-rank lattices, covolume, and the dual lattice, whose covolume is $covol (Λ) = ∣ \det A ∣$ .

[F1]

The lattice notation is that of Full-rank lattices, covolume, and the dual lattice: $Λ = A Z^{n} = {A k : k \in Z^{n}}$ , and $A$ is invertible (A finite square real matrix is invertible if and only if its determinant is nonzero).

[F2]

For every real $t$ there is exactly one integer $m$ with $m \leq t < m + 1$ , written $⌊ t ⌋$ ; consequently every real $t$ has a unique decomposition $t = m + s$ with $m \in Z$ and $s \in (0, 1]$ , namely $m = ⌊ t ⌋$ and $s = t - ⌊ t ⌋$ when $t > ⌊ t ⌋$ , and $m = ⌊ t ⌋ - 1$ , $s = 1$ when $t = ⌊ t ⌋$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

[F3]

The half-open box $(0, 1]^{n} = \prod_{i = 1}^{n} (0, 1]$ is Lebesgue measurable with $λ_{n} ((0, 1]^{n}) = 1$ (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included, Axis-parallel rectangles in $R^{m}$ and their volume).

[F4]

If $T : R^{n} \to R^{n}$ is linear with matrix $A$ and $\det A \neq 0$ , then $T [E]$ is Lebesgue measurable for every Lebesgue measurable $E$ and $λ_{n} (T [E]) = ∣ \det A ∣ λ_{n} (E)$ (A linear map $T$ of $R^{n}$ sends Lebesgue measurable sets to Lebesgue measurable sets, with $λ_{n} (T [E]) = ∣ \det T ∣ λ_{n} (E)$ when $T$ is invertible and $T [E]$ Lebesgue null when it is not); this volume supplier assumes Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F5]

Products $A k$ of a matrix with a column vector have the entries $(A k)_{i} = \sum_{j = 1}^{n} A_{i j} k_{j}$ , so $A ((0, 1]^{n}) = {\sum_{i} t_{i} a_{i} : 0 < t_{i} \leq 1}$ (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

Proof

technique · direct

1.1F1F2F5givenalgebra

Write an arbitrary $x \in R^{n}$ as $x = A y$ with $y = A^{- 1} x$ , possible and unique because $A$ is invertible [F1]. By [F2] each coordinate $y_{i}$ has a unique decomposition $y_{i} = m_{i} + s_{i}$ with $m_{i} \in Z$ and $s_{i} \in (0, 1]$ : if $m_{i} + s_{i} = m_{i}^{'} + s_{i}^{'}$ then $m_{i} - m_{i}^{'} = s_{i}^{'} - s_{i} \in (- 1, 1) \cap Z = {0}$ . With $m = (m_{i})$ and $s = (s_{i})$ this gives $x = A m + A s$ , where $A m \in Λ$ and $A s \in F$ by [F5].

2.1step 1.1F1F5algebra

The representation of step 1.1 is unique: if $A m + A s = A m^{'} + A s^{'}$ with $m, m^{'} \in Z^{n}$ and $s, s^{'} \in (0, 1]^{n}$ , then injectivity of $A$ gives $m + s = m^{'} + s^{'}$ and [F2] gives $m = m^{'}$ , $s = s^{'}$ coordinatewise. Hence every $x$ lies in exactly one translate $F + λ$ , $λ \in Λ$ : the translates are pairwise disjoint and cover $R^{n}$ .

3.1step 2.1F1F3F4F5given∎

Volume: $F = A ((0, 1]^{n})$ by [F5], the box $(0, 1]^{n}$ is Lebesgue measurable of measure one [F3], and $A$ is an invertible linear map; by the change-of-variables theorem for linear maps [F4] the set $F$ is Lebesgue measurable with $λ_{n} (F) = ∣ \det A ∣ λ_{n} ((0, 1]^{n}) = ∣ \det A ∣ = covol (Λ)$ [F1]. Only the volume computation uses Countable Choice, inherited from both [F3] and [F4]; the decomposition and uniqueness of steps 1.1 and 2.1 are choice-free.

Depends on

Used by

Dependency tree · two levels

85 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

Lior Silberman, Fourier series and the Poisson summation formula (Math 604/613 notes, UBC) (standard reference, not scraped)
Michael E. Taylor, Fourier Analysis, Distributions, and Constant-Coefficient Linear PDE (author PDF) (standard reference, not scraped)