---
slug: the-half-you-can-never-reach
passed: 2026-10-14
by: the assay line (research/assay-line/queue-1014c/), Codex fixer directed by claude-assaying-boyle-1014; source record by Codex, checked by Codex; fix-check repair by Codex
checked: 142
confirmed: 120
wrong: 20
unverifiable: 0
observed: 0
stale: 2
---

This record covers the 20 queue-1014c triage items and the subsequent fix-check repair. The 120 CONFIRMED lines retain the checker's attributed source rereads at f5e5f84f34. Two previously confirmed historical inferences are now WRONG (R1 and R2) after comparison with Slocum's account of the published challenge. Counts are 120 CONFIRMED + 16 WRONG + 4 MINOR + 2 STALE = 142; the wrong field includes the four MINOR findings. X5, X17, X18, R1 and R2 remain open in the encoded film or poster despite corrected editable text. The claims gate will reject these placeholders until then.

## Claims
- WRONG | X1 (history-1880-prize): "In 1880 Sam Loyd offered $1000 for sliding a board with 14 and 15 swapped back into order; nobody collected." | https://www.scribd.com/document/437941054/Homage-to-a-Pied-Puzzler-Ed-Pegg-Jr | Slocum, pp. 14-17: first published challenge on 4 January 1896, with a $1000 reward. The 1896 terms did not specify the final gap position; the page now states the stricter goal used by its instrument.
- WRONG | X2 (history-loyd-promoted): "The puzzle-maker Sam Loyd sharpened the craze to a point:" | https://utenti.quipo.it/base5/loyd/g15verastoria.htm | Slocum separates the January 1880 US craze from the January 1896 article and explicitly denies that Loyd promoted or popularized the earlier craze.
- WRONG | X3 (history-johnson-story-roles): "Johnson showed the swapped board can't be solved, and Story supplied the parity reason you've just been sliding around in." | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | Johnson, p. 398, proves that returning the gap entails an even number of interchanges. Story credits that obstruction and constructs the complementary solvability result on pp. 400-402.
- WRONG | X4 (sign-alone): "If the sign were the whole story, you could never get back to a solved board with the gap home" | git show e722f8d174:public/strata/the-half-you-can-never-reach/index.html | Executed the page controller: ArrowRight then ArrowLeft returns the solved 8-puzzle with signs -1 then +1. Only an odd starting arrangement with the gap home is obstructed.
- WRONG | X5 (magic-tricks): "That is the whole secret of every "swap two pieces" magic trick done on a grid: it isn't a swap, it's a hidden three-cycle." | https://www.jaapsch.net/puzzles/fifteen.htm | Scherphuis describes swapping the final visible letters while also exchanging identical R tiles. Two transpositions form an even permutation, not a single three-cycle.
- WRONG | X6 (search-visits-362880): "it visits 362,880 boards and stops." | git show e722f8d174:public/strata/the-half-you-can-never-reach/index.html | Executed buildUniverse: reached 181440, array length 362880, unvisited 181440. The verifier separately enumerates all arrangements after its BFS.
- MINOR | X7 (verifier-every-number): "Every number here is recomputed in `research/fifteen-puzzle/verify.mjs` (36/36):" | git show e722f8d174:research/fifteen-puzzle/verify.mjs | Read all of verify.mjs. Its numerical checks establish puzzle mathematics, not historical dates or reward amounts.
- MINOR | X8 (verifier-no-float): "no floating point." | git show e722f8d174:research/fifteen-puzzle/verify.mjs | verify.mjs computes solv / N and compares its distance from 0.5 with 0.01. The auxiliary sample uses floating point; exhaustive counts remain exact integers.
- MINOR | X9 (verifier-every-claim): "every claim re-checked offline in research/fifteen-puzzle/verify.mjs (36/36)." | git show e722f8d174:research/fifteen-puzzle/verify.mjs | Read all of verify.mjs. It reads the Lean file but neither the page nor historical sources. The footer overstated coverage; kept MINOR as directed.
- WRONG | X10 (lean-live-typecheck): "a live typecheck asserts the [propext, Quot.sound] footprint when the toolchain is present." | git show e722f8d174:research/fifteen-puzzle/verify.mjs | A scratch proof using axiom FP.audit_extra passed the old verifier, 36/36. The repaired verifier rejects it, 35 passed and 1 failed. The authentic proof still passes 36/36; empty and smaller permitted footprints are accepted.
- MINOR | X11 (lean-md-unconditional): "then typechecks the proof live." | git show e722f8d174:research/fifteen-puzzle/verify.mjs | The live Lean invocation is conditional on finding a usable toolchain; the fallback performs static and model-fidelity checks only.
- WRONG | X12 (wilson-general-theorem): "on almost every puzzle graph the reachable group is exactly the alternating group." | https://www.sciencedirect.com/science/article/pii/0095895674900987 | The indexed publisher abstract explicitly permits all or half of the labelings on a non-separable graph, except polygons and one other graph. Direct publisher opening failed; the primary-source search result was readable.
- WRONG | X13 (film-reproducible): "Reproducible from a fresh checkout: bash research/fifteen-puzzle/film/build.sh." | git show e722f8d174:research/fifteen-puzzle/film/build.sh | Read build.sh, render.mjs and package manifests. render.mjs imports playwright and launches Chromium; the repository declares neither as a film prerequisite and does not install the browser. Inspected code only; no build or media generation was run.
- STALE | X14 (check-last-date): "Last verified 20 June 2026, when it was written." | git show e722f8d174:memory/log.d/2026-07-20T0930Z-fifteen-puzzle-machine-checked.md | Read the July 20 committed log, which records 36/36 and new Lean work. The layer verifier was rerun in this pass. The placard is regenerated from this dated claims record, under the triage no-line exception.
- STALE | X15 (metadata-modified): ""dateModified":"2026-06-20"" | git show e722f8d174:memory/log.d/2026-07-20T0930Z-fifteen-puzzle-machine-checked.md | The July 20 log records changes after June 20. This repair changes the page, so dateModified is now 2026-10-14. No separate Updated line, as directed.
- WRONG | X16 (related-thue-fairness): "using it to take turns cancels the first mover's advantage exactly;" | https://arxiv.org/pdf/1110.1137 | Cooper and Dutle discuss approximation, not universal equality. Direct ABBA allocation of 8,4,2,1 gives 9 and 6. The linked layer states the restricted power-sum equality used in the replacement.
- WRONG | X17 (film-st-louis): "St Louis, 1891" | https://www.scribd.com/document/437941054/Homage-to-a-Pied-Puzzler-Ed-Pegg-Jr | Slocum, pp. 14-15, dates the first published prize challenge to 4 January 1896. The old film header attaches 1891 and an unsupported city to it. Source corrected; the MP4 and poster remain unchanged. The poster was inspected directly in the repair pass; the MP4 timestamp 00:17 is reported by fixcheck.md.
- WRONG | X18 (film-history-loyd): "1891 Loyd claims the puzzle & offers $1000 for the swap" | https://www.scribd.com/document/437941054/Homage-to-a-Pied-Puzzler-Ed-Pegg-Jr | Slocum, pp. 12-15, separates the 1891 inventorship claim from the 1896 reward challenge. The film source now preserves that separation; MP4 remains unchanged.
- WRONG | X19 (added-initial-board): (added) "Loyd's box simply started in the wrong half. Here it is" | git show e722f8d174:public/strata/the-half-you-can-never-reach/index.html | Executed the original initialization: a legal shuffle from solved has J=+1. The repaired initial board is the existing 14/15-swap configuration with J=-1.
- WRONG | X20 (added-thue-permutation): (added) "Both are about the parity of a permutation doing quiet, decisive work." | https://arxiv.org/pdf/1110.1137 | Cooper and Dutle define Thue-Morse by binary digit parity. The shared concept is parity, with permutation parity and gap position determining this puzzle.
- CONFIRMED | "Sam Loyd offered $1000 to anyone who could slide the tiles back into order." | https://www.mathpuzzle.com/loyd/cop234-235.jpg | N2 source reread at f5e5f84f34, retained from N2-codex.md: history-prize: Viewed the scan itself. Page 235 says "A prize of $1,000" and "has never been claimed"; its diagram and preceding paragraph specify the 14/15 exchange and restoration of the other positions. This is a retrospective account, not evidence for an 1880 date.
- CONFIRMED | "The money was never paid." | https://www.mathpuzzle.com/loyd/cop234-235.jpg | N2 source reread at f5e5f84f34, retained from N2-codex.md: history-prize-unclaimed: Viewed the scan itself. Page 235 says "A prize of $1,000" and "has never been claimed"; its diagram and preceding paragraph specify the 14/15 exchange and restoration of the other positions. This is a retrospective account, not evidence for an 1880 date.
- CONFIRMED | "In January 1880 a small wooden box of fifteen numbered tiles set the United States, and then Europe, briefly out of their minds." | https://utenti.quipo.it/base5/loyd/g15verastoria.htm | N2 source reread at f5e5f84f34, retained from N2-codex.md: history-craze: Slocum: "began in January 1880 in the US and in April in Europe". The description of the initial US craze and subsequent European craze matches.
- CONFIRMED | "and offered $1000 to the first person who could slide them straight, purely by legal moves." | https://www.mathpuzzle.com/loyd/cop234-235.jpg | N2 source reread at f5e5f84f34, retained from N2-codex.md: history-arrangement: Viewed the scan itself. Page 235 says "A prize of $1,000" and "has never been claimed"; its diagram and preceding paragraph specify the 14/15 exchange and restoration of the other positions. This is a retrospective account, not evidence for an 1880 date.
- WRONG | R1 (history-knew): "Loyd almost certainly knew it." | https://www.scribd.com/document/437941054/Homage-to-a-Pied-Puzzler-Ed-Pegg-Jr | Fix-check repair: Slocum, pp. 16-17, describes the published 1896 problem as solvable because it omitted the final gap position. The earlier N2 entry cited MacTutor's assertion of knowledge; that assertion does not establish knowledge of an impossible 1896 challenge. Removed the inference from the film source; its encoded copy and the poster remain open. No contrary mental state is inferred.
- CONFIRMED | "For decades Loyd claimed he invented the puzzle. He did not." | https://utenti.quipo.it/base5/loyd/g15verastoria.htm | N2 source reread at f5e5f84f34, retained from N2-codex.md: history-inventor-denial: Slocum: "Loyd first claimed in 1891" and "a 20 year campaign"; he explicitly rejects Loyd as inventor.
- CONFIRMED | "The historians Jerry Slocum and Dic Sonneveld traced the real origin to Noyes Palmer Chapman, a postmaster in Canastota, New York, around 1874;" | https://divisbyzero.com/2011/03/01/a-picture-of-frustration-sam-loyds-15-puzzle/ | N2 source reread at f5e5f84f34, retained from N2-codex.md: history-chapman: Richeson: "invented around 1874 by Noyes Palmer Chapman, a postmaster from Canastota, New York." The surrounding paragraph attributes the research to Slocum and Sonneveld.
- CONFIRMED | "Loyd's authorship claim first appeared in 1891 and he repeated it until his death in 1911" | https://utenti.quipo.it/base5/loyd/g15verastoria.htm | N2 source reread at f5e5f84f34, retained from N2-codex.md: history-1891: Slocum: "Loyd first claimed in 1891" and "a 20 year campaign"; he explicitly rejects Loyd as inventor.
- CONFIRMED | "his death in 1911" | https://divisbyzero.com/2011/03/01/a-picture-of-frustration-sam-loyds-15-puzzle/ | N2 source reread at f5e5f84f34, retained from N2-codex.md: history-death: Richeson explicitly dates "his death in 1911"; MacTutor independently gives 10 April 1911.
- CONFIRMED | "a story that "fooled everyone for 115 years," as Slocum put it." | https://divisbyzero.com/2011/03/01/a-picture-of-frustration-sam-loyds-15-puzzle/ | N2 source reread at f5e5f84f34, retained from N2-codex.md: history-quotation: The quoted words "Fooled Everyone for 115 Years" occur in the book subtitle. The source identifies both authors; the Open Library catalog independently dates the book to 2006. This is a subtitle quotation, not a separately documented remark.
- CONFIRMED | "The impossibility was first proved by Johnson & Story (1879);" | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: history-first-proof: The original cover identifies "Wm. Woolsey Johnson and William E. Story" and "Vol. 2, No. 4 (Dec., 1879), pp. 397-404". Sections I and II supply impossibility and sufficiency. Richeson calls it the "first proof in 1879".
- CONFIRMED | "The impossibility was proved in 1879 by William Woolsey Johnson and William E. Story in the American Journal of Mathematics" | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: history-proof-names: The original cover identifies "Wm. Woolsey Johnson and William E. Story" and "Vol. 2, No. 4 (Dec., 1879), pp. 397-404". Sections I and II supply impossibility and sufficiency. Richeson calls it the "first proof in 1879".
- WRONG | R2 (history-prize-impossible): "Loyd's prize was offered into a wall that had already been described in print." | https://www.scribd.com/document/437941054/Homage-to-a-Pied-Puzzler-Ed-Pegg-Jr | Fix-check repair: the prize followed the 1879 proof, but that chronology does not make the 1896 published challenge impossible. Slocum, pp. 16-17, gives a solution under its unspecified final-gap terms. The page, film source and verifier label now reserve impossibility for the goal with every tile and the gap home. The film and poster still conflate those goals.
- CONFIRMED | "The 15 puzzle is the sliding box of fifteen numbered tiles with one empty square." | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: puzzle-definition: Johnson, p. 397: "the 16th square being left blank" and "The counter occupying any adjacent square may now be moved"; diagonal moves are excluded.
- CONFIRMED | "fifteen numbered tiles in a four-by-four box, all in place except 14 and 15, swapped." | https://www.mathpuzzle.com/loyd/cop234-235.jpg | N2 source reread at f5e5f84f34, retained from N2-codex.md: puzzle-four-by-four: The source-record excerpt establishes a generic puzzle, not the particular swap. The separately viewed Cyclopedia p. 235 diagram and text say "only with the 14 and 15 reversed".
- CONFIRMED | "Every legal move does exactly one thing: the gap trades places with a tile next to it." | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: puzzle-rule: Johnson, p. 397: "the 16th square being left blank" and "The counter occupying any adjacent square may now be moved"; diagonal moves are excluded.
- CONFIRMED | "exactly half can never be reached by sliding" | https://orbilu.uni.lu/bitstream/10993/40106/1/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: half-unreachable: Read the Luxembourg PDF, p. 2, after the automatic fetch failed. It says "all permutations with invariant 1 are possible configurations" and defines the invariant by transpositions plus the gap's row and column distances. The product form is equivalent; a legal slide flips both factors.
- CONFIRMED | "In the language of permutations, that is a single transposition" | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: transposition: Johnson, pp. 397-399, models slides by interchanges and proves "m is an even number" when the gap returns. An odd transposition of two numbered tiles with the gap fixed cannot be undone. A chain of legal moves is a chain of such interchanges.
- CONFIRMED | "The whole puzzle is just a long chain of transpositions applied to the starting order." | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: chain: Johnson, pp. 397-399, models slides by interchanges and proves "m is an even number" when the gap returns. An odd transposition of two numbered tiles with the gap fixed cannot be undone. A chain of legal moves is a chain of such interchanges.
- CONFIRMED | "Mathematicians attach a sign to every arrangement: +1 if it takes an even number of swaps to reach from the solved order, −1 if odd." | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: sign-definition: Johnson, pp. 398-399, proves that odd and even numbers of interchanges cannot give the same permutation and that one interchange flips the parity of the cycle count. Pairing each permutation with a fixed transposition gives equally many signs. Here the tile counts are 8 or 15, so the alternating group has index two.
- CONFIRMED | "the count's parity never depends on how you swap." | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: sign-well-defined: Johnson, pp. 398-399, proves that odd and even numbers of interchanges cannot give the same permutation and that one interchange flips the parity of the cycle count. Pairing each permutation with a fixed transposition gives equally many signs. Here the tile counts are 8 or 15, so the alternating group has index two.
- CONFIRMED | "Each move flips the sign, every time: even ⟷ odd." | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: sign-flips: Johnson, pp. 398-399, proves that odd and even numbers of interchanges cannot give the same permutation and that one interchange flips the parity of the cycle count. Pairing each permutation with a fixed transposition gives equally many signs. Here the tile counts are 8 or 15, so the alternating group has index two.
- CONFIRMED | "returning the gap to its corner takes an even number of moves" | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: return-even: Johnson, pp. 397-399, models slides by interchanges and proves "m is an even number" when the gap returns. An odd transposition of two numbered tiles with the gap fixed cannot be undone. A chain of legal moves is a chain of such interchanges.
- CONFIRMED | "Loyd's swap is a single transposition away from solved: sign −1, odd." | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: loyd-odd: Johnson, pp. 397-399, models slides by interchanges and proves "m is an even number" when the gap returns. An odd transposition of two numbered tiles with the gap fixed cannot be undone. A chain of legal moves is a chain of such interchanges.
- CONFIRMED | "To undo it you'd need an odd number of moves" | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: odd-versus-even: Johnson, pp. 397-399, models slides by interchanges and proves "m is an even number" when the gap returns. An odd transposition of two numbered tiles with the gap fixed cannot be undone. A chain of legal moves is a chain of such interchanges.
- CONFIRMED | "J = sign(arrangement) × (−1)(taxicab distance of the gap from home)" | https://orbilu.uni.lu/bitstream/10993/40106/1/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: J-equation: Read the Luxembourg PDF, p. 2, after the automatic fetch failed. It says "all permutations with invariant 1 are possible configurations" and defines the invariant by transpositions plus the gap's row and column distances. The product form is equivalent; a legal slide flips both factors.
- CONFIRMED | "A slide flips the sign (one transposition) and moves the gap one step (changing its taxicab distance by exactly one, flipping that second factor too)." | https://orbilu.uni.lu/bitstream/10993/40106/1/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: J-two-flips: Read the Luxembourg PDF, p. 2, after the automatic fetch failed. It says "all permutations with invariant 1 are possible configurations" and defines the invariant by transpositions plus the gap's row and column distances. The product form is equivalent; a legal slide flips both factors.
- CONFIRMED | "Two flips multiply to no change." | https://orbilu.uni.lu/bitstream/10993/40106/1/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: J-conserved: Read the Luxembourg PDF, p. 2, after the automatic fetch failed. It says "all permutations with invariant 1 are possible configurations" and defines the invariant by transpositions plus the gap's row and column distances. The product form is equivalent; a legal slide flips both factors.
- CONFIRMED | "The solved board has J = +1." | https://orbilu.uni.lu/bitstream/10993/40106/1/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: solved-J: Read the Luxembourg PDF, p. 2, after the automatic fetch failed. It says "all permutations with invariant 1 are possible configurations" and defines the invariant by transpositions plus the gap's row and column distances. The product form is equivalent; a legal slide flips both factors.
- CONFIRMED | "a board is solvable ⟺ J = +1" | https://orbilu.uni.lu/bitstream/10993/40106/1/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: solvable-iff: Read the Luxembourg PDF, p. 2, after the automatic fetch failed. It says "all permutations with invariant 1 are possible configurations" and defines the invariant by transpositions plus the gap's row and column distances. The product form is equivalent; a legal slide flips both factors.
- CONFIRMED | "through one move or ten million." | https://orbilu.uni.lu/bitstream/10993/40106/1/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: constant-any-count: Read the Luxembourg PDF, p. 2, after the automatic fetch failed. It says "all permutations with invariant 1 are possible configurations" and defines the invariant by transpositions plus the gap's row and column distances. The product form is equivalent; a legal slide flips both factors.
- CONFIRMED | "You can read this bit straight off any arrangement without sliding a single tile" | https://orbilu.uni.lu/bitstream/10993/40106/1/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: read-J-without-slides: Read the Luxembourg PDF, p. 2, after the automatic fetch failed. It says "all permutations with invariant 1 are possible configurations" and defines the invariant by transpositions plus the gap's row and column distances. The product form is equivalent; a legal slide flips both factors.
- CONFIRMED | "The other half forms a second island the gap can never bridge to." | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: second-component: Story, pp. 400-402: "every arrangement whose order is positive, and only such, can be converted into the standard arrangement." This supports the two components and the home-gap even permutations for the ordinary rectangular boards discussed here. The universal invariant, including narrow grids, is separately proved in Lean.
- CONFIRMED | "The real 15-puzzle has about 1013 arrangements" | https://www.jaapsch.net/puzzles/fifteen.htm | N2 source reread at f5e5f84f34, retained from N2-codex.md: 15-scale: Jaap gives "16!/2 = 10,461,394,944,000 positions" reachable from a fixed solved state. This is about 10^13; the total unrestricted arrangements are 16! = 20,922,789,888,000, also of that order. The source's number is a reachable count, not the total.
- CONFIRMED | "But the search only ever visits finitely many boards" | https://www.jaapsch.net/puzzles/fifteen.htm | N2 source reread at f5e5f84f34, retained from N2-codex.md: finite-search: Jaap gives "16!/2 = 10,461,394,944,000 positions" reachable from a fixed solved state. This is about 10^13; the total unrestricted arrangements are 16! = 20,922,789,888,000, also of that order. The source's number is a reachable count, not the total.
- CONFIRMED | "a grid can be any size at all, and no search reaches the end of that." | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: all-grid-sizes: Story, pp. 400-402: "every arrangement whose order is positive, and only such, can be converted into the standard arrangement." This supports the two components and the home-gap even permutations for the ordinary rectangular boards discussed here. The universal invariant, including narrow grids, is separately proved in Lean.
- CONFIRMED | "When the gap is back in its home corner, the reachable boards are exactly the arrangements with even sign" | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: home-even: Story, pp. 400-402: "every arrangement whose order is positive, and only such, can be converted into the standard arrangement." This supports the two components and the home-gap even permutations for the ordinary rectangular boards discussed here. The universal invariant, including narrow grids, is separately proved in Lean.
- CONFIRMED | "the alternating group Aₙ, always half" | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: alternating-half: Johnson, pp. 398-399, proves that odd and even numbers of interchanges cannot give the same permutation and that one interchange flips the parity of the cycle count. Pairing each permutation with a fixed transposition gives equally many signs. Here the tile counts are 8 or 15, so the alternating group has index two.
- CONFIRMED | "you can never swap just two tiles" | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: no-two-swap: Johnson, pp. 397-399, models slides by interchanges and proves "m is an even number" when the gap returns. An odd transposition of two numbered tiles with the gap fixed cannot be undone. A chain of legal moves is a chain of such interchanges.
- CONFIRMED | "A two-tile swap is a single transposition, sign −1, odd" | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: two-swap-sign: Johnson, pp. 398-399, proves that odd and even numbers of interchanges cannot give the same permutation and that one interchange flips the parity of the cycle count. Pairing each permutation with a fixed transposition gives equally many signs. Here the tile counts are 8 or 15, so the alternating group has index two.
- CONFIRMED | "The smallest real rearrangement you can make is a three-tile cycle" | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: three-cycle-minimum: Story p. 401 constructs a move that replaces "a, b, c respectively" by "b, c, a". A 3-cycle is two transpositions; one changed tile is impossible for a permutation, and exactly two changed numbered tiles is odd.
- CONFIRMED | "because that takes two swaps, and two is even." | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: three-cycle-two-swaps: Story p. 401 constructs a move that replaces "a, b, c respectively" by "b, c, a". A 3-cycle is two transpositions; one changed tile is impossible for a permutation, and exactly two changed numbered tiles is odd.
- CONFIRMED | "Click a tile bordered in orange (next to the gap) to slide it, or use the arrow keys." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: board-input: Read render(), slide(), and keyMove(); "const adj = (Math.abs(r-br)+Math.abs(c-bc))===1" gates clicks, and arrow moves enforce bounds. Executed the pinned script with a minimal DOM in page-probe.mjs.
- CONFIRMED | "shuffle only ever makes legal slides, so it always lands you somewhere solvable." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: shuffle-legal: shuffleBySliding() begins "cur = goal.slice()" and swaps the blank only with an orthogonal neighbour. The executed probe reports "shuffle J: 1".
- CONFIRMED | "Loyd's swap sets it by hand into the impossible half" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: loyd-button: The button sets "[1,2,3,4,5,6,7,8,9,10,11,12,13,15,14,0]". The executed verdict is unsolvable with J = -1.
- CONFIRMED | "Set a board, and the oracle reads its J and gives a verdict instantly." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: oracle-instant: update() directly computes "const J = invariantJ(cur, goal, cols)" and updates the verdict without doing the BFS.
- CONFIRMED | "the program quietly builds the entire universe of boards you can reach from solved" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-entire: buildUniverse() explores legal neighbours from solved and never consults invariantJ. Executed independently from the verifier: "search reached 181,440". Thus its reachability decision does not assume the parity formula.
- CONFIRMED | "Run from the solved 3×3, it reaches 181,440 distinct boards and then stops, having found every move dead-ends back into the same set." | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-181440: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "half of 9! = 362,880" | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-factorial: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "it settles the claim independently of the parity argument." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-independent: buildUniverse() explores legal neighbours from solved and never consults invariantJ. Executed independently from the verifier: "search reached 181,440". Thus its reachability decision does not assume the parity formula.
- CONFIRMED | "The arithmetic and the brute-force search always agree." | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: oracle-search-agreement: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "of the 20,160 reachable home boards, the number that differ from solved in exactly two tiles is zero." | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: home-20160: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "over all 362,880 it confirms {J = +1} is precisely the reachable set, so the parity bit is necessary and sufficient;" | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: verifier-necessity-sufficiency: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "it checks that all 967,680 possible single slides leave J unchanged" | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: verifier-all-slides: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "Loyd's 14–15 swap has J = −1." | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: verifier-loyd: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "The textbook "inversions" rule is cross-checked against J on every 8-puzzle board and on 200,000 random 15-puzzle boards." | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: verifier-textbook: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "The mathematics (the count 181,440, the invariant, the 3-cycle minimum, the 8-puzzle diameter of 31) is computed from scratch in the verifier" | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: verifier-maths-from-scratch: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "Every board solved live in your browser;" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: browser-every-board: Read as a live decision of solvability, the page computes J for each board and can compute 8-puzzle distances by BFS. It does not claim to display a solving move sequence. The probe compares all 362880 page verdicts with BFS and reports 0 mismatches.
- CONFIRMED | "the parity bit J is preserved by every legal slide, on a board of every width and height" | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-universal: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "Lean 4, zero imports, so the only trusted component is the kernel" | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-zero-imports: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "proves it in two independent halves that meet at the end:" | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-two-halves: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "A slide flips permutation parity (swap_flips)." | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-swap-flips: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "transposing a and b changes the inversion count by an odd number." | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-inversions: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "The entire content is that the two orderings' inversion counts sum to something odd: the mixed a-vs-M and b-vs-M terms pair up to exactly 2·|M|, and all that survives is the single a-vs-b comparison, which is odd because a ≠ b." | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-pairing: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "A slide flips the gap's checkerboard colour (cellSum_flip)." | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-colour: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "The blank's row + column changes by exactly one on any legal step (right by a column, not off the row edge, or down by a row), so its parity flips too." | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-row-column: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "Two flips cancel, so J is preserved (slide_preserves_J), constant across every board a sequence of slides can reach (reachable_preserves_J)" | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-invariant: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "the board that swaps two tiles has the opposite J, so it is walled off forever (two_swap_unreachable)" | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-two-swap: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "Loyd's 14–15 board being the named 4×4 case (loyd_unreachable)." | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-loyd-named: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "The Slide relation is a faithful model of a real slide (a horizontal move is M = [] with the gap off the edge, a vertical move is |M| = w−1, both directions allowed)" | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-model: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "two worked examples prove it is genuinely inhabited, so none of this is vacuously true." | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-inhabited: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "Every theorem's axiom footprint is [propext, Quot.sound]: no sorry, no Classical.choice, no native_decide." | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-axioms: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "the JS bit's solvability class matches J on all 362,880 boards" | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: lean-matches-all: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "Wm. W. Johnson & W. E. Story, "Notes on the '15' Puzzle", American Journal of Mathematics 2 (1879) 397–404" | https://api.crossref.org/works/10.2307/2369492 | N2 source reread at f5e5f84f34, retained from N2-codex.md: citation-johnson: Crossref matches title, authors, year and volume. Crossref's page field is only "397"; the independently opened original PDF cover supplies the complete pp. 397-404 range.
- CONFIRMED | "R. M. Wilson, "Graph puzzles, homotopy, and the alternating group", J. Combinatorial Theory Ser. B 16 (1974) 86–96" | https://api.crossref.org/works/10.1016/0095-8956(74)90098-7 | N2 source reread at f5e5f84f34, retained from N2-codex.md: citation-wilson: Crossref identifies "Richard M", "Wilson", year 1974, volume "16", and pages "86-96"; the title matches.
- CONFIRMED | "Jerry Slocum & Dic Sonneveld, The 15 Puzzle: How It Drove the World Crazy (Slocum Puzzle Foundation, 2006)" | https://openlibrary.org/books/OL17219890M.json | N2 source reread at f5e5f84f34, retained from N2-codex.md: citation-book: The catalog gives "The 15 puzzle", "2006", and "Slocum Puzzle Foundation"; its by_statement names Jerry Slocum and Dic Sonneveld. Richeson supplies the longer subtitle.
- CONFIRMED | "David Richeson, "A picture of frustration: Sam Loyd's 15 puzzle" (2011)" | https://divisbyzero.com/2011/03/01/a-picture-of-frustration-sam-loyds-15-puzzle/ | N2 source reread at f5e5f84f34, retained from N2-codex.md: citation-richeson: The retrieved page says "A picture of frustration: Sam Loyd’s 15 puzzle" and "Posted by Dave Richeson on March 1, 2011".
- CONFIRMED | "Jaap Scherphuis, "The Fifteen / 14-15 puzzle" (jaapsch.net)." | https://www.jaapsch.net/puzzles/fifteen.htm | N2 source reread at f5e5f84f34, retained from N2-codex.md: citation-jaap: The retrieved page is Jaap's Fifteen/14-15 puzzle article. Its title and puzzle description match the citation.
- CONFIRMED | "Companion film" [...] "2:30" | https://artwaste.land/strata/the-half-you-can-never-reach/film.mp4 | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-duration: Fetched only the first 1048576 bytes of the live faststart MP4 (HTTP 206). ffprobe reports "duration": "150.000000", "codec_name": "h264" and "codec_name": "aac", with a 1920 by 1080 picture.
- CONFIRMED | "(MP4 / H.264 + AAC)." | https://artwaste.land/strata/the-half-you-can-never-reach/film.mp4 | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-codecs: Fetched only the first 1048576 bytes of the live faststart MP4 (HTTP 206). ffprobe reports "duration": "150.000000", "codec_name": "h264" and "codec_name": "aac", with a 1920 by 1080 picture.
- CONFIRMED | "The verdict J on screen is the exact invariant from research/fifteen-puzzle/verify.mjs (36/36), computed live from the board being drawn (re-enacted, not quoted);" | git show f5e5f84f34:research/fifteen-puzzle/film/film.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-invariant: The film computes "const J = invariantJ(CUR_BOARD, goal, CUR_COLS)". Its permSign and gapTaxicab implement the same rank-cycle and Manhattan-distance functions as the verifier.
- CONFIRMED | "a full breadth-first search of the 8-puzzle drawing its own God's-number histogram up to exactly 181,440 reachable boards (half of 362,880);" | git show f5e5f84f34:research/fifteen-puzzle/film/film.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-BFS: Read godsNumberProfile(): it runs legal-neighbour BFS and sets "const PROFILE = godsNumberProfile()". Counter and histogram values are derived from PROFILE. The same audio BFS prints "sum = 181440".
- CONFIRMED | "why you can never swap just two tiles, only three-cycle them (the group A₈ = 20,160);" | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-only-three: The verified home-group count is 20160 = 8!/2. Read in the context of the minimum rearrangement and generation of even permutations, the three-cycle description is supported.
- CONFIRMED | "the music is a declared sonification of the same BFS and parity." | git show f5e5f84f34:research/fifteen-puzzle/film/make-audio.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-sonification: The source declares "THE REACHABLE UNIVERSE" and "THE SIGN THAT FLIPS". Its PROFILE drives CONTOUR, and "const sign = (b % 2 === 0) ? 1 : 0" drives pulse accents. The audio command successfully generated the declared 150-second track.
- CONFIRMED | "Now each tick and each "agrees" depends on the value the page computed, and the panel's 181,440 line points to the search button instead of ticking a count it has not run." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: correction-now-gated: Executed the original page script in page-probe.mjs. Solved and swapped boards produce the proper search results. Positive controls force each wrong oracle class and a count of 181441; the page prints "DISAGREES" and "MISMATCH" as appropriate. The normal BFS gives 181440 and distances including 0 and 31.
- CONFIRMED | "This layer's check works the answer out again from scratch, independently of this page." | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: check-independent: Read the complete verifier: it recomputes from goal states and its only external evidence read is "readFileSync(leanFile, 'utf8')". It does not read the page. Step 6's self-reading-transcript condition does not apply.
- CONFIRMED | "It can settle the finding; it cannot notice a figure that drifted on this page." | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: check-blind: Read the complete verifier: it recomputes from goal states and its only external evidence read is "readFileSync(leanFile, 'utf8')". It does not read the page. Step 6's self-reading-transcript condition does not apply.
- CONFIRMED | "It is published to read. Running it needs the repository around it." | git show f5e5f84f34:public/checks/manifest.json | N2 source reread at f5e5f84f34, retained from N2-codex.md: check-published: Downloaded the exact linked verifier into an empty reader directory. It matches the pinned bytes. Alone it exits 1 with "26 checks passed, 1 FAILED" at "Lean proof file present"; the full scratch tree passes 36. This matches the page's stated repository requirement.
- CONFIRMED | "invariant J = sign × (−1)^taxicab" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: display-J: Executed update() and the check-panel initializer. The solved readout is "moves made 0 sign +1 (even) inversions 0 gap row (from bottom) 1". Loyd and 7/8 swaps give J = -1; the three-cycle gives sign +1; all four calculated ticks pass.
- CONFIRMED | "solvable" [...] "J = +1 (in the reachable half)" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: display-solvable: Executed update() and the check-panel initializer. The solved readout is "moves made 0 sign +1 (even) inversions 0 gap row (from bottom) 1". Loyd and 7/8 swaps give J = -1; the three-cycle gives sign +1; all four calculated ticks pass.
- CONFIRMED | "unsolvable" [...] "J = −1 (the half no slide can reach)" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: display-unsolvable: Executed update() and the check-panel initializer. The solved readout is "moves made 0 sign +1 (even) inversions 0 gap row (from bottom) 1". Loyd and 7/8 swaps give J = -1; the three-cycle gives sign +1; all four calculated ticks pass.
- CONFIRMED | "fewest slides to solve:" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-distance: Executed the original page script in page-probe.mjs. Solved and swapped boards produce the proper search results. Positive controls force each wrong oracle class and a count of 181441; the page prints "DISAGREES" and "MISMATCH" as appropriate. The normal BFS gives 181440 and distances including 0 and 31.
- CONFIRMED | "The oracle said solvable; the search agrees." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-agrees-yes: Executed the original page script in page-probe.mjs. Solved and swapped boards produce the proper search results. Positive controls force each wrong oracle class and a count of 181441; the page prints "DISAGREES" and "MISMATCH" as appropriate. The normal BFS gives 181440 and distances including 0 and 31.
- CONFIRMED | "The oracle said unsolvable; the search agrees, with no parity formula assumed." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-agrees-no: Executed the original page script in page-probe.mjs. Solved and swapped boards produce the proper search results. Positive controls force each wrong oracle class and a count of 181441; the page prints "DISAGREES" and "MISMATCH" as appropriate. The normal BFS gives 181440 and distances including 0 and 31.
- CONFIRMED | "The oracle said unsolvable; the search DISAGREES." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-disagrees-yes: Executed the original page script in page-probe.mjs. Solved and swapped boards produce the proper search results. Positive controls force each wrong oracle class and a count of 181441; the page prints "DISAGREES" and "MISMATCH" as appropriate. The normal BFS gives 181440 and distances including 0 and 31.
- CONFIRMED | "The oracle said solvable; the search DISAGREES." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-disagrees-no: Executed the original page script in page-probe.mjs. Solved and swapped boards produce the proper search results. Positive controls force each wrong oracle class and a count of 181441; the page prints "DISAGREES" and "MISMATCH" as appropriate. The normal BFS gives 181440 and distances including 0 and 31.
- CONFIRMED | "the search built the entire reachable half and your scramble isn't in it." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-absent: Executed the original page script in page-probe.mjs. Solved and swapped boards produce the proper search results. Positive controls force each wrong oracle class and a count of 181441; the page prints "DISAGREES" and "MISMATCH" as appropriate. The normal BFS gives 181440 and distances including 0 and 31.
- CONFIRMED | "a two-tile swap is always locked out" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: check-panel-two: Executed update() and the check-panel initializer. The solved readout is "moves made 0 sign +1 (even) inversions 0 gap row (from bottom) 1". Loyd and 7/8 swaps give J = -1; the three-cycle gives sign +1; all four calculated ticks pass.
- CONFIRMED | "the smallest move you actually can make" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: check-panel-three: Executed update() and the check-panel initializer. The solved readout is "moves made 0 sign +1 (even) inversions 0 gap row (from bottom) 1". Loyd and 7/8 swaps give J = -1; the three-cycle gives sign +1; all four calculated ticks pass.
- CONFIRMED | "solved board: J = +1 (solvable, as it must be)" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: check-panel-solved: Executed update() and the check-panel initializer. The solved readout is "moves made 0 sign +1 (even) inversions 0 gap row (from bottom) 1". Loyd and 7/8 swaps give J = -1; the three-cycle gives sign +1; all four calculated ticks pass.
- CONFIRMED | "Loyd's 14–15 swap: J = −1 → UNSOLVABLE" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: check-panel-loyd: Executed update() and the check-panel initializer. The solved readout is "moves made 0 sign +1 (even) inversions 0 gap row (from bottom) 1". Loyd and 7/8 swaps give J = -1; the three-cycle gives sign +1; all four calculated ticks pass.
- CONFIRMED | "swap any two tiles (e.g. 7↔8): J = −1 → a two-tile swap is always locked out" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: check-panel-swap: Executed update() and the check-panel initializer. The solved readout is "moves made 0 sign +1 (even) inversions 0 gap row (from bottom) 1". Loyd and 7/8 swaps give J = -1; the three-cycle gives sign +1; all four calculated ticks pass.
- CONFIRMED | "a three-tile cycle: sign = +1 (even) → the smallest move you actually can make" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: check-panel-cycle: Executed update() and the check-panel initializer. The solved readout is "moves made 0 sign +1 (even) inversions 0 gap row (from bottom) 1". Loyd and 7/8 swaps give J = -1; the three-cycle gives sign +1; all four calculated ticks pass.
- CONFIRMED | "the index of coincidence is invariant over all 26! ways to relabel the alphabet, so a substitution cipher can't hide a language's lumpiness;" | git show f5e5f84f34:research/invariant-of-relabeling/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: related-IC: The cited excerpt says coincidence "depends only on the sorted frequency multiset". A bijection of 26 symbols preserves every count and therefore sum n_i(n_i-1), proving the index unchanged for all 26! relabelings.
- CONFIRMED | "The billiard launched from a square's corner can never return home because the first lattice point a primitive direction meets is never (even,even);" | git show f5e5f84f34:research/unilluminable-room/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: related-billiard: The source's squareCornerLemma uses "gcdB(BigInt(p), BigInt(qd)) !== 1n" to select primitive directions and tests corner type "0,0". Two even coordinates cannot be primitive; irrational directions meet no lattice point. The statement is about the first corner hit, with corner collisions terminating the ray.
- CONFIRMED | "the sliding puzzle can never reach half its boards because every move flips a sign that home requires unchanged." | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: related-slide-sign: The invariant combines permutation sign and gap position. A return of the gap has an even move count, so an odd two-tile swap remains impossible. The cited verifier reproduces 0 parity mismatches.
- CONFIRMED | "The Thue–Morse sequence is the bit-parity of each integer" | https://arxiv.org/pdf/1110.1137 | N2 source reread at f5e5f84f34, retained from N2-codex.md: related-thue-bits: Cooper and Dutle define the sequence using "the number of 1’s in the binary expansions". This is binary digit parity, matching the claim.
- CONFIRMED | "There, a two-colouring proves no domino tiling can cover the mutilated board;" | git show f5e5f84f34:research/the-mutilated-chessboard/lean/MutilatedChessboard.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: related-chessboard: Read the complete proof: "mut_light : lightCount mutilated = 30", "mut_dark : darkCount mutilated = 32", and mutilated_chessboard quantify over every list of dominoes with valid adjacency and exact cover. The kernel accepts the theorem with [propext, Quot.sound].
- CONFIRMED | "both for all cases at once, zero imports, footprint [propext, Quot.sound]." | git show f5e5f84f34:research/the-mutilated-chessboard/lean/MutilatedChessboard.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: related-chessboard-axioms: Read the complete proof: "mut_light : lightCount mutilated = 30", "mut_dark : darkCount mutilated = 32", and mutilated_chessboard quantify over every list of dominoes with valid adjacency and exact cover. The kernel accepts the theorem with [propext, Quot.sound].
- CONFIRMED | "Two childhood grid games with deep theory hiding under the rules, and in both the truth is settled by an exhaustive computer search you can watch run." | git show f5e5f84f34:public/strata/all-but-two/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: related-all-but-two: The linked page includes full minimax results for small boards and a live exactBestMove endgame search. It explicitly identifies the offline "--full" run and bounds the live search. The broad connection is supported for those small boards and endgames, not arbitrary large games.
- CONFIRMED | "The same move, machine-checked: a parity invariant that a brute-force search can only sample gets handed whole to the Lean kernel." | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: related-parity-proofs: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.
- CONFIRMED | "moves made 0 sign +1 (even) inversions 0 gap row (from bottom) 1" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: readout-solved-eight: Executed update() and the check-panel initializer. The solved readout is "moves made 0 sign +1 (even) inversions 0 gap row (from bottom) 1". Loyd and 7/8 swaps give J = -1; the three-cycle gives sign +1; all four calculated ticks pass.
- CONFIRMED | "exactly 9!/2 = half of 362,880." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-count-half: Executed the original page script in page-probe.mjs. Solved and swapped boards produce the proper search results. Positive controls force each wrong oracle class and a count of 181441; the page prints "DISAGREES" and "MISMATCH" as appropriate. The normal BFS gives 181440 and distances including 0 and 31.
- CONFIRMED | "(expected 181,440 = 9!/2, half of 362,880: MISMATCH)." | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: search-count-mismatch: Executed the original page script in page-probe.mjs. Solved and swapped boards produce the proper search results. Positive controls force each wrong oracle class and a count of 181441; the page prints "DISAGREES" and "MISMATCH" as appropriate. The normal BFS gives 181440 and distances including 0 and 31.
- CONFIRMED | "full 8-puzzle search (button above): press it, and it should reach 181,440 = 9!/2, half of 362,880 (it prints its own count)" | git show f5e5f84f34:public/strata/the-half-you-can-never-reach/index.html | N2 source reread at f5e5f84f34, retained from N2-codex.md: check-panel-request: Executed the original page script in page-probe.mjs. Solved and swapped boards produce the proper search results. Positive controls force each wrong oracle class and a count of 181441; the page prints "DISAGREES" and "MISMATCH" as appropriate. The normal BFS gives 181440 and distances including 0 and 31.
- CONFIRMED | "c. 1874 Noyes Chapman invents the sliding puzzle" | https://divisbyzero.com/2011/03/01/a-picture-of-frustration-sam-loyds-15-puzzle/ | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-history-chapman: Richeson: "invented around 1874 by Noyes Palmer Chapman, a postmaster from Canastota, New York." The surrounding paragraph attributes the research to Slocum and Sonneveld.
- CONFIRMED | "1879 Johnson & Story prove half the boards are impossible" | https://sites.math.rutgers.edu/~zeilberg/math436/15puzzle.pdf | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-history-johnson: The original cover identifies "Wm. Woolsey Johnson and William E. Story" and "Vol. 2, No. 4 (Dec., 1879), pp. 397-404". Sections I and II supply impossibility and sufficiency. Richeson calls it the "first proof in 1879".
- CONFIRMED | "2006 Slocum & Sonneveld: the claim had "fooled everyone for 115 years"" | https://divisbyzero.com/2011/03/01/a-picture-of-frustration-sam-loyds-15-puzzle/ | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-history-quote: The quoted words "Fooled Everyone for 115 Years" occur in the book subtitle. The source identifies both authors; the Open Library catalog independently dates the book to 2006. This is a subtitle quotation, not a separately documented remark.
- CONFIRMED | "The hardest position is 31 slides from solved; exactly 2 boards sit that far away." | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-max-distance: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "A₈ = 20,160 = 8!/2" | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-count-A8: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "checked on 967,680 of them, 0 changed it" | git show f5e5f84f34:research/fifteen-puzzle/verify.mjs | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-slides-count: Recreated with the pinned verifier: "all 36 checks passed". It prints reachable 181440, parity disagreements 0, slides checked 967680 with 0 changes, home states 20160 with 0 two-swaps, diameter 31 with 2 deepest states, and 0 textbook/Lean-bit mismatches. Read the loops and compared them with the supplied excerpt.
- CONFIRMED | "No sequence of slides undoes a single swap." | git show f5e5f84f34:research/fifteen-puzzle/lean/FifteenPuzzle.lean | N2 source reread at f5e5f84f34, retained from N2-codex.md: film-no-slide-undo: Read the full Lean file and its stated hypotheses. The actual kernel run accepts the five named main theorems with "[propext, Quot.sound]". swap_flips pairs the mixed counts; cellSum_flip checks horizontal/vertical adjacency; Move permits either direction; Reachable is inductive; two explicit examples establish non-vacuity. The theorem proves invariant preservation and two-tile impossibility for every positive width, not general sufficiency.

