Hexagon

Submitted works

math.DS — Dynamical Systems

Uniqueness of four-body convex central configurations for all masses

Contributed by Tejasvi Singh Tomar

We prove that for every choice of four positive masses and every cyclic ordering of the bodies there is exactly one strictly convex planar central configuration with that ordering, up to similarity. This answers Problem 10 in the list of Albouy, Cabral and Santos, which Santoprete calls the Simó--Yoccoz conjecture. The main step is a uniform lower bound for the Hessian at convex central configurations: it is at least one quarter of its radial part, which vanishes only on translations and rotations. Dziobek's relations turn the indefinite part of the Hessian into a negative multiple of a square, and a Cauchy--Schwarz argument bounds this term by the radial part times the trace of an explicit $2\times2$ matrix in which the masses do not appear. We prove that this trace is less than $\frac34$ by interval arithmetic on the three-dimensional set of normalized convex central configurations, in the coordinates of Corbera, Cors and Roberts. Uniqueness then follows by a covering argument from the case of four equal masses. The computation has been repeated with a second, independently written program. The Hessian bound and the uniqueness theorem, including the computation, have been formalized in the Lean proof assistant and checked by its kernel, using only the standard axioms. As consequences, every degenerate four-body central configuration is concave, the convex central configuration depends analytically on the masses, and the known symmetry theorems for kites, isosceles trapezoids and rhombi follow in a few lines. The analytic dependence and the symmetry theorems are also formalized.

A mix of human-written and AI-generated textHuman understanding: all parts

Oct 26, 2026PDF ↗View work →

hexagon:2610.00550v1

math.DS — Dynamical Systems

Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean

Contributed by Tejasvi Singh Tomar

We prove that for every choice of five positive masses the planar five-body problem has finitely many central configurations up to similarity. This settles Smale's sixth problem for five bodies in the plane. Albouy and Kaloshin proved it for masses outside a closed algebraic subset of codimension two. We follow their method. Infinitely many central configurations would give an algebraic curve of complex solutions. At the places at infinity of the curve the valuations of the mutual distances must balance. We determine the possible valuation vectors at all positive masses, together with the mass conditions under which each can occur. We treat limits in which four bodies form a cluster of zero potential energy by expanding the potential, which is constant along the curve, at a place. This excludes, at every positive mass, one of the two diagrams in which such clusters occur, and part of the other. The same expansion excludes one further diagram at every positive mass. What remains is an exact analysis, by computer algebra, of the sets of mass conditions that can hold together at positive masses. Exact rational certificates show that the balance fails under each of them, except on a few one-parameter families of masses, which we treat separately. On the rays through $(1,4,4,4,4)$ and $(1,1,4,4,4)$ the certificates do not apply. On the first ray they cannot apply: there the complex equations have a continuum of solutions, as Albouy and Kaloshin observed. On these rays we count the real central configurations: there are 306 and 294 up to orientation-preserving similarity. The certificates, the programs that check them and a proof of the theorem in the Lean proof assistant are available.

A mix of human-written and AI-generated textHuman understanding: all parts

Oct 26, 2026PDF ↗View work →

hexagon:2610.00548v1

math.RA — Rings and Algebras

The rank of 3×3 matrix multiplication over F2 is 23

Contributed by Tejasvi Singh Tomar

The rank of the tensor of $3\times 3$ matrix multiplication over the field with two elements is at most $23$ by Laderman's algorithm, and Rudich and Rousseau recently proved that it is at least $22$ . We prove that it equals $23$ . Hence Laderman's algorithm uses the fewest multiplications among all bilinear algorithms over $\mathbb{F}_2$ and among all bilinear algorithms with integer coefficients. The proof uses the substitution method in the form developed by D'Ambrosio, Wang and Yang et al., which bounds the number of first factors of a decomposition that lie in a given subspace of the space of first factors. We sharpen these bounds for $111$ of Wang's $496$ classes of subspaces, constrain the ranks of the first factors through a $27\times 27$ flattening of the tensor, and list, up to symmetry, all sets of $22$ first factors that satisfy these constraints. An exact completion search shows that none of them is the set of first factors of a decomposition. The computation emits certificates, which are checked in the Lean 4 proof assistant. In one formal proof the largest checks are evaluated as compiled code, and in a second one the kernel evaluates every check, so that its final theorem depends only on the three standard axioms of Lean. The Lean proofs build on the formalization of Rudich and Rousseau and import their table of bounds and their reduction for block algorithms.

A mix of human-written and AI-generated textHuman understanding: all parts

Oct 26, 2026PDF ↗View work →

hexagon:2610.00552v1

math-ph — Mathematical Physics

Area law for three-dimensional U(1) lattice gauge theory with the Wilson action at every coupling

Contributed by Tejasvi Singh Tomar

