Papers

We prove that the pairs of integers $0\le m<n$ for which a nondecreasing integer sequence can remain complete after every deletion of $m$ terms and become incomplete after every deletion of $n$ terms are exactly those with $m\le1$. Here a sequence is complete if every sufficiently large integer is a finite sum of terms with distinct indices. This answers Erdős Problem 348, posed by Graham and later included in the book of Erdős and Graham. The proof uses a central-interval theorem: if a complete nondecreasing positive integer sequence $(a_i)$ has prefix sums $S_j$ with $S_j-a_{j+1}\to\infty$, then each sufficiently long prefix represents every integer from any fixed completeness threshold $T$ to $S_j-T$. We also refute Graham's conjecture, later repeated by Erdős and Graham, that $(\lfloor t\gamma^n\rfloor)_{n\ge1}$ is complete for every $t>0$ and $1<\gamma<(1+\sqrt5)/2$. We obtain the counterexample by combining Dubickas's fractional-part theorem with an elementary sign adjustment. For a common base in this range, we further construct two such sequences whose interleaving is incomplete and whose coefficient ratio is not a rational multiple of any integer power of the base.

In this note, we present an integral representation of the $k$-generalized Fibonacci sequence and provide a proof using contour integration. This representation enables the derivation of several known identities and a Binet-type formula related to the $k$-generalized Fibonacci sequence.

We study a jointly exercised American condor contract whose payoff is a call condor payoff plus a positive cash amount. Its plateau and positive tails produce two inner exercise boundaries and two outer cash-exercise boundaries. We construct the unique bounded solution of the associated variational inequality, strong on each side of the plateau, and identify it with the optimal stopping value. We prove monotonicity and continuity of the four boundaries and determine their limits at expiry. Following Broadie and Detemple, we express the inner boundaries as cutoffs of the boundaries of uncapped contracts with the same cash components. We also prove call-side convexity and volatility monotonicity under a sufficient condition, solve the stationary problems explicitly and present numerical results.

Florian Luca devoted the last paper of his life to the set $\mathcal K$ of odd positive integers $k$ such that $2^n k+1$ is a Carmichael number for some positive integer $n$. He proved that if $m\ge 5$ is fixed and odd, then there are only finitely many primes $p$ with $p^m\in\mathcal K$. In this note, written as a small tribute to his memory, we extend his result in three directions, using only his published work as our reference base. First, we extract from his arguments explicit quantitative bounds: every Carmichael number $N=2^n p^m+1$ with $m$ odd satisfies $n<2^{2\cdot10^7(m+1)^2m^2(\log p)^2}$, and if $p>m$ the much sharper bound $n<25m^4\log p$ holds; for $p>500m^5\log m$ we further record the uniform bounds $\omega(N)\le 26m^7$ on the number of prime factors. As an application, the number of such Carmichael numbers up to $x$ is $O_m(x^{1/m})$. Second, we generalize the multiplicative independence step of Luca's proof from base $2$ to an arbitrary even base $b$: if $b$ is even, $m\ge3$ is odd and coprime to $b$, $p>m$ is prime and $N=b^n p^m+1$ is Carmichael, then $b^n p^m$ and $b^a p^\beta$ are multiplicatively independent whenever $b^a p^\beta+1$ is a prime factor of $N$. Third, we report an exhaustive computation showing that the only Carmichael number $2^n p^m+1\le 10^{18}$ with odd $3\le m\le 37$ is $1729=2^6\cdot 3^3+1$, that no such number exists with odd $5\le m\le 37$ (extended to $10^{21}$ for $5\le m\le 15$), and that the only example with even $4\le m\le 36$ is $46657=2^6\cdot 3^6+1=13\cdot 37\cdot 97$, where $3^6=27^2$ is the square of the smallest element of $\mathcal K$.

This note provide a proof of Conjecture 2.5 in Fang et al. (J. Appl. Probab., 58(4):851–867, 2021), with the help of GPT-6 Astra. We show that the number of edges lying above zero of a random walk generated from the uniform permutation has the discrete arcsine law. The proof is short but hinges on an unexpected representation. We also make several comments on solving the problem using large language models.

