Boundary vertex conjecture for minimal lattice covering bodies

### What is the conjecture
Let $\Lambda \subset \mathbb{R}^n$ be a full-rank lattice. A compact convex body $K \subset \mathbb{R}^n$ with non-empty interior is called a **lattice covering body** with respect to $\Lambda$ if the family of translates covers Euclidean space:

$$
K + \Lambda = \bigcup_{v \in \Lambda} (K + v) = \mathbb{R}^n.
$$

$K$ is called a **minimal covering body** (MB) if no strictly smaller compact convex body $K' \subsetneq K$ satisfies $K' + \Lambda = \mathbb{R}^n$.

The source paper establishes (Proposition 3.2) that every minimal covering body is a convex polytope generated by translations of lattice polytopes. Following this polytopality property, the authors formulate the following boundary constraint conjecture:

**Conjecture (Lian–Xue, 2026):** If $K + \Lambda$ is a minimal covering of $\mathbb{R}^n$, and $K$ contains a translation of a full-dimensional lattice polytope $Q$ (meaning the vertices of $Q$ belong to $\Lambda$, $\dim(Q) = n$, and $Q + x \subseteq K$ for some translation vector $x \in \mathbb{R}^n$), then all vertices of the translated polytope $Q + x$ must lie on the topological boundary $\partial K$.

* **Source Paper:** *Minimal Covering Bodies and a Minkowski-Type Criterion for Lattice Coverings* ([arXiv:2606.14584](https://arxiv.org/abs/2606.14584), [HTML](https://arxiv.org/html/2606.14584), [PDF](https://arxiv.org/pdf/2606.14584))
* **Authors:** Yanlu Lian, Fei Xue
* **In-Paper Location:** [Conjecture 3.3 (Page 11)](https://arxiv.org/pdf/2606.14584#page=11) in Section 3 "Definition and Properties of minimal covering Bodies"
* **OpenConjecture ID:** 3747 ([OpenConjecture](https://github.com/davisrbr/conjectures-arxiv))

### Prerequisites needed
The definitions of convex sets, convex hulls, extreme points, topological boundaries, and lattices in Euclidean space exist in Mathlib4:
* Convex sets and convex combinations: [`Mathlib.Analysis.Convex.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Convex/Basic.html)
* Convex hulls of finite sets (polytopes): [`Mathlib.Analysis.Convex.Hull`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Convex/Hull.html)
* Extreme points of convex sets: [`Mathlib.Analysis.Convex.Extreme`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Convex/Extreme.html)
* Topological interior and boundary: [`Mathlib.Topology.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Basic.html)
* Euclidean space $\mathbb{R}^n$: [`Mathlib.Analysis.InnerProductSpace.PiL2`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/PiL2.html)

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

This issue was generated by an AI agent and reviewed by me.

Start with Conjecture 3.3 in the linked source paper, then inspect the listed Mathlib modules for convex bodies, polytopes, boundaries, and Euclidean space. The issue names no repository file, entry point, or test; done means adding a formal Lean statement of the conjecture that fits the repository and builds successfully.

Written by the indexing model from the issue text.