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

Minkowski convex-body theorem at equality

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $n \geq 1$ , let $Λ \subseteq R^{n}$ be a full lattice with $covol (Λ) > 0$ (Full Euclidean lattice and covolume), and let $C \subseteq R^{n}$ be compact, convex and centrally symmetric (A convex subset of $R^{m}$ contains every line segment between two of its points). If

$λ_{n} (C) \geq 2^{n} covol (Λ),$

then $C$ contains a nonzero point of $Λ$ .

Facts & Assumptions

Given: The Axiom of Choice, a full lattice $Λ$ with $covol (Λ) > 0$ , and a compact convex centrally symmetric $C$ with $λ_{n} (C) \geq 2^{n} covol (Λ)$ .

[A1]

The Axiom of Choice gives the Axiom of Countable Choice (AC implies DC implies countable choice), which licenses the countable selection of one nonzero lattice point $v_{m}$ from each of the sets $S_{m} \cap Λ$ in step 2.1; the strict theorem [F1] and the tiling lemma [F3] are applied under the Axiom of Choice assumed in the statement, and no further choice is used.

[F1]

Strict Minkowski: if a Lebesgue measurable convex centrally symmetric set $S$ satisfies $λ_{n} (S) > 2^{n} covol (Λ)$ , then $S$ contains a nonzero point of $Λ$ (Minkowski convex-body theorem, strict form).

[F2]

For nonzero real $t$ , $λ_{n} (t S) = ∣ t ∣^{n} λ_{n} (S)$ for Lebesgue measurable $S$ (For a nonzero real $c$ , dilation by $c$ multiplies Lebesgue outer measure by $∣ c ∣^{n}$ , and reflection in the origin preserves it).

[F3]

Every bounded subset of $R^{n}$ meets $Λ$ in finitely many points (Fundamental parallelotope and finite bounded intersections).

[F4]

$C$ convex: $(1 - t) x + t y \in C$ for $x, y \in C$ , $t \in [0, 1]$ ; $C$ compact, hence closed; central symmetry gives $- C = C$ , so $0 \in C$ since $C$ is nonempty; and for $c \in C$ the convexity relation $c / 2 = \frac{1}{2} c + \frac{1}{2} \cdot 0$ gives $c / 2 \in C$ (A convex subset of $R^{m}$ contains every line segment between two of its points).

Proof

1.1F2F4given

For every $m \geq 1$ the dilate $S_{m} : = (1 + 1 / m) C$ is compact, convex and centrally symmetric, and by [F2] $λ_{n} (S_{m}) = (1 + 1 / m)^{n} λ_{n} (C) \geq (1 + 1 / m)^{n} 2^{n} covol (Λ) > 2^{n} covol (Λ)$ because $covol (Λ) > 0$ and $(1 + 1 / m)^{n} > 1$ .

2.1A1F1step 1.1

By [F1] each $S_{m}$ contains a nonzero lattice point; using [A1] choose one, say $0 \neq v_{m} \in S_{m} \cap Λ$ , for every $m \geq 1$ .

3.1F3F4step 2.1

Since $1 + 1 / m \leq 2$ for $m \geq 1$ and $0 \in C$ , convexity of $C$ gives $S_{m} \subseteq 2 C$ , so every $v_{m}$ lies in the bounded set $2 C$ ; by [F3] the set $2 C \cap Λ$ is finite, so some $v \in 2 C \cap Λ$ equals $v_{m}$ for infinitely many $m$ .

4.1F4step 3.1

Fix such an infinite set of indices $m$ . For each of them $v \in (1 + 1 / m) C$ , hence $v / (1 + 1 / m) \in C$ ; as $m \to \infty$ through those indices $v / (1 + 1 / m) \to v$ , and $C$ is closed by [F4], so $v \in C$ .

5.1step 4.1∎

The point $v$ is nonzero by step 2.1 and lies in $C \cap Λ$ , so $C$ contains a nonzero lattice point.

Remarks

Compactness is used twice: it makes $2 C \cap Λ$ finite and it makes $C$ closed, so that the limit of the points $v / (1 + 1 / m)$ stays in $C$ . For non-closed bodies the conclusion can fail: the open cube $(- 1, 1)^{n}$ has $λ_{n} = 2^{n} covol (Z^{n})$ and meets $Z^{n}$ only in the origin.

Depends on

Used by

Mixing scaled and unscaled Minkowski covolumes fails Counterexample
Small nonzero element in a number-field ideal Theorem
The logarithmic unit image is a full lattice Theorem

Dependency tree · two levels

42 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)
Brian Conrad and Aaron Landesman, Math 154 Algebraic Number Theory (standard reference, not scraped)