The δ-calculus
δ derives the laws of arithmetic from how records are built, opening a path to mathematics grounded in physical reality.
What is a number before we give it a symbol? Make a distinction. Keep its record. Do it again.
The δ-calculus builds counting from those records, addition from joining them, and multiplication from repeating a group. The familiar laws of arithmetic follow from the construction.
Build the first number ↓From an act to arithmetic
01 / A record
Start with an empty record. Each time you repeat the act, append a mark and retain the marks already there. We call the empty record zero, and the operation of adding one mark successor.
The marks may look alike. Their places in the record keep the repetitions apart.
The empty record has no marks.
The buttons stop at eight marks to keep the picture legible. The construction has no largest record.
There are two ways to form these finite records: begin empty, or append a mark to a record already formed. Empty and extended records differ. If two extended records are equal, removing their last marks leaves equal records. Every record can be reached by finitely many extensions. These construction rules yield zero, successor and induction.
A single difference between two things does not by itself supply this entire construction. We also specify how records are formed, retained and compared. These rules are part of the foundation being made explicit.
Formal definitions: DistinctionNat, zero_ne_succ, succ_injective, induction. Proof sources ↓
Beneath the axioms
Peano’s axioms describe the behavior of counting: a start, a next step, and a way to reason about every number. The δ construction asks what makes those properties hold.
Take the word “again” seriously. If the record is to count repetitions, it must keep the difference between doing something once and doing it twice. It must do the same for every finite number of repetitions.
The construction begins empty. An extension keeps the earlier record and adds one mark. Every record is formed in one of those two ways. To compare two extended records, compare the records they extend. These rules give us three properties. Try removing one and see what changes.
A separate state. It leads back to itself, and the counting path never enters it.
3 steps taken. The record reads 3. The path above shows every step taken.
Each extension retains its earlier record. Different counts remain different, and every record is made by repetition.
The picture stops after twelve steps. The full-record and extra-state constructions continue without a largest count. The proofs cover the whole constructions, including records beyond this picture.
Suppose two records match. If one is the start and the other is an extension, the first requirement is broken. If both are extensions, the second lets us compare their predecessors. Repeat until both reach the start: they must contain the same number of steps. The third requirement ensures that there are no other records left out of this comparison.
If a system preserves every different count and every state comes from counting, it satisfies all three requirements. The proof works in both directions. Each alternative above keeps two requirements while failing the remaining one.
A faithful system of counting records has the same mathematics, whatever its marks look like. There is exactly one translation from δ that preserves the start and the step, and it loses no information.
A statement or comparison already makes a distinction. Keeping and repeating distinctions adds a specific construction: empty records, extensions, and reasoning over everything formed that way. In the formal framework, these are the formation, computation and induction rules. From them, δ derives the separation of zero from a successor, the preservation of differences by successor, and the laws of arithmetic.
The familiar properties of arithmetic follow from how the records are built. The construction itself has rules. Distinction Before Logic examines those rules, including the types and equality reasoning needed to express them. Lean checks the proofs within its own type theory.
Every record is empty or extends an earlier record. To establish something about them all, establish it for the empty record and show that extending a record preserves it. The formation rule licenses this way of reasoning. No further class of records is being silently included.
The examples above make its role visible. The property “lies on the counting path” holds at the start and survives a step. It fails at the extra state. A system containing that state cannot satisfy this induction rule.
Now use those records. Joining them gives addition; repeating a group gives multiplication. The next examples let you perform both operations.
Read the formation proof, download its complete source package, or inspect the verification. The proof uses the library’s counting records and its existing uniqueness theorem. The three examples establish independence of the stated requirements; they do not claim historical novelty.
02 / Addition
Keep the first record. Append the marks of the second, one at a time. Two marks joined to three marks make five.
The symbols 2 + 3 = 5 describe that operation. Change the symbols and the operation still works.
2 + 3 = 5
Circles and squares both retain one place for every mark.
Joining an empty second record leaves the first unchanged. Joining a record with one more mark appends one more mark to the result. Those two rules determine addition on every finite record. They also let us prove its laws, including that reversing the two counts preserves the total.
A faithful representation has a way back: translating the displayed record back recovers the original count. The Lean framework proves both directions of this correspondence and proves that addition is preserved.
DistinctionNat.add, add_comm, toNat_add, ofNat_toNat.
03 / Multiplication
Take the record of two marks. Join three copies of it. The result contains six marks.
Multiplication repeats addition: 2 × 3 means three copies of a group of two in this construction.
2 × 3 = 6
2 + 2 + 2 = 6
Zero copies give the empty record. One more copy joins one more group to the result already built. These are the two defining rules of multiplication. Commutativity and the distributive laws can then be proved from the construction.
DistinctionNat.mul, mul_comm, toNat_mul.
04 / Signed numbers
Put two records side by side: positive marks and negative marks. Pair one of each. What remains determines the difference.
Two positive and three negative marks leave one negative. Add a positive and a negative together, and the difference stays the same.
(2, 3) represents −1
Two pairs cancel. One negative mark remains.
Compare (2, 3) with (4, 5). They represent the same difference because 2 + 5 = 4 + 3. This test uses the addition we already constructed.
An integer collects all the pairs that pass this comparison with one another. The framework proves that this relation agrees exactly with equality of the integer values, and that arithmetic respects it.
SignedOrbit.balanced, balanced_iff_toInt_eq, PRCInt.
05 / Fractions
One of two equal parts and two of four equal parts give the same share. The records differ; the relationship is equal.
We can test that equality using whole records: a/b = c/d exactly when a × d = c × b, with nonzero denominators.
1 / 2 = 2 / 4
The cross-products match: 1 × 4 = 2 × 2 = 4.
The bars illustrate the comparison. The proof uses multiplication on records. Rational numbers identify signed numerators and nonzero counting denominators when their cross-products balance. The full construction therefore includes negative fractions too; this picture uses nonnegative examples.
RatioOrbit.crossEq, crossEq_iff_toRat_eq, PRCRat.
06 / Losing information
A three-position counter reads 0, then 1, then 2, then 0 again. After three steps, its display matches the beginning. The full record has acquired three marks.
The counter preserves counting modulo three: counts that differ by a multiple of three share a display. That is useful mathematics, with a different equality.
Display 0. Full count 0.
Worked collision: full counts 2 and 5 both display 2. The display alone cannot tell them apart.
The circle-to-square translation can be reversed. The counter reading cannot recover the full count. It deliberately treats several counts as equal. Mathematicians call this a quotient.
The δ research program also classifies counters with an initial stretch followed by a repeating cycle. Recovering that structure requires a rule that respects composition, a way to decide whether states match, and a witnessed repetition. A repeated observation alone does not establish all those conditions. Try recovering a controller’s cycle and predicting a distant state →
The lesson’s counter is the explicit map n ↦ n mod 3. Its collision is checked in the lesson proof.
The connection to reality
Follow a closed path around an obstacle twice. Change its shape without crossing the obstacle. It still goes around twice. The count belongs to the winding of the path.
The Lean framework constructs a spatial path for each finite δ record. One act adds one turn in a fixed direction. A decoder recovers the record from the winding. The proof establishes that the record survives continuous deformations in the specified space, and that joining two paths corresponds to joining their records.
Addition can be the composition of paths. The arithmetic is preserved because the operation preserves what is being counted.
Make one turn, then make the reverse turn. The net winding is zero. Two acts have occurred. Reading only the net winding cannot recover their count.
Keep a separate tally for each direction. A forward act extends the first record; a reverse act extends the second. Their difference gives the net change. Joining the two records gives the number of acts.
Two records, two questions
Forward acts recorded
Reverse acts recorded
Each act adds a turn to its own record. The numbers count traversals of the routes drawn above.
How many acts?
What is the net change?
2 acts recorded. Net change 0. The net change matches the start. The records show what happened.
Changing the order leaves both tallies unchanged. The strip remembers order; the two tallies remember only how many acts occurred in each direction. Different records answer different questions.
This example stops at eight acts. The spatial proof constructs a pair of winding records and proves how their counts combine. It does not specify a device that writes or reads them.
It can count acts that all add turns in one direction. If reversal is allowed to cancel the stored winding, a nonnegative count cannot both survive deformation and add correctly for every joined path. A turn and its reverse would have to count as zero acts together. Since neither count is negative, each would have to count as zero.
The proof establishes this for every such readout, not just the decoder used in the example. The two-record construction avoids that cancellation by keeping the directional tallies separate. Their sum follows δ’s append operation even when the net change returns to zero.
Read the native δ tally proof, its spatial correspondence, and the verification report. For the richer problem of retaining loop order, read the paper on recognition and memory.
The obstacle must remain excluded. The path must be retained and read with its traversal count, and the device must perform the stated joining operation. A still image of the route is insufficient: one trip and two trips can draw the same circle.
The construction proves how records and operations correspond in the specified geometry. Establishing a physical realization means deriving or supplying those retention, readout and operation conditions. A device with room for only a finite record also has a capacity limit. No finite device stores every counting number at once.
Read the spatial-record proof and its source and verification scope.
The larger thesis
The claim we aim to establish
Forced mathematics = physically real
In this argument, forced means that the structure follows from the starting operations: no alternative satisfies the same requirements. For counting, retaining each repetition determines the arithmetic. The larger proposal is that physical reality supplies the operations from which mathematics follows.
That would change what mathematics tells us. A derivation could explain why a physical structure has to exist and behave as it does. The arithmetic and path constructions above establish parts of this connection. The full equality requires showing both what physical processes can realize and what mathematical structure those processes require.
Quantum mechanics
A bound quantum system can have separated energy levels. δ asks which allowed states and measurement rules follow from the underlying operations. A derivation must account for interference and probabilities as well as the levels.
Quantized outcomes alone do not establish that derivation. Quantum mechanics also uses continuous quantities and can have continuous spectra.
General relativity
General relativity describes gravity through smooth spacetime geometry. δ asks whether physical constructions can give rise to that geometry and its equations, with a calculable range of accuracy.
The continuum would then describe a large-scale limit. A continuum theory can remain accurate even if its mathematical continuum is not the underlying physical structure.
The complete real line adds something that finite arithmetic does not require. The δ boundary paper proves that finite records cannot name every real number exactly. It also distinguishes finite names from executable procedures. Those results identify an additional mathematical assumption; they do not establish that every continuum description is physically false.
A finite rule can still specify an irrational number and approximate it as closely as requested. The next example does exactly that for √2. The question for physics is which constructions nature realizes, and when a smooth description preserves their predictions.
No. Imagine a binary sequence whose digits can be queried one at a time. Every finished query returns a finite answer. Any two different sequences can be distinguished by querying a digit where they differ. Yet the set of all infinite binary sequences is uncountable, so finite records cannot give each sequence its own exact name.
Whether nature can realize such a device is a separate question. The example shows why finite measurement results alone do not settle the structure of the states being measured. That connection needs a physical argument.
See one finite example. Follow a pulse into a retained mark, count the written cells and account for every unit of energy. Explore the recording model →
Read The Boundary of the δ-Calculus for the distinction between constructions, exact outcomes and continuous laws. Background on the conventional theories: MIT on discrete and continuous quantum spectra; the Albert Einstein Institute on geometric gravity.
Beyond fractions
Take a square with sides of length 1. Its diagonal has length √2: the positive number whose square is 2. No fraction equals that number.
Yet a short rule locates it as closely as we ask. Begin between 1 and 2. Square the midpoint. If the result is above 2, keep the left half. If it is below 2, keep the right half. Repeat.
Every decision uses fractions. Every step cuts the width in half.
Find √2 by halving an interval
The current interval is enlarged to fill the strip. Test its midpoint to choose the next half.
(3/2)² = 9/4 > 2
The midpoint squared is greater than 2. Keep the left half. Its width will be 1/2.
After n steps, the bounds are exactly 1/2n apart, and √2 remains between them. Choose any positive rational error allowance: finitely many steps make the interval narrower than that allowance. We have an exact rule with a proved error bound, even though each answer is a pair of fractions.
The Lean example uses δ’s interval-refinement structure and proves that its value is √2. It also constructs each rational bound from δ’s signed records and ratios, and proves that their displayed values and squares agree. This is the familiar bisection method, used here to make the extension from arithmetic explicit.
Suppose p/q is in lowest terms and its square is 2. Then p² = 2q², so p is even. Write p = 2k. Substitution gives q² = 2k², so q is even too. Both have a factor of 2, contradicting lowest terms.
Adding this number therefore extends the fractions. It does not change what any existing fraction means.
Read the refinement proof, download its complete source package, or inspect the checks.
Where the construction reaches
The example separates three commitments that can look like one when we write a decimal.
The square-and-halve procedure is finite. Each requested step terminates, uses exact fractions and comes with an error bound. Running more steps requires more time and storage.
The positive solution of x² = 2 is uniquely determined. We can work with its refinement rule. When we interpret that rule in the usual real numbers, the completeness of that system supplies its limit. The proof identifies that value as √2.
Order-completeness says that every nonempty set of numbers bounded above has a least upper bound. This concerns all such sets, far beyond a single algorithm. The ordered-field laws alone do not force completeness: the fractions obey them and still leave a gap at √2.
Adding √2 closes one gap in the fractions. Adding every real algebraic number still gives a countable collection. The full real line is uncountable. A fixed collection of finite rules over a countable alphabet cannot individually generate all its points.
The library’s general interval structure allows any function from a step number to a rational interval, provided the intervals nest and shrink at the required rate. Those mathematical conditions alone do not say that a program computes the function.
The √2 example supplies that program explicitly. The library’s theorem that every real has an interval representation instead starts with a real number and uses it to choose bounds. It establishes a representation theorem; it does not turn all real numbers into finite programs.
For fractions, cross-multiplication settles equality and order. Bounds can also settle an inequality once two intervals separate. But intervals that still overlap do not settle equality, however many digits agree.
Particular rules can have proofs of equality, as this one has a proof that its value is √2. A decision that works for arbitrary Cauchy reals requires more. The boundary paper identifies the additional logical principles for universal equality and order decisions.
These distinctions are developed in The Boundary of the δ-Calculus. They specify what each extension adds, so that a construction of one kind is not mistaken for a proof of another.
Continue the argument
Jonathan Washburn and Milan Lj. Zlatanović. Builds the number tower from finite records and establishes which distinctions survive a counting system. The linked PDF is the accepted author manuscript.
Jonathan Washburn and Milan Zlatanović. Shows why transition counts and any fixed finite memory cannot recover loop order on cube graphs, and how an unbounded stack recovers the reduced loop word.
The metatheory of iterated distinction, measured. Derives the Peano properties from explicit formation and reasoning rules, and identifies what the construction needs.
Distinguishes the forced arithmetic tower, finite descriptions, effective procedures and the physical premise connecting them. Locates the additional commitments of the continuum.
Read the worked Lean example. It imports the integrated δ definitions rather than replacing them with ordinary arithmetic. The browser’s drawings are an implementation of the lesson; verification of the browser and verification of the formal statements are separate checks.
The examples compile in Lean. The browser was compared against native δ calculations over every value offered by its controls, including all 1,764 fraction comparisons. Read the verification report or download the complete lesson proof package.
Read the proof beneath the counting example, download its complete source package, or see its checks and the spatial-source references.
The wider library is maintained in the mathematics repository (GitHub access may be required).