arXiv++ Combinatorics

In this paper, we strengthen the connection between the combinatorics of difference sets and the dynamics of group rotations. Our main result shows that sets which have non-empty intersection with all difference subsets of a commutative semigroup possess local Bohr structure. This generalizes results of Bergelson, Furstenberg, and Weiss and Host and Kra from the integers to arbitrary commutative semigroups. We accomplish this by A) utilizing a recent result showing that the regionally proximal relation is an equivalence relation for minimal actions of commutative semigroups and by B) describing a new, DeMorgan-type algebra on Furstenberg families that allows for efficient manipulation and computation. We formally verify all of the results in this paper in Lean. The main results are verified in a Palomar submission, and we link to a Github repository containing code for the complete verification.

Let $k$ be a field of characteristic $p\ge0$. We prove that $m$ points and $n$ lines in $k^2$ determine at most $3(mn)^{2/3}+m+n+2mn/p$ incidences, the last term being omitted in characteristic zero. Over the prime field $\mathbb{F}_p$ the coefficient of $mn/p$ can be replaced by $1$. The proof uses the polynomial method, and for $m=n$ the bound is sharp up to an absolute constant over prime fields. As applications, over prime fields in which $-1$ is not a square we obtain the $L^2\to L^r$ extension estimate for the paraboloid in $\mathbb{F}_p^3$ for $r>10/3$. Over every odd prime field, we show that a two-source extractor construction of Bourgain has exponentially small error at every min-entropy rate greater than $1/3$. We also improve sum-product estimates for small sets in positive characteristic and obtain projection and Furstenberg estimates over prime fields. The incidence inequalities with exact constants have been formalized in Lean.

Harwit and Sloane conjectured that every nonsingular entrywise-nonnegative matrix $A\in\mathbb R^{n\times n}$ satisfies $\|A^{-1}\|_F\ge 2n(n+1)^{-1}\|A\|_{\max}^{-1}$, with equality precisely for positive multiples of $S$-matrices. Zhang has given a complete proof of this conjecture by a centered pseudoinverse and spectral variance method. We present an independently obtained, structurally different proof of the strict even-dimensional inequality. Starting from the structural identities of Frankel and Urschel, we derive an exact global defect budget and combine binary rounding, fixed intersections, and Gram projection. A ten-row obstruction handles every even $n\ge66$; a finite exact calculation handles $4\le n\le64$, $n\ne6$; and a multi-column energy argument treats $n=6$. The order-two case is elementary. The even-dimensional argument is formalized in Lean 4, conditional on Frankel--Urschel Lemma 2.1 as an explicit external mathematical input. The finite evaluations use Lean's native evaluator; their trust boundary and exact certificates are documented. Together with Cheng's odd-dimensional theorem, the argument recovers the full S-matrix theorem and its equality characterization.

For a finite forest $F$ let $i_k(F)$ be the number of independent sets of $F$ with $k$ vertices. Zhang and Li proved that the sequence $i_0(F),i_1(F),\dots,i_{α(F)}(F)$ is unimodal for every finite forest $F$, which answers Erdős Problem 993. We give a second proof. It starts from their decomposition relative to a fixed independent set and from the bounds of Zhang and Li and of Fang, Lu, Nevo, Yao and Zheng that confine a valley of the sequence to an explicit window of ranks. For a forest with at least $25$ vertices, one moment argument excludes a valley at every rank of the window: at the activity where the hard-core mean equals the rank, the size of a random independent set is a mixture of binomial laws over an independent set of maximum weight, a valley is a moment inequality for this mixture, and it is excluded by duality given three bounds that hold for every forest, on the variance of the number of free vertices and on its Laplace transforms, and on the variance ratio. The variance bound is proved by hand up to finitely many interval checks and the other two bounds are verified by computer on finite interval-arithmetic coverings; on the resulting parameter domain a valley is excluded by exact tests on finitely many rational boxes while the mean number of free vertices is below an explicit starting mean between $19$ and $50$, and above it by one inequality, with explicit constants, for the fibers of a weighted valley kernel, proved by hand up to a finite list of explicit checks and averaged over the mixture. Forests with at most $24$ vertices are treated by exact counting, by hand except for exact rational evaluations of two explicit formulas at $43$ parameter triples. No forest is enumerated. A formal proof of the theorem in Lean 4 accompanies the paper.

