The number of optimal least-squares matchings between two sets of n points in the plane under rotation

### What is the conjecture
Consider two lists of points $A=(a_1,\ldots,a_n)$ and $B=(b_1,\ldots,b_n)$, $a_i,b_j\in \mathbb{R}^2$ of length $n$. For any congruent copy $B'$ of $B$. We can look for the least-squares matching between $A$ and $B'$: The permutation $\pi\in S_n$ that minimizes $\sum_{i=1}^n \lVert a_i-b'_{\pi_i}\rVert^2.$
We consider the set $S_{\mathrm{opt}} = \{ \pi\in S_n \mid \exists B'\colon \pi \text{the unique optimal matching between } A and B'\}$.
The conjecture is that the number of permutations in $S_{opt}$ is polynomially bounded in $n$.

We need to count only unique optimal permutations, because there can be degenerate situations with an exponential number of optimal permutations. If the conjecture is true, it implies a polynomial-time algorithm for least-squares matching under rotations.

The optimum permutation is unaffected by positive scaling of $A$ or of $B'$, as well as translation of one of the sets.

References with some weaker results on a related problem (which I might also propose):
- Günter Rote: Partial least-squares point matching under translations. In: 26th European Workshop on Computational Geometry (EuroCG'10), Dortmund, March 2010, pp. 249–251, Editor: Jan Vahrenhold. https://page.mi.fu-berlin.de/rote/Papers/abstract/Partial+least-squares+point+matching+under+translations.html
- Rinat Ben-Avraham, Matthias Henze, Rafel Jaume, Balázs Keszegh, Orit E. Raz, Micha Sharir, Igor Tubis. Partial-Matching RMS Distance Under Translation: Combinatorics and Algorithms. Algorithmica 80, 2400–2421 (2018). https://doi.org/10.1007/s00453-017-0326-0

### Prerequisites needed
Euclidean geometry, finite point sets in the plane, distances

### [AMS categories]

* ams-52

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

Start by surveying the repository’s existing Lean formalized conjecture statements and conventions, since no target file or test is named. Then determine how to represent the point sets, rotations, least-squares matching, uniqueness, and polynomial bound in Lean; done means the conjecture is added in the repository’s established style.

Written by the indexing model from the issue text.