δ is mathematics derived from distinction and necessity: the structure that reality enacts when distinctions are made, repeated and retained.
A statement, an observation or a comparison already distinguishes something. Keep each repetition, and those records have a uniquely determined arithmetic. The δ-calculus constructs it and proves why its laws must hold.
Joining records gives addition; repeating groups gives multiplication. Signed numbers and fractions follow from the same construction. The examples below let you perform these operations and follow their connection to physical recognition.
The symbols come after the operation. The construction tells us why the answer holds.
01 / A record
Keep one more mark.
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 record
empty
Its numeral
The empty record has no marks.
The buttons stop at eight marks to keep the picture legible. The construction has no largest record.
Why does this give counting?
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.
To build arithmetic, we specify how records are formed, retained and compared. A difference between two things supplies the starting distinction; the record rules let us keep and repeat it.
Peano’s axioms describe the behavior of counting: a start, a next step, and a way to reason about every number. δ derives these properties from the rules that form finite records. No independent Peano postulates are added to those formation rules.
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.
The state after each step
0→1→2→3
extra ↺
A separate state. It leads back to itself, and the counting path never enters it.
Steps taken
The record reads
3 steps taken. The record reads 3. The path above shows every step taken.
The start is never the result of a step.Holds
A step never merges two different states.Holds
Every state can be reached from the start.Holds
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.
Why these three requirements?
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.
The arithmetic is forced. Every faithful system generated from a start and a next step has the same structure. There is exactly one translation from δ that preserves those operations, and it loses no information.
That uniqueness is the point. Changing the marks, the notation or the faithful representation leaves the arithmetic intact. Its laws express what retaining and composing these distinctions requires.
Where does the derivation begin?
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.
Distinction Before Logic makes the formal starting point explicit: rules for functions, identity, an empty type, a universe of types and the generated records. The orbit’s separation and canonicity proofs require no additional declared axioms. Lean checks those proofs within its type theory; the paper accounts for the formation rules they use.
How does induction arise from formation?
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.
Inspect the formation verification. The proof uses the library’s counting records and its existing uniqueness theorem. The three familiar counterexamples show why each stated requirement is needed.
02 / Addition
Join two records.
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.
First
+
Second
Joined record
2 + 3 = 5
Circles and squares both retain one place for every mark.
Why must the answer be the same?
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.
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
What about zero copies?
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
A difference can have many records.
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.
Positive
++
Negative
−−−
(2, 3) represents −1
Two pairs cancel. One negative mark remains.
When do two different pairs count as equal?
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.
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
1 / 2 = 2 / 4
The cross-products match: 1 × 4 = 2 × 2 = 4.
Are the shaded bars the proof?
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
The display comes back. The history does not.
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.
0→1→2↶ back to 0
Steps retained in the record
empty
Display 0. Full count 0.
Worked collision: full counts 2 and 5 both display 2. The display alone cannot tell them apart.
What makes this different from changing circles to squares?
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
A path can record a count.
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 labels count trips around the center. Each drawn line shows the route, which can be followed more than once. This is a planar schematic of the spatial construction.
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.
Going back is another act.
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?
Order of acts in this example
+−
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.
Could one winding record retain every act?
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.
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.
Mathematics describes what recognition necessarily does.
The starting acts belong to reality. Distinguishable occurrences exist. Comparing them requires information about both. Examining an earlier record is itself another occurrence. Recognition Science follows the structure of these acts into physics; δ develops its mathematics.
The connection is explicit in the formal library. A native RS recognition process carries δ’s arithmetic, with truth preserved in both directions. A separate finite recording construction connects physical signal operations to retained marks, readable counts and conserved energy.
The arithmetic connection
Recognition carries the same laws.
Take the native RS process whose successive ratio states are 1, 2, 4, 8, and so on. They represent zero steps, one step, two steps and three steps. RS’s comparison cost, J, vanishes exactly when two states agree.
The start and the step satisfy the counting requirements proved above. Addition and multiplication on these stages obey δ’s recursion laws. Every formula in δ’s arithmetic language has the same truth value here as in its canonical arithmetic interpretation.
Every generated arithmetic theorem accepted by δ’s proof checker therefore holds in this process, with its proof certificate retained.
The recording connection
Physical operations make a count.
In the finite recording model, a prepared pulse writes a mark into an available cell through RS’s signal operation. A successful write increases the readable δ count by one. The specified free evolution preserves the mark and its count.
The proofs follow the same signals through the write, the retained record and the energy accounting. Joining the cell banks adds their counts. The example supplies its pulses, blank cells and readout conditions explicitly.
This gives “actual” a concrete meaning: arithmetic is the necessary structure of these recognition operations. A faithful change of representation preserves it. The research follows that structure into further physical laws, deriving each connection from the operations and conditions involved.
What exactly does the δ–RS proof establish?
The native process proves its own counting properties. Its comparison is J(x/y), which is zero exactly when x and y are equal. The arithmetic formula translation preserves and reflects truth; the generated-theorem result retains the checker’s original certificate.
The result covers the generated natural-number arithmetic language. It uses the equality test supplied by J. Quantitative costs require the separate RS comparison laws and calibration.
The sequence 1, 2, 4, 8, … is one realization. The library also proves the same arithmetic correspondence for every ratio sequence 1, g, g², … with g > 1. The arithmetic does not select a unique value of g. This representation independence is part of what has been proved.
The intrinsic construction and the finite recording model have different scopes. A laboratory recorder still needs the specified preparation, retention and readout conditions. The full identification of all forced mathematical structure with physical reality extends beyond these arithmetic and recording results.
Formal anchors: rsDeltaAlgebra_peano, msatJ_iff_sat and rs_generated_closure in Delta/Physicality/RSDeltaClosure.lean; msatBaseGJ_iff_sat and msatBaseGJ_generator_invariant in Delta/Physicality/RSDeltaBaseCountermodel.lean. These are part of the integrated δ library’s recorded verification of 8 September 2026. This real-valued construction uses Lean’s standard classical foundations.
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.
Keep this halfToo large
13/22
(3/2)² = 9/4 > 2
Steps taken
Interval width
The midpoint squared is greater than 2. Keep the left half. Its width will be 1/2.
What makes this an exact construction?
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.
Why can no fraction equal √2?
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.
δ makes the commitments behind a mathematical construction visible. It distinguishes what finite operations force from what an extension adds. The real numbers provide a concrete example: an exact finite rule, the number it specifies and the completed continuum are three different commitments.
A rule that produces bounds
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.
A number specified by the rule
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.
A completed real number line
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.
Does every refinement rule give a computer program?
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.
Can two numbers always be compared exactly?
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.
Does a finite measurement imply that every physical state has a finite description?
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.
Tracking these additions is part of δ’s result. We can use a continuum description while stating exactly which construction, completeness assumption or decision principle supports the conclusion.
Jonathan Washburn and Milan Lj. Zlatanović. Proves initiality and the unique correspondence between faithful counting structures, constructs the number tower without the axiom of choice, and establishes the exact logical principles needed for its recognition-quotient classification.
Jonathan Washburn and Milan Zlatanović. Proves that identical directed transition tallies can hide different reduced loop words. Separately, no fixed finite-state reader recovers every loop word, while an unbounded stack does. The shortest closed cube walk with trivial abelianization but nontrivial degree-two commutator information has 14 edges. Posted 16 September 2026 as arXiv:2609.19218. Read the paper (PDF) or explore the interactive guide.
Check the constructions
The worked Lean example 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.