The shifted lonely runner conjecture was recently disproved by Blanco, Criado and Santos. We give quantitative bounds on its failure as the number of runners grows. The loneliness of a configuration is the maximum, over time, of the distance from the origin to the nearest runner. We write $1/(n+1+E_n)$ for the infimum of loneliness over configurations of $n$ runners on the unit circle with distinct positive integer velocities and arbitrary initial shifts. We prove $E_n\ge\lfloor n/287\rfloor$, which together with the elementary bound $E_n\leq n-1$ implies that $E_n$ grows linearly in $n$. We also show that $E_n\geq1$ for every $n\geq95$.

We study row-softmax self-attention with independent Gaussian query and key weights in the proportional regime, at fixed inverse temperature. Hayase, Collins, and Karakida proved Gaussian equivalence for the empirical squared singular-value distribution after removal of the Perron direction. A global law alone does not exclude finitely many nonleading outliers. We prove that no such outliers persist: the rescaled squared singular value $\ell s_k(A)^2$ converges in probability to the upper edge of their bulk law for every fixed $k\ge 2$. In fact, this convergence is uniform over any deterministic sublinear number of leading non-Perron indices. The proof uses an exact decomposition of the softmax normalization, conditions on the key matrix, identifies the conditional covariance exactly with a diagonally conjugated inner-product kernel, linearizes that kernel in operator norm, and applies the outside-support local law of Fan, Ma, Paquette, and Wang. A separate stability argument identifies the finite conditional deformed Marchenko-Pastur edge with the limiting bulk edge. We also derive a scalar formula for that edge throughout the proportional regime and recover the explicit square-model formula of Hayase, Collins, and Karakida, including its physical branch.

We propose a new framework for noncommutative stochastic integration in $L^p$, inspired by Bichteler's notion of $L^p$-integrators, that massively generalizes our previous theory of $L^2$-valued stochastic integration against $L^2$-decomposable processes. Central to our framework is a noncommutative analog of a predictable integrand we call a predictable linear process. We develop basic properties of stochastic integrals against "noncommutative $L^p$-integrators" and establish a useful criterion for a noncommutative stochastic process to be a noncommutative $L^p$-integrator. This criterion applies, in particular, to a rich class of processes we call measured decomposable processes, which includes free Brownian motion and, more generally, the $q$-Brownian motions. We also show that, when specialized appropriately, our framework recovers the classical notion of an $L^p$-integrator up to the fact that the noncommutative theory sees only the modification class of a classical stochastic process. As an application, we use our theory to study noncommutative stochastic differential equations (SDEs) in $L^p$. Under natural local-Lipschitz and boundedness assumptions, we establish the existence and uniqueness of maximal solutions and show that a maximal solution with finite lifetime must blow up in $L^p$ norm. As corollaries, we obtain new existence and uniqueness results for free SDEs and SDEs driven by $q$-Brownian motion. Notably, in the free case, our results apply to coefficients arising through the continuous functional calculus from merely locally Lipschitz scalar functions, as opposed to locally operator-Lipschitz functions.

We give an explicit non-random example of nonadditivity of minimum output von Neumann entropy. The proof uses a finite-dimensional construction which imitates free Haar unitary behavior. The same channel gives a violation of additivity for the minimum output Rényi-$p$ entropy for any $p\in[1,\infty]$. Additionally, given any $p_0>0$ and $\mathfrak g>0$, we extend the construction to obtain an explicit non-random channel which has entropy gap $\ge\mathfrak g$ uniformly over $p\in[p_0,\infty]$.

Lee-Yang theorems are a powerful tool for studying many-body systems, with applications ranging from analyzing phase transitions to proving the efficiency of certain classical and quantum algorithms. In this work, we prove a Lee-Yang zero-freeness theorem for the partition function of a broad class of interacting fermion models, implying the existence of a provably efficient quantum algorithm for estimating their ground-state energies. This class includes several well-known models such as the attractive Hubbard model, repulsive Hubbard model on bipartite graphs, and the interacting Hofstadter model. Our results also rigorously establish the nonexistence of phase transitions in these models in the presence of a nonzero local external field.