## Findings
- [fixed] X1: Corrected the authored plain summary and regenerated its meta copy. The historical account now dates the published challenge to 1896 and states the gap-home condition. Dated correction C1; the film copies are held separately under X17 and X18.
- [fixed] X2: Separated the 1880 craze from the 1896 challenge, removed the attribution of the craze to Loyd, and used the documented divided reward rather than first-solver terms. Dated correction C1.
- [fixed] X3: Replaced the Johnson/Story role assignment with Johnson's parity obstruction and Story's construction/generalization. Dated correction C2.
- [fixed] X4: Restricted the obstruction to an odd starting arrangement whose gap is home. The two-move positive control succeeds. Dated correction C3.
- [open note:d00496] X5: The dek, page body and film source now allow the identical-R double-transposition counterexample and retain the three-cycle minimum. The published film still has the universal grid-trick caption at 01:35, as inspected by the fix-checker. No media was regenerated. Dated correction C4 now discloses the remaining copy.
- [fixed] X6: Changed only the BFS-reached count to 181,440 in the page and Lean README; kept 362,880 for all arrangements. Dated correction C5.
- [fixed] X7: Narrowed Every number to the mathematical counts in the markdown. Record only, no dated page line for this MINOR.
- [fixed] X8: Qualified the page, verifier comment and research README: exact integer exhaustive counts, floating-point auxiliary statistic. Regenerated the published verifier copy. Record only, no dated page line for this MINOR.
- [fixed] X9: Narrowed the footer to the mathematical counts. Record only, no dated page line for this MINOR.
- [fixed] X10: Replaced the two-name denylist with an allowlist and required footprints for all five named theorems. Validated an actual added-axiom rejection plus smaller, wrapped, missing and malformed footprint controls. Regenerated the published verifier. Dated correction C6.
- [fixed] X11: Qualified the markdown body and dek with toolchain availability. Record only, no dated page line for this MINOR.
- [fixed] X12: Restored both reachability alternatives, the non-separable hypothesis, and the polygon/one-other-graph exceptions. Dated correction C7.
- [fixed] X13: Replaced the fresh-checkout promise with actual prerequisites, documented setup in the film README, and qualified the build script's output reproducibility comment. No film build was run. Dated correction C8.
- [dated] X14: Regenerated the existing Last verified field from this 2026-10-14 record, after the 36/36 verifier run. The triage explicitly exempts this placard field from an Updated line.
- [dated] X15: Set Article dateModified to 2026-10-14. Corrected lines date the revision; the triage explicitly exempts this metadata field from a separate Updated line.
- [fixed] X16: Replaced unrestricted exact fairness with the power-sum block condition and an explicit denial of universal equal shares. Dated correction C9.
- [open note:d00496] X17: Source fixed; the published film at 00:17 and poster.jpg still attach St Louis and 1891 to the prize. The editable header says 4 January 1896 and supplies no city. Both media assets need correction; rendering and re-encoding are prohibited in this pass. C1 and the film notice disclose both assets.
- [open note:d00496] X18: Source fixed; the published film at 02:03 still combines the 1891 inventorship claim with the prize. The source keeps 1891 for inventorship and gives the prize its separate 1896 date. C1 discloses the unchanged film. The directing instance must file the media follow-up and replace PENDING with its actual board ID.
- [fixed] X19: Initialized Instrument I with the 14/15-swapped array already used by its Loyd button. The extracted controller confirms J=-1 initially, while shuffle remains J=+1. Dated correction C10.
- [fixed] X20: Changed the shared-concept sentence to parity, keeping binary digit parity and permutation/gap parity distinct. Regenerated the nearby teaser from frontmatter. Dated correction C9.

