A fundamental question in the foundations of mathematics is where numbers come from. This paper proposes a minimalist answer: start with a single primitive act called "distinction," written as a Greek letter delta, which simply means taking one step from something to something new, like adding a fresh mark to a record. By repeatedly applying this act, you generate a sequence of distinct objects that behaves exactly like the natural numbers. The paper then builds a formal logical system around this idea, called the delta-calculus, which can express and prove statements about arithmetic using only constructive reasoning as its foundation.
A key feature of the system is a built-in accounting mechanism called a "ledger." Every mathematical proof carries a running tab that tracks exactly which non-constructive logical principles were used, such as the law of excluded middle (the assumption that every statement is either true or false) or Markov's principle (a weaker but still non-trivial assumption). Proofs that use none of these extra principles are called "forced," and the paper shows that anything provable by forced reasoning is actually true in the ordinary sense. Starting from the delta construction, the authors build up integers and rational numbers without making any arbitrary choices along the way, and they show that the usual number systems embed naturally into this framework.
The paper also takes a detour into abstract algebra, asking how the additive structure of the natural numbers can be mapped onto simpler objects. It turns out that any such "recognition map" either perfectly distinguishes all numbers or collapses them into a specific finite repeating pattern, characterized by two numbers: a starting point and a cycle length. The ledger framework lets the authors determine precisely how much logical muscle is needed to prove each case of this classification. For example, identifying a concrete collapsing pattern requires only a mild non-constructive principle, while handling the fully general case requires the law of excluded middle. The authors verified all their main results using the Lean 4 proof assistant, a computer system for checking mathematical proofs.