We study the detectability of split surfaces in isogeny graphs of principally polarized superspecial abelian surfaces, a question relevant to the security analysis of dimension-$2$ isogeny-based cryptography. Our approach uses refined Humbert invariants to replace explicit isogeny computations with primitive representation problems for positive definite quadratic forms in five variables. We develop algorithms to detect $(N,N)$-splittings and to compute the minimum $(N,N)$-splitting level of a superspecial Jacobian without constructing the corresponding isogeny path. The same framework detects embeddings of real multiplication (RM) orders through primitive representations of discriminants of real quadratic orders. For RM, we use exhaustive small-prime data together with $100{,}000$ random polarizations per prime for $227\leq p\leq1619$, testing primitive representations of square-free discriminants $D\leq100$; the first nontrivial primitively represented discriminant is typically small. We apply these methods experimentally in two regimes. For $11\leq p\leq251$, where the irreducible principal polarizations are known exhaustively, the automorphism data recovered from the refined Humbert invariant reproduces the counts of Ibukiyama–Katsura–Oort for the irreducible polarizations. For large parameters, we reach primes of $1000$ bits, where the splitting degrees produced satisfy $\log_2N\approx\log_2p$ with a distribution whose shape is stable across the whole range, so the detected $(N,N)$-isogeny has degree about $p^{2}$; the smallest observed largest prime-power divisor of $N$ remains small up to $250$ bits and increases sharply from $300$ bits onward.

Let $\Pi$ denote the independence copula and $M,W$ the upper and lower Fréchet–Hoeffding copulas. Catalano and Lavenant (2025) conjectured that $M$ and $W$ maximize the quadratic Wasserstein distance from $\Pi$ among all bivariate copulas. We prove this conjecture and characterize all equality cases: $\mathcal W_2^2(C,\Pi)\leq 1/10$, with equality if and only if $C\in\{M,W\}$. We also determine explicitly the optimal Monge map from $\Pi$ to $M$. The proof is constructive and combines the optimal transport from independence to the diagonal, a sharp convex-order inequality for 1-Lipschitz functions, the conditional convex order, and a coupling construction based on conditional comonotonicity and the supermodular order. As a consequence, we obtain a normalized Wasserstein-based dependence measure that characterizes independence and attains its maximal value exactly for comonotone and countermonotone dependence.

We prove that a Hall $\pi$-subgroup $H$ of a finite group $G$ is normal if and only if every irreducible constituent of the permutation character $1_H^G$ has $\pi'$-degree.

This paper establishes time-uniform accuracy guarantees for deterministic square-root ensemble Kalman filters in linear–Gaussian state-space models under perfect-model dynamics. For hyperbolic, detectable systems, we prove that the ensemble means and covariances approximate their Kalman filter counterparts uniformly in time, with high probability and without inflation or resampling. The required ensemble size depends on the effective rank of the initial covariance and the dimension of the unstable subspace, rather than on the ambient state dimension. We also analyze a localized square-root ensemble Kalman filter for weakly coupled spatial systems. We show that the stabilizing Kalman covariance inherits spatial decay from the dynamics and derive accuracy bounds that separate sampling error from localization bias. For the localized filter, the required ensemble size depends on the local intrinsic dimension and only logarithmically on the number of spatial blocks, while the localization bias scales with the interaction strength. Our analysis combines stability and forgetting for possibly singular Riccati recursions, nonasymptotic covariance concentration, and perturbation estimates for localized covariance dynamics.

Let $\lambda_k$ be the $k$th eigenvalue of the Dirichlet Laplacian on an open set $\Omega\subset\mathbb R^n$ of finite positive measure. The direct individual consequence of the Berezin–Li–Yau sum inequality has leading coefficient $n/(n+2)$ relative to the Weyl term. The main contribution of this paper is a strict improvement of this coefficient. Energy orthogonality gives a frequency-dependent cap on the Fourier density of the first $k$ eigenfunctions. Combining this cap with the standard Bessel bound and a bathtub principle for the radial capacity yields \[ \lambda_k\geq c_n(2\pi)^2\omega_n^{-2/n} |\Omega|^{-2/n}k^{2/n}, \qquad \frac{n}{n+2}<c_n<1, \] for every $k\geq1$ and every $n\geq2$, without boundary regularity. The constants are characterized by explicit scalar equations; in dimension two, $c_2=0.5383068077\ldots$, giving a $7.66\%$ improvement over the individual Li–Yau coefficient. We emphasize that this improves the leading coefficient in the individual eigenvalue bound and the new constant $c_n$ is independent of the geometry and index $k$.

