Search papers, labs, and topics across Lattice.
This paper investigates the impact of allowing negative integers in sets used for $h$-basis representations of integers up to $n$. Specifically, it analyzes the largest integer $n^{\flat}_h(k)$ representable by the sumset $hA$ where $A$ has size $k+1$ and contains at least one negative element, comparing it to the classical postage stamp problem's $n_h(k)$. The key finding is that for $k=2$, $n^{\flat}_h(2) < n_h(2)$ when $h$ is odd or $h=4$, and $n^{\flat}_h(2) = n_h(2)$ otherwise, with these results formally verified by an AI agent.
Allowing negative integers in $h$-basis sets can surprisingly *reduce* the range of representable integers compared to using only non-negative elements, a counter-intuitive finding formally verified by AI.
A set $A$ of integers is an $h$-basis for $n$ if every integer in $[0,n] = \{0,1,2,\ldots,n\}$ belongs to the sumset $hA$, that is, can be represented as the sum of exactly $h$ not necessarily distinct elements of $A$. The classical postage stamp problem asks for the largest integer $n_h(k)$ such that $[0,n_h(k)] \subseteq hA$ for some set $A$ of nonnegative integers of size $k+1$. We consider the effect of allowing negative elements. Let $n^{\flat}_h(k)$ be the largest integer such that $[0,n^{\flat}_h(k)] \subseteq hA$ for some set $A$ of integers of size $k+1$ containing at least one negative integer. For $k=2$, we have $n^{\flat}_h(2) < n_h(2)$ if $h$ is odd or $h=4$ and $n^{\flat}_h(2) = n_h(2)$ if $h$ is even and $h \neq 4$. Proofs of these comparison results were autonomously discovered and formally verified in Lean by https://aristotle.harmonic.fun/}{Aristotle}, a formal reasoning agent developed by https://www.harmonic.fun/}{Harmonic}. In this paper we give new proofs of these results.