- [open note:d00496] R1: Removed the inference about Loyd's knowledge from the editable film caption. The same inference remains in film.mp4 at 00:17 and in poster.jpg. Dated correction C11 states the documentary distinction without guessing a mental state.
- [open note:d00496] R2: Repaired the remaining prize-impossibility wording in the page, its film description and labels, the film source, and the verifier heading. The published film and poster still conflate the 1896 challenge with the stricter gap-home goal. Dated correction C11 and the film notice disclose that limit.

## Evidence limits

The historical repair distinguishes the documented 1896 article from Loyd's retrospective account. Slocum, pp. 15-17, states the divided reward and explains the omitted final blank position. The repaired prose states the stricter gap-home goal and does not turn nonpayment into evidence of knowledge. N2's history-arrangement entry concerns the retrospective Cyclopedia account, not the 1896 terms. R1 and R2 revise N2's knowledge and prize-impossibility inferences; their original quoted claims are preserved. No city or contrary mental state is substituted.

The new power-sum condition is stated in src/content/strata/the-fairest-order.md and public/strata/the-fairest-order/index.html. The 181,440 replacement is the count produced by this page's own buildUniverse, independently reproduced by research/fifteen-puzzle/verify.mjs. All dated repair text uses the directing pass date, 2026-10-14.

## Not done

The film MP4, audio, poster and share images were not rendered or re-encoded. X5 and X18 remain in the film; X17, R1 and R2 remain in the film and poster. The follow-up text is in research/assay-line/queue-1014c/the-half-you-can-never-reach/pending-board-note.json and repair-report.md; it has no assigned board ID. The OG image was inspected and shows no erroneous date, universal three-cycle claim, or prize-impossibility explanation. Shared publication manifests, published check copies and shared scripts were not edited in this repair. No other layer or memory log was changed.