Verification / 16 September 2026
Checking the square-root construction.
Repeatedly halve a rational interval while keeping √2 between its endpoints. The proof connects this executable rule to native δ ratio records and the real number √2; the browser checks compare each displayed step with Lean’s evaluation.
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.
The example applies the familiar bisection method to the library’s interval and ratio constructions.
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. The proof uses Lean’s type theory and Mathlib’s rational and real arithmetic, including those named axioms.
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 lesson and its six unchanged δ dependencies were built independently on the research server using pinned dependencies. 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.