Actual Mathematics / A worked example
A count needs somewhere to stay.
An event can pass. A count requires something that remains. Here is a finite signal model that turns prepared pulses into lasting marks and accounts for the energy at every step.
← Mathematics and physical realitySix pulses · Six cells
Make a record.
read
- #1
- #2
- #3
- #4
- #5
- #6
- Blank
- Blank
- Blank
- Blank
- Blank
- Blank
- No outgoing pulses yet
- Unused input
- 6.00
- Stored marks
- 0.00
- Outgoing signals
- 0.00
- Total energy
- 6.00
Six prepared pulses and six blank cells. Each successful write moves 0.36 energy units into a cell and leaves 0.64 in the outgoing signal.
The small hands show signal phase. A written cell stays fixed under the model’s free time evolution. “Start again” supplies a new example; it does not simulate a physical erasure.
01 / Retain a distinction
The mark survives
the passing signal.
Each pulse has two components. The write operation routes one into a blank cell. The other leaves through an output. Under the model’s free evolution, that outgoing component changes phase; the recorded component stays fixed.
A reader scans the cells and adds one δ mark for each signal above a fixed intensity threshold. The displayed count comes from those cells. It is not a separate counter that remembers how many times you clicked.
Writing to a fresh cell matters. Reusing the same cell with the reversible operation can return its stored component to the other port. A device that keeps counting needs a supply of blank cells and a controller that selects them.
02 / Account for the resources
Nothing appears
for free.
After six writes, the cells contain 2.16 units and the outgoing signals contain 3.84. The total is still six. The recorder is full: another event needs another prepared pulse and another blank cell.
These numbers describe this pulse and this recorder. They are not universal constants or a minimum energy cost for every possible memory.
What the example establishes
A number read
from retained acts.
The construction connects an explicit signal operation to a retained difference, a readout and a δ record. It shows how counting can follow from what a specified system does, with finite capacity and supplied resources made visible.
The proof establishes a finite model. A laboratory realization would need a way to prepare and route the pulses, supply blank cells, protect stored records from other interactions and read their intensity. The result advances the bridge to physical reality without establishing the full claim that all forced mathematics is physically real.
How the reader distinguishes blank from written
The reader measures the intensity of the retained component. A blank cell gives 0; a written cell gives 9/25. It writes one δ mark when the reading is greater than 9/50, halfway between them.
The proof also covers imperfect readings: any intensity error strictly smaller than 9/50 preserves this classification for the two prepared states. It does not assert that an actual detector meets that bound.
What the animation represents
The signal has eight sample positions. This example uses two Fourier components of that signal. Their amplitudes are exact fractions, and their phase changes by a fixed eighth-turn. The Lean embedding proves that the operations used here agree with the integrated model’s write operation and free evolution.
“Send one pulse” applies one write step to the selected pulse and the first blank cell. Other ports are unchanged. “Advance time” applies one free step to every port. Phase is shown modulo eight; the underlying phase count is retained.
The illustration uses exact symbolic states. It does not simulate environmental noise, material hardware or quantum measurement probabilities.
Read the proofs
Lean checks that writing conserves energy, preserves the bank’s capacity and adds one readable mark when a prepared pulse reaches a blank cell. Free evolution preserves both the count and the energy. The browser code is compared with states evaluated directly by Lean.
Verification and source →Download the Lean construction ↓