Papers

We present the formalization of Carleson's theorem in the proof assistant Lean. This paper describes the mathematical content, organization of the project, the blueprint, and the main design decisions behind the formalization. It is the result of a large collaborative effort, written and developed in public.

A packing of $n$ congruent balls in $\mathbb{R}^3$ is a family of interior-disjoint Euclidean balls all having the same radius. The contact number of a packing is the number of touching pairs of balls. In this paper we investigate the problem of determining the maximum contact number, $c(n)$, of a packing of $n$ congruent balls in $\mathbb{R}^3$. We first show that all packings of $n$ congruent balls that have a contact number of $c(n)$ are minimally rigid. Furthermore, we show that $c(n)=3n-6$ for $n=6,7,8,$ and $9$. These two results resolve a conjecture of K. Bezdek and Khan. During the proof of the latter result, we also enumerate the contact structures of all packings of $n$ congruent balls with contact number $c(n)$ for $n=6,7,$ and $8$. Additionally, we provide a lower bound construction which shows $c(n)> 6n-6\sqrt[3]{2}n^\frac{2}{3}$ when $n=16k^3-33k^2+24k-6$ where $k\in \mathbb{N}$. We also look at the restricted problem where each ball is centered on the face-centered cubic lattice $A_3$. In this case let $c_{A}(n)$ denote the maximum contact number. We show that $c_{A}(n)\leq 6n-\frac{6}{\sqrt[6]{2}}n^\frac{2}{3}$ for all $n$, and determine the asymptotics of $c_{A}(n)$ to be $c_{A}(n)=6n-(1+o(1))6\sqrt[3]{2}n^\frac{2}{3}$.

