# A finite recording construction

Five source files accompany the worked example at
https://recognitionphysics.org/mathematics/recorder/ .

Lean version: 4.27.0-rc1.

The files require the integrated IndisputableMonolith library, including
IndisputableMonolith.Foundation.ConservedRecordedCommit and
IndisputableMonolith.Foundation.DeltaTrace. This download contains the teaching
construction; it is not a standalone copy of all imported library dependencies.
The verification receipt identifies the checked source files and direct import
versions by SHA256. Verification used an existing integrated dependency build,
not a fresh rebuild of the whole library.

## Reproduce with the integrated library available

Place these files in one directory. From the integrated project's `lake env`
shell, change to that directory and add it to LEAN_PATH:

```sh
export LEAN_PATH=.:$LEAN_PATH
lean -o FiniteRecording.olean FiniteRecording.lean
lean -o FiniteRecordingEnergy.olean FiniteRecordingEnergy.lean
lean -o RecordingProfile.olean RecordingProfile.lean
lean -o RecordingMachine.olean RecordingMachine.lean
lean --run RecordingFixtures.lean > recording-fixtures.json
```

FiniteRecording: actual recording operation, retained bank, native delta trace,
finite capacity, and an intensity error margin.
FiniteRecordingEnergy: energy conserved by writing, the calibrated split,
a budget for this unary recorder, and addition by joining port lists.
RecordingProfile: exact rational/phase profiles embedded in the actual Signal8
operations, with identical energy, intensity, and native trace readout.
RecordingMachine: executable finite selection of the first zero-amplitude cell;
count, capacity and energy theorems; free evolution of every port.
RecordingFixtures: exact native evaluation of 2,555 write/wait histories.

## Physical scope

The specified protocol supplies prepared input pulses, zero ports, a controller,
isolation under the free evolution, and readout of one mode intensity. It is a
finite mathematical realization of recording in this signal model. It does not
derive an autonomous resource supplier, a laboratory detector, immunity to
other interactions, or a spatial winding device.

The calibrated physical-energy claim uses the integrated conservation theorem:
a norm-like complex signal size, phase and permutation invariance, positive
exponent and gain, and conservation under the specified two-port comparison
for all its inputs. Those conditions force a squared norm up to a positive
scale. The browser uses input-normalized units of that squared norm. The
3/5 and 4/5 amplitudes are chosen normalized inputs, not forced universal
constants. The energy-per-mark bound concerns this fixed unary recorder,
not all possible information storage.

The count is read from intensity in the cells, not an independently incremented
state variable. A new run supplies a new prepared state; resetting the browser
is not modeled as a free physical erasure.