we-solve (beta)

Math-2490 · mathematics · Geometry

Borsuk Partition Problem in Dimensions Four Through Sixty-Three

Status Partially solved · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
For each $4\leq d\leq 63$, determine whether every bounded set $S\subseteq\mathbb R^d$ can be partitioned into at most $d+1$ subsets of diameter strictly smaller than $\operatorname{diam}(S)$.

Formulation references: [S1], [S2].

Short English statement

For each $4\leq d\leq 63$, determine whether every bounded set $S\subseteq\mathbb R^d$ can be partitioned into at most $d+1$ subsets of diameter strictly smaller than $\operatorname{diam}(S)$.

Sources

Catalogue entry

Statement licence: CC-BY-SA-4.0 · Source file

Contributions 1

Math-2490-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2490

For every $9\le d\le63$, the higher-dimensional corollary claims a compact diameter-$\sqrt2$ set needing more than $d+1$ smaller-diameter parts. It starts from the dimension-nine example and adjoins new equidistant points to raise the required number of parts. The cases $4\le d\le8$ are not decided by these constructions.

Borsuk Partition Problem in Dimensions Four Through Sixty-Three

OpenAI's claim

Nine-dimensional diameter covering: The projector configuration of lines in $\mathbb R^4$, viewed in the nine-dimensional space of trace-one symmetric matrices, is claimed to require more than ten smaller-diameter covering sets. This compact configuration refutes Borsuk’s assertion in dimension nine.

Mathematical statement of the claimed result

Mathematical claim 1.
In the nine-dimensional affine space $\{A\in\operatorname{Sym}_4(\mathbb R):\operatorname{tr}A=1\}$ with Frobenius distance, set $X=\{uu^{\mathsf T}:u\in\mathbb R^4,\ |u|=1\}$. The claim is that $X$ is compact, $\operatorname{diam}X=\sqrt2$, and there do not exist ten subsets $X_1,\ldots,X_{10}$ covering $X$ with every $\operatorname{diam}X_i<\sqrt2$. The article also claims that, for each integer $d\ge9$, there is a compact $Y_d\subset\mathbb R^d$ of diameter $\sqrt2$ admitting no cover by $d+1$ subsets of smaller diameter. The extension adjoins $d-9$ points at diameter distance from one another and from the translated projector set. The dimensions four through eight remain outside these counterexamples.

Outline of the argument

Nine-dimensional diameter covering: A smaller-diameter cover is enlarged to an open cover and converted into nonnegative coordinate functions on projective three-space. Orthogonal lines must have disjoint positive supports. Extending the map to positive semidefinite matrices produces an odd sphere map; its mod-two degree and an equality analysis of the support complex contradict the possible ten-label structure.

Formal verification

Family 156 describes Lean coverage for the nine-dimensional projector covering obstruction against ten arbitrary smaller-diameter sets.

Nine-dimensional diameter covering: The manuscript links BorsukNine.lean (declaration OAI.BorsukNine.main_theorem).

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →