# Power savings for planar halving lines and <i>k</i>-sets

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

- [A power saving for planar halving lines](../../preprints/A-power-saving-for-planar-halving-lines-September-25-2026/main.pdf)

## Scope

A halving pair in an even planar point set is a pair whose line leaves equally many remaining points on each side. The formalization proves that some absolute $\varepsilon>0$ and $C$ bound the number of halving pairs by $Cn^{4/3-\varepsilon}$ for every sufficiently large even $n$ and every $n$-point set with no three collinear. It also proves a bound of the same form for all level-switch counts under the additional generic-position assumptions in the statement. The constants are existential.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Power-saving bounds for halving pairs and level switches | [HalvingLines.lean](../ComparatorChallenges/HalvingLines.lean) |