What was
verified.

The formal construction

CounterRecovery.lean imports the existing δ classification and returns an executable recovery value. Its fields contain the index, positive period, proof of the exact classified relation, and search bounds.

• recover performs the two least-witness searches. Its input includes decidable comparisons and an actual collision at counts a < b.
• every_query_within_witness proves that neither search needs a count beyond b. The value’s search_bound proves period + index + 1 ≤ b + 1.
• recovery_predicts proves that reducing a count to its startup or cycle position preserves its observed state.
• stateCongruence derives the required compatibility with further events from a fixed update on the complete state.
• orbit_recovery_correct and orbit_recovery_predicts connect the result to native δ records through the library’s proved additive equivalence.

The construction and all eight printed declarations compile without sorry, new axioms, or Classical.choice. The recovery and native-record theorems depend on Lean’s propext and Quot.sound; the prediction theorem uses propext; the fixed-update construction has no axiom dependencies. These statements concern the checked declarations, not every theorem in the imported library.

The standalone source package contains six unchanged δ modules, the lesson, and pinned Lean and Mathlib versions. All six modules were rebuilt in that package using the existing dependency cache. Lean: v4.27.0-rc1. Mathlib: d7ea5678e6d426e87e9b4a65a48143c4874dc501.

The executable checks

The Lean construction evaluates 450 examples covering starting indices 0–4, periods 1–5, six collision offsets, and three positive multiples of the period. The JavaScript search agrees with every recovered index, period and comparison count. Its queries stay within the witnessed bound.

A second check enumerates every transition function on one through five labelled states, starting from state 0: 3,413 machines. Recovery agrees with an independently implemented Floyd cycle finder. Predictions agree with direct iteration through tick 39, and later collisions recover the same structure. This is a correspondence test, not a speed benchmark.

A negative control supplies a misleading display: four internal states show 0, 1, 0, 2. The repeated zero has different next displays. Treating it as a complete state produces the predicted failure at tick 3.

The page

The DOM checks cover all four presets, both collision options, 36 prediction counts for each combination, custom controllers including 32-state limits, invalid inputs and recovery after correction. Every input has a label; results expose live status messages.

Chromium checks cover 1280, 390 and 320 pixel widths, including a 32-state cycle. Selected keyboard paths exercise the disclosure, button and native selection. With scripts disabled, the worked default example remains readable and inactive controls are hidden.

Reproduce or inspect

The machine-readable report includes receipts, axiom output and source hashes. The Lean-generated values, model checker and DOM checker are available alongside the application. The source package README gives the Lean commands. Run the model checker with Node and the fixture path; the DOM checker also needs jsdom and a directory containing this page and its two scripts.

The formal theorem assumes the comparison law stated in its inputs. The supplied transition table establishes that law for this model; a finite observed trace alone cannot establish it for an unknown physical device. The tests do not prove correctness of every browser, establish hardware behavior, or measure a reader’s understanding.