LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-generatedprecheck passaudited 2026-10-02

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.

Blichfeldt lattice-point principle

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $n \geq 1$ and let $Λ \subseteq R^{n}$ be a full lattice with $covol (Λ) > 0$ (Full Euclidean lattice and covolume). If $S \subseteq R^{n}$ is Lebesgue measurable with $λ_{n} (S) > covol (Λ)$ , then there are distinct points $x, y \in S$ with $x - y \in Λ$ .

Facts & Assumptions

Given: The Axiom of Choice, a full lattice $Λ = Z b_{1} \oplus \dots \oplus Z b_{n}$ in $R^{n}$ with covolume $covol (Λ) > 0$ , and a Lebesgue measurable set $S \subseteq R^{n}$ with $λ_{n} (S) > covol (Λ)$ .

[A1]

The Axiom of Choice gives the Axiom of Countable Choice (AC implies DC implies countable choice), the choice hypothesis of the complete-measure fact [F2], invoked in step 2.1; the translation-invariance fact [F3], the defining properties of a measure [F4] and the countability facts [F5] use no choice principle, and no further choice is used.

[F1]

The half-open fundamental parallelotope $P = {\sum_{i} t_{i} b_{i} : 0 < t_{i} \leq 1}$ tiles $R^{n}$ uniquely by $Λ$ -translates, $P$ is Lebesgue measurable with $λ_{n} (P) = covol (Λ)$ , and every bounded subset of $R^{n}$ meets $Λ$ in finitely many points (Fundamental parallelotope and finite bounded intersections).

[F2]

Assuming countable choice, $L (R^{n})$ is a sigma-algebra and $λ_{n}$ is a measure on it (Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume).

[F3]

Translations preserve measurability and measure: $E$ is Lebesgue measurable if and only if $E + h$ is, and then $λ_{n} (E + h) = λ_{n} (E)$ (Lebesgue outer measure, Lebesgue measurability and Lebesgue measure are unchanged by translation).

[F4]

A measure is countably additive: for pairwise disjoint measurable sets $E_{k}$ one has $μ (⋃_{k} E_{k}) = \sum_{k} μ (E_{k})$ , extended nonnegative sums included (Measures on sigma-algebras).

[F5]

$Z$ is at most countable: the quotient map $N \times N \to Z$ of The integers as equivalence classes of pairs of naturals is surjective, $N \times N$ is at most countable ( $N \times N \approx N$ , A product of two at most countable sets is at most countable), and an at most countable set that is a surjective image of an at most countable set is at most countable (A nonempty set is at most countable iff it is a surjective image of $N$ ). Hence $Z^{n}$ is at most countable, and so is $Λ$ , being a surjective image of $Z^{n}$ under $(m_{1}, \dots, m_{n}) \mapsto \sum_{i} m_{i} b_{i}$ (Finite, countably infinite, countable, uncountable).

Proof

1.1assume-contra

Assume for contradiction that there are no distinct $x, y \in S$ with $x - y \in Λ$ .

1.2F5A1

$Λ$ is at most countable by [F5], and it is infinite because $b_{1} \neq 0$ gives the distinct multiples $k b_{1}$ ; being at most countable and infinite, it is countably infinite, so fix a bijection $λ : N \to Λ$ , $k \mapsto λ_{k}$ (Finite, countably infinite, countable, uncountable). By [A1] the Axiom of Countable Choice holds; it discharges the choice hypothesis of the complete-measure fact [F2] applied below.

2.1F1F2F3step 1.2

For each $k$ put $S_{k} : = S \cap (P + λ_{k})$ and $T_{k} : = S_{k} - λ_{k}$ . Each $S_{k}$ is measurable: $S$ is measurable by hypothesis, the translate $P + λ_{k}$ is measurable by [F3] applied to the measurable tile $P$ of [F1], and the intersection is measurable because [F2] makes $L (R^{n})$ a sigma-algebra, its Countable Choice hypothesis having been discharged in step 1.2.

2.2F1F4step 1.2

The $S_{k}$ are pairwise disjoint with union $S$ , since the translates $P + λ$ tile $R^{n}$ by [F1]; hence $λ_{n} (S) = \sum_{k} λ_{n} (S_{k})$ by countable additivity [F4].

3.1F1F3step 2.1

By [F3] applied to the translation by $- λ_{k}$ , $T_{k}$ is measurable with $λ_{n} (T_{k}) = λ_{n} (S_{k})$ ; and $T_{k} \subseteq P$ , since $P + λ_{k}$ translated by $- λ_{k}$ is $P$ .

4.1step 1.1step 3.1

The sets $T_{k}$ are pairwise disjoint: if $z \in T_{j} \cap T_{k}$ with $j \neq k$ , then $z = x - λ_{j} = y - λ_{k}$ with $x \in S_{j} \subseteq S$ and $y \in S_{k} \subseteq S$ , so $x - y = λ_{j} - λ_{k} \in Λ$ while $x \neq y$ because $λ_{j} \neq λ_{k}$ ; this contradicts step 1.1.

5.1F4step 2.2step 3.1step 4.1

By countable additivity [F4] applied to the pairwise disjoint measurable sets $T_{k}$ , $λ_{n} (⋃_{k} T_{k}) = \sum_{k} λ_{n} (T_{k}) = \sum_{k} λ_{n} (S_{k}) = λ_{n} (S)$ , using steps 2.2, 3.1 and 4.1.

6.1F1F4step 5.1

Since $⋃_{k} T_{k} \subseteq P$ , monotonicity of a measure (additivity [F4] applied to $P = (⋃_{k} T_{k}) \cup (P ∖ ⋃_{k} T_{k})$ ) gives $λ_{n} (S) = λ_{n} (⋃_{k} T_{k}) \leq λ_{n} (P) = covol (Λ)$ .

7.1step 1.1step 6.1discharge-contradiction∎

Step 6.1 contradicts the hypothesis $λ_{n} (S) > covol (Λ)$ ; therefore the assumption of step 1.1 is false, and there exist distinct $x, y \in S$ with $x - y \in Λ$ .

Remarks

The proof works for unbounded $S$ and even for $λ_{n} (S) = + \infty$ : $S_{k} \subseteq P + λ_{k}$ and $T_{k} \subseteq P$ , so each piece has finite measure, but their measure sum may be infinite. Countable additivity permits extended nonnegative sums; under the no-pair assumption, the $T_{k}$ are disjoint in $P$ , which bounds that sum by $λ_{n} (P)$ and gives the contradiction. The hypothesis is strict: for $S = (0, 1]^{2}$ and $Λ = Z^{2}$ one has $λ_{2} (S) = covol (Λ) = 1$ and no two distinct points of $S$ differ by a lattice vector.

Depends on

Used by

Minkowski convex-body theorem, strict form Theorem
Minkowski second theorem on successive minima Theorem

Dependency tree · two levels

73 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

J. S. Milne, Algebraic Number Theory v3.08 (standard reference, not scraped)
Ben Green, Additive Combinatorics, Lecture 3 §3.7 (standard reference, not scraped)