We prove that three-dimensional U(1) lattice gauge theory with the Wilson action confines static charges at every coupling. More precisely, for each $\beta>0$ there are $\sigma(\beta)>0$ and $R_1(\beta)<\infty$ such that rectangular Wilson loops of sides $R,T\ge R_1(\beta)$ satisfy $\langle\cos\theta_C\rangle\le\exp(-\sigma(\beta)RT+c(R+T))$ , uniformly in the finite box, with an absolute constant $c$ and an explicit lower bound on $\sigma(\beta)$ . For the Villain action this is the theorem of G\"opfert and Mack. For the Wilson action it is cited as known but has remained open. The proof rests on a comparison. The Wilson plaquette weight is a mixture of Villain weights whose coupling has a very light upper tail. Hence, by Ginibre's inequality, the Wilson loop at coupling $\beta$ is at most an average, over a sparse Bernoulli set of frozen plaquettes, of the Villain loop at coupling $K\beta$ , and frozen plaquettes are insulating walls for the monopole gas. A variational regularization, built on the smallest minimizer of a cut functional, freezes more plaquettes, which only increases the loop. It produces slit domains on which the multiscale analysis of G\"opfert and Mack, with wall fields graded by their periods around the handles, runs with uniform constants. On these domains the loop decays like the exponential of the minimal spanning area with frozen plaquettes free. A Peierls estimate shows that this area is at least $(1-\eta)RT$ outside an event of probability at most $e^{-RT+O(R+T)}$ , with $\eta\to0$ as $K\to\infty$ . We carry over the steps cited from Brydges\textendash Federbush and G\"opfert\textendash Mack with explicit changes and prove them in full in Part S4 of the supplementary material, including a tree-graph counting step of Brydges whose printed deduction is incomplete. As corollaries, we obtain the area law at every coupling for all closed subgroups of U( $n$ ) containing the scalars, also with a Higgs field blind to the centre (as for U(2) with an adjoint Higgs field), and for the Georgi\textendash Glashow model at infinite Higgs coupling.

A mix of human-written and AI-generated textHuman understanding: all parts

Oct 26, 2026PDF ↗View work →

hexagon:2610.00549v1

cs.DS — Data Structures and Algorithms

Sorting networks on 13 inputs need 45 comparators

Contributed by Tejasvi Singh Tomar

Let $S(N)$ be the least number of comparators in a sorting network on $N$ inputs (the Bose--Nelson problem). The values are known for $N\le12$ , and for $13$ inputs the smallest known sorting network, found by Juill\'e, has $45$ comparators. We prove $S(13)\ge45$ , so $S(13)=45$ . Deleting the comparators met by the largest and the second largest input leaves a sorting network on $N-2$ inputs, so $S(N)\ge S(N-2)+P(2,N)$ , where $P(2,N)$ is the least possible worst-case number of comparators met by these two values. Van Voorhis stated $P(2,N)\ge\lceil\lg F(N)\rceil$ for an explicit function $F$ , but Mericanii showed that his proof is invalid. We prove $P(2,N)=\lceil\lg F(N)\rceil$ for $3\le N\le32$ by a finite search, which rests on the structure of the tree of paths of the largest value, the comparators on these paths, and a forest of comparators that carries the second largest value. With $S(11)=35$ this bound gives only $S(13)\ge44$ . For $45$ we apply it to the suffix of a network: if a network with $L$ comparators sorts a set $X$ of $0$ - $1$ vectors, then for suitable pairs of inputs the two values meet at most $L-c$ comparators, where $c$ is the cost of sorting the residual set left when their paths are deleted. A breadth-first search over the sets produced by prefixes of a hypothetical sorting network with $44$ comparators discards each set for which no single network stays within all these budgets, and no set survives at depth $25$ . A separate verifier checks the certificate written by the search. Two proofs in Lean 4 check the same certificate, and in one of them Lean's kernel checks every computation, with only the standard axioms. Juill\'e's network is checked in the kernel as well. As a consequence, each of the twenty lower bounds on $S(N)$ for $13\le N\le32$ that rested on Van Voorhis's inequality is proved and raised by one.

A mix of human-written and AI-generated textHuman understanding: all parts

Oct 26, 2026PDF ↗View work →

hexagon:2610.00530v1

quant-ph — Quantum Physics

A matching threshold of 2×10⁻³ for the rotated surface code under circuit-level noise

Contributed by Tejasvi Singh Tomar

We consider the rotated surface code of odd distance $d$ with its standard syndrome-extraction circuit, under circuit-level depolarizing noise in which every gate, idle step, preparation and measurement fails independently with probability $p$ , decoded by minimum-weight perfect matching with the log-likelihood weights of single faults. We prove that a memory experiment with $T$ rounds fails with probability at most $0.061\,(T+1)(d+1)\,\lambda^{d}/(1-\lambda)$ , where $\lambda=0.999\,(p/p_{\ast\ast})^{9/25}$ , for every $p\le p_{\ast\ast}=2\times10^{-3}$ . Hence the logical error rate per round decays exponentially in $d$ for all $p\le p_{\ast\ast}$ . Earlier rigorous thresholds for matching on surface-code circuits are $1.7\times10^{-4}$ , due to Dennis, Kitaev, Landahl and Preskill, and $7.4\times10^{-4}$ , due to Fowler. We keep their reduction of a failure to a weighted self-avoiding path in the decoding graph, but bound these paths by a local criterion for non-backtracking walks, which gives the threshold $1.04\times10^{-3}$ in closed form. To reach $2\times10^{-3}$ we use the minimality of the correction along the path, for a canonical choice among the minimum-weight corrections: labellings of short stretches of the path into error and correction edges that contradict this minimality are excluded, and the remaining labelled walks are counted with a potential function that is checked in exact arithmetic. For a leaner schedule with fused measure-and-reset steps the two arguments give $1.53\times10^{-3}$ and $3\times10^{-3}$ , respectively. With error rates that depend on the type of operation, they certify exponential decay for error models built from the published component error rates of Quantinuum's Helios and H2 and of IBM's Heron r3 processor ibm_boston, mapped onto this circuit. All theorems are also proved in the proof assistant Lean 4, with all computations checked by its kernel. Any argument that bounds the failure probability by the probability of an increasing event, ours included, is limited by the smallest such event that contains all failures, and Monte Carlo estimates place the threshold of this event near $4\times10^{-3}$ for this circuit.

A mix of human-written and AI-generated textHuman understanding: all parts

Oct 26, 2026PDF ↗View work →