Let $K$ be a finite field of characteristic two with $|K| = 2^{n}$, let $\gcd(k,n) = 1$, let $d_{k} = 4^{k} - 2^{k} + 1$ be the Kasami exponent, and let $Δ_{k} = \{(b+1)^{d_{k}} + b^{d_{k}} + 1 : b \in K\}$ be the image of the normalised derivative of the Kasami monomial in the direction $1$. We show that, for all distinct nonzero $v_{1},v_{2} \in K$, \[ \bigl|\{(x,y,z) \in Δ_{k}^{3} : v_{1}x + v_{2}y + (v_{1}+v_{2})z = 0\}\bigr| = 2^{2n-3}. \] This establishes the cyclic-additive difference-set condition introduced by Carlet and later posed for the Kasami functions at NSUCRYPTO~2019. Starting from the known half-size property of the derivative image, we express the Fourier correction as twisted root counts and prove their required nonnegativity by an incidence argument on the Fermat cubic. An exact average over the slopes then forces equality pointwise. The argument covers every admissible pair $(n,k)$ and has been formalised and machine-checked in Lean~4 with Mathlib.

We exhibit simple, rotationally symmetric Venn diagrams with 17 curves, with 19 curves and with 23 curves: $n$ Jordan curves carried to one another by rotation through $2π/n$, with every one of the $2^n$ regions present and connected and, since the diagrams are simple, every crossing on exactly two curves. Symmetric Venn diagrams exist for every prime number of curves (Griggs, Killian and Savage, 2004), but those diagrams have many curves through a point; simple ones were known only up to 13 curves (Mamakani and Ruskey, 2014). Four 17-curve, nine 19-curve and five 23-curve diagrams were found by a Metropolis walk on rotation-invariant quadrangulations of the sphere in which regions may temporarily be duplicated, started from the Griggs-Killian-Savage diagram with its multiple crossings resolved. At 23 curves the walk was held for two weeks by duplicated regions near the poles; the two lineages that finished were the first whose $E=92$ states had none. Every diagram is given by a machine-checkable certificate; one certificate each of the 17- and 19-curve sizes has been verified by a formal proof in Lean 4. All of the diagrams are non-monotone, which is why the crossing-sequence searches that found the 11- and 13-curve diagrams could not have found them.

We prove Sabidussi's compatibility conjecture. Let $G$ be a finite connected multigraph in which every vertex has even degree and the minimum degree is at least four, and let $T$ be an Euler tour of $G$. The edges of $G$ can be partitioned into circuits (connected $2$-regular subgraphs) so that no circuit contains two edges used consecutively anywhere in $T$. In fact, the edges can be four-coloured so that every such pair receives different colours and every colour class has even degree at every vertex. We use a counting argument based on the Chevalley-Warning theorem to show that a four-colouring with the required properties exists. Splitting each colour class into circuits then gives the desired compatible decomposition. Formalization in Lean 4 is also available in the author's github.

We prove both Erdős-Ulam conjectures on monochromatic union-closed families. Every two-colouring of the subsets of a finite set contains a monochromatic union-closed family whose size grows faster than any fixed power of the size of the set, while suitable colourings admit no monochromatic union-closed family of exponential size. Both results hold for any number of colours and are verified in Lean.

We prove that the Turán density of the tetrahedron $K_4^{(3)}$ satisfies $π(K_4^{(3)}) \le 14993367693127837/26880000000000000 < 0.557789$, improving Baber's upper bound of $0.5615$ and closing about $62\%$ of the gap to the conjectured value $5/9$. The proof uses an exact seven-vertex flag-algebra certificate incorporating degree-stationarity from Razborov's differential method. To find the certificate, we combine the established techniques of cutting planes and column generation to optimize jointly over flag families whose types have at most five vertices. We give a complete formal proof of this Turán density bound in Lean 4.

Choose a uniformly random ordering of the vertices of a finite tree and run the usual greedy maximal-independent-set algorithm. We compare the resulting law on maximal independent sets with the uniform law. We prove that exact uniformity occurs only for the one-vertex tree and the single edge. The proof is structural: a diameter endpoint exposes a pendant star, and the remaining one-pendant-leaf case is resolved by a strict injection between exact permutation fibres obtained by swapping the pendant leaf with its support vertex. Exact uniformity is therefore rigid, but it can be approached closely. For an explicit mixed-spider family $T_{k,l}$ we count the maximal independent sets and compute the exact probability of every output. With $l=2^k-k$ the total-variation bias is positive and satisfies [ b(T_{k,2^k-k})=O!\left(\frac{\sqrt{k}}{4^k}\right) =O!\left(\frac{\sqrt{\log n_k}}{n_k^2}\right), \qquad n_k=2^k+k+1. ] The theorem package has also been formalised in Lean and registered with Palomar. These records document machine-checked formal verification and the checked axiom boundary; they are not peer review or a certificate of novelty.

