Leaving the Hall: explicit formulas for Neguţ operators

Abstract

Recent major breakthroughs in $q,t$-combinatorics include the introduction of the Dyck path algebra $\mathbb{A}_{q,t}$ by Carlsson and Mellit and of the Catalanimals by Blasiak et al., both of which led, among other things, to independent proofs of different extensions of the rational shuffle conjecture of Bergeron et al. The first main contribution of this paper is a simple, explicit formula inside the algebra $\mathbb{A}_{q,t}$ for the Neguţ operators, yielding a direct, elementary connection between the original operators of the rational shuffle conjecture and the corresponding Catalanimals. Our formula bypasses the elliptic Hall algebra, turning these operators into transparent, workable tools whose action we can compute exactly and efficiently on any symmetric function, not just constants. Our second main contribution consists of a series of explicit formulas relating the Neguţ operators to the Theta operators introduced by D'Adderio et al. To prove these formulas, we provide an extension of the aforementioned Theta operators to the entire algebra $\mathbb{A}_{q,t}$, allowing us to obtain a series of new combinatorial results. The algebraic computations underlying this extension have been formalized in Lean. To showcase the power of our results, we give a proof, also partially formalized in Lean, of the Theta conjecture of D'Adderio et al., first stated in 2019.

Disclosure

“asier to compute and manipulate, allowing us to obtain a series of new combinatorial results in the form of explicit formulas. The computations used to define this extension have been formalized in Lean 4 using Harmonic’s Aristotle [1], an AI system for formal verification. As a notable application of our new formulas, we prove the Theta conjecture [15, Conjecture 9.1] using (among other tools) a bijective argument that we also formalized in Lean 4 using Aristotle. Our formulas potent”

PDF page 4

Classification

Code generation, completion, or debugging

Multiplier

2

Verified

2026-08-23T05:15:57.729443Z

Structural counts