Actual Mathematics / Verification

The finite recording example.

Writing moves a signal component into a cell; waiting advances the model’s free evolution. The browser represents both operations exactly in the integrated signal model and reads the count from the cells.

What Lean checks

The construction uses the existing reversible recording operation, its retained component and its energy conservation theorem. The finite bank connects those operations to the native δ trace:

• A prepared pulse and a blank cell produce an outgoing signal and a retained mark.
• A successful write increases the readable count by one and preserves the number of cells.
• Free evolution preserves each written mark, the read count and the total energy.
• Input energy divides into 9/25 stored and 16/25 outgoing for the chosen 3/5, 4/5 pulse.
• The complete budget includes unused pulses, stored marks and outgoing signals.
• Joining two banks adds their counts. A fixed threshold distinguishes the two prepared cell states with an explicit error margin.

The rational and phase representation used in the browser is embedded in the actual eight-sample complex signal space. The proofs establish agreement for writing, free evolution, intensity, energy and the native δ trace readout.

What was verified

Four teaching modules compiled with Lean 4.27.0-rc1 against an existing integrated dependency build. All 29 reported theorem dependencies contain only the standard axioms propext, Classical.choice and Quot.sound, or a subset. None contains sorryAx or a project-specific axiom. This was not a fresh rebuild of the whole library.

A fifth source file evaluates 2,555 histories directly in Lean: every write/wait sequence of length zero through eight, for five combinations of input supply and cell capacity. The JavaScript results match every signal profile, phase, count and energy budget. All 511 histories with six pulses and six cells also pass through the page controls. A deliberately incorrect energy fixture is rejected.

Chromium checks cover 1280, 390 and 320 pixel widths, the initial and full banks, keyboard operation, phase changes, the energy diagram and content without JavaScript. The screenshots were visually inspected. These checks are not a study of reader comprehension or a full assistive-technology audit.

Scope of the physical claim

The protocol supplies the normalized pulses, blank ports, selection of a fresh cell and access to an intensity reader. Retention is proved under the specified free evolution. Other interactions, building the detector and autonomous resource preparation are outside this example.

The energy derivation starts from a norm-like complex signal size, phase and permutation invariance, a positive exponent and gain, and conservation under the specified two-port comparison for every input. Under those conditions the source theorem forces a squared norm up to a positive scale. The example measures energy relative to one prepared pulse.

The amplitudes 3/5 and 4/5 are a chosen normalized preparation. Their energy split is derived from that choice; it is not a universal constant. The storage budget applies to this unary recorder. It does not establish a minimum energy cost for all memory, a working laboratory device or the full equivalence between forced mathematics and physical reality.

Sources and verification records

The full Lean teaching sources are maintained privately. The public records identify what was checked; read the verification scope.

Compiler outputSource hashesNative fixturesBrowser comparisonBrowser checks