A set $B$ in an abelian group is a $B_h$ set if every $h$-term sum has a unique representation up to permutation; for $h=2$ these are the Sidon sets. We study a weighted removal problem for this collision-free property: if the $h$-fold sum map has small Rényi entropy loss, how much probability mass must be deleted so that the remaining support is a $B_h$ set? Two Rényi orders arise: $\alpha$ is the order at which the coarsening loss is measured, whereas $\beta$ is the order of the entropy constraint. The diagonal specialization $\beta=\alpha$ ties the two roles together. We determine the resulting stability problem on the positive $(\alpha,\beta)$-quadrant. Stability holds exactly when $\beta\le1$ and $\alpha\ge\beta$. Inside this region the optimal deletion rate is polynomial for $\beta<1$ and logarithmic on the boundary $\beta=1$, where the leading constant is exact; outside it, stability fails through two distinct mechanisms: a supercritical budget and dilution by light atoms. In both unstable regimes the limiting defect is computed exactly. The upper bounds follow from a coarsening inequality with best possible constant, which also yields an entropy-free removal theorem, a finite combinatorial consequence for moments of the representation function, and extensions to $B_h[g]$ sets. Matching constructions show that the phase boundaries and rates are sharp.

We determine the electrostatic Dirichlet-to-Neumann map of an arbitrary four-dimensional Majumdar–Papapetrou spacetime. For a minimally coupled spectator Maxwell field, the potentials of the disconnected extremal horizons may be prescribed independently, and the resulting flux charges are related by an exact capacitance matrix. If the centers have masses $M_A$ and coordinate separations $R_{AB}$, its entries are $C_{AA}=M_A+\sum_{B\ne A}M_AM_B/R_{AB}$ and $C_{AB}=-M_AM_B/R_{AB}$. The matrix is a positive diagonal term plus the weighted Laplacian of the complete graph of horizons, giving an exact common-mode and differential-mode decomposition of the field energy. The grounded Dirichlet Green function shows that a point charge partitions its flux among infinity and the horizons according to elementary harmonic measures. A direct translation of the multicenter Green function of Frolov and Zelnikov gives the diagonal completion used in their published Eq.~(68), whose component-resolved Gauss flux preserves the total horizon charge but generally transfers charge between horizons. The symmetric Green function that preserves every horizon charge instead contains the inverse of the full capacitance matrix. For a binary, the difference gives a finite, negative-semidefinite shift of the electrostatic self-energy and a corresponding exact self-force difference without an additional ultraviolet subtraction. We finally extend the response matrix, flux partition, and fixed-charge Green function to $D=n+3$ dimensions, where the graph weights acquire the universal factor $\pi^{n/2}/\Gamma(n/2)$.

This paper presents a nonlinear control law for a quadrotor unmanned aerial vehicle (UAV) under single-rotor failure that guarantees set stabilization via quasi-static feedback (QSF). Given a geometric curve in three-dimensional space, we characterize and stabilize the zero-dynamics manifold, also known as the path-following manifold, which represents all feasible motions along the path. Stabilizing this manifold ensures path-invariance: a UAV with a failed rotor initialized on the path with an appropriate orientation remains on the path for all future time. Furthermore, local exponential convergence to the manifold is guaranteed under certain conditions, implying that, under the stated assumptions, rotor failure during flight does not cause transverse deviation from the path. The proposed controller thus provides theoretical safety guarantees, which are validated through numerical experiments in the Drake physics-based simulation engine. The code is publicly available at https://gradslab.github.io/quasistatic-ftc/.

We show that the fractional illumination number of every convex body in $\mathbb{R}^d$ is at most $2^d$, with equality exactly for parallelotopes. We also prove that every such body can be covered by at most $2^d(d\log d+d\log\log d+O(d))$ smaller positive homothetic copies as $d\to\infty$, establishing the optimal exponential rate in Hadwiger's covering conjecture. The proofs use a covering measure obtained by minimizing an overlap energy and a greedy covering argument on a finite net.

Let $p_n$ be a random polynomial of degree $n$ whose roots are independent and identically distributed according to a rotationally invariant probability measure $\mu_0$ on the complex plane with finite logarithmic moment. If $k_n/n\to t\in(0,1)$, we prove that, as $n \to \infty$, the empirical zero measure of the $k_n$-th derivative of $p_n$ converges weakly in probability to a deterministic rotationally invariant probability measure. We describe the limiting measure explicitly in terms of the radial quantile function of $\mu_0$. This proves a conjecture of Hoskins and Kabluchko [Exp. Math. 32 (2023), no. 4].

