# The Euclidean Steinitz–Bergström bound

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The Euclidean Steinitz–Bergström theorem](../../preprints/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026.pdf)

## Scope

The formalized result gives the Euclidean Steinitz–Bergström bound with one absolute constant $C$. For every finite family of vectors in the unit ball of $\mathbb R^d$, signs can be chosen so that every prefix in the prescribed order has norm at most $C\sqrt d$. When the vector sum is zero, a permutation makes every unsigned prefix satisfy the same bound. Repeated and zero vectors are included. The result is existential and does not supply an online algorithm.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Euclidean signed and reordered prefix bounds | [SteinitzBergstrom.lean](../ComparatorChallenges/SteinitzBergstrom.lean) |