Mathematics from distinction

Checking the lesson.

The lesson has two parts to verify: the mathematical statements in Lean, and the browser implementation that draws and manipulates the records. These were checked separately on 16 September 2026.

The formal construction

ArithmeticLesson.lean imports the native δ number, signed-pair and ratio definitions. It proves the worked calculations, the equality of the signed pairs (2, 3) and (4, 5), the equality of 1/2 and 2/4, and the inequality of 1/2 and 2/3. It also proves that converting a record to its numeral and back recovers the record, while the three-position counter sends distinct records to the same display.

Download the complete lesson proof package. It contains the five unchanged library modules needed by the lesson, the lesson source, a minimal build configuration, and a pinned dependency manifest. The package compiled separately from the larger research repository, using cached dependencies. Its README gives the commands to repeat that check.

The toolchain is leanprover/lean4:v4.27.0-rc1. Mathlib is pinned to d7ea5678e6d426e87e9b4a65a48143c4874dc501.

What the axiom report means

The concrete sum, product, signed-pair balance, fraction comparisons and counter non-injectivity proofs print an empty axiom list. The general record–numeral recovery proof uses propext. The general counter–remainder proof uses propext and Quot.sound. None of these lesson proofs uses sorryAx or a newly declared axiom.

Lean’s type theory, inductive constructions and rules of inference remain the setting in which those results are checked. An empty printed axiom list does not mean a proof has no logical setting.

The interactive implementation

Lean evaluates the native δ operations to produce a comparison fixture. The browser correspondence check compares the JavaScript operations and rendered results with that fixture. It covers all choices offered by the controls: 81 addition pairs, 49 multiplication pairs, 81 signed pairs, 1,764 fraction comparisons and 13 counter histories. The operation check also covers multiplication through 8 × 8, beyond the picture’s six-group limit.

Checks include zero, unequal fractions, a rejected zero denominator, cancelling pairs, input limits, reset buttons, and changing circles to squares without changing the result. All pass. The browser checks use Node.js and JSDOM; the test source requires the jsdom package.

Chromium checks also pass at widths of 320, 390 and 1,280 pixels. Buttons, number selections and proof disclosures were operated by keyboard. With scripts disabled, the worked examples remain visible and the interactive controls are hidden. Desktop and phone screenshots were inspected for clipping and legibility.

These checks establish correspondence over the displayed examples and the tested interaction paths. They are not a formal verification of every JavaScript runtime, an assistive-technology audit, or a study of reader comprehension.

Read the check results and source hashes.

What follows from this

The worked example connects visible operations to the framework’s actual definitions and proofs. It establishes that faithful changes of representation preserve the count, and that the counter’s coarser equality loses information. The broader claim connecting distinction to physical reality requires its own argument; it is not inferred from the browser test.