--- slug: the-missing-square passed: 2026-10-14 by: the assay line (research/assay-line/cited-1014b/), Codex fixer directed by claude-assaying-boyle-1014; source record by Codex, checked by Codex checked: 114 confirmed: 99 wrong: 15 unverifiable: 0 observed: 0 stale: 0 --- This was the 2026-10-14 directed fixer pass for the-missing-square at f5e5f84f34, following research/assay-line/cited-1014b/the-missing-square/triage.json. I reread each triage item's evidence before editing, including the actual geometry code, retained source texts and the scan of Simson p. 369. The record carries one line for each of the 15 triage items and the 99 CONFIRMED claims reread by the source checker in N2-codex.md; those inherited notes describe that checker's work, with entries 100 and 104 updated to the corrected current wording. The wrong count includes 6 WRONG and 9 MINOR claims. After the 2026-10-14 repair review, five findings are fixed, eight listed MINOR findings are declined as directed, and X1 and X15 remain open for copies in another layer; no WRONG claim is declined. The local corrections remain in place. ## Claims - WRONG | X1 "Below is an 8×8 board" […] "64 unit squares, you can count them. It is cut into four pieces: two triangles and two trapezoids, with edges of length 3, 5, 8 and 13" […] "consecutive Fibonacci numbers." | public/strata/the-missing-square/index.html (pieces); research/the-missing-square/verify.mjs | Re-evaluated the authored pieces(3,5): triangle squared edge lengths are 9,64,73 and trapezoid squared edge lengths are 9,25,25,29. No edge is 13; w=(3+5)+5=13 is the assembled frame width. Corrected the lede and relation note. - WRONG | X2 "The trick survives slow motion. The pieces don't stretch, don't overlap, don't leave a visible hole" […] "and yet 64 of something has become 65 of the same something." | public/strata/the-missing-square/index.html (pieces and morph); research/the-missing-square/verify.mjs | At u=0.5, (1,2.75) is strictly inside pieces 0 and 2: oriented edge cross-products are [2,21,1] and [13.2582521472,12.3483495706,9.9739808998,4.4194173824], all positive. The rigid motion preserves area. The no-overlap statement now applies only to the finished n=6 arrangement. - MINOR | X3 "Even n: the rectangle gains a unit (a gap)." | https://www.cut-the-knot.org/Generalization/CevaPlus.shtml | The N1 excerpt records absolute error only. The complete signed Cassini identity, with this page's F(1)=F(2)=1 convention, gives rectangle minus square = (-1)^n. Even n therefore gives +1. The source-record precision issue remains MINOR; no page change. - MINOR | X4 "And as n grows, the consecutive ratios race toward the golden ratio φ = 1.618…" […] "so the two mismatched slopes converge, the lozenge narrows, and the swindle becomes, for the eye, perfect." | https://mathworld.wolfram.com/DissectionFallacy.html; git show f5e5f84f34:public/strata/the-missing-square/index.html; https://mathshistory.st-andrews.ac.uk/Biographies/Simson/; research/the-missing-square/verify.mjs | MathWorld supports the improving illusion but its cited excerpt does not state the ratio limit. MacTutor's Simson biography states that adjacent Fibonacci ratios approach the golden ratio. The page assigns phi to consecutive ratios, not to the slopes, so this sentence is correct. The recurrence yields F(n)=(phi^n-psi^n)/sqrt(5), psi=(1-sqrt(5))/2, and abs(psi/phi)<1, establishing the ratio limit and hence the slope limit phi^-2. - MINOR | X5 "This joins the Wasteland's other machine-checked strata" […] "the irrationality of every non-square root and why the pentagon can't tile, where the same golden-ratio wall (5 is not a perfect square) does its other day-job." | git show f5e5f84f34:src/content/strata/seventeen-and-no-more.md; git show f5e5f84f34:research/crystallographic-restriction/lean/CrystallographicRestriction.lean | The sibling's no_order_five theorem assumes an integer matrix with determinant one and M^5=I, and concludes M=I. Its nonsquare-5 argument forbids a fivefold lattice rotation; this is not a general pentagonal tiling theorem. Retained as the triage's MINOR description of the linked check's scope. - MINOR | X6 "The honest apparatus" […] "every claim with its source, every uncertainty named rather than smoothed over." | research/assay-line/cited-1014b/the-missing-square/N1-sources.json (mitchell-garbling); public/strata/the-missing-square/index.html | N1's mitchell-garbling entry explicitly has source: none and records unsuccessful provenance searches. This limits the every-claim sourcing promise but does not establish that the tentative garbling conjecture is false. Local apparatus wording retained as directed. - MINOR | X7 "First in print: Oskar Schlömilch, "Ein geometrisches Paradoxon," Zeitschrift für Mathematik und Physik 13 (1868), p. 162." | https://pt.slideshare.net/slideshow/recreation-mathematics/34140548; https://www.cs.purdue.edu/homes/gnf/book/Booknews/ch23.html | Singmaster's printed p. 15 actually says Otto; the original quotation in N1 remains intact. Frederickson's chapter 23 updates identify Oskar Schlömilch, both in the chessboard discussion and the biographical heading. The page's Oskar name is supported; the discrepancy belongs in this annotation rather than a page correction. - MINOR | X8 "H. S. M. Coxeter (1953) mistakenly credited the 1868 article to Schlegel" […] "a documented mix-up, now resolved in Schlömilch's favour." | https://www.puzzlemuseum.com/singma/singma6/SOURCES/singma-sources-edn8-2004-03-19.htm | The retained Singmaster section 6.P.1 says this seems right and apparently confusing. His Vanishing Area Puzzles, p. 15, preserves those qualifications. Those sources support a likely Coxeter confusion but do not justify the page's unqualified resolved-mix-up wording. Listed as MINOR excess certainty, as directed. - WRONG | X9 "the first to connect the construction to the Fibonacci numbers." | https://pt.slideshare.net/slideshow/recreation-mathematics/34140548 | Read Singmaster's Vanishing Area Puzzles, printed p. 15: it dates recognition to 1877 and identifies the relevant dimensions as consecutive Fibonacci numbers. Reference [4], printed p. 19, names Darwin's 1877 paper. This contradicts first priority for Schlegel in 1879; the revised text names prior recognition without naming a new first discoverer. - WRONG | X10 "Whether Simson's 1753 paper stated the identity itself, or only the fact that consecutive Fibonacci ratios approach φ, is a genuine disagreement: the Fibonacci-identity literature credits him with the identity, while Simson's biographies (MacTutor; Wikipedia) describe only the golden-ratio limit." | https://archive.org/download/paper-doi-10_1098_rstl_1753_0056/paper-doi-10_1098_rstl_1753_0056.pdf | Visually reread the retained scan of Simson's 1753 paper, printed p. 369 (PDF page 2). It states the alternating unit difference, illustrates it with 8^2 versus 5*13 and 13^2 versus 8*21, and proves both induction cases. Removed the alleged disagreement and contested labels. The reported lack of access at publication remains explicitly dated 2026-06-30. - WRONG | X11 "Simson's biographies (MacTutor; Wikipedia) describe only the golden-ratio limit." | https://mathshistory.st-andrews.ac.uk/Biographies/Simson/; https://en.wikipedia.org/w/index.php?title=Robert_Simson&oldid=1342966250 | The retained API response for Wikipedia revision 1342966250 has timestamp 2026-03-11T14:36:12Z and known_for includes Simson's identity. It predates the June publication. MacTutor's prose discusses the ratio limit, but the claim that both biographies describe only that limit is false. Corrected with X10 in one dated notice. - MINOR | X12 "Every number on this page is recomputed from scratch by verify.mjs" | git show f5e5f84f34:research/the-missing-square/verify.mjs | Read the whole verifier. It computes a slope difference with Math.abs but contains no Math.atan and no displayed-angle check. Qualified the footer and matching local scope statements to the listed mathematical checks; the live table claim now names that table. This MINOR fix has no correction notice of its own. - MINOR | X13 "The other place the number 5 builds a wall: there, 5 not being a perfect square forbids the pentagon from tiling; here, the Fibonacci ratios built from 5 and φ." | git show f5e5f84f34:src/content/strata/seventeen-and-no-more.md | The sibling explicitly connects the nonsquareness of 5 to excluding a fivefold lattice rotation. Its integer-matrix theorem does not prove a general pentagonal tiling prohibition. This is the same linked-proof scope overstatement as X5 and is retained as MINOR per triage. - MINOR | X14 "is spread along a diagonal nearly 95 units long, so its width is about a hundredth of a unit." | public/strata/the-missing-square/index.html (lozPts); src/content/strata/the-missing-square.md | The n=10 gap vertices are (0,0),(55,21),(89,34),(34,13). The long diagonal is sqrt(9077)=95.2732911156; area/diagonal gives mean width 0.01049612108798, while maximum transverse width is 0.02099224217596. About a hundredth is correct for mean width. The missing convention is MINOR, so the page stays unchanged. - WRONG | X15 "the slopes converge to φ and the gap becomes invisible, but Cassini proves it never closes." | public/strata/the-missing-square/index.html (drawMini); research/the-missing-square/verify.mjs | The actual slopes are F(n-2)/F(n) and F(n-3)/F(n-1), both tending to phi^-2=(3-sqrt(5))/2=0.3819660112501051. Recomputed at n=30: 0.38196601124945917 and 0.38196601125179636. Their difference tends to zero; consecutive Fibonacci ratios tend to phi. Corrected the relation note, markdown footer and verifier heading; its comment now names the implemented slope pair. - CONFIRMED | "Cut a 64-square into four pieces. Rearrange them into a rectangle. Count again: 65. One square has come from nowhere" […] "so where is it?" | git show f5e5f84f34:public/strata/the-missing-square/index.html | 001 opening-paradox. Read as the stated illusion, resolved below it: the source defines the two frames as "H8" and "H13"; the unchanged pieces total 64 and the target frame has area 65. - CONFIRMED | "Slide the control, and the four pieces rearrange into a 5×13 rectangle." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 003 rearrangement-control. "uIn.addEventListener" calls "drawMain"; the four rigid motions end at the 13 by 5 frame, with the disclosed unit gap. Recreated from the pinned script in audit_page.mjs. - CONFIRMED | "A 5×13 rectangle has area 65." | git show f5e5f84f34:research/the-missing-square/verify.mjs | 004 rectangle-area. The calculation "F[5] * F[7] === 65n" passes; 5 times 13 is 65. - CONFIRMED | "The same four pieces. One more square." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 005 same-four-pieces. The source uses "morph(pc, u)" on the same four polygons. Areas remain 12, 12, 20, 20; the extra unit belongs to the surrounding frame. - CONFIRMED | "An 8 by 8 square of area 64 dissected into four pieces that rearrange into a 5 by 13 rectangle of area 65." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 006 stage-accessible-description. The accessible label accurately names the source square and target frame dimensions in the context of the subsequent gap explanation. Coordinates in "pieces(3, 5)" reproduce them. - CONFIRMED | "Show the gap, finish the rearrangement, and look along the rectangle's diagonal." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 008 gap-control. The "gapBtn.addEventListener" handler changes "showGap" and redraws. Recreated at u=1: the disclosed polygon has the four stated corners and its label is displayed. - CONFIRMED | "The pieces almost meet along the rectangle's diagonal, but not quite." | https://mathworld.wolfram.com/DissectionFallacy.html | 009 edges-almost-meet. The source says the edges "have distinct slopes". Its image alternatives supply 2/5 and 3/8; the pinned coordinates independently reproduce the gap. - CONFIRMED | "What looks like one straight cut is really two edges with slightly different slopes, and between them lies a long, impossibly thin parallelogram" […] "a sliver of area exactly 1." | https://www.cut-the-knot.org/Generalization/CevaPlus.shtml | 010 sliver-shape-area. The source says "a narrow parallelogram is left uncovered". Its Pick argument and the pinned integer shoelace calculation both give area 1. - CONFIRMED | "That sliver is the missing square. It was never gone; it was rolled out into a splinter the eye refuses to register." | https://mathworld.wolfram.com/DissectionFallacy.html | 011 sliver-invisible. The source attributes the illusion to "tiny, negligible imperfections of shape". This is the same concealed area, rather than destroyed material. - CONFIRMED | "the triangles' long edgerise / run = 3 / 8 = 0.3750" | git show f5e5f84f34:research/the-missing-square/verify.mjs | 012 triangle-slope. The verifier defines "const slopeTri = 3 / 8" and reproduces 0.375 exactly. - CONFIRMED | "the trapezoids' slanted edgerise / run = 2 / 5 = 0.4000" | git show f5e5f84f34:research/the-missing-square/verify.mjs | 013 trapezoid-slope. The verifier defines "const slopeTrap = 2 / 5" and reproduces 0.4 exactly. - CONFIRMED | "the rectangle's true diagonal5 / 13 = 0.3846… (lies between them)" | git show f5e5f84f34:research/the-missing-square/verify.mjs | 014 diagonal-slope. The verifier defines "const slopeDiag = 5 / 13"; 0.375 < 0.3846153846 < 0.4. - CONFIRMED | "Because 3/8 ≠ 2/5, the four pieces' edges do not lie on one line." | git show f5e5f84f34:research/the-missing-square/verify.mjs | 015 noncollinear-edges. The source checks "slopeTri !== slopeTrap". The two rational slopes differ by 1/40, so their segments cannot be one line. - CONFIRMED | "The gap between them is the lozenge with corners (0,0), (8,3), (13,5), (5,2); its area, by the shoelace formula on whole-number coordinates, is |2|/2 = 1" […] "exactly." | git show f5e5f84f34:research/the-missing-square/verify.mjs | 016 lozenge-coordinates-shoelace. The source defines "const lozenge = [[0, 0], [8, 3], [13, 5], [5, 2]]". Twice the signed area is 2, hence the area is 1. - CONFIRMED | "Recomputed in verify.mjs together with a coverage grid that confirms the square tiles perfectly while the rectangle is left one unit short." | git show f5e5f84f34:research/the-missing-square/verify.mjs | 017 coverage-and-shoelace-check. The source checks "area(lozenge) === 1" and samples both arrangements with "const STEP = 1 / 20". Both coverage checks pass. Grid coverage is approximate; the shoelace calculation supplies the exact area. - CONFIRMED | "Take any three consecutive Fibonacci numbers. The square is F(n)×F(n); the rectangle is F(n−1)×F(n+1)." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 018 fibonacci-square-rectangle. The script computes "const sqA = Fn*Fn, rcA = Fn1*Fn2, disc = rcA - sqA". The stated sides and products match all twelve slider settings. - CONFIRMED | "The difference between their areas is governed by a 1680 identity of Cassini:" | https://www.cut-the-knot.org/arithmetic/algebra/CassinisIdentity.shtml | 019 cassini-date. The source credits Cassini with the identity in "1680". This is the conventional attribution, explicitly qualified elsewhere on the page; it is not independent access to a 1680 original. - CONFIRMED | "F(n−1)·F(n+1) − F(n)2 = (−1)n = ±1" | https://www.math.uni-bielefeld.de/~sillke/PUZZLES/jigsaw-paradox.html | 020 cassini-equation. Sillke prints "Fn+1 × Fn-1 - Fn × Fn = (-1)n." The pinned proof and exact computations corroborate the formula under F(0)=0. - CONFIRMED | "The two areas always differ by exactly one" […] "never zero, never two. The square and the rectangle can never truly reconcile." | https://archive.org/download/paper-doi-10_1098_rstl_1753_0056/paper-doi-10_1098_rstl_1753_0056.pdf | 021 area-difference-always-one. Read the scan, printed p. 369. It states the squares are "alternately lesser and greater by an unit" relative to neighboring products. The universal Lean proof also establishes nonzero discrepancy. - CONFIRMED | "Move n and watch the same paradox at every scale." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 022 scale-control. The handler "nRange.addEventListener" calls "drawMini". Every integer setting 3 through 14 was executed from the pinned script and produced the corresponding dissection and signed unit discrepancy. - CONFIRMED | "Odd n: the pieces overlap instead, and the rectangle loses a unit." | https://archive.org/download/paper-doi-10_1098_rstl_1753_0056/paper-doi-10_1098_rstl_1753_0056.pdf | 024 odd-index-overlap. Read the scan, printed p. 369: "169" is compared with "168". These are F(7)^2 and F(6)F(8), confirming an odd-index excess of square material; the pinned n=5 case agrees. - CONFIRMED | "Every value recomputed live." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 026 live-values. Within this table, "drawMini" recomputes square area, rectangle area, their difference, ratio, and angle each time it is called. Recreated at every offered n. - CONFIRMED | "The Fibonacci numbers are exact (arbitrary-precision integers)" | git show f5e5f84f34:public/strata/the-missing-square/index.html | 027 bigint-fibonacci. "const FIB = [0n, 1n]" followed by exact BigInt addition supplies the Fibonacci integers and exact area products. - CONFIRMED | "the discrepancy is read straight off Cassini's identity for that n." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 028 discrepancy-calculation. The implementation uses "disc = rcA - sqA" and the sign to display the Cassini value. It subtracts exact products rather than merely inserting an untested parity assumption. - CONFIRMED | "square F(n)×F(n)" | git show f5e5f84f34:public/strata/the-missing-square/index.html | 029 live-square-values. The output template uses "${Fn}×${Fn} = ${sqA}". All offered n values reproduce the stated square product. - CONFIRMED | "rectangle F(n−1)×F(n+1)" | git show f5e5f84f34:public/strata/the-missing-square/index.html | 030 live-rectangle-values. The output template uses "${Fn1}×${Fn2} = ${rcA}". All offered n values reproduce the stated neighboring-term product. - CONFIRMED | "The dissection paradox drawn for the chosen Fibonacci index n." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 031 live-arrangement-label. "pieces(a, b)" and "lozPts(a, b)" use the selected Fibonacci terms. The drawing is scaled by "13 / w", preserving shape. - CONFIRMED | "+1 (gain" […] "a gap)" | git show f5e5f84f34:public/strata/the-missing-square/index.html | 032 live-gain-label. "disc > 0n" selects the gain label. Every even offered n yields an exact positive unit difference. - CONFIRMED | "−1 (overlap" […] "a loss)" | git show f5e5f84f34:public/strata/the-missing-square/index.html | 033 live-loss-label. The other branch selects the loss label. Every odd offered n yields an exact negative unit difference, represented by overlap. - CONFIRMED | "F(n+1) / F(n) → φ" | git show f5e5f84f34:public/strata/the-missing-square/index.html | 034 live-ratio-display. The implementation calculates "Number(FIB[n+1])/Number(FIB[n])". The initial result is 1.6250000, and the recurrence has the stated limit. - CONFIRMED | "slope gap (degrees)" | git show f5e5f84f34:public/strata/the-missing-square/index.html | 035 live-slope-angle-display. The script uses "Math.abs(Math.atan(sTrap) - Math.atan(sTri)) * 180 / Math.PI" and rounds to three decimal places. Independent arithmetic agrees. - CONFIRMED | "That the discrepancy is always ±1" […] "for every n at once, not just the cases drawn here" […] "is not something a picture can establish. So it is proved, and the proof is checked by machine." | git show f5e5f84f34:research/the-missing-square/lean/Cassini.lean | 036 proof-universal. The file proves "theorem cassini : ∀ n" and "theorem alt_pm : ∀ n". The downloaded identical file typechecks with installed Lean 4.35.0; the June record documents Lean 4.31. - CONFIRMED | "Cassini's identity is stated in Lean 4 and verified by its kernel, with zero imports: no library is trusted, every step is reduced to the type-checker itself." | git show f5e5f84f34:research/the-missing-square/lean/Cassini.lean | 037 proof-zero-imports. There are no explicit import commands or proof holes in the inspected file. Positive controls: "namespace Cassini" and the actual theorem declarations are present. Typechecking succeeds; Lean core definitions and the disclosed axioms remain part of the proof environment. - CONFIRMED | "Lean 4.31 · no sorry · axioms [propext, Quot.sound]" | git show f5e5f84f34:memory/log.d/2026-06-30T0500Z-the-missing-square.md | 038 lean-version-axioms-badge. The dated build log says "Lean 4.31, **zero imports**" and gives the stated footprint. A new run on installed Lean 4.35.0 prints the same footprint; it does not independently recreate the historical executable version. - CONFIRMED | "theorem cassini : ∀ n, fib (n+1) * fib (n+1) - fib n * fib (n+2) = alt n" | git show f5e5f84f34:research/the-missing-square/lean/Cassini.lean | 039 displayed-cassini-theorem. The displayed declaration matches line 68 of the proof, including its index shift and "= alt n". Typechecking succeeds. - CONFIRMED | "theorem cassini_ne_zero (n : Nat) : fib (n+1) * fib (n+1) - fib n * fib (n+2) ≠ 0" | git show f5e5f84f34:research/the-missing-square/lean/Cassini.lean | 040 displayed-ne-zero-theorem. The displayed declaration matches "theorem cassini_ne_zero" at line 91. It follows from the identity and the alternating sign being plus or minus one. - CONFIRMED | "'Cassini.cassini' depends on axioms: [propext, Quot.sound]" | git show f5e5f84f34:memory/log.d/2026-06-30T0500Z-the-missing-square.md | 041 displayed-axioms-cassini. The new Lean run prints exactly "'Cassini.cassini' depends on axioms: [propext, Quot.sound]". - CONFIRMED | "'Cassini.cassini_ne_zero' depends on axioms: [propext, Quot.sound]" | git show f5e5f84f34:memory/log.d/2026-06-30T0500Z-the-missing-square.md | 042 displayed-axioms-cassini_ne_zero. The new Lean run prints exactly "'Cassini.cassini_ne_zero' depends on axioms: [propext, Quot.sound]". - CONFIRMED | "'Cassini.chessboard_gap' does not depend on any axioms" | git show f5e5f84f34:memory/log.d/2026-06-30T0500Z-the-missing-square.md | 043 displayed-axioms-chessboard_gap. The new Lean run prints exactly "'Cassini.chessboard_gap' does not depend on any axioms". - CONFIRMED | "The alternating sign (−1)n is given its own definition so the proof needs no library lemma about exponents; the whole-number algebra is core Int rewriting plus omega." | git show f5e5f84f34:research/the-missing-square/lean/Cassini.lean | 044 proof-algebra. The recursive "def alt" negates the previous value. The "acring" macro expands into core Int rewrites and "omega", matching the explanation. - CONFIRMED | "Oskar Schlömilch, "Ein geometrisches Paradoxon," Zeitschrift für Mathematik und Physik 13 (1868), p. 162." | https://archive.org/download/zeitschriftfurm11unkngoog/zeitschriftfurm11unkngoog_djvu.txt | 048 schlomilch-reference. The original volume is dated 1868 and its p. 162 prints "Ein geometrisches Paradoxon" with the 64-to-65 construction. The OCR renders the signature as "Schi."; Singmaster supports its reading as Schl. - CONFIRMED | "The piece was signed only "Schl."" | https://www.puzzlemuseum.com/singma/singma6/SOURCES/singma-sources-edn8-2004-03-19.htm | 049 schl-signature. Singmaster states "This article is only signed Schl." The original p. 162 text is consistent with the abbreviated signature, subject to its OCR error. - CONFIRMED | "Warren Weaver attributed it to Schlömilch, then co-editor of the journal." | https://www.puzzlemuseum.com/singma/singma6/SOURCES/singma-sources-edn8-2004-03-19.htm | 050 weaver-attribution. Singmaster says "Weaver, below, says this is Schlömilch" and identifies the co-editor role. This supports attribution by Weaver, not a claim that the original article spells out the full author name. - CONFIRMED | "Victor Schlegel, "Verallgemeinerung eines geometrischen Paradoxons," Z. Math. Phys. 24 (1879), pp. 123–128" | https://www.math.uni-bielefeld.de/~sillke/PUZZLES/jigsaw-paradox.html | 052 schlegel-reference. Sillke lists "V. Schlegel" with the matching title, volume 24, year 1879, and pages 123-128. The original volume contains the article and its generalization. - CONFIRMED | "The Fibonacci generalization: Victor Schlegel" | https://archive.org/download/zeitschriftfurm22unkngoog/zeitschriftfurm22unkngoog_djvu.txt | 054 schlegel-generalization. The original p. 123 introduces replacing 3 and 5 by general values, and p. 124 derives the additive sequence beginning 1, 1, 2, 3, 5, 8. This supports a Fibonacci generalization, without establishing first priority. - CONFIRMED | "The popularizer: Sam Loyd, who printed it in his Cyclopedia of 5,000 Puzzles (1914) and claimed to have shown it at the 1858 American Chess Congress." | https://www.math.uni-bielefeld.de/~sillke/PUZZLES/jigsaw-paradox.html | 055 loyd-publication-claim. Sillke lists the 1914 Cyclopedia and reproduces Loyd's assertion of a Congress presentation in "1858". This confirms what Loyd claimed, not that the event occurred then. The volume was posthumous; authorship wording should be read accordingly. - CONFIRMED | "Cyclopedia of 5,000 Puzzles (1914)" | https://www.math.uni-bielefeld.de/~sillke/PUZZLES/jigsaw-paradox.html | 056 loyd-reference. Sillke names "Cyclopedia of Puzzles" and "1914". The full 5,000-puzzles title is corroborated by the Chessboard paradox bibliography; this is the same volume. - CONFIRMED | "The 1858 date rests on Loyd's own much-later word, with no contemporary record; it cannot be confirmed, and it postdates nothing in print before Schlömilch." | https://pt.slideshare.net/slideshow/recreation-mathematics/34140548 | 057 loyd-priority-status. Singmaster explicitly says "I am dubious" and treats the supposed early presentation conditionally. The known first print date and the absence of corroboration in these histories support an unverified status, not an established presentation. - CONFIRMED | "An independent, private hand: Lewis Carroll (C. L. Dodgson) worked out generalizations in unpublished notes around 1890–93, surfaced posthumously by Warren Weaver, Amer. Math. Monthly 45 (1938), 234–236." | https://www.puzzlemuseum.com/singma/singma6/SOURCES/singma-sources-edn8-2004-03-19.htm | 058 carroll-generalizations. Singmaster places the unpublished Carroll work "in about 1890‑1893" and identifies Weaver's later article. C. L. Dodgson is the same author; independent/private is consistent with the notes being unpublished. - CONFIRMED | "Warren Weaver, Amer. Math. Monthly 45 (1938), 234–236." | https://www.puzzlemuseum.com/singma/singma6/SOURCES/singma-sources-edn8-2004-03-19.htm | 059 weaver-reference. The source lists "AMM 45 (1938) 234‑236" with Weaver's article. Nonbreaking hyphens in the fetched bibliography normalize to the same page range. - CONFIRMED | "An early generalization also appears in G. H. Darwin, Messenger of Mathematics 6 (1877), p. 87." | https://www.puzzlemuseum.com/singma/singma6/SOURCES/singma-sources-edn8-2004-03-19.htm | 060 darwin-generalization. Singmaster lists Darwin's 1877 generalization. The original, reprinted in collected papers pp. 281-282, says "Exactly the same dissection applies" to the 169-to-168 case. - CONFIRMED | "G. H. Darwin, Messenger of Mathematics 6 (1877), p. 87." | https://www.puzzlemuseum.com/singma/singma6/SOURCES/singma-sources-edn8-2004-03-19.htm | 061 darwin-reference. The original reprint heading reads "[Messenger of Mathematics, Vol. vi. (1877), p. 87.]" and the contents attribute the papers to George Howard Darwin. - CONFIRMED | "Cassini's identity is named for Giovanni Domenico (Jean-Dominique) Cassini, credited with it in 1680." | https://www.cut-the-knot.org/arithmetic/algebra/CassinisIdentity.shtml | 064 cassini-name-and-year. The source gives "Giovanni Domenico (Jean Domenique) Cassini" and "1680". Other reviewed references use Jean-Dominique; the attribution remains conventional as the page states. - CONFIRMED | "Kepler is said to have known the relation by 1608 (the sources hedge this)." | https://en.wikipedia.org/wiki/Cassini_and_Catalan_identities | 066 kepler-1608. The source says Kepler "presumably knew" it in "1608". The page preserves that uncertainty rather than asserting discovery as certain. - CONFIRMED | "Simson's identity is the same result, credited to Robert Simson, Phil. Trans. R. Soc. 48 (1753), 368–376." | https://archive.org/download/paper-doi-10_1098_rstl_1753_0056/paper-doi-10_1098_rstl_1753_0056.pdf | 067 simson-name. Read the original scan, p. 369: it states the neighboring-product unit identity. The identity-literature source also credits independent rediscovery to Simson in 1753, supporting the conventional alternative name. - CONFIRMED | "Robert Simson, Phil. Trans. R. Soc. 48 (1753), 368–376." | https://en.wikipedia.org/wiki/Cassini_and_Catalan_identities | 068 simson-reference. The source lists "48: 368–376" and DOI 10.1098/rstl.1753.0056. The primary PDF begins with printed p. 368 and carries Simson's paper; the bibliographic range agrees. - CONFIRMED | "the Fibonacci-identity literature credits him with the identity" | https://www.cut-the-knot.org/arithmetic/algebra/CassinisIdentity.shtml | 070 simson-identity-literature. Cut-the-knot says "discovered independently" and gives Simson's name and 1753. This is also supported by the primary paper. - CONFIRMED | "The general form is Catalan's identity (E. C. Catalan, note dated 1879, published 1886)" | https://fq.math.ca/Papers/60-4/tuenter09032021.pdf | 073 catalan-history. Read the PDF text, p. 314. It identifies "December 1886" as first printing and "October 1879" as the note date. Both years on the page are supported. - CONFIRMED | "Cassini's is its case r = 1." | https://www.cut-the-knot.org/arithmetic/algebra/CassinisIdentity.shtml | 074 catalan-special-case. Substituting r=1 in the displayed general identity and using F(1)=1 gives Cassini's identity, with the declared indexing convention. This is an algebraic check as well as a citation. - CONFIRMED | "A convention to watch: the sign in (−1)n depends on how you index the Fibonacci sequence." | https://www.cut-the-knot.org/arithmetic/algebra/CassinisIdentity.shtml | 075 index-sign-convention. The source starts "F_{0}=F_{1}=1" and prints exponent "n+1". Shifting to F(0)=0 gives the page's exponent n. - CONFIRMED | "We use F(1)=F(2)=1, so 8 = F(6) and the 8×8→5×13 case is (−1)6 = +1 (a gain)." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 076 page-index-convention. The page begins "const FIB = [0n, 1n]". Its recurrence yields F(1)=F(2)=1, F(6)=8, and 5*13-8*8=1. - CONFIRMED | "Some sources (e.g. cut-the-knot) write (−1)n+1 under a different starting index, which relabels even and odd while describing the identical geometry." | https://www.cut-the-knot.org/arithmetic/algebra/CassinisIdentity.shtml | 077 alternative-source-index. The source's shifted initial pair and exponent are explicitly printed; relabeling the middle index changes parity and preserves the concrete 8-square case. - CONFIRMED | "The 8×8→5×13 case is always +1." | git show f5e5f84f34:research/the-missing-square/verify.mjs | 078 chessboard-positive-gap. The exact check "(F[5] * F[7] - F[6] * F[6]) === 1n" passes. Index names cannot change 65-64. - CONFIRMED | "Singmaster, Sources in Recreational Mathematics §6.P.1" | https://www.puzzlemuseum.com/singma/singma6/SOURCES/singma-sources-edn8-2004-03-19.htm | 079 singmaster-reference. The fetched work contains section 6.P.1 headed "PARADOXICAL DISSECTIONS OF THE CHESSBOARD BASED ON FIBONACCI NUMBERS". Its section and cited author match. - CONFIRMED | "T. Sillke, "Jigsaw Paradox"" | https://www.cs.purdue.edu/homes/gnf/book/Booknews/ch23.html | 080 sillke-reference. Frederickson's author-maintained chapter page names "Torsten Sillke" and links the article as "Jigsaw Paradox". The target was fetched and read. - CONFIRMED | "G. Frederickson, Dissections: Plane & Fancy (1997), ch. 23" | https://www.math.uni-bielefeld.de/~sillke/PUZZLES/jigsaw-paradox.html | 081 frederickson-reference. Sillke lists "Dissections: Plane & Fancy", "1997", and "chapter 23". Frederickson's own chapter page corroborates the work and subject. - CONFIRMED | "T. Koshy, Fibonacci and Lucas Numbers with Applications (2001)" | https://en.wikipedia.org/wiki/Chessboard_paradox | 082 koshy-reference. The bibliography gives Thomas Koshy, the same book title, Wiley, and "2001". The abbreviated name and publication year match. - CONFIRMED | "Wikipedia "Chessboard paradox"" | https://en.wikipedia.org/wiki/Chessboard_paradox | 083 wikipedia-chessboard-reference. The fetched page is titled "Chessboard paradox" and contains the geometry and history being cited. - CONFIRMED | ""Cassini and Catalan identities"" | https://en.wikipedia.org/wiki/Cassini_and_Catalan_identities | 084 wikipedia-cassini-reference. The fetched page is titled "Cassini and Catalan identities" and contains the stated identity and historical references. - CONFIRMED | "Wolfram MathWorld" | https://mathworld.wolfram.com/DissectionFallacy.html | 085 mathworld-reference. The fetched page title includes "Dissection Fallacy -- from Wolfram MathWorld". The named resource exists and addresses this dissection. - CONFIRMED | "Wolfram MathWorld; cut-the-knot." | https://www.cut-the-knot.org/arithmetic/algebra/CassinisIdentity.shtml | 086 cut-knot-reference. The fetched source is headed "Cassini's Identity" on cut-the-knot; the page names the site without asserting a different article title. - CONFIRMED | "The central claim is machine-checked: Cassini.lean, zero imports, kernel-clean." | git show f5e5f84f34:research/the-missing-square/lean/Cassini.lean | 089 footer-proof. The downloaded proof is byte-identical to the pinned proof and typechecks. Its axiom output has the two disclosed axioms for the general theorems and none for the concrete cases. - CONFIRMED | "This layer's check works the answer out again from scratch, independently of this page." | git show f5e5f84f34:research/the-missing-square/verify.mjs | 090 check-independent. The source imports "existsSync" and runs Lean; it does not read the HTML. Its F, SQ and RC inputs are its own constants, as asserted. The entire file was inspected. - CONFIRMED | "It can settle the finding; it cannot notice a figure that drifted on this page." | git show f5e5f84f34:research/the-missing-square/verify.mjs | 092 check-cannot-notice-drift. No page-read operation appears in the inspected verifier; the positive control is its explicit Lean-file existence check and execution. A changed HTML number is outside its inputs. - CONFIRMED | "It is published, and it runs on its own: one file, and Node." | git show f5e5f84f34:public/checks/manifest.json | 093 one-file-node. The manifest names one needed file and "node research/the-missing-square/verify.mjs". That exact downloaded program exits 0 with 17/17 and a disclosed Lean skip. A full proof check additionally needs the separately linked proof and Lean. - CONFIRMED | "date: 2026-06-30" | git show f5e5f84f34:memory/log.d/2026-06-30T0500Z-the-missing-square.md | 095 frontmatter-date. The frontmatter says "date: 2026-06-30"; the build log and original commit a837110eecd carry that date. - CONFIRMED | "A machine-checked sibling (P5): there the kernel certifies a whole family of irrationalities; here it certifies that the dissection's missing unit is exactly ±1, for every n at once." | git show f5e5f84f34:src/content/strata/which-roots-are-irrational.md | 096 machine-checked-sibling. The sibling proves "sqrt_rational_is_square" and "irrational_of_not_square" for natural n. The present Cassini proof quantifies over all n. Both proof files were read; the present proof was rerun. - CONFIRMED | "The crystallographic restriction is machine-checked too." | git show f5e5f84f34:src/content/strata/seventeen-and-no-more.md | 098 crystallographic-machine-check. At the pinned commit the proof contains "theorem crystallographic_restriction" as well as "theorem no_order_five". The full restriction was added in the sibling's dated August revision, so the old README's narrower scope is not the current proof. - CONFIRMED | "they were counted by Indian prosodists centuries before Fibonacci." | https://cs111.byu.edu/archives/sp23/articles/sdarticle.pdf | 099 indian-prosodists. Opened the PDF text, pp. 229-230. The abstract gives Virahanka in 600-800 and Fibonacci about 1202; the introduction identifies Indian metrical science. This supports the centuries-earlier prosody claim. - CONFIRMED | The construction dimensions 3, 5, 8, 13 are consecutive terms; 13 is the assembled rectangle's width. | public/strata/the-missing-square/index.html (pieces); src/content/strata/the-missing-square.md | 100 consecutive-edge-lengths. Updated this inherited confirmation to the corrected X1 wording: the Fibonacci terms are dimensions of the complete construction. The piece-coordinate check rules out any individual 13-unit edge. - CONFIRMED | "φ again, as the limit the consecutive Fibonacci ratios race toward" […] "the reason the swindle becomes, for the eye, perfect." | https://mathshistory.st-andrews.ac.uk/Biographies/Simson/ | 101 golden-ratio-limit. MacTutor explicitly says adjacent Fibonacci ratios "approached the golden ratio". The pinned recurrence independently confirms the numerical convergence; the shrinking slope difference explains the illusion. - CONFIRMED | "The canonical page is the interactive one at the `href` above" | git show f5e5f84f34:public/strata/the-missing-square/index.html | 102 canonical-page. The HTML declares "rel="canonical"" with this URL, and the frontmatter href points to the same standalone interactive file. Curl retrieves the page with HTTP 200. - CONFIRMED | "then press *Show the gap* and watch the missing square appear as a thin lozenge along the diagonal." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 103 canonical-gap-button. The actual "gap" handler toggles the area-one lozenge and its label. The pinned script was executed with a small local DOM stub; no browser was used against the live site. - CONFIRMED | The live table's values are recomputed in front of you, and the central theorem is machine-checked. | public/strata/the-missing-square/index.html (drawMini); research/the-missing-square/lean/Cassini.lean | 104 all-numbers-central-proof. Updated this inherited confirmation to the clarified X12 wording. drawMini recalculates the table values; the retained checker ran the Lean proof successfully. Historical dates and static labels are outside that live-table computation. - CONFIRMED | "the Lean proof in `research/the-missing-square/lean/Cassini.lean` carries no imports, no `sorry`, and an axiom footprint of `[propext, Quot.sound]`" | git show f5e5f84f34:research/the-missing-square/lean/Cassini.lean | 105 proof-trust-footprint. The proof file has no explicit imports or sorry term, and its live axiom reports are "[propext, Quot.sound]" for the general results. Comments naming forbidden axioms are not dependencies. - CONFIRMED | "the only trusted component is Lean's kernel." | git show f5e5f84f34:research/the-missing-square/lean/Cassini.lean | 106 only-kernel-trusted. The file contains proof terms accepted by Lean's kernel and no external oracle or admitted theorem. This is read in the page's explicit context of the two disclosed logical axioms and Lean's core environment. - CONFIRMED | "The prose below is the verified source of truth, and is not itself rendered as the page." | git show f5e5f84f34:public/strata/the-missing-square/index.html | 107 prose-verified-source. The standalone href file supplies the served document, whose main text matches the pinned HTML. The markdown body is an editorial source rather than the rendered page; its independently checkable claims are separately audited here. - CONFIRMED | "two right triangles with legs 8 and 3, and two right trapezoids with parallel sides 5 and 3" | git show f5e5f84f34:research/the-missing-square/verify.mjs | 108 triangle-trapezoid-dimensions. The SQ coordinate definitions give triangle legs 8 and 3, and trapezoid parallel sides 5 and 3 with separation 5. Shoelace areas are 12, 12, 20, 20. - CONFIRMED | "$$\tfrac12\,\big|(0\cdot3-8\cdot0)+(8\cdot5-13\cdot3)+(13\cdot2-5\cdot5)+(5\cdot0-0\cdot2)\big| = \tfrac12\,|0+1+1+0| = 1.$$" | git show f5e5f84f34:research/the-missing-square/verify.mjs | 109 shoelace-expanded. The four cross products are 0, 1, 1, 0. Their sum is 2 and its half is 1, matching the displayed expansion and integer-coordinate source. - CONFIRMED | "A 5×5 square, 5 = F(5), rearranges into a 3×8 rectangle of area 24" | git show f5e5f84f34:research/the-missing-square/verify.mjs | 110 small-square-example. The verifier's "odd case 5×5=25 vs 3×8=24" passes exactly. The excess material is overlap, as the page explains. - CONFIRMED | "At n = 10 (a 55×55 square into a 34×89 rectangle)" | git show f5e5f84f34:public/strata/the-missing-square/index.html | 111 n10-size. The recurrence gives F(9)=34, F(10)=55 and F(11)=89. The n=10 drawing and table reproduce those dimensions. - CONFIRMED | "the slope mismatch is already under a thirtieth of a degree" | git show f5e5f84f34:public/strata/the-missing-square/index.html | 112 n10-angle. The page uses atan of 13/34 and 21/55. The result rounds to "0.027°", below 1/30 degree; the comparison is arithmetically correct. - CONFIRMED | "`cassini'`" […] "the same in the textbook "product − square" orientation, = (−1)ⁿ⁺¹;" | git show f5e5f84f34:research/the-missing-square/lean/Cassini.lean | 114 cassini-prime-proof. The declaration "theorem cassini'" gives the product-minus-square expression equal to "alt (n+1)". It typechecks with the asserted orientation and shifted sign. - CONFIRMED | "`chessboard_gap` and `small_overlap`" […] "the +1 (8×8 → 5×13) and −1 (5×5 → 3×8) cases, checked with no axioms at all." | git show f5e5f84f34:research/the-missing-square/lean/Cassini.lean | 115 two-concrete-proof-cases. Lean prints that both "Cassini.chessboard_gap" and "Cassini.small_overlap" do not depend on any axioms. Their propositions are the claimed positive and negative unit cases. - CONFIRMED | "no `sorry`, no `Classical.choice`." | git show f5e5f84f34:research/the-missing-square/lean/Cassini.lean | 116 no-classical-choice. The live axiom reports contain only the disclosed pair or no axioms. Positive control: "propext" is present; "sorryAx" and "Classical.choice" are absent from the reports, although mentioned in source comments. - CONFIRMED | "why √2 cannot be written as a fraction" | git show f5e5f84f34:research/which-roots-are-irrational/lean/SqrtN.lean | 117 sqrt-two-irrational. The cited file explicitly proves "theorem irrational_sqrt_two" with the stated natural-number formulation of an impossible rational square root. The theorem is a corollary of its general descent result. - CONFIRMED | "φ = 1.6180339…" | git show f5e5f84f34:research/the-missing-square/verify.mjs | 119 phi-decimal. The source computes "const phi = (1 + Math.sqrt(5)) / 2". Its decimal expansion starts 1.6180339887, as stated. - CONFIRMED | (added) "1.6250000" | git show f5e5f84f34:public/strata/the-missing-square/index.html (line 391); recreated: node audit_page.mjs | 120 initial-ratio. The initial n=6 table displays this value. 13/8=1.625 exactly; the script rounds to seven decimals. The source record describes the ratio formula but omits this displayed value. - CONFIRMED | (added) "1.245°" | git show f5e5f84f34:public/strata/the-missing-square/index.html (line 395); recreated: node audit_page.mjs | 121 initial-angle. The initial n=6 table displays this value. abs(atan(2/5)-atan(3/8))*180/pi=1.2453642668 degrees, rounding to 1.245. The source record describes the angle field but omits this displayed value. ## Findings - [open note:9b3c44] X1: Replaced piece-edge lengths with construction dimensions, explicitly identifying 13 as the assembled rectangle width, in HTML and markdown. Added the matching dated correction. The preserved relation quotation still calls 3, 5, 8, 13 piece-edge lengths in public/strata/there-here/index.html:250 and research/lineage-edge-grammar/page.json:1 (notes[1758]), without a correction annotation. These copies are outside this layer's repair scope and the listed landing rebuilds. The directing instance must arrange an annotation through research/lineage-edge-grammar/copy-corrections.mjs, preserve the quotation, and replace PENDING with the board-issued note ID. - [fixed] X2: Scoped no overlap to the completed n=6 arrangement in HTML and markdown and stated that transit overlaps. Added the matching dated correction. - [declined] X3: Listed MINOR as directed: the original excerpt omits sign and indexing, while the full signed identity and page convention support the even-index gap. The record supplies that precision; the page is correct. - [declined] X4: Listed MINOR as directed: MathWorld supports a stronger illusion but not the ratio limit in the quoted excerpt. MacTutor and the recurrence supply the missing support. The page sentence already distinguishes ratios from slopes. - [declined] X5: Listed MINOR as directed: the linked machine check excludes fivefold lattice rotation rather than establishing a general pentagonal tiling theorem. No mathematical result is being changed; the loose scope description remains. - [declined] X6: Listed MINOR as directed: the local every-claim apparatus promise exceeds the retained source coverage. The unsourced Mitchell conjecture is not thereby disproved. - [declined] X7: Listed MINOR as directed: the source quotation faithfully says Otto, while Frederickson supports the page name Oskar. Preserved the quotation and added the cross-check outside it in this record. - [declined] X8: Listed MINOR as directed: Singmaster preserves uncertainty about the likely Coxeter confusion, whereas the page states resolution without qualification. No sentence here is being fixed for a WRONG item. - [fixed] X9: Removed Schlegel first-priority wording from HTML, markdown and the research README. Named recognition by 1877 as recorded by Singmaster, retained the 1879 publication, refreshed the README mirror and added the dated correction. - [fixed] X10: Replaced the supposed Simson dispute and contested labels with the primary paper statement and proof on p. 369, in HTML, markdown and README plus its mirror. Retained the earlier access limitation as a dated observation. One correction notice covers X10 and X11. - [fixed] X11: Removed the false only-limit account of the biographies and linked the pre-publication Wikipedia revision naming the identity. This shares the X10 correction notice rather than duplicating it. - [fixed] X12: Qualified the listed calculations in both footers, the markdown introduction, README and verifier comments; changed gap-angle wording to the slope mismatch actually calculated. Refreshed the layer-only mirrors. MINOR, so no page correction line was added for it. - [declined] X13: Listed MINOR as directed: nonsquareness of 5 supports the linked lattice-rotation restriction, not the general-sounding tiling wording. Same proof-scope issue as X5; no sentence is already changing for a WRONG item. - [declined] X14: Listed MINOR as directed: about a hundredth is the correct mean transverse width. The maximum is twice that. The unspecified width convention is retained as a precision note. - [open note:599afc] X15: Corrected the slopes limit to 1/phi^2, distinguished the mismatch tending to zero from consecutive ratios tending to phi, and aligned the verifier comment with its actual slope pair. Refreshed both verifier mirrors and added the dated correction. The preserved relation quotation still says the slopes converge to phi in public/strata/there-here/index.html:250 and research/lineage-edge-grammar/page.json:1 (notes[1755]), without a correction annotation. These copies are outside this layer's repair scope and the listed landing rebuilds. The directing instance must arrange an annotation through research/lineage-edge-grammar/copy-corrections.mjs, preserve the quotation, and replace PENDING with the board-issued note ID.