It is widely remarked that Minkowski's lattice theorem (or, convex body theorem) is a kind of geometrical pigeonhole principle. And it seems it should have a very elementary proof at least for convex bodies defined by very elementary means. But I find nothing about this in Simpson's SOSOA or in Hajek and Pudlak Metamathematics of First Order Arithmetic, or searching on line.
Here, as my references show, I do not mean "elementary " in the sense of "easy to see" but in the sense of using no strong logical principles.
Are there known results on provability of forms of this theorem in fragments of Peano Arithmetic?
You could state the theorem for convex bodies symmetric around the origin and with Riemann integrable volume greater than $2^nd(L)$, so $\mathsf{WKL}_0$ can give the usual proof. That would suffice for many applications of the theorem, but I am not sure if it misses important ones. And that is surely too strong for versions that only need convex bodies determined by quadratic bounds. They do not need full Riemann integration. I wonder what might be known closer to the level of EFA (Elementary Function Arithmetic).
