Verification / 16 September 2026
Checking the square-root construction.
The example connects an executable refinement rule, the library’s interval structure, native δ ratio records and the real number √2. Its mathematical proofs and browser checks establish different things.
The mathematical statements
The algorithm starts at [1, 2]. It squares the rational midpoint and keeps the appropriate half. Each interval has nonnegative ordered endpoints whose squares bracket 2. Successive intervals nest, and the width after n steps is exactly 1/2ⁿ. For every positive rational error allowance, some finite step has a smaller width.
RefinementLesson.lean constructs an actual DeltaReal.Protocol: its intervals satisfy the library’s required width bound, 1/(n+1). A separate theorem identifies the protocol’s real-valued interpretation as √2, and the standard irrationality theorem shows that it equals no rational number.
For each rational bound, the lesson builds a native RatioOrbit from signed counting records and a nonzero denominator. Theorems establish that displaying this record returns the original rational and that native multiplication displays its square. The browser is therefore checked against the formal construction’s own ratio records.
This is a worked application of the familiar bisection method, not a claim to have discovered that algorithm.
What the proof uses
The eight printed theorem reports contain only propext, Classical.choice and Quot.sound. There are no admitted proofs or new project axioms in these dependencies. This is not an empty-axiom result. The formal setting includes Lean’s type theory and Mathlib’s rational and real arithmetic.
The interval algorithm is computable and never queries a real-number value. Its interpretation as a point of the usual real line uses the library’s noncomputable value map, defined using real completeness. The general interval interface also permits noncomputable sequences; its representation theorem for all real numbers does not supply a finite program for every real.
The complete source package contains the lesson, six unchanged δ modules, pinned dependency metadata and reproduction instructions. It was built independently on the research server. Read the compiler output and axiom reports.
What the browser checks
Lean evaluates thirteen steps, from 0 through 12, including each pair of bounds, midpoint, next-half decision and native-ratio displays. The browser uses exact integer arithmetic. Its values and controls are checked against every fixture, including moving the precision slider backward, resetting and stopping at the demonstration’s limit.
A deliberately wrong fixture must fail the comparison. Chromium checks cover all thirteen states at desktop and narrow widths, keyboard use, and the static explanation with JavaScript disabled. These checks establish the tested implementation correspondence, not human comprehension or a physical realization of an unbounded computation.