In 1965, D. H. Lehmer conjectured that the permutations of every multiset admit an imperfect Hamiltonian traversal by adjacent swaps: a walk in the neighbor-swap graph that visits every word, with some words visited twice in order to reach a neighbor and return. The question is posed as an unsolved research problem in Knuth's Art of Computer Programming. Verhoeff (2017) chose the stutter words, in which every domino is a double, as the words to be reached this way, and reformulated the conjecture as the Hamiltonicity of the graph $N(S)$ on the non-stutter words, with two exceptional families --- binary signatures with an odd multiplicity, and the permutations of $(2k,1,1)$ --- that admit a Hamiltonian path but no cycle. This article proves the reformulated conjecture, and with it Lehmer's conjecture. The key structure is a partition of the words into hypercubes: the swaps inside dominoes turn each class of words with the same domino contents into a hypercube, and the stutters are exactly the $0$-dimensional classes. When every multiplicity is even, Hamiltonian cycles of the hypercubes are glued along a spanning tree, with no finite check. The case of exactly one odd multiplicity reduces to the all-even case and to a theorem of Stachowiak (1992), the one inherited Hamiltonicity input, which also settles two or more odd multiplicities. The only finite ingredients are two explicit cycles, of 28 and 84 words. Every construction is implemented in Python and checked against brute-force graphs, and the proof is formalized in Lean 4 over Mathlib.

We give an algorithm counting the permutations that avoid a fixed pattern of the following form: the direct sum of an increasing pattern and 231. The first members of the family are 1342 and 12453. For each member the algorithm uses polynomially many operations and stored integers, with degrees that grow linearly in the length of the pattern. It comes from a recurrence that reads a permutation from left to right and records the constraints that the letters read so far impose on those still unread. This recurrence has exponentially many states, but part of each state is protected: later steps carry it along unchanged and do not depend on it, and factoring the protected part out leaves a dynamic program of polynomial size. For 12453 a translation symmetry sharpens the bounds to degree seven for the operations and degree four for the storage. We also compute the number of 12453-avoiding permutations of every length up to 150. The previously published series, due to Biers-Ariel (2019), reached length 38. We also give a sampler of uniformly random avoiders. A floating-point implementation of it, proved to be within total variation distance $3.5\cdot10^{-5}$ of uniform for ideal random bits, draws the one million 12453-avoiding permutations of length 300 shown in a heatmap. The literal and kernel recurrences for 1342 and 12453 are verified in the Lean 4 proof assistant.

We study a support-collapse version of graph pebbling on paths. A configuration is stackable if a sequence of legal pebbling moves can produce a nonzero configuration supported on a single vertex. On the path P_n, we choose a configuration uniformly from all weak compositions of total n times mu_n, where mu_n is a positive integer. We prove a two-sided fixed-offset transition for the logarithmic density. The transition is centred at sqrt(log_2 n) - (1/2) log_2 log_2 n + log_2(3e). For every fixed epsilon greater than zero, the stackability probability tends to zero when log_2 mu_n is eventually at most the centre minus epsilon, and tends to one when it is eventually at least the centre plus epsilon. No assertion is made at zero offset. The proof uses an exact recursive stackability score on trees, a one-dimensional path-message recurrence, binary-partition asymptotics for rare dyadic deficit excursions, a constant-cost regeneration argument, and an exact deep-message necessity theorem. Conditioning independent geometric occupancies on their sum returns the uniform fixed-total model. The finite deterministic necessity theorem and its exact fixed-total corollary are formalised in Lean and registered with Palomar; the full probabilistic asymptotic theorem is not part of that registration.

For a graph $H$, let $f(n,e,H)$ be the least number of colors in an edge-coloring of some $n$-vertex graph with at least $e$ edges in which every copy of $H$ is rainbow. Burr, Erdős, Graham, and Sós conjectured that $f(n,\lfloor n^2/4\rfloor+1,C_{2k+1})=(1/8+o(1))n^2$ for every fixed $k\ge3$, and Bucić, Chen, and Ma recently proved this for all $k\ge4$. We prove the remaining case $k=3$: \[ f\left(n,\left\lfloor n^2/4\right\rfloor+1,C_7\right) =\left(\frac18+o(1)\right)n^2. \] The lower bound rests on a weighted palette inequality, which we prove with an exact rational certificate on five sampled vertices. Its main ingredients are a fractional matching of compatible triangular edges and private resources attached to nontriangular edges. A stable form of the inequality, combined with regularity, triangle removal, and a direct argument for graphs close to bipartite, transfers the bound to arbitrary edge-colorings. We also describe a Lean 4 formalization of the conjecture for every fixed $k\ge3$, which combines the new seven-cycle proof with a formalization of the Bucić-Chen-Ma argument for $k\ge4$.

