Verification / 16 September 2026

What a retained count preserves.

A forward act and a reverse act have zero net effect on a winding count. They are still two acts. This example connects that distinction to native δ records and the library’s spatial paths.

The counting construction

RetentionLesson.lean uses two instances of the actual Trace type. An act extends one of them. Joining both traces produces the total record; subtracting their lengths gives the net change.

The proof covers every finite sequence of directions. Each act appends exactly one δ mark to the total record. Joining histories joins their directional tallies and adds their net changes. A forward–reverse pair leaves the net change unchanged while retaining two additional marks. Reversing the order of that pair leaves the tallies unchanged, demonstrating that directional counts do not retain order.

The spatial correspondence

RetentionSpatial.lean assigns each tally to the existing winding construction in DeltaRetention.lean. Each channel is a closed path in the specified three-dimensional obstacle complement. Deformations that avoid the obstacle preserve its decoded tally.

Joining the actual paths, using Path.trans, gives the same records as δ append. This is proved before reading their total or net change. A forward–reverse pair in these separate channels cannot deform to the pair representing no acts.

The existing AppendRetention.lean supplies the cancellation result: a deformation-invariant, nonnegative readout that is additive on all concatenations of directed turn paths must be zero. Its proof uses a turn and its inverse. It also establishes the exact boundary for the existing absolute-winding decoder: two paths combine their nonnegative counts precisely when their windings have a common weak sign.

What was checked

All three files compile in Lean 4.27.0-rc1 on the research server. The seven tally theorem reports contain only propext and Quot.sound, or no axioms. The seven spatial reports and eight reports in the cancellation module contain only propext, Classical.choice and Quot.sound. None contains an admitted proof or a new project axiom.

This check compiled the three files against the existing integrated library; it was not a fresh build of the whole framework. The imported DeltaRetention source matches the version already linked in the page’s spatial verification record.

Tally compiler report · Spatial compiler report · Cancellation compiler report

Lean evaluates all 511 direction sequences of length zero through eight. The browser’s two tallies, total and net change agree with these values, including through the actual page controls. The checks also cover resetting, stopping at eight acts and comparing opposite orders. A deliberately incorrect net-change fixture must fail.

Chromium checks cover desktop and narrow layouts, keyboard use and the worked example with JavaScript disabled. Native evaluations · Correspondence checks · Browser checks

What remains to connect

The spatial construction specifies records and their composition. It does not derive an apparatus that writes them from RS dynamics, guarantee a reader’s precision, or provide unlimited storage. Each channel must retain its own directed count. Reversing an action writes in the other channel; it does not erase the first channel.

Retaining the full order of a path is a further problem. The two tallies deliberately discard that information. From One Generator to Loop Order studies richer records that preserve reduced loop words.

Download the three lesson sources and reproduction instructions. The spatial proof requires their existing integrated-library dependencies.