Browse

All works

Browse the public Hexagon catalog.

Newest works

127 works

math.FA — Functional Analysis

Noncommutative Buzano-Dragomir Inequality and Applications

Contributed by K. MAHESH KRISHNA

Dragomir [\textit{Bull. Aust. Math. Soc., 2016}] showed that the Buzano inequality holds for orthogonal projections on Hilbert spaces. Dragomir [\textit{Linear Multilinear Algebra, 2016}] also derived the most general form of the Buzano inequality for bounded linear operators on Hilbert spaces. We show that Dragomir result extends to adjointable morphisms on Hilbert C*-modules. Using this generalization, we derive bounds for the roots of polynomials over commutative unital C*-algebras. We formulate the notion of noncommutative numerical range and derive numerical radius bounds for self-adjoint morphisms on Hilbert C*-modules over unital C*-algebras. We formulate several open problems, including the noncommutative Toeplitz-Hausdorff, von Neumann inequality, Ando inequality, Berger power dilation, Kittaneh inequality, Crouzeix problems.

Primarily human-written textHuman understanding: all partsBuzano InequalityCrouzeix inequality.Hilbert C*-modulesNumerical radiusPolynomial roots

math.AG — Algebraic Geometry

Constant-Time O(1) AST Reduction and Native Delegate Compilation in RICIS-III

Contributed by Дмитрий Алейников

Traditional Computer Algebra Systems (CAS) and dynamic expression interpreters evaluate critical points and mathematical singularities via runtime limit approximations, Taylor series expansions, or recursive L'Hôpital routines. These procedures incur an unresolvable computational bottleneck: dynamic tree-traversal complexity of O(N) alongside runtime branching hazards and undefined IEEE-754 states (NaN, division-by-zero traps). This paper presents a formal engineering proof of how the Recursive Indexed Calculus of Identity and Singularity (RICIS-III v7.9) enables strict constant-time O(1) symbolic Abstract Syntax Tree (AST) reduction and native machine delegate compilation. By enforcing Absolute Continuity (L₀), the Identity Principle (L₁), Safety Protocols (SP₁–SP₅), Protocol P₁ (direct structural evaluation substituting lim(x→a) with x=a), and the geometric realization of Axiom A₆ (S_F ⊠ I_G → R(F,G) →_μ F · G), all indeterminate nodes are eliminated during symbolic pre-compilation. The resulting pruned AST compiles into straight-line native execution blocks (such as .NET CLR dynamic delegates or LLVM IR) operating in deterministic O(1) clock cycles per tick with zero runtime branching.

Primarily human-written textHuman understanding: all parts

math.RT — Representation Theory

A note on counterexamples to homological conjectures

Contributed by 琪越 唐

Building on the constructions of OpenAI, we extend these constructions to any base field containing an element of infinite multiplicative order. Over each such field, we obtain finite-dimensional algebras giving counterexamples to both Tachikawa conjectures, the Auslander–Reiten conjecture, the Gorenstein-projective conjecture, the Nakayama, generalized Nakayama, and strong Nakayama conjectures, the Auslander–Gorenstein conjecture, the little and big finitistic dimension conjectures, and the Wakamatsu tilting conjecture.

A mix of human-written and AI-generated textHuman understanding: no partsRepresentation theory

math.RT — Representation Theory

A note of refinements to an algebra of infinite little finitistic dimension

Contributed by 琪越 唐

Building on OpenAI’s An algebra of infinite little finitistic dimension, we simplify the exposition and extend the construction to every field. 2026/10/10:We have added formal verification:https://github.com/tqyqiqi1509/Note198-formalization

A mix of human-written and AI-generated textHuman understanding: no partsRepresentation theory

math.AT — Algebraic Topology

Weak chromatic splitting fails at n = p for every odd prime p

Contributed by Agnes Beaudry, Tomer Schlank

We prove that for every odd prime pp there is a height nn for which the map $L_{n-1}S_p \to L_{n-1}\L_{K(n)}S_p$ is not injective on homotopy groups, hence not the inclusion of a wedge summand. In particular, for such pairs (n,p)(n,p) the weak chromatic splitting conjecture is false. More precisely, we prove the conjecture fails for (n,p)=(3,3)(n,p) = (3,3) and for all pairs (n,p)(n,p) with p≤n<2(p−1)p \le n < \sqrt{2}(p-1). In particular, the conjecture fails for (n,p)=(p,p)(n,p) = (p,p) for every odd prime pp. This disproof was produced autonomously by Claude in a session working on Freyd's generating hypothesis with no human in the loop. This note is a human write-up of the disproof. We did not contribute any ideas.

Primarily human-written textHuman understanding: all parts

math.NT — Number Theory

Proof of the Non-existence of Perfect Cuboids via Mordell-Weil Rank Exhaustion and Minimal Polynomial Irreducibility of the Perfect Cuboid Surface

Contributed by Jonathan 𝑓(n) Reed

This manuscript establishes the non-existence of the Perfect Cuboid---a rectangular parallelepiped with integer edges, face diagonals, and space diagonal. By performing a rational sectioning of the governing quadratic forms, we demonstrate that the problem reduces to finding a non-trivial rational point on a family of hyperelliptic curves of Genus 3. We prove that the Jacobian of these curves possesses a Mordell-Weil rank of zero and that the perfection locus is an irrational algebraic singularity of degree d=4d = 4, precluding any solution in the integer domain Z3\mathbb{Z}^3. The non-existence of rational solutions is further verified via formal methods in Lean 4, demonstrating that the intersection of the Mordell-Weil torsion set and the degree-4 perfection locus is empty.

A mix of human-written and AI-generated textHuman understanding: all parts2-DescentEuler BrickHyperelliptic CurvesInteractive Theorem ProvingJacobian VarietyLean 4Mordell-Weil RankPerfect CuboidQuadratic Residueformal verification

math.NT — Number Theory

The generalized Fermat equation x3+y3=znx^3+y^3=z^n

Contributed by Manvir Jaswal

