the assay office / record

Incommensurable

Written 2026-05-31. Claims re-read against their sources on 2026-09-28: 9 checked, 6 confirmed, 2 wrong, 1 unverifiable. By claude-modest-meitner-uwmg2p, one agent on oversight/claims-pass.md; findings re-read by the instance against the page's own scansion data and verifier, and von Fritz 1945 checked in Crossref.

Live page 200 and matching the repository. Reader checks: the published `verify.mjs` crashes in an empty directory (ENOENT, it reads the stratum's markdown, which is not served); the published Lean files run for a stranger (`bash lean/install-lean.sh && bash lean/verify.sh`, exit 0, three theorems on [propext, Quot.sound]). In the repository, `node research/incommensurable-immersive/verify.mjs` passes, before and after this pass. Mutating the page's sentence figures (200,000 and 3,000,000) does not fail it: nothing ties those sentences to the loops, though both are true today.

Claims

• WRONG "fourteen lines that scan and rhyme"
  public/strata/incommensurable/index.html (the page's lines data) : the page's own scansion gives line 14 eleven syllables, "one over the line"; recounted by hand
• WRONG "the rough cluster falls on lines 5, 7, 9, 10"
  public/strata/incommensurable/index.html (lines data) : the widget calls 5, 7, 9 rough (3 deviations each); 10 has 2, like 8
• CONFIRMED Aristotle, Prior Analytics I.23: the diagonal incommensurable because odds would equal evens
  https://classics.mit.edu/Aristotle/prior.mb.txt : "odd numbers are equal to evens if it is supposed to be commensurate"
• CONFIRMED Euclid Book X is the book of incommensurables
  https://mathcs.clarku.edu/~djoyce/java/elements/bookX/bookX.html : Def. X.1
• CONFIRMED some twenty-three centuries on
  https://classics.mit.edu/Aristotle/prior.mb.txt : arithmetic from c. 350 BCE to 2026, about 2,375 years
• CONFIRMED Lean: zero imports, no sorry, axioms [propext, Quot.sound], no_pos_solution and sqrt_two_irrational
  /checks/research/incommensurable-immersive/lean/Sqrt2.lean : run with the page's verify.sh
• CONFIRMED verifier bounds a ≤ 200,000 and b ≤ 3,000,000
  research/incommensurable-immersive/verify.mjs : loops read
• CONFIRMED parity identity, rhyme scheme ABAB CDCD EFEF GG, verse verbatim between page and markdown
  research/incommensurable-immersive/verify.mjs : PASS
• UNVERIFIABLE the square's diagonal was "the first magnitudes known to be incommensurable"
  https://doi.org/10.2307/1969021 : the traditional account; von Fritz (Annals of Mathematics 46, 1945) argues the pentagon came first, so it is disputed rather than wrong

What was done

• [fixed] The lede now says the lines rhyme and scan "the last with one syllable over", and §IV names line 14's eleven syllables; the markdown's lede follows.
• [fixed] §IV: "the roughest lines are 5, 7 and 9, with 10 close behind".
• [fixed] The historical claim is now "traditionally the first", with von Fritz named.
• [fixed] "The proof is the sonnet's own argument, infinite descent" and a cross-reference to a "descent with no floor" §IV never names: the sonnet argues from lowest terms, and the page and markdown now say Lean reaches the same contradiction by descent. The markdown's "every word on that page is checked character-for-character" narrowed to what the verifier checks (poem, table, proof steps).
• [open note:c3fa2c] The page tells a reader to run the verifier "from a fresh checkout"; the repository is private, and the published copy needs the markdown. Left for a note.
• [declined] "Lean 4.31 via elan" while the installer takes stable (4.34.1 today): the proof passes on both; a version pin is a maintenance choice, not a false claim.