appendix sectiontutorials

ch:real-numbers: ch:real-numbers

Problem and invariant. Bisect dyadic brackets for the positive square root of two. Represent a bracket by $(l, u, d)$ and maintain $l^{2} < 2 d^{2} < u^{2}$ .

Two representations. One can implement normalized rational numbers with signed numerators. The companion uses natural numerators over a shared positive denominator. The rational representation is reusable; the shared-denominator representation makes each bisection and invariant check an exact natural calculation.

First complete version. Given $(l, u, d)$ , represent the midpoint by $(l + u) / (2 d)$ . Compare $(l + u)^{2}$ with $2 (2 d)^{2}$ and retain the half whose endpoints still straddle $\sqrt{2}$ . Starting from $(1, 2, 1)$ , check the three results $(2, 3, 2)$ , $(5, 6, 4)$ , and $(11, 12, 8)$ together with the square invariant.

Observable result. The accepted corpus prints four named PASS lines and then All 4 Chapter 196 corpus cases passed.

A failing version. Omit the factor two on the right side of the midpoint comparison. This mutation still typechecks, but the second and third bracket oracles change and the inline test exits nonzero.

Acceptance test. Run the four commands in appendix E. Require a silent check, one passing inline test, the exact five-line run transcript, and an empty audit. Restore the accepted source after replaying the mutation and repeat all four commands.

Mathematical boundary. The program checks three finite instances of the locator-driven nested-bracket refinement used in the proof of theorem 74.72, including the strict-square invariant at every endpoint. It does not construct a Dedekind real and does not prove the general Cauchy-completeness theorem theorem 74.67.