A proof and a sonnet are two forms that share no common measure. What follows sets one down inside the other so that each stays wholly itself — fourteen lines that scan and rhyme, and a proof that holds step for step — and then gives an honest accounting of every place the two pull against each other. The seam is the subject.
Touch any line of the poem to light the proof step it carries and the seam where the form presses on it. Touch a proof step to light the lines that do its work. Then turn on the toggles.
The poem leans twice on a fact it never proves — an even square has an even root — pointing at it with as we declared (line 7) and so implied (line 11). The verse can name the lemma; only the column beside it can discharge it. Here it is, and here you can run it: an odd number is 2k + 1, and (2k + 1)² = 2(2k² + 2k) + 1 is odd — so an even square can never come from an odd root.
The square keeps the parity of its root. Try to break it.
The claim is one of the oldest in mathematics: no fraction, however large its terms, has a square equal to 2. The argument is a reductio — assume, build, collide, withdraw. Above, each numbered step is hinged to the lines that carry it; here it is in plain symbols.
Two lines do no logical work. Line 6's and more— is filler that exists to reach a rhyme; line 12 is pure restatement. They are here because a Shakespearean sonnet wants three quatrains and a couplet, and the proof's skeleton has fewer than twelve joints — so the form has slack, and slack fills with ornament. I have left them rather than disguise them. The apparatus is the point. (Turn on logical load above to see which lines are doing work, which are echoing, and which are pure form.)
The real strain is the parity lemma. The verse leans on it twice and proves it neither time — that is not a flaw to hide but a division of labour, discharged in §II. Where the sonnet says as we declared and so implied, read it as a pointer to the column. The two are one argument; neither is complete alone.
Metrically, the place where the mathematics is densest is exactly the place the meter breaks — and that correspondence is worth more than a clean foot. Turn on scansion and watch it: the setup quatrain (lines 1–4) and the two slack lines (6, 12) run smooth iambs; the rough cluster falls on lines 5, 7, 9, 10 — square both sides, the parity lemma, substitute, halve — the working core of the proof. Line 5 opens on a spondee (Then square:), two stresses where the meter wants one, the most audible seam in the poem.
One thing here is not a computation. The marks you turn on are a scansion — one defensible reading, not a fact. Stress in English verse is partly given (a dictionary fixes be·HIND, com·MON) and partly performed: a skilled reader could foot a line differently, especially the variable-names (a, b, c take an ictus here that a bare letter would not) and the line-initial inversions (thus, But). The rule used: lexical stress for polysyllables; content words stressed and function words unstressed among the monosyllables; and the iambic ideal placed under it for contrast (a weak beat on the odd positions, a strong beat on the even). The marked deviations are read off that grid.
So the robust claim is local, and it survives any reasonable re-scansion: line 5 opens on two adjacent stresses where an iamb wants weak-then-strong, and that is the line where the algebra (a² = 2b²) first lands. The wider pattern — roughness clustering on the working lines, smoothness on the slack ones — is offered as a reading you can inspect and argue with, not a measurement. Everything else on this page is checked by machine; this one layer is labelled a reading because that is what it honestly is.
And the title is not decoration. The irrationality of √2 is the discovery that the diagonal of a square shares no common measure with its side: the first magnitudes known to be incommensurable. The result is ancient — Euclid's Elements, Book X — and Aristotle, in the Prior Analytics, alludes to a reductio of just this shape, proving the diagonal incommensurable by forcing odd numbers to come out equal to even. The parity collision in the couplet above is, in spirit, that same odd-and-even contradiction, some twenty-three centuries on, wearing a rhyme.
Everything in the verifier below recomputes the arithmetic — but a program can only ever test finitely many cases. It checks the parity lemma for n below 200,000, and that a² = 2b² has no solution for b below 3,000,000. That is corroboration, not proof: the claim is about every integer, and no amount of sampling reaches the end of the number line.
So the descent has now been handed to a proof assistant, which settles all of them at once. research/incommensurable-immersive/lean/Sqrt2.lean proves in Lean 4, for every pair of natural numbers a and b, that a² = 2b² ⟹ b = 0 — and hence that no positive a, b satisfy it at all, which is to say √2 is not a/b for any whole numbers. The proof is the sonnet's own argument, infinite descent, made mechanical: a positive solution forces a even, a = 2c, hence b² = 2c² with c = a/2 strictly smaller than b — a smaller solution wrung from any solution; and because the naturals cannot descend forever, the only solution is the trivial zero. This is exactly the “descent with no floor” §IV names.
The file has zero imports — no library, only Lean's kernel — so the one thing you must trust is the type-checker itself. The axiom footprint of every theorem is [propext, Quot.sound]: no sorry, no classical choice, nothing smuggled in. Reproduce it from a fresh checkout in a minute or two: bash research/incommensurable-immersive/lean/install-lean.sh then bash research/incommensurable-immersive/lean/verify.sh. What the sonnet argues in fourteen lines, the kernel now certifies for all integers without exception — the third machine-checked layer in this ground, after the zero-one principle and Nim's XOR theorem.
incommensurable.md; the parity lemma, the even-square⇒even-root step, and the bottom line that a²=2b² has no solution (b up to 3 × 10⁶) are checked by exact integer arithmetic; the poem is 14 lines rhyming ABAB CDCD EFEF GG; and the descent itself is machine-checked in Lean (zero imports; axioms [propext, Quot.sound], no sorry, no choice — §VI). Recompute from a fresh checkout:node research/incommensurable-immersive/verify.mjs