The Vlasov-Maxwell system with Newtonian particle transport is linearised about the Poisson equilibrium on $\mathbb{R}^3$, with the speed of light $c$ treated as a large parameter. For uniformly controlled initial data, with transverse fields that may remain of order one, the difference between the Vlasov-Maxwell perturbation and its linearised Vlasov-Poisson counterpart is bounded uniformly in time by their initial discrepancy plus a term of order $c^{-1}$. The same estimate holds for their scattering states, and the rate in $c$ is sharp. The longitudinal dynamics are governed by the same Volterra equation as in linearised Vlasov-Poisson and undergo Landau damping. The transverse fields exhibit Klein-Gordon-type dispersion, and control of their accumulated effect along free transport yields the uniform comparison.

For Gaussian location mixtures with identity covariance, we prove that the nonparametric maximum likelihood estimator of the mixing distribution is unique for Lebesgue-almost every dataset, for every sample size and dimension. In particular, uniqueness holds almost surely whenever the joint distribution of the observations is absolutely continuous. The proof uses the finite-support theorem for Gaussian location NPMLEs and almost-everywhere differentiability of the optimal log-likelihood. Wherever this optimal value is differentiable, all NPMLEs have the same density derivatives at the observations. A minimal linear dependence among Gaussian evaluation vectors then rules out distinct solutions. An appendix extends the result to arbitrary fixed, known, observation-specific positive-definite covariances.

For any positive integer $k$, let $J_{k}$ be Jordan's totient function. We show that $J_{k}$ is not injective when $k=3,4,6$.

We prove the long-standing conjecture that, for every odd prime $p$, the only integral solutions of $a^2-2=b^p$ are $(a,b)=(\pm 1, -1)$. We also completely solve the analogous equations $y^2-D=x^p$ for $D=3$ and $D=5$ and describe a general approach for other positive squarefree values of $D \not \equiv 1 \pmod 8$. The proof refines the interpolation determinant method for linear forms in two logarithms in special cases, introducing new ideas for both the arithmetic lower bounds and the analytic upper bounds.

Ring All-Reduce is a widely used protocol for aggregating gradients across workers in large-scale distributed training. For a system with $N$ workers, its normalized per-worker communication is $2(N-1)/N$. In this work we present a communication-efficient Ring All-Reduce (CERAR) protocol for “approximate” gradient aggregation. CERAR partitions each local gradient into $c$ components and relies on linear encoding and decoding operations. It performs $L=c+N-2$ communication rounds over an $N$-worker ring, yielding normalized communication rate $1+(N-2)/c$ and normalized storage rate $1+N/c$. We present an explicit Vandermonde matrix based construction whose approximation error can be made arbitrarily small, with communication and storage rates approaching one as $c$ increases. However, this comes at the cost of ill-conditioned encoding matrices. We therefore give an alternate construction whose error is $O(\epsilon)$, while the relevant condition numbers are $O(\epsilon^{-r_\star})$, where $r_\star=\lceil c/N\rceil-1$. This motivates a condition-number-constrained optimization formulation for obtaining numerically stable practical designs. Our experiments show that, compared with the production-standard NCCL on NVIDIA A100 PCIe GPU clusters with low-bandwidth PCIe interconnect, CERAR reduces raw All-Reduce time by up to 47%. For training a 1.4-billion-parameter Pythia model, it reduces training time by about 17% for the same number of iterations while achieving essentially identical validation loss. On GPU clusters with high-bandwidth NVLink interconnects, CERAR performs worse in the All-Reduce phase and slightly worse in overall training time. However, the gap narrows for larger model sizes, suggesting that further gains may be possible with more optimized CERAR implementations.

We prove the Zygmund conjecture in all parameters: the maximal operator associated with products of cubes with side lengths $(s_1,\ldots,s_{m-1},\phi(s_1,\ldots,s_{m-1}))$, where $\phi$ is any positive coordinatewise nondecreasing function, satisfies the weak $L(\log L)^{m-2}$ estimate for every $m\geq3$. The estimate is new for $m>3$. Our approach is to prove Rey's recent conjecture on the exponential integrability of the overlap function $h_{\mathcal G}=\sum_{I\in\mathcal G}\mathbf{1}_I$, with exponent $1/(m-1)$, for sparse incomparable families $\mathcal G$ of $m$-parameter dyadic rectangles, $m\geq2$. The Zygmund conjecture, even in the continuous form above, follows by strengthening a reduction given by Rey.

