Historical rules meet model checking
The One Move That Changed the Game
Recomputing the frozen publication result locally.
Provenance before result: Lucas did not publish a second edition. His 1887 article printed the retreat rule, solved that game, then recommended removing the complication. This page compares Roy’s patent with Lucas’s proposed simplification. Whether a commercial printing adopted it remains unknown.
Running the complete finite comparison.
Enumerating locally from the transcribed rules.
The first difference
Four moves, two boards
The first three concrete moves exist in both machines. The fourth is Roy’s one-time permission for a tower that has never moved. Lucas’s proposed deletion refuses it.
The ordinary method beside the foreign one
What counts as the same game?
Lucas judged the complication unnecessary because deleting it did not change the initial winner. A full native tablebase and the imported instrument both detect change, but certify different consequences.
The initial two-number native summary ties at Tower win, rank 16. The complete native tables do not tie: 162 Roy history states, covering 102 Lucas projections, change winner. The baseline was frozen before this artifact ran equivalence, but the scout had already seen the four-ply split, so the study was not blinded. Infinite evasion and a Tower-turn deadlock count as Army success in the native solver; neither convention enters the trace comparison.
Observation sensitivity
With mover-only labels the trace result is HELD: both machines admit an infinite play, so both languages contain every finite prefix of A,T,A,T,.... The broader phrase “the game changed” is therefore conditional on observing exact moves.
The declared exact-move result
Every action here is the exact triple mover:from>to. From any state, one such label has at most one successor. The machines are deterministic, so closure of the synchronized product is exactly equality of their prefix-closed exact-move legal trace languages.
Fault injection
Break the evidence two ways
Choose a fault. Each click clones the typed source fixture, doctors its data, and runs the same constructor and comparator as the headline result.
Every number has a route home
The check
The same dependency-free modules run here and in the check that stands behind this page. Published observations are named as published; generated values are inserted only after the browser completes the finite searches.
Home calibration
Independent transcriptions
Lucas’s placement arithmetic
Ordinary native tablebase
Imported target test
Fault controls
Home field: strong bisimulation before history
The engine first runs the deterministic right-hand alarm clock from Figure 2.5 of Groote and Mousavi’s Modeling and Analysis of Communicating Systems: unset --set--> set, then alarm loops and reset returns to unset. A renamed copy must yield exactly {(unset,q0), (set,q1)}. Deleting only the renamed reset transition must break at depth 2 on [set, reset]. It also runs the published nondeterministic three-state clock against the right-hand clock: their trace languages must be HELD while strong bisimulation must be BROKE. The historical target is disabled unless all checks pass.
Scan against OCR, two visible corrections
Letter a and digit 0 remain distinct.
C(11,3) × 8 = 165 × 8 = 1,320, which independently checks the scan.
Adapter audit: loss first
Every mapping destroys context. Red text is the loss, not a footnote. The legal machine retains topology, setup, turns, moves, history, and immediate immobilization only.
Complete node renaming:
Both 22-road transcriptions:
| Source field | Formal field | Convention supplied | What is lost |
|---|
Fields dropped completely
Hand-supplied conventions
Ablate one mapping at a time
“Survives” means the initial native values and headline four-ply mismatch remain exactly unchanged. Every row below was computed once at startup. Pressing its RUN button clones the source fixture, disables that field in the data, and reruns the unchanged production constructor, native solver, and synchronized comparison. A missing mapping reports its named constructor failure.
| Disabled | Computed result | Headline survives? |
|---|
Independent target checks
Lucas’s scan prints the corrected placement count 1,320. The withheld current Ludii description parses to Towers moving only Forwards Rightward Leftward and carries no virgin-piece flag. Piette et al. (2021) independently report that Towers win the no-retreat Lucas game. Neither source was used to tune the historical adapter. Their win statement is weaker than this page’s computed 16-individual-ply optimum; Lucas’s “douzaine de coups” and the paper’s 24-ply line use a unit that should not be silently equated with this one. Ludii 1.3.14 also contains an extra Army-home terminal that this page does not model.
Source fetch ledger and reuse boundary
Fetched 10 September 2026. No key, login, or registration was used. Restricted scans are linked but not shipped. Auxiliary rights and catalogue pages were hashed separately from the target extract.
| Source and role | HTTP | Bytes | Type | SHA-256 | Licence and access |
|---|
Uncertainties, exclusions, and search boundary
- No stable direct INPI image for patent 173665 was obtained. Boutin’s protected 2020 article is a wrapper around the reproduced patent, so none of its pages are shipped.
- The first-move consumption of a retreat privilege is the natural reading of “those which have not yet been moved,” but no contemporary worked position was found that tests a forward-first tower. The executable convention probe separates it from the looser lifetime-token reading on A:2>5, T:1>4, A:5>2, T:4>1.
- The source says a move limit was fixed in advance but does not preserve its value. Under the page’s modern unbounded convention both initial positions are Tower wins at rank 16. A cap below 16 individual plies makes the Army succeed in both; a cap at or above 16 permits the Tower win.
- The fetched Ludii 1.3.14 rules add an immediate Army-home terminal that this page omits. The held-out Ludii result therefore checks the weaker Tower-win claim, not this page’s complete rank map.
- Whether a commercial 1887 printing enacted Lucas’s proposal is unknown. A dated rules leaflet would decide it.
- CNUM allows attributed noncommercial reuse and requires permission for commercial reuse. This page redraws factual topology and embeds no scan crop.
- Semantic Scholar was attempted without a key and returned HTTP 429. It is not counted as searched coverage.
We searched Crossref, OpenAlex, the open web, the Digital Ludeme Project and Ludii catalogue, Google Patents, INPI discovery pages, and Internet Archive on 10 September 2026, and did not find a legal-trace or bisimulation comparison between Roy’s 1886 patent rules and Lucas’s 1887 proposed no-retreat simplification.