Let $E_{A,B}\colon y^2 +Axy + By = x^3$ be an elliptic curve over $\mathbb{Q}$. The $3$-torsion point $(0,0)$ induces a $3$-isogeny $\phi\colon E_{A,B}\to E_{A,B}'$. Assuming $E_{A,B}$ has good reduction at $3$, we construct an explicit $(m+t)\times m$ matrix $M_{A,B}'$ over $\mathbb{F}_3$, whose kernel encodes the dual isogeny Selmer group $\operatorname{Sel}_{\widehat{\phi}}(E_{A,B}')$ modulo the image of the torsion point $(0,0)$. Here, $m = \omega(B) - 1$, and $t$ encodes the global Selmer ratio $3^{t-2}$. We compute $M_{A,B}'$ in various regimes for billions of elliptic curves $E_{A,B}$. Based on our data, and motivated by prevalence of random linear algebraic models throughout number theory, we conjecture that, for fixed $m$ and $t$, the matrices $M_{A,B}'$ become uniformly distributed, and we formulate a corresponding conjecture for the distribution of $\operatorname{Sel}_{\phi}(E_{A,B})$. Our model predicts that, for fixed $t$, the average size of $\operatorname{Sel}_{\phi}(E_{A,B})$ is $1 + 3^t$.

We study hyperedge partial duals of finite hypermaps in a purely combinatorial framework, without assuming orientability. A hypermap is represented by three fixed-point-free involutions $(\tau_0,\tau_1,\tau_2)$ on its flag set. We first give an explicit construction of the medial map from this model: $02$-orbits become the medial vertex discs, while $\tau_1$-transpositions become the medial bands; a local orientation system and its twist data then provide a signed rotation description of the medial map. We next prove that the state circles associated with a chosen set of hyperedges are in natural bijection with the vertex orbits of the corresponding partial dual, yielding a crossing-total characterization of all Eulerian hyperedge partial duals. For bipartiteness, the twist data lead to a modified medial map in which inserted bars record the obstruction to a global orientation. We prove that a partial dual is bipartite if and only if its dualized hyperedge set is exactly the set of $c$-type hyperedges identified by an all-crossing orientation of this modified medial map. When the hypermap is orientable, these constructions specialize to the known orientable-hypermap results; when every hyperedge has valence two, they specialize to the ribbon-graph results.

An algebraic $q$-difference equation for $|q|>1$ is considered. A sufficient condition is proposed for the convergence of a solution to such an equation in the form of a Dulac series within a sector centered at the origin. An example illustrating the application of this sufficient condition is provided.

The present work proposes a new operator splitting technique. The method leverages ideas used in PDE-constrained domain decomposition, adapting them to the objective of decoupling equations defined on the same geometric domain. The methodology is applied here to the resolution of coupled flow and deformation in the linear quasi-static Biot problem. An overview of its main characteristics is provided, also in comparison with the well established fixed-stress split for poroelasticity.

We find bounds for the genus and for the number of boundary components of a surface that is either index one as a free boundary minimal surface or stable as a free boundary constant mean curvature surface in a Riemannian three-manifold with convex boundary and non-negative Ricci curvature, provided the first Dirichlet eigenvalue of its Jacobi operator is non-negative. As an application, we establish strong topological restrictions on such surfaces in compact strictly convex domains of three-dimensional normal homogeneous spaces.

We introduce lower bounds on the minimum distance of one-generator quasi-cyclic codes of arbitrary index, obtained by puncturing and shortening the code at the level of its blocks. For balanced codes, these bounds form a nondecreasing chain whose first term is the Jensen bound. We apply these bounds to conduct a computer search and obtain many Hermitian LCD codes with good parameters. Among them there are six codes of length at most 30 which improve the corresponding lower bounds of Araya and Harada. These codes further give maximal-entanglement entanglement-assisted quantum codes, which we compare with the parameters currently recorded in the literature.

Finite-aperture near-field sensing leads to a super-resolution geometry fundamentally different from the translation-invariant Fourier setting. In the Fresnel regime, wavefront curvature introduces a range-dependent quadratic aperture phase, so distinguishability is governed by incomplete quadratic exponential sums of the form \( \sum_{n=0}^{N_r-1} a_n e^{i(\omega_1 n+\omega_2 n^2)} \), rather than by angular separation alone. We develop a deterministic recovery theory for sparse measures with ranges on a finite grid and continuous angles, and introduce a support-uniform quadratic-phase aperture criterion replacing classical minimum separation. Under this criterion, total-variation minimization exactly recovers every sparse measure in the admissible support class, uniformly over all nonzero complex amplitudes. The proof develops nonasymptotic support-uniform bounds for finite quadratic sums and combines them with a gauged Hermite dual certificate controlling interpolation, local curvature, and off-support leakage. We further construct a finite-harmonic Bessel-Vandermonde lift with explicit truncation error. In the far-field limit, the quadratic phase disappears and the theory reduces to Fourier-type angular super-resolution.

The harmonic centrality of a vertex $v$ in a graph $G = (V,E)$ is the sum of reciprocals of distances of vertices of $G$ from $v$. The vertices of $G$ which have the maximum (minimum) harmonic centrality form the harmonic center (or periphery, resp.) of $G$. We study harmonic centers of graphs and their localization in graph blocks, presenting sufficient conditions for graphs (in terms of diameter or number of edges) to have those centers contained in a single block; in addition, we show that each connected graph is the harmonic center as well as harmonic periphery of some graphs.

In this paper we prove a version of Shnirelman's inequality in the two-dimensional square $[0,1]^2$. More precisely, given a target fluid configuration $f$ (a volume-preserving diffeomorphism) we construct a divergence-free velocity field $v\in L^q_tL^p_x$ whose flow connects $f$ to the identity and whose $L^q_{t} L^p_x$-norm can effectively be bounded by the $L^p$-difference of $f$ and $id$. However, higher regularity of the vector field might be affected. The main difference with the higher dimensional case is that, because of the topological obstructions of dimension $\nu=2$, we have to allow that different fluid trajectories 'intersect' in space. We also observe that this choice leads to the emergence of irreversible behaviors in the Eulerian dynamics.

We prove that nilpotent and metabelian products of groups with decidable word problem have decidable word problem. In contrast, we exhibit families of groups with decidable word problem for which their solvable product have undecidable word problem. In doing so, we exhibit hyperbolic groups with undecidable membership problem in its derived subgroups.

We study synchronized boundary and kernel approximation for harmonic measure systems satisfying nested mean-value identities. Under boundary concentration along a common subsequence, joint limits yield representation on a common refinement, and gluing gives uniqueness on the minimal boundary. Neighborhood nonvanishing gives full-sequence synchronized selection. For a compact set whose removal from a bounded $C^{1,1}$ domain in dimension at least three leaves a connected domain, zero Newtonian capacity is equivalent to concentration of one normalized singular kernel, constructed from harmonic measures, on a subsequence of one relatively compact exhaustion. For such zero-capacity sets, capacitary estimates give quantitative recovery of finite signed source measures on every prescribed relatively compact exhaustion. On rectifiable curve networks in three dimensions, the logarithmic error bound is sharp for this recovery formula in the class of finite measures. Boundary splitting and finite weighted metric graphs illustrate the gluing conclusions.

We give an explicit quasi-isometry from the flip graph of triangulations $\mathscr{F}_{g,n}$ to the $\epsilon$-thick part of Teichmüller space equipped with the Teichmüller metric, by mapping each ideal triangulation to the hyperbolic surface whose shearing coordinates along that triangulation are all equal to zero. Extending this construction, we obtain a quasi-isometry $Q$ from the hexagon graph $\mathscr{H}_{g,n}$ to the augmented Teichmüller space $\overline{\operatorname{Teich}}_{g,n}$ equipped with the Weil-Petersson metric, and we estimate its width, that is, the Hausdorff distance between $Q(\mathscr{H}_{g,n})$ and $\overline{\operatorname{Teich}}_{g,n}$. By bounding the Weil-Petersson distance along grafting rays and the Teichmüller distance along shearing deformations, we show that the width is at most $\sqrt{g+n}\log(g+n)$. We also provide an explicit projection from any point in $\overline{\operatorname{Teich}}_{g,n}$ to the thick part of boundary strata, maintaining simultaneous control over the Weil-Petersson distance and the shearing coordinates.

We present a Banach space $X_\alpha$, equipped with an explicit norm, whose properties resemble those of the predual $JT_*$ of the James Tree space. In particular, $X_\alpha$ admits a shrinking dyadic basis with the property that the sums of its elements over any segment are uniformly bounded. The space $X_\alpha$ is complementably $\ell_2$-saturated, and its dual $X_\alpha^*$ does not contain an isomorphic copy of $\ell_1$. Finally, the bidual $X_\alpha^{**}$ is also complementably $\ell_2$-saturated, and the quotient $X_\alpha^{**}/X_\alpha$ is isometric to $c_0(2^{\mathbb{N}})$.

We develop foundations for metastable homotopy theory using Heuts' 2-truncated Tate coalgebras.

We revisit the correspondence between three-dimensional gauged linear sigma models and K-theoretic Gromov-Witten theory. We show that the K-theoretic Hori-Vafa formula for the grassmannian arises from the three-dimensional gauge theory upon including an appropriate anomaly-cancellation factor. Furthermore, we derive K-theoretic I-functions for isotropic grassmannians by incorporating symmetric and anti-symmetric tensor representation fields together with suitable boundary conditions.

We study the Goodwillie tower of the identity evaluated at the circle. Our main result is the p-local equivalence $\Omega P_{p^k}I(S^1) \simeq \mathbb{Z} \times \Omega^{\infty+2k}\tau_{>0}\mathbb{Sp}^{p^k}$ obtained from the work of Behrens and Kuhn on the Whitehead conjecture. In particular, this identifies the Goodwillie approximations of the circle as infinite loop spaces, a phenomenon which does not hold in general. The equivalence also reduces the computation of their homotopy groups to a stable problem, making them accessible to tools such as the Adams spectral sequence and to computer calculations. We place these computations in a more general framework by developing a Goodwillie-calculus analogue of the Gray sequence, which relates the homotopy groups of successive stages of the tower.

We study the right derivative of the zeta-star correspondence between binary expansions and multiple zeta-star values of infinite depth. At a finite-index point, this derivative is a normalized difference of two finite-depth multiple zeta-star values. We use this identity to express its local behavior in terms of lower-truncated star sums and their boundary coefficients. The homogeneous contribution at summation variable three contracts with ratio $2/3$; the full coefficient also receives a positive forcing term. A weighted sum of the remaining coefficients contracts by at most $1/2$ at each binary step. On the open parameter interval, we prove that the derivative is right-continuous everywhere and continuous precisely at the non-dyadic points. Its left jump at a dyadic point is given by an explicit positive multiple series, with divergence exactly at $1/2-2^{-M}$, $M\ge2$. A refinement of the index gives an infinite upper right Dini derivative at every interior point. We also prove that the Hausdorff, packing, and modified upper box dimensions of the graph are all $\log_2(8/3)$. The Hausdorff lower bound uses the dimension of the Bernoulli convolution with parameter $2/3$, together with a separate measure-transfer argument. Finally, the pointwise Hölder exponent at a non-dyadic point is $\log_2(3/2)$ divided by its dyadic approximation exponent, and the corresponding Hausdorff spectrum is linear.

Let $P$ and $Q$ be proper upward monotone unary generalized quantifiers on a fixed domain $D$. We study the validity, over all structures $M$ with domain $D$, of \[ M \models Px\,Qy\,R(x,y) \rightarrow Qy\,Px\,R(x,y), \] called scope dominance. The iteration of two quantifiers lies between their branching product, which is generated by rectangles, and the dual of the branching product of their duals. We give criteria for equality with these bounds, obtain a new proof of the countable characterization of scope dominance, and characterize the case in which the inner quantifier is "at least $\kappa$ many." Under the Generalized Continuum Hypothesis, Goldberg's theorem shows that, for ultrafilters, scope dominance is equivalent to equality between iteration and the branching product, whereas an elementary counterexample on a domain of size $\aleph_2$ shows that this equivalence fails for arbitrary upward monotone quantifiers. For the case where both quantifiers are filters, the question becomes set-theoretic: the existence of a counterexample is equiconsistent with the existence of a measurable cardinal.

In this paper, we consider the local minimizers to a class of non-autonomous functional with double-phase Orlicz growth: \begin{equation*} u \in W^{1,1}(\Omega; \mathbb{R}^N) \mapsto \int_\Omega \Big( {\varphi_1}\big(|Du|_{\mathbb{A}^u}\big) + a(x)\,{\varphi_2} \big(|Du|_{\mathbb{A}^u}\big) \Big)\, dx, \end{equation*} where $|Du|_{\mathbb{A}^u} := \big\langle \mathbb{A}(x,u)\,Du, Du \big\rangle^{\frac{1}{2}}$ with $\mathbb{A}(x,u) = \big\{A^{\alpha \beta}_{ij}(x, u)\big\}_{i,j = 1\cdots N}^{\alpha,\beta = 1\cdots n}$ as the uniformly elliptic bounded symmetric tensor field, and $\varphi_k(\cdot)$ for $k=1,2$ are two different $N$-functions. We prove the partial regularity of their local minimizers if the continuity modulus of $a(\cdot)$ and $\varphi_k(\cdot)$ are fit for the gap conditions, and $\mathbb{A}(x,u)$ meets an optimal regularity in $(x,u)$. This is an extension from the single Orlicz growth functional to the double-phase one based on an essential improvement of several important inequalities.

We prove that the Pólya-Szegő inequality for the $L^p$ norm of the Riesz fractional $s$-gradient fails for every $p\in[1,2)$ and $s\in(0,1)$, thus providing a negative answer to a question posed by Nguyen and Squassina in 2017.

In this paper, we study the elliptical shape of the numerical range of tridiagonal matrices of orders $3,4$ and $5$ with zero entries on the main diagonal, a positive constant value $a$ along the super-diagonal, and sub-diagonal entries are \begin{align*} \begin{cases} r, sr^2, r^3, sr^4,\ldots, r^{n-1} & \mbox{ if $n$ is even, and } r, sr^2, r^3, sr^4,\ldots, sr^{n-1} & \mbox{ if $n$ is odd}, \end{cases} \end{align*} where $n$ denotes the order of the matrix, $s>0$ and $r$ is a real number. We further investigate the flat portions on the boundary of the numerical range of these $n\times n$ matrices in the special case $r=-1$. Some results given in \cite{chien2011numerical} are obtained as a particular case of our results.

Convergence in parameter estimation classically requires “persistency of excitation," which is a non-degeneracy condition on a trajectory-dependent signal. This paper develops, to the best of our knowledge, the first such excitation theory for a nonlinear partial differential equation. In the context of identifying the unknown viscosity from spectral observations in the two-dimensional Navier–Stokes equations for incompressible fluids, our excitation condition is computable, verifiable a priori, and sharp with respect to scaling. Our approach employs a data assimilation methodology to account for an unknown initial state and select candidate viscosities by minimizing the loss between the low-mode observations of the fluid velocity and low-mode projection of a nudging-based filter that assimilates these observations. The main novelty of our framework is to distinguish a new functional, $\mathsf{W}$, representing the work done by the filter's associated sensitivity variable on the enstrophy, around which our entire analysis is centered. We show that $\mathsf{W}$ is explicitly comparable to the observability Gramian of the associated Gauss–Newton iteration, and subsequently establish the following dichotomy at every critical point of the observational loss: either $\mathsf{W}$ exceeds a certain threshold, in which case the candidate viscosity obeys an explicit error estimate that depends inversely on $\mathsf{W}$ and the observational density $N$, but directly on the error between initial conditions, or else $\mathsf{W}$ is below the threshold and the observations are quantitatively insensitive to parameter updates in a way that is detectable to the user. Notably, our approach is energy-based, and therefore expected to be adaptable to many other nonlinear dissipative systems.

We investigate the classification of $C^*$-algebras generated by pairs of isometries $(V_1, V_2)$ satisfying $V_1V_2=qV_2V_1$, where $q=e^{2\pi i\theta}$ with $\theta$ irrational, up to unitary equivalence. Using a functional model that realizes pure $q$-commuting pairs on vector-valued Hardy spaces in terms of a uniquely associated triple $(\mathcal{F}, P, U)$ consisting of Hilbert space $\mathcal{F}$, an orthogonal projection $P$ and a unitary operator $U$, we analyze the internal structure of $C^*(V_1,V_2)$ via an extension of the $C^*$-algebra generated by its minimal $q$-commuting unitary extension by the defect ideal $\mathcal{I}_{\mathcal{D}} =\langle [V_1^*, V_1],[V_2^*, V_2]\rangle$. For pairs that are essentially doubly $q$-commuting, we show that $PUP|_{\operatorname{ran} P}$ is semi-Fredholm and prove that $|\operatorname{ind} PUP|_{\operatorname{ran} P}|$ is invariant under unitary equivalence of the corresponding $C^*$-algebras, thereby providing an explicit criterion for distinguishing non-equivalent pairs. This work extends the seminal 1978 results of Berger, Coburn, and Lebow for commuting isometries, while addressing the key technical nuances of this noncommutative setting: most notably, navigating the failure of Gelfand theory due to noncommutativity and replacing the classical Toeplitz extension by an extension of the noncommutative torus by the ideal of compact operators.

We prove Koebe's conjecture for John domains by showing that every planar John domain is conformally equivalent to a circle domain. Our proof is based on a geometric property of John domains, which we prove to be sufficient for uniformization by a circle domain. As a consequence, we obtain an alternative proof of Koebe's conjecture for inner uniform and Gromov hyperbolic domains, recovering results established in earlier work of the authors. Finally, we derive a necessary and sufficient condition for a domain to satisfy Koebe's conjecture by using Schramm's transboundary modulus and well-behaved exhaustions of circle domains constructed by the second author and Rajala.

Hengartner asked whether a pluriharmonic mapping between equidimensional complex Euclidean domains is locally one-to-one precisely at the points where its real Jacobian is nonzero. Naser had earlier claimed the conclusion in complex dimension two, and a recent theorem of Kalaj supplies a complete proof in that dimension. We prove the result in every complex dimension. The main ingredient is a singularity-theoretic characterization which is of independent interest: if $q\colon(\C^n,0)\to(\C,0)$ is a nonconstant holomorphic germ, then $dq(0)\ne0$ if and only if one (equivalently, every) phase hypersurface \( \{\Repart(e^{-i\theta}q)=0\} \) is a rational homology $(2n-1)$-manifold at the origin. The difficult direction combines local conical structure, Alexander duality, the Milnor fibration, and A'Campo's vanishing theorem for the Lefschetz number of local monodromy. The argument requires neither an isolated critical point nor a reducedness hypothesis. It follows that the real critical set of any pluriharmonic self-dimensional mapping agrees exactly with its local noninjectivity set. As a quantitative application, combining our theorem with Kalaj's boundary regularity theorem shows that, in every complex dimension, a quasiconformal pluriharmonic homeomorphism of the unit ball onto a bounded $C^1$-Dini domain is bi-Lipschitz.

For distinct integers $a$ and $b$, an $\{a,b\}$-edge-weighting assigns $a$ or $b$ to each edge and labels each vertex by the sum of its incident weights. Such a weighting is proper if adjacent vertices receive distinct labels. We prove that, for every fixed pair of distinct integers, deciding whether a proper weighting exists is NP-complete even for simple cubic planar graphs. On planar multigraphs with $m$ edges, we give an exact $2^{O(\sqrt m)}$-time algorithm and, assuming the Exponential Time Hypothesis (ETH), exclude $2^{o(\sqrt m)}$-time algorithms even for simple cubic planar graphs. As a consequence, locally irregular $2$-edge-coloring is NP-complete on simple cubic planar graphs, admits a deterministic $2^{O(\sqrt n)}$-time algorithm on $n$-vertex graphs in this class, and admits no $2^{o(\sqrt n)}$-time algorithm under ETH. For maximizing the number of edges joining vertices with distinct labels, we give a deterministic efficient polynomial-time approximation scheme (EPTAS) on planar multigraphs, a polynomial-time $1/2$-approximation on multigraphs, and APX-completeness even on simple cubic graphs. Extending a partial $\{a,b\}$-edge-weighting to a proper one is NP-complete for every fixed pair even on simple cubic planar bipartite graphs, while it is polynomial-time solvable on trees. The hardness persists even when the prescribed edges form disjoint paths of length $6$ and all edges of each path have the same prescribed weight.

We prove that on the Sierpinski gasket, a prototype of compact fractal space, Dirac distributions arise as the weak limit of probability measures associated with sequences of high energy eigenfunctions of the Laplacian in a way that cannot happen in compact Riemannian manifolds.

We study two hierarchies of bivariate generating functions defined by differential recursions: a self-dual hierarchy and a reduced-symmetry hierarchy. Their rational coefficient functions produce palindromic and anti-palindromic triangles, including OEIS A336110 and A140136. For general differential order $p$, the reduced hierarchy decomposes into $p-1$ Horn-type companions. An explicit differential intertwiner of order $p-3$ relates the last companion to the normalized self-dual generating function. The companions share a principal symbol and a rationally parametrized characteristic curve with a projective $S_3$ action. At $p=2$ this construction yields the Narayana quadratic. At $p=3$ the symmetry lifts to $S_4$: two algebraic sectors are edge resolvents of one quartic root configuration, and the nonsymmetric Gross–Witten–Wadia generating function has degree four. For $p=4$ and $p=5$ we derive algebraic equations of degrees six and eight, respectively, and find Galois groups $S_6$ and $S_8$ at generic specializations. At $p=6$ we verify a degree-ten specialization with Galois group $S_{10}$. Their discriminants exhibit a universal cubic characteristic factor and a squared lower-order factor. A boundary factorization explains the observed algebraic degrees and discriminant monomials. We formulate conjectures on algebraicity and Galois groups in the reduced hierarchy and identify a possible mechanism for transcendence in the higher self-dual hierarchy.