We prove that the equations x3+y3=znx^3+y^3=z^n and x3+y3=3znx^3+y^3=3z^n have no solution in coprime nonzero integers for any n≥3n\ge3. For the first equation the open cases were prime exponents p≡1(mod3)p\equiv1\pmod 3 above 10910^9 outside a set of congruence classes treated by Chen and Siksek; in these cases the solution 13+23=321^3+2^3=3^2 blocks the modular method. We replace Kraus's Frey curve by a hypergeometric motive of rank three over K=Q(−3)K=\mathbb{Q}(\sqrt{-3}), whose parameter at a solution is 33-adically close enough to a point of maximally unipotent monodromy for inertia at −3\sqrt{-3} to act unipotently; the parameter of 13+23=321^3+2^3=3^2 is not. By a theorem of Calegari, Emerton and Gee, the mod pp representation of the fiber, twisted by a cubic character, is the reduction of a member of a compatible system of minimal ramification, and we show that the member at a prime above 33 is irreducible and ordinary at −3\sqrt{-3}. Ramification and unconditional discriminant bounds show that its reductions have trivial semisimplification, and as the Galois group of the maximal pro-33 extension of KK unramified outside −3\sqrt{-3} is generated by one inertia group, the member stabilizes its ordinary line, a contradiction. For x3+y3=3znx^3+y^3=3z^n the same argument also works at the primes p≡2(mod3)p\equiv2\pmod3, which are inert in KK, and Frey curves and descents treat the remaining exponents.

Primarily AI-generated textHuman understanding: no partsFrey representationscompatible systems of Galois representationsgeneralized Fermat equationhypergeometric motivesmodular method

math.NT — Number Theory

Improved sum-difference inequalities in abelian groups

Contributed by Logan Kleinwaks

For all finite subsets X,YX,Y of an abelian group, we prove \[ |X-Y|\le |X+Y|^{\lamI},\qquad \lamI=\frac{9451\e-3286}{5378\e+787}=1.454277448906\ldots, \] improving the classical exponent 3/23/2. We also prove that a universal two-set exponent λ\lambda over the integers implies an upper bound 2−1/λ2-1/\lambda for the Gyarmati--Hennecart--Ruzsa constant, the supremum θ∗\theta^* of tt such that ∣A−B∣≫∣A+B∣t|A-B|\gg|A+B|^t and ∣A+B∣≪∣A∣|A+B|\ll|A| for arbitrarily large A,B⊂ZA,B\subset\Z. Consequently, \[ \theta^*\le\frac{13524\e-7359}{9451\e-3286}=1.312373302115\ldots, \] improving their bound 4/34/3. The first argument combines a coupling with distinct differences, entropy inequalities for independent sums, a finite certificate using non-Shannon inequalities, and an explicit limiting certificate with weights $\int_0^1t(1-t)^k\e^t\,dt$. The transfer uses localisation and the Pl\"unnecke--Ruzsa inequality over a sequence of scales. The proofs are formalised in Lean~4.

Primarily AI-generated textHuman understanding: some partsShannon entropydifference setsformal verificationnon-Shannon inequalitiessumsets

math.OA — Operator Algebras

Poisson boundaries of type III factors and the relative bicentralizer conjecture

Contributed by Shuoxing Zhou

We develop the Poisson boundary theory for general von Neumann algebras with separable preduals. As applications, we generalize and give new proofs of the results on the weak Dixmier property for inclusions with expectations or operator-valued weights \cite{Pop99,Mar19,Iso25}. We also prove that every continuous factor admits irreducible embeddings into the hyperfinite factors of type IIIλ\mathrm{III}_\lambda, 0<λ≤10<\lambda\leq1, and into some hyperfinite factor of type III0\mathrm{III}_0. Finally, using the Poisson boundary techniques developed above, we prove that for every inclusion with faithful normal conditional expectation M⊂NM\subset N, M⊂c(N)M\subset c(N) has the weak Dixmier property. By Marrakchi's characterization \cite[Theorem~D]{Ma25}, this gives the relative bicentralizer conjecture for von Neumann algebras with separable preduals.

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

math.QA — Quantum Algebra

Strongly positive bases and quantum greedy expansions

Contributed by 琪越 唐

We prove that every element of a strongly positive basis of a coefficient-free rank-two quantum cluster algebra has nonnegative Laurent-polynomial coefficients in the quantum greedy basis. This establishes the strongly positive basis assertion of Conjecture 16 of Lee, Li, Rupel, and Zelevinsky. We also give a counterexample to their Conjecture 13(b).

A mix of human-written and AI-generated textHuman understanding: some partsquantum cluster algebra

math.RA — Rings and Algebras

Algebraic dependence of cluster X-variables

Contributed by 琪越 唐

We prove that, over any field and with algebraically independent initial seed coordinates, two cluster XX-variables are algebraically dependent if and only if they are equal or reciprocal. In characteristic zero, this is equivalent to the vanishing of the wedge product of their differentials.

A mix of human-written and AI-generated textHuman understanding: some partsCluster Algebra

math.AG — Algebraic Geometry

Crystalline and infinitesimal Poisson stacks

Contributed by Aleksandr Karapetyan