A weak form of the Hellinger conjecture of Anantharam, Bogdanov, Chakrabarti, Jayram, and Nair for the binary symmetric channel is proved: dictator functions maximize Hellinger $Φ$-entropy among all Boolean functions of the input and all one-bit statistics of the output of a noisy channel. The technical heart of the matter is an explicit inequality in three real parameters, which is proved using explicit polynomial approximations and computer-assisted positivity checks. The results are also formally verified in Lean 4.

Every finite nonempty incomplete uniquely decipherable code with maximum word length $k$ has an uncompletable word of length at most $4k^2-3k$. The bound is independent of the number of codewords and their total length. Deleting a complete codeword cycle gives a finite path-counting identity; Kraft equality then supplies a short word of deficient compressed mass. Cyclic averaging and padding turn it into an uncompletable word. Conditional expectation makes the construction polynomial-time and also decides completeness. First-return words extend the bound to mortal families of nonnegative integer $n\times n$ matrices with joint spectral radius at most one, provided every strongly connected component has a vertex meeting every cycle. Such a family has a zero product of length at most $4n^2-3n$. A binary partial deterministic family with $2k-1$ states has shortest zero product of length $k^2+k-1$, establishing the optimal quadratic order. The bounds and the explicit-code algorithm, including its polynomial work bound, are proved in Lean.

We study the sequence $a(0)=0$, $a(1)=1$ and $a(n)=n-a(n-a(n-a(n-1)))$ for $n\ge 2$, listed as A076502 in the On-Line Encyclopedia of Integer Sequences. We identify $a(n)$ as a two-position shift in the greedy Padovan numeration system, with a finite-state correction. The proof constructs an addition automaton from an exact integer-carry invariant and certifies its completeness by finite-language inclusion; a synchronized automaton then verifies the nested recurrence. We establish bounded discrepancy from the line of slope $c$, where $c^3-c^2+2c-1=0$, and show that the exact set of offsets from $\lfloor cn\rfloor$ is $\{-1,0,1,2\}$. We construct an explicit 26-letter non-erasing morphic presentation of the first-difference word, prove that its least balance constant is 4, and give an effective procedure for enclosing the global discrepancy extrema to arbitrary accuracy. We formalize the recurrence identification, six-decimal discrepancy bound, exact offset set, concrete morphic identity, least balance constant, and an effective extrema algorithm in Lean. Separate exact computations refine the numerical enclosures.

Santos asked when intersections of dilated Hadamard simplices with cubes are integral, smooth, or normal, in a prescribed affine lattice. We construct a nonintegral example in dimension eleven and prove that no smaller-dimensional example exists. We characterize smoothness completely and show that every smooth member of this family is normal. An explicit example in dimension fifteen shows that integrality alone does not imply normality. For Sylvester simplices of order at least sixteen, we establish a sharp uniform integrality bound and construct counterexamples immediately below it. We also obtain sufficient normality bounds for general Hadamard simplices and stronger bounds for the Sylvester family. The proofs use integer decomposition for boxes with separated corner cuts and rounding under three signed slab constraints. All numbered results have formal counterparts verified in Lean.

We give an elementary proof that every positive rational number $a/b$ with $b$ squarefree is a finite sum of distinct unit fractions $1/n$, where each $n$ is a product of two distinct primes (Erdős Problem #306). After a reduction to small targets, we take a single complete bipartite graph between the primes in $(y^2,2y^2]$, together with $2$ and the primes of $b$, and a tuned initial segment of the primes in $(y^8,y^9]$, and show that some subgraph has reciprocal sum congruent to $a/b$ modulo $1$; the small total mass then forces equality. Writing the number of such subgraphs as a finite Fourier sum, we sort the frequencies into three cases using a table indexed by the two sides of the graph. The small integer frequencies give a positive main term, and all other frequencies are negligible by a divisor-counting argument and a no-wrap-around form of the Chinese remainder theorem. The only inputs about primes are Chebyshev-type bounds. The circle-method framework comes from Tang's Lean development, which gave the first proof; our construction removes its anchor-synchronisation step. The proof has been formalised in Lean 4, apart from a cited inequality of Ramanujan. This work is a human-AI collaboration: AI tools contributed substantially to the construction, the experiments and the writing.

The stacking number of a graph is the least integer t >= 2 such that every configuration of t pebbles can be transformed by pebbling moves into a configuration supported on one vertex. We prove that, for every finite tree T with at least two vertices, this number equals the rooted distance-and-degree estimator conjectured by Csernák and Soukup. The proof uses an exact recursive characterization of stackability at a prescribed vertex, an explicit zero-score obstruction, and a weighted cancellation argument for arbitrary nonstackable configurations. The complete theorem is formalized in Lean 4; the formal result has also passed Palomar mechanical verification and is publicly registered as PALOMAR-2026-09-25-000010.