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.

computing

Running the complete finite comparison.

Enumerating locally from the transcribed rules.

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

waiting

Independent transcriptions

waiting

Lucas’s placement arithmetic

waiting

Ordinary native tablebase

waiting

Imported target test

waiting

Fault controls

waiting
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
initial tower labelOCR o   scan 3

Letter a and digit 0 remain distinct.

raw placementsOCR 1520   scan 1320

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: waiting

Both 22-road transcriptions: waiting

Source fieldFormal fieldConvention suppliedWhat 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.

      DisabledComputed resultHeadline survives?
      Independent target checks
      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 roleHTTPBytesTypeSHA-256Licence 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.