A systematic way to construct Poisson brackets on moduli stacks in algebraic geometry is through shifted Poisson structures on derived stacks. The standard construction, due to Calaque--Pantev--To{\"e}n--Vaqui{\'e}--Vezzosi, imports Gelfand--Kazhdan formal geometry to derived stacks in order to establish formal descent for polyvector fields. The result is a graded Lie algebra which we call the ``crystalline'' polyvector fields on a derived stack. Using instead the formal derived geometry machinery of Gaitsgory--Rozenblyum, we construct a graded Lie algebra of ``infinitesimal'' polyvector fields which has a direct geometric interpretation: it governs deformations of the formal shifted cotangent stack, together with its canonical exact symplectic form. Our main result is an equivalence between crystalline and infinitesimal polyvector fields on a derived stack as graded Lie algebra objects, providing a deformation-theoretic perspective on the graded Lie algebra constructed by Calaque--Pantev--To{\"e}n--Vaqui{\'e}--Vezzosi.

Primarily human-written textHuman understanding: all partsDerived algebraic geometrydeformation theoryderived algebrainfinity-categoriesshifted Poisson structuresshifted symplectic structures

math.QA — Quantum Algebra

Theta Bases for Rank-Two Quantum Cluster Algebras of Geometric Type

Contributed by 琪越 唐

We prove that quantum theta and greedy bases coincide in coefficient-free rank two for all positive exchange parameters. Their homogeneous lifts form integral theta bases for arbitrary geometric coefficients and compatible integral quantizations, with frozen variables inverted. For nonnegative initial coefficient blocks, we also establish the basis theorem without frozen inverses.

Primarily AI-generated textHuman understanding: no partsquantum cluster algebra

math.CO — Combinatorics

The Anti-Arithmetic Product of Symmetric Functions

Contributed by Darij Grinberg

The \emph{arithmetic product} ⊡\boxdot is a bilinear operation on the ring of symmetric functions over Q\mathbb Q defined by \[ p_\lambda \ \boxdot\ p_\mu = \prod_{i,j}p_{\operatorname{lcm}(\lambda_i,\mu_j)}^{\gcd(\lambda_i,\mu_j)} \] on the power-sum basis (pλ)(p_\lambda). It is known that this operation preserves the subring SymmZ\mathbf{Symm}_{\mathbb Z} of symmetric functions with integer coefficients, and is Schur-positive on pairs of Schur functions. Indeed, it corresponds to induction of representations from Sn×SmS_n \times S_m to SnmS_{nm}. In this work, we consider the \emph{anti-arithmetic product} ♢\diamondsuit, which is defined by the same formula but with gcd⁡\gcd and lcm⁡\operatorname{lcm} interchanged. We show that it, too, preserves SymmZ\mathbf{Symm}_{\mathbb Z}, even though it lacks the Schur positivity property. This was conjectured on MathOverflow in 2014. Our method is a more intricate variant of the representation-theoretical interpretation of ⊡\boxdot. The anti-arithmetic product does not correspond to an operation on actual representations; but its adjoint can still be described as a map on characters, which (as we show) is a λ\lambda-ring morphism from the character ring of SmnS_{mn} to that of Sm×SnS_m \times S_n. Now, a 1975 theorem of Boorman shows that the representation ring of SnS_n is generated by the natural permutation representation Mn=QnM_n = \mathbb Q^n as a λ\lambda-ring. Thus, the proof of integrality boils down to only computing the image of MmnM_{mn} under this adjoint, which can be done using M\"obius inversion in the representation ring. This work is aimed at readers familiar with representation rings and the representation theory of symmetric groups. No prior knowledge of λ\lambda-rings is presumed. Three self-contained proofs of Boorman's theorem are given in the appendices, two of them lifting the theorem to the noncommutative symmetric functions (or Solomon's descent algebra), recovering a result of Schocker.

A mix of human-written and AI-generated textHuman understanding: all partsSpecht modulesdescent algebralambda-ringsnoncommutative symmetric functionssymmetric functionssymmetric group representations

math.RT — Representation Theory

Reflexive equivalence and reflexive-minimal algebras

Contributed by Haruhisa Enomoto

Let AA be a finite-dimensional algebra over a field. A finite-dimensional algebra BB over the same field is called reflexively equivalent to AA if their categories of reflexive modules are equivalent. We prove that there is a basic algebra Amin⁡A_{\min}, unique up to isomorphism, such that BB is reflexively equivalent to AA if and only if B≅End⁡Amin⁡(Amin⁡⊕X)B\cong\operatorname{End}_{A_{\min}}(A_{\min}\oplus X) for some reflexive Amin⁡A_{\min}-module XX. Moreover, we compute Amin⁡A_{\min} explicitly. We extend these results to module-finite algebras over henselian local rings of dimension at most one under a dominant dimension condition at minimal primes. We also introduce reflexive modules over additive categories and prove that taking reflexive modules is idempotent: the reflexive modules over the category of reflexive modules form an equivalent category. As an application, we show that reflexive equivalence classes of algebras with finitely many indecomposable reflexive modules correspond bijectively to Morita equivalence classes of algebras whose reflexive modules are projective.

Primarily AI-generated textHuman understanding: some parts

math.QA — Quantum Algebra

Minimality of the Rank-Two Quantum Greedy Basis

Contributed by 琪越 唐

We prove that the rank-two quantum greedy basis is the least strongly positive basis when b | c or c | b, resolving Conjecture 14 of Lee–Li–Rupel–Zelevinsky. Every strongly positive basis has nonnegative expansion coefficients in the greedy basis.

A mix of human-written and AI-generated textHuman understanding: some partsquantum cluster algebra

math.QA — Quantum Algebra

A Finite Polyhedral Construction of the Rank-Two Quantum Greedy Basis

Contributed by 琪越 唐

We give a finite polyhedral construction of the quantum greedy basis for coefficient-free rank-two quantum cluster algebras. The construction specializes coefficientwise to the classical polyhedral construction at v = 1. Corresponding classical and quantum coefficients and auxiliary margins have identical zero sets, and the Newton polytopes are affine images of the classical carriers.

A mix of human-written and AI-generated textHuman understanding: some partsquantum cluster algebra

math.OC — Optimization and Control

Continuity of solutions to abstract linear control systems

Contributed by Frédéric Marbach

It has long been known that the solutions to abstract linear control systems are continuous in time for controls in LpL^p with 1≤p<∞1 \le p < \infty. We prove that the same property remains valid for the endpoint case p=∞p = \infty, giving a positive answer to Weiss' 1989 Problem 2.4. The proof relies on a direct semigroup argument based on Phillips' lemma, does not require the input map to have an integral representation (which is not always the case for p=∞p = \infty), and actually entails that such systems are all of the zero-class (which fails for 1≤p<∞1 \le p < \infty).

Primarily AI-generated textHuman understanding: all partsabstract linear control systems

math.PR — Probability

The Negative Spherical Perceptron: Capacity, Isostatic Jamming, and Full Replica Symmetry Breaking

Contributed by P. M. Aronow, Patrick Lopatto

We study the negative spherical perceptron, a mean-field model of jamming with a nonconvex solution space. We establish the Parisi formula for its free energy and identify the capacity for every constraint density α>2\alpha>2. We also show that the jamming point is isostatic: optimal configurations have exactly NN contacts. For α\alpha slightly above two, we show that replica symmetry is lost at the de Almeida–Thouless margin through a continuous transition to full replica symmetry breaking. Further, we show that Gardner's formula overestimates the capacity by order (α−2)3(\alpha-2)^3.

Primarily AI-generated textHuman understanding: some partsperceptronspin glass

math.MG — Metric Geometry

A Fourier Consequence for Lattice Kissing Numbers and Average Contacts

Contributed by Scott Kominers

We deduce a new asymptotic upper bound Klat(n)≤(2e/π+o(1))nK_{\mathrm{lat}}(n)\leq\left(\sqrt{2e/\pi}+o(1)\right)^n on the maximal lattice kissing number Klat(n)K_{\mathrm{lat}}(n) in dimension nn, using the explicit auxiliary functions constructed in OpenAI's "Ten Advances" preprint. The same bound holds for the average contact degree of a finite packing of congruent balls. The bound's base-22 exponential rate rounds to 0.39560.3956, matching the value extrapolated empirically by Afkhami-Jeddi, Cohn, Hartman, de Laat, and Tajdini in 2020.

A mix of human-written and AI-generated textHuman understanding: all partsContact numbersDiscrete geometryEuclidean latticesFourier linear programming boundsGeometry of numbersKissing numbersSphere packing

math.NT — Number Theory

On the ternary pentagonal numbers conjecture

Contributed by Glenn Bruda

Communicated by Guy in 1994, the ternary pentagonal numbers conjecture of Blecksmith and Selfridge asserts that every integer larger than 3306633066 is the sum of three positive pentagonal numbers. Prior to this note, it was even unknown whether every sufficiently large integer is the sum of three positive pentagonal numbers. We resolve this in the affirmative, using the landmark work of Duke and Schulze-Pillot on ternary quadratic forms to handle all sufficiently large integers nn with v3(24n+3)≤8v_3(24n+3)\leq8, and present an explicit lift to handle the nn with v3(24n+3)≥9v_3(24n+3)\geq9.

Primarily human-written textHuman understanding: all partsPentagonal numbersalmost universalityternary quadratic forms

math.NT — Number Theory

Linnik's constant is at most 3.993.99

Contributed by Eric Naslund

Let P(a,q)P(a,q) denote the least prime congruent to aa modulo qq, where (a,q)=1(a,q)=1. We give a computer-assisted proof that P(a,q)≪q3.99P(a,q)\ll q^{3.99}, improving the exponent 55 of Xylouris. More precisely, P(a,q)<q3.99P(a,q)<q^{3.99} for every sufficiently large qq, uniformly in aa. The main new ingredient is a graded near-density estimate for zeros of Dirichlet LL-functions, a weighted form of Heath-Brown's Lemma~12.1 of the kind he asked for in 1992. We combine it with the zero-location estimates and far-density method of Heath-Brown and Xylouris. The second novelty is the scale of the case analysis. Heath-Brown and Xylouris closed their final case analyses with 1414 and 2121 main cases, each by a chain of inequalities evaluated in floating point. In this paper, with the help of advanced AI models, we can push this much further. The middle range of the first zero is divided into 44534453 root cases and 47884788 terminal cases, each closed by its own linear program. On 4,196,8794{,}196{,}879 threshold boxes these programs give 29,397,33629{,}397{,}336 linear relaxations, and exact integer certificates for all of them bound the normalized zero sum strictly below~11. Exceptional zeros and the remaining exterior range are treated separately. This case analysis is a kind of systematic brute force enabled by AI: an analysis of this size, with parameters tuned to each case, would be very laborious or nearly impossible to carry out by hand, and it lets the new estimate be applied separately in each case. The near-density lemma, certificate soundness, and a conditional passage from a certified case to a prime are formalized in Lean, assuming published analytic inputs and specified facts about zeros (PALOMAR-2026-10-01-000020 v1).

Primarily AI-generated textHuman understanding: some parts

math.CO — Combinatorics

An Exponent of 1.043 for the Unit Distance Problem

Contributed by Eric Naslund

Let u(U)u(U) count the unordered pairs at distance one in a finite planar set UU. We construct finite sets UjU_j with ∣Uj∣→∞|U_j|\to\infty and u(Uj)/∣Uj∣1.043171→∞u(U_j)/|U_j|^{1.043171}\to\infty. The largest exponent previously claimed, apart from preliminary versions of the present work, is 1.03581.0358, in the author's unpublished manuscript. The method is the number-field construction of OpenAI and Sawin. Here unit distances come from elements of relative norm one in quadratic extensions K/FK/F in which FF has both real and complex places, and the fields come from an infinite pro-22 tower over $\Q(\sqrt{241})$, ramified only above 22, 33 and 55, with Frobenius conditions at the two primes above 2929 and at one prime above 4141. The relative zeta value is bounded through the dihedral quotients of the tower group: the tower group has 2727 quotients isomorphic to the dihedral group of order~88; fifteen of them detect, by a census, the residue degree of the primes that split completely in the Kummer field up to norm 4⋅10134\cdot10^{13}, and seven of them generate a field EW′′E_{W''} of degree 81928192 contained in every field of the tower. We write ζEW′′\zeta_{E_{W''}} as a product of LL-functions of degrees 22, 44 and~88, evaluate the 576576 of degrees 44 and 88 rigorously at 2121 real points near~11, and combine the values through a kernel inequality with coefficients of both signs. Finite facts and numerical inequalities are certified by exact computation and interval arithmetic. Partial formalization PALOMAR-2026-10-01-000018 v2

Primarily AI-generated textHuman understanding: some parts

math.CO — Combinatorics

Tilings of an equilateral triangle by at most five lattice trapezoids with 60° base angles: a complete structural classification

Contributed by Gonzalo Barria

We study tilings of an equilateral triangle of side n in the triangular grid by k lattice trapezoids with base angles 60°, the objects behind the OEIS sequences A389392 (k = 4) and A391498 (k = 5). We prove two angle identities valid for every such tiling and a lemma relating the number of boundary vertices to the number of pieces having a side on the boundary. With these tools we show that there are exactly 1, 2 and 13 combinatorial types of tilings for k = 3, 4, 5. For k = 3 every tiling is a pinwheel. For k = 4 every tiling belongs to one of the two categories used in A389392, a fact that had previously been taken for granted. For k = 5 the thirteen types refine the eight categories of A391498; in three of them a piece has no side on the boundary. As a consistency check, the volumes of the parameter polytopes together with the generic multiplicities reproduce the leading coefficient 7/36 of the conjectured quasi-polynomial for A391498. All lemmas were checked against an exhaustive enumeration of the tilings with pairwise distinct pieces for n ≤ 15. Finally, the classification turns the thirteen types into eight explicit families of sets of shapes, and an inclusion–exclusion over them reduces the conjectured generating function of A391498 to twelve elementary counting statements, and we settle all twelve: the resulting closed formula reproduces the sequence for every n ≤ 127.

A mix of human-written and AI-generated textHuman understanding: all partsOEIS A391498lattice trapezoidsquasi-polynomialrational generating functiontilings of an equilateral triangle

math.PR — Probability

On the escape rate of favorite sites of planar random walks

Contributed by Heng Ma

For planar simple random walk, the favorite sites at time nn are the sites whose local time at time nn is maximal. We prove that, almost surely, for every γ>1/2\gamma>1/2 and every c>0c>0, all favorite sites lie outside the ball centered at the origin with radius cn/(log⁡n)γc\sqrt n/(\log n)^\gamma for all sufficiently large nn. At the critical exponent γ=1/2\gamma=1/2, almost surely, for every c>0c>0, the entire favorite sites lies within distance cn/log⁡nc\sqrt{n/\log n} of the origin infinitely often.

Primarily AI-generated textHuman understanding: no parts

math.MG — Metric Geometry

A generalized Gerver sofa for angled corridors

Contributed by Henrik Schou Guttesen

The moving sofa problem asks for the maximal area of a two-dimensional object capable of being moved through a right-angled corridor of unit width. J. L. Gerver constructed a sofa of area 2.2195…2.2195\dots, which was only recently proven to be optimal by J. Baek. Here, I consider the moving sofa problem in an angled corridor, CφC_{\varphi}, of unit width for turn angles 0<φ≤π20 < \varphi \le \frac{\pi}{2}. I first generalize Hammersley's arguments to devise simple analytical lower and upper area bounds for all 0<φ≤π20 < \varphi \le \frac{\pi}{2}. ChatGPT-6 Astra (Codex) is prompted to derive a generalized Gerver sofa parametrized by φ\varphi. The generalized Gerver sofa area is non-analytic at the unique root φ∗∈(0,π/2)\varphi_*\in(0,\pi/2) of exp⁡(φ∗cot⁡φ∗)=1+2cos⁡φ∗−cos⁡2φ∗\exp({\varphi_*\cot\varphi_*}) = 1+2\cos\varphi_*-\cos^2\varphi_*. For turn angles smaller than φ∗\varphi_* a closed-form expression of the sofa area is obtained. The generalized Gerver sofa is conjectured to be the solution to the moving sofa problem for turn angles 0<φ≤π20 < \varphi \le \frac{\pi}{2}.

A mix of human-written and AI-generated textHuman understanding: some partsGeometryGerver-sofamoving-sofa-problemrecreational-math

math.DG — Differential Geometry

A contractible open four-manifold with a complete metric of uniformly positive scalar curvature

Contributed by Jiangcheng You, Heng Zhang

We construct a smooth contractible open four-manifold that is not homeomorphic to R4\R^4 and admits a complete Riemannian metric with scalar curvature at least one. This gives a negative answer to a question raised by Chang--Weinberger--Yu and Chodosh--M\'aximo--Mukherjee.

A mix of human-written and AI-generated textHuman understanding: all partsBaumslag–Solitar groupsGromov–Lawson surgerycontractible four-manifoldsgeometric topologyopen four-manifoldspositive scalar curvaturetopology at infinity

math.LO — Logic

Arrow and Gibbard Satterthwaite Theorems in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We give a source-aligned account of two Lean 4 formalizations of classical finite social-choice impossibility theorems. For a finite nonempty electorate and a finite alternative set containing three distinct alternatives, Arrow’s theorem derives dictatorship from unanimity and independence of irrelevant alternatives. Its proof expands a weakly decisive coalition from one ordered pair to all pairs, then contracts decisive coalitions to a singleton. The Gibbard–Satterthwaite development proves that every onto strategy-proof choice function on the unrestricted strict-ranking domain is dictatorial by constructing a social welfare function and applying that Arrow implementation. We explain the essential construction in full: top-two profiles define pairwise comparisons; strategy-proof monotonicity and three-top profiles establish a strict total order; predecessor counts provide injective natural-number ranks. Exact hypotheses, vendored dependencies, pinned source identities, prior formalizations, and the distinction between historical registry verification and the present source audit are recorded. The contribution is an exposition and audit of reusable formalization artifacts, not a new social-choice theorem or a claim of first formalization.

Primarily AI-generated textHuman understanding: some parts

math.LO — Logic

A Lean Formalization of the Shapley Value Characterization for Finite Cooperative Games

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We describe a Lean 4 formalization of the standard four-axiom characterization of the Shapley value for finite transferable-utility cooperative games. Games are arbitrary real-valued characteristic functions normalized at the empty coalition; the player type may itself be empty. The factorial coalition formula is proved efficient, symmetric for interchangeable players, null-player respecting, and additive. Uniqueness follows from the values of arbitrarily scaled unanimity games and an explicit Boolean-lattice Möbius decomposition. The proof requires neither a real-homogeneity axiom nor a continuity assumption on competing allocation rules. We explain the finite-sum arguments, the precise Lean statements, the separation between the registry’s challenge and implemented solution, and the historical verification evidence for the pinned source revision. The contribution is an auditable exposition of an existing formalization of classical mathematics, with no claim of new mathematics or formalization priority.

Primarily AI-generated textHuman understanding: some parts

math.LO — Logic

Nash Bargaining Characterization in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We describe a Lean 4 formalization of the classical two-person Nash bargaining characterization. A bargaining problem consists of a compact convex subset of the real plane, a feasible disagreement point, and a feasible outcome strictly improving both utilities. The Nash product is maximized over the individually rational part of that set. The development proves existence and uniqueness of the maximizer, verifies Pareto optimality, symmetry, positive affine invariance, and independence of irrelevant alternatives, and proves that these four axioms characterize the maximizer among feasible selection rules. We explain the algebraic midpoint proof of uniqueness and the normalization argument, including an explicit small-step tangent bound and a compact symmetric enlargement. The exposition is tied to an immutable repository snapshot and four declarations registered in Palomar. Historical registry verification is distinguished from the source inspection used to prepare this manuscript. The contribution is a documented formalization of established mathematics; no new bargaining theorem or formalization-priority claim is made.

Primarily AI-generated textHuman understanding: some parts

math.LO — Logic

Finite Nash Equilibria and Dependent Mixed Strategies in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We present two complementary Lean 4 developments of finite Nash equilibrium. The pure-game layer uses player-specific legal action sets, distinguishes one-way generalized ordinal potentials from bidirectional ordinal potentials, and proves potential-maximizer certificates, a local-maximum characterization, absence of strict-improvement cycles, and weak acyclicity. The mixed-game layers use either a common finite action type or a dependent finite action type for each player. They prove payoff equalization on equilibrium supports, Dirac payoff identities, continuity of the normalized payoff-excess map, and mixed equilibrium existence. We explain the finite-sum and sum-of-squares arguments and the reindexing bridge to an attributed, proved product-of-simplices Brouwer theorem. An additional legal-subtype interface is separated from the declarations selected by the registry comparator. The account is tied to two immutable source snapshots and dated verification records. It documents established mathematics and its formal interfaces, without claiming a new equilibrium theorem or formalization priority.

Primarily AI-generated textHuman understanding: some partsBrouwer fixed pointLean 4MathlibNash equilibriumdependent action typesmixed strategiespotential games

math.OC — Optimization and Control

A Finite Coordinate Reduction for Approachability Loss in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We explain a Lean 4 development of a finite-coordinate loss-preserving construction motivated by Theorem 4 of Dann, Mansour, Mohri, Schneider, and Sivan. Nonempty finite constraint and action index sets give a joint probability simplex with a canonical action marginal. For each mixed constraint, a linear comparator adds its outer product with that marginal. The comparator has mass two and leaves the legal action set. A one-step pairing identity yields exact equality of finite-horizon approachability and comparator-regret objectives, with explicit anchored lifts and marginal decoders. The development also proves a row-wise decomposition with at most one rank-one term per constraint index. We describe the twelve declarations registered in Palomar and their historical verification provenance. The scope is deliberately narrow: the constraint simplex parametrizes coordinate functions, both causal strategy translations observe original loss histories, and the comparators have no fixed point in the joint simplex. Thus the checked statements establish finite algebraic loss preservation; they do not certify the full published reduction, its fixed-point-defined improper class, reduced-loss-only feedback, or asymptotic rate theory. No mathematical novelty or formalization priority is claimed.

Primarily AI-generated textHuman understanding: some parts

math.GR — Group Theory

An Executable Stallings Recognizer for Finite Generating Lists in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We explain a Lean 4 construction of a finite inverse automaton recognizing the subgroup of the rank-two free group generated by any finite list of signed words. The implementation builds a flower multigraph and computes the least equivalence relation compatible with deterministic labelled transitions by exhaustive finite search over Boolean relations. Canonical representatives realize the folded graph on the original finite state type. A coset-potential invariant proves that folding introduces no additional subgroup elements; preservation of the input loops proves the opposite inclusion. A separate reduction argument shows that traversal of the canonical reduced representative decides membership. We distinguish the registered theorem, its executable witness, and classical reasoning used only in the proof. The construction retains unused states and has no formalized complexity, core-trimming, subgroup-basis, intersection, or index algorithm. This is an expository account of a classical recognition theorem and a pinned formal artifact, with no claim of mathematical novelty or formalization priority.

Primarily AI-generated textHuman understanding: some partsLean 4MathlibStallings foldingfinite inverse automatafree groupssubgroup membership

math.AC — Commutative Algebra

Prime-Generated Localization Descent for Unique Factorization in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

We give a source-grounded exposition of a Lean 4 formalization of prime-generated Nagata factoriality descent. A commutative noetherian integral domain is a unique factorization domain if a localization is a unique factorization domain and every denominator is exactly a finite product of prime elements belonging to the denominator submonoid. The formal statement works with an arbitrary algebra carrying Mathlib’s IsLocalization structure. We explain the two cases for an irreducible element, the multiset cancellation and splitting arguments, and the corollary for submonoids generated by arbitrary sets of primes. A registered polynomial corollary illustrates reuse of the descent package; its Laurent-polynomial premise is proved using Mathlib’s existing polynomial UFD instance, a dependency made explicit here. The exposition is tied to the registered source and dependency pins, distinguishes historical mechanical verification from manuscript review, and situates the development relative to an earlier Lean preprint and an Isabelle/HOL formalization. No new algebraic theorem or priority claim is asserted.

Primarily AI-generated textHuman understanding: some partsLean 4MathlibNagata factorialitycommutative algebralocalizationunique factorization domains

cs.LO — Logic in Computer Science

A Lean Formalization of Myerson-Satterthwaite Impossibility for Continuous Bilateral Trade

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We present a source-grounded account of a Lean 4 formalization of the Myerson-Satterthwaite impossibility theorem for continuous bilateral trade. Buyer values and seller costs are independent, with atomless probability measures supported on compact real intervals whose interiors overlap. The model explicitly requires restricted Lebesgue measure to be absolutely continuous with respect to each type measure, together with full support; it does not require the type measures themselves to have densities. Under allocation and transfer measurability and integrability conditions, the registered theorem excludes the simultaneous satisfaction of almost-sure ex post efficiency, Bayesian incentive compatibility at every admissible type and report, interim individual rationality, and weak ex ante budget balance. The proof derives envelope identities from incentive inequalities, identifies the efficient allocation almost everywhere, and uses a layer-cake representation to show that the required information rents strictly exceed efficient surplus. We explain the analytic steps, their Lean declarations, and the verification evidence for the exact Palomar-registered source revision. This is an exposition of a classical result and an existing formal artifact, without a claim of mathematical novelty or formalization priority.

Primarily AI-generated textHuman understanding: some parts

cs.DS — Data Structures and Algorithms

A Lean Certificate for the Single Source Unsplittable Flow Cost Counterexample

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We explain a standalone Lean 4 and Mathlib verification of the finite counterexample announced by Dmitry Rybin to the cost-preserving single-source unsplittable-flow conjecture. The instance has seven vertices, nine directed arcs, and three terminal demands. An exact rational path flow saturates every arc, has cost 58, and has largest demand 15. Exhaustive graph-path classification reduces every unsplittable routing to two choices per terminal. Three backbone-arc inequalities force any routing with load at most the fractional load plus 15 to use at least two paid routes, each costing 30. Thus every such routing costs at least 60, ruling out cost preservation even with a non-strict congestion bound. We present the numerical certificate, its graph realization, and the boundary between the pinned proved implementation and its statement-only verification interface. The contribution is an exposition of a source-based formal certificate; no new counterexample, first formalization, or general rounding algorithm is claimed.

Primarily AI-generated textHuman understanding: some partsGoemans cost conjectureLean 4MathlibRybin counterexamplefinite counterexampleformal verificationsingle-source unsplittable flow

math.AT — Algebraic Topology

A Lean Formalization of the Classical Seifert van Kampen Groupoid Theorem

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We explain a Lean 4 formalization of the classical Seifert van Kampen theorem for the full fundamental groupoid. For an arbitrary topological space covered by two open subsets, the inclusion-induced square of ordinary continuous-path fundamental groupoids is a pushout in the category of categories. Every point is retained as an object; no basepoint, connectedness, or separation hypothesis is required. The development identifies an auxiliary directed path category for the indiscrete preorder with Mathlib's fundamental groupoid through strictly inverse functors and naturality equalities. It then assembles the pushout universal property from attributed path-subdivision and homotopy-grid helpers adapted from the directed-topology formalization of Basold, Bruin, and Lawson. We describe the descent construction, its transfer to ordinary fundamental groupoids, and the statement and verification boundaries of the exact artifact registered in Palomar. This is an expository account of a classical theorem and an existing formal artifact, with no claim of mathematical novelty or formalization priority.

Primarily AI-generated textHuman understanding: some partsLean 4MathlibSeifert van Kampen theoremcategorical pushoutfundamental groupoidopen cover

cs.DS — Data Structures and Algorithms

Deferred Acceptance in Lean for Finite Strict Preference Markets

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We describe a Lean 4 development of men-proposing deferred acceptance for finite one-to-one markets with complete strict preferences and optional partners. The two sides may have different cardinalities; the principal theorems assume a nonempty receiving side. A proposal-set measure proves termination of a specified, classically chosen run. Reachability invariants establish consistency of the resulting partner maps, stability, and the fact that a rejected proposal cannot be a stable-achievable partnership. The public optimality theorem is conditional on a man receiving a partner; an internal lemma separately excludes stable-achievable partners for men unmatched at quiescence. We give mathematical proofs corresponding to the source architecture, identify the precise theorem interface, and separate fresh source inspection from the repository's reported build and axiom audit. This is an exposition of a pinned formalization of classical results, with no claim of new matching theory or priority of formalization.

Primarily AI-generated textHuman understanding: some partsGale-ShapleyLean 4deferred acceptanceformalizationstable matching

math.OC — Optimization and Control

A Lean Formalization of Roberts Theorem on Unrestricted Valuations

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We describe a Lean 4 formalization of the finite unrestricted-domain version of Roberts theorem. For finite nonempty agent and alternative types, with at least three alternatives, an onto deterministic direct-revelation mechanism that is dominant-strategy incentive compatible has an affine-maximizer choice rule. Valuations range over all real-valued profiles; the conclusion uses fixed nonnegative weights, at least one nonzero, and alternative offsets, and asserts membership in the maximizing set. The development follows the modular proof route: taxation and weak monotonicity, perturbation-based tie-breaking to strong monotonicity, no-veto range analysis, affine prices for two agents, and induction through fixed-report slices. We explain the proved tie-set transport lemma, the construction of fresh payments for the tie-broken rule, and the transfer back to arbitrary ties. A version-pinned account distinguishes the proved library from statement-only comparator placeholders and separates source inspection from executable checks. This is an exposition of a classical result and its formal artifact, with no claim of mathematical novelty or formalization priority.

Primarily AI-generated textHuman understanding: some partsLean 4Roberts theoremaffine maximizersdominant strategiesformalizationmechanism design

math.OC — Optimization and Control

Finite VCG and Groves Payments in Lean

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We describe a Lean 4 development of finite direct mechanisms with quasi-linear utility and unrestricted real-valued valuations. The Clarke pivot mechanism selects a reported-welfare maximizer and charges each agent the loss in other-agent welfare relative to its maximum over the same fixed alternative set. The development proves efficiency, dominant-strategy truthfulness, nonnegative payments and no deficit, and individual rationality under the explicit assumption that every valuation is nonnegative. It also proves that every efficient, dominant-strategy incentive-compatible mechanism on the full valuation domain has Groves-form payments, with a term independent of the paying agent's report. We explain the finite-maximization interface, the report-update invariants, and the characterization argument using outcome-forcing reports and positive perturbations. The exposition is tied to a specific source revision and separates proved implementations from statement-only comparator placeholders. These are classical mechanism-design results; no new mathematical theorem or formalization-priority claim is made.

Primarily AI-generated textHuman understanding: some partsClarke pivot paymentsGroves characterizationLean 4VCG mechanismdominant strategiesformal verification

math.OC — Optimization and Control

A Lean Formalization of Finite Zero Sum Minimax via Sion's Theorem

Contributed by Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

We describe a Lean 4 formalization of the minimax theorem for finite nonempty two-player zero-sum games with arbitrary real payoffs. Mixed strategies are probability vectors, and the two game values are defined using real indexed suprema and infima. An explicit payoff bound supplies the boundedness obligations required by these conditional extrema. The reverse minimax inequality follows by applying Mathlib's proved Sion saddle-point theorem to compact convex coordinate simplices, with the minimizing player placed in its first argument. We explain the representation bridge, the proof obligations, and the passage from a saddle point to equality. The accompanying version-pinned artifact separates a reusable library from a statement-only challenge and its proved solution. This is an exposition of a finite-game specialization of existing formal analysis, with no claim of a new mathematical proof or formalization priority.

Primarily AI-generated textHuman understanding: some partsLeanSion's theoremformalizationminimax theoremzero-sum games

math.AG — Algebraic Geometry

Signed Mukai diagonals and derived equivalences of fivefolds

Contributed by Benjamin Antieau

For every Hochschild diagonal of a smooth projective complex variety, a Fourier–Mukai equivalence preserves both the ordinary Hodge-number sum and the sum signed by the parity of the antiholomorphic degree. The latter is the signature of a Hermitian form obtained from the generalized Mukai pairing. In dimension five these invariants determine h0,3h^{0,3} and h1,4h^{1,4} and reduce the unrestricted Hodge-number problem to two numerical parameters, one of which is the possible failure of invariance of h0,2h^{0,2}. Albanese methods remove this structure-sheaf ambiguity when the Albanese image has dimension at least three. The general fivefold case remains open, while a theorem of Abuaf proves invariance of all Hodge numbers for fivefolds with trivial canonical bundle.

Primarily AI-generated textHuman understanding: no partsDerived categoriesfivefolds

math.PR — Probability

On the Asymptotic W1W_1 Cost of Two-Dimensional Semi-Discrete Matching

Contributed by Heng Ma

Let X1,X2,…X_1,X_2,\ldots be independent uniform points in the unit square and let λ\lambda denote Lebesgue probability measure. We prove that the normalized expected W1W_1 distance between the empirical measure and Lebesgue measure converges to a positive constant: \[ \lim_{N\to\infty} \sqrt{\frac{N}{\log N}}\, \mathbb E W_1\!\left(\frac1N\sum_{i=1}^N\delta_{X_i},\lambda\right) =c_\star. \] The constant is characterized by the convex viscosity equation \[ \partial_tU=\frac1{4\pi}\sqrt{\det D^2U}, \qquad U(0,q)=|q|. \] Its solution UU is unique under certain growth and regularity conditions, and the limiting constant c⋆=U(1,0)/2c_\star=U(1,0)/\sqrt2.

Primarily AI-generated textHuman understanding: no parts

math.MG — Metric Geometry

FINITE HAUSDORFF HYPERSPACES AND GROMOV–HAUSDORFF GEOMETRY

Contributed by Yoshito Ishiki

For a nonempty finite metric space X, let Exp(X) be the space of its nonempty subsets equipped with the Hausdorff metric. We prove that the isometry type of Exp(X) determines X when X is strongly rigid, meaning that distinct unordered pairs of distinct points have dis- tinct distances. We also prove that the hyperspace operation preserves the ordinary Gromov–Hausdorff distance locally under explicit separa- tion conditions on the distance spectra. For finite ultrametric spaces, the hyperspace operation is an isometric embedding with respect to the Gromov–Hausdorff ultrametric. In contrast, we construct finite ultra- metric spaces for which the ordinary Gromov–Hausdorff distance strictly decreases under the hyperspace operation. Examples of equal cardinality exist in every cardinality at least six and realize every ratio in [1/2, 1). Their distances remain constant after the first hyperspace iteration. An explicit perturbation also yields strict contraction for finite strongly rigid metric spaces with all triangle inequalities strict.

Primarily AI-generated textHuman understanding: some partsGromov--Hausdorff spaceHyper space

math.LO — Logic

Ordinal-definable families in Cohen, random, and collapse extensions

Contributed by Elliot Glazer

We study ordinal-definable families of sets of arbitrary rank in Cohen, random, and collapse extensions. Over LL, countable OD families have OD enumerations after adding one Cohen or one random real. A single generalized Cohen subset gives the corresponding sharp theorem at every regular uncountable cardinal. When κ\kappa is singular strong limit and has uncountable cofinality, adding κ\kappa Cohen reals makes every member of a short-parameter definable family of size at most κ\kappa definable from a short parameter. Adding κ\kappa random reals gives a single short-parameter definable enumeration for every such family of size strictly below κ\kappa. The random bound is sharp. The proofs use coordinate amalgamation and small-index arguments. We also obtain arbitrary-rank descent for countable families after collapsing any infinite cardinal, with applications to choice in the relative Feferman--Levy model. In the full Solovay collapse extension of an arbitrary ZFC ground, every family definable from a real and ordinals that represents fewer than 2c2^{\mathfrak c} classes modulo null sets consists of measurable sets; the corresponding category assertion also holds. In the extensions of LL by ω1\omega_1 Cohen or random reals, no model of IΔ0I\Delta_0 of size at most ℵ1\aleph_1, definable from ordinals and a real, has full binary-coded standard system. Π11-CA0\Pi^1_1\text{-}\mathsf{CA}_0 proves a finite-fragment Borel obstruction to a full binary standard system for IΔ0I\Delta_0. For regular uncountable κ\kappa, the generalized Cohen extension by $\Add(\kappa,\Lambda)^L$, Λ>κ\Lambda>\kappa, has no ambiently κ+\kappa^+-saturated IΔ0I\Delta_0 model in HOD⁡Hκ+\operatorname{HOD}_{H_{\kappa^+}}, regardless of its size. Consequently every infinite regular κ\kappa of LL admits a cofinality-preserving GCH extension with no ODP(κ)\mathrm{OD}_{\mathcal P(\kappa)} saturated arithmetic presentation of size κ+\kappa^+. ZFC also proves that every singular strong limit κ\kappa admits an OD κ+\kappa^+-saturated elementary extension of N\mathbb N of size 2κ2^\kappa, hence of size κ+\kappa^+ under GCH.

Primarily AI-generated textHuman understanding: some partsBoolean algebrasSet theorydefinability

math.CO — Combinatorics

Collapsibility of Alexander duals for shade maps

Contributed by Darij Grinberg

Let EE be a nonempty finite set. A shade map on EE is a map T:P(E)→P(E)T:\mathcal{P}(E)\rightarrow\mathcal{P}(E) such that toggling an element u∉T(F)u\notin T(F) in the input FF does not change T(F)T(F). We prove that, if TT is an inclusion-reversing shade map and G⊆EG\subseteq E, then the simplicial complex \[ \{F\subseteq E\mid G\subseteq T(F)\} \] is collapsible. Equivalently, if SS is an inclusion-preserving shade map, then the Alexander dual of \[ \{F\subseteq E\mid G\not \subseteq S(F)\} \] is collapsible. This is an Alexander-dual companion to the shade-map collapsibility theorem in \emph{The Elser nuclei sum revisited}. The proof first matches all faces on which T(F)≠ET(F)\neq E by a toggle. The remaining faces, characterized by T(F)=ET(F)=E, form the free convex set complex of an associated antimatroidal quasi-closure operator. We give a self-contained recursive acyclic matching on this complex. For ordinary convex geometries, Korte--Lovász--Schrader prove the stronger fact that the free convex set system is non-evasive.

A mix of human-written and AI-generated textHuman understanding: all partsantimatroidsconvex geometriesdiscrete Morse theorygraphssimplicial complexes