We introduce and study $\mathcal{FG}$-order continuous operators between Riesz spaces, based on Tantrawan's generalized (unbounded) order convergence. This framework includes several familiar classes of operators and allows their properties to be studied in a unified setting. We establish order boundedness and lattice-theoretic results; in particular, we show that strongly order continuous operators are automatically order bounded and prove that the modulus of an order bounded $\mathcal{FG}$-order continuous operator remains $\mathcal{FG}$-order continuous under suitable assumptions. The latter result gives an affirmative answer to a previously posed problem for strongly order continuous operators. We also establish a general result ensuring classical order continuity, from which order continuity results for several familiar classes of operators follow. Furthermore, we characterize, under suitable hypotheses, when the space of order bounded $\mathcal{FG}$-order continuous operators is a band. Finally, we prove an extension theorem for positive $\mathcal{FG}$-order continuous operators, providing a counterpart of Veksler's extension theorem in this framework.

A set pair system $\{(A_i,B_i)\}_{i=1}^m$ is $1$-cross intersecting if $|A_i \cap B_i|=0$ for all $i$ and $|A_i \cap B_j| = 1$ whenever $i \neq j$. Let $m(a,b,1)$ denote the maximum size $m$ of a $1$-cross intersecting set pair system $\{(A_i,B_i)\}_{i=1}^m$ where $|A_i| \leq a$ and $|B_i| \leq b$ for all $i$. We prove a conjecture of Füredi, Gyárfás, and Király [Combin. Probab. Comput. 32 (2023)] that asserts $m(n,n,1)/\binom{2n}{n} \to 0$ as $n \to \infty$.

Let $F$ be a singular fibre of a relatively minimal complex elliptic fibration with smooth total space, and let $\Omega$ be a nonvanishing holomorphic two-form near $F$. We show that a small neighbourhood of $F$ is a Weinstein domain for $\mathrm{Re}\,\Omega$ whose completion is a Legendrian surgery, with cocores obtained by completing holomorphic disks transverse to the components of $F$. For every coefficient field and every multiplicative bulk class, we compute the wrapped Floer cohomology of these cocores and prove that it is concentrated in degree zero. The cocores generate, so the bulk-deformed wrapped Fukaya category is equivalent to the category of perfect modules over an explicit algebra: a multiplicative preprojective algebra of affine type for the normal crossing fibres, and a quiver algebra with relations for types $II$, $III$ and $IV$. Applications include formality of the affine plumbing dg algebras; mirrors given by resolved affine surfaces at every classical bulk class for affine D, E and types II, III, IV; and mirrors given by quotient stacks of algebraic tori at root-of-unity bulk classes for the four affine stars.

We classify, up to quasi-isometry, the large-scale geometry of Galton–Watson trees for every finitely supported offspring distribution. Apart from the trivial finite diameter regimes, we condition on infinite diameter. We find that the remaining classes are the ray class, the full tree class (which includes the binary tree), one chain class $(\mathrm{C}_\Lambda)$ for every possible branching semigroup $\Lambda$, and the bushy class. Two independent trees almost surely admit a root-preserving quasi-isometry when their offspring distributions belong to the same class and are almost surely not quasi-isometric when they belong to different classes. Any two survival-conditioned supercritical realisations with finitely supported offspring laws nevertheless a.s.~admit quasi-isometric embeddings in both directions. We prove that the class of a realisation depends only on the support of the offspring distribution, not its specific distribution. For offspring distributions supported on $\{1,2\}$, we additionally obtain an explicit exponential tail bound for the probability of non-existence of a root-preserving $D$-quasi-isometry. The classification also implies that the corresponding random Cantor boundaries are almost surely quasisymmetrically equivalent. Conditioned on nonextinction, this applies to strongly separated fractal percolation, even when the underlying self-similar iterated function systems and retention parameters differ. We also classify two families of trees with continuous random branching times. Our proofs use new automorphism-matching theorems for random graph labellings of trees, based on contraction estimates for mismatch potentials. These matching results for Markov labellings on the binary tree may be of independent interest. The quasi-isometry classification, embeddability, and matching theorems are formally verified in Lean.