Verification / 16 September 2026
Checking the construction beneath counting.
The lesson has two kinds of checks: Lean checks the mathematical statements, and browser tests check that the controls show the corresponding examples.
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 establish independence of these particular conditions. They are not presented as new historical discoveries about Peano arithmetic.
FormationLesson.lean imports four unchanged native δ modules. The complete source package includes them, a README, the pinned Lean toolchain and the dependency manifest. After installing Lean, follow the README to fetch the pinned dependencies, build the modules and compile the lesson.
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 linked 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 two files belong to the integrated research library and need its dependencies. Unlike the counting package, they are not a standalone build.
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 page reuses that receipt; it does not represent it as a fresh build of the whole geometry. 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 general equivalence between forced mathematics and physical reality remains a research target.