Verification / 16 September 2026
Checking the construction beneath counting.
The proof identifies exactly when a start-and-step structure preserves counting. Browser checks then compare the interactive examples with values evaluated by Lean.
What the proof establishes
For the library’s start-and-step structures, the map from δ records is both injective and surjective exactly when the structure satisfies the three Peano-model conditions. These are separation of the start from a successor, injectivity of successor, and induction over the structure. The translation preserving start and step is unique.
Three explicit structures each satisfy two conditions and fail the third: a three-state cycle, a two-state saturated counter, and the ordinary counting path with one additional, unreachable state. These familiar counterexamples establish that none of the three stated conditions follows from the other two.
FormationLesson.lean imports four unchanged native δ modules. Compiling the lesson requires those integrated-library dependencies and the pinned Lean toolchain.
The six theorem axiom reports are empty. That result concerns named axiom dependencies; Lean’s type theory, inductive formation, equality, recursion and elimination rules remain the setting of the proof. Read the compiler output.
What the browser checks
Native Lean evaluation supplies thirteen counts for each of the four models. The JavaScript and the rendered controls are compared with all 52 combinations. Tests also check resets, limits, changes of model, the unreachable state, condition labels and proof links.
Chromium checks cover desktop and narrow screens, keyboard interaction and the examples with JavaScript disabled. A deliberately incorrect fixture is rejected by the comparison test. These are implementation checks, not a study of human comprehension.
Native evaluations · Correspondence results · Browser results
The spatial construction
The geometry uses the complement of a fixed circular trace in three-dimensional space. A unary δ record is encoded by a path’s winding around that excluded trace. Decoding recovers the record; allowed continuous deformations preserve it. Actual path concatenation realizes record append up to free deformation.
The page’s flat drawing is a schematic. Its labels count traversals. It does not claim that a still image of a circle distinguishes one trip from two, or that a finite physical device stores every natural number.
DeltaTrace.lean gives the records; DeltaRetention.lean gives the spatial encoding and concatenation proof. These modules are maintained in the private integrated research library.
Their SHA-256 hashes match the successful integration receipt dated 8 September 2026. That run checked 102 declarations across three bridge modules, with permitted dependencies on propositional extensionality, classical choice and quotient soundness. This report relies on that integration run for the spatial construction. Inspect the source comparison and receipt scope.
A physical implementation must provide the excluded obstacle, retain the path and its traversal count, permit the specified readout and implement joining. The theorem establishes the mathematical correspondence under those conditions. The full identification of all forced mathematical structure with physical reality extends beyond this spatial construction.
Related physical constructions
The mathematics account also includes a native RS realization that preserves and reflects arithmetic truth, and a finite recorder construction under specified write and readout conditions. This receipt verifies the lesson described here; the physical correspondence results have their own sources and verification records.