langtons_highway: SAT catalogue of every highway up to period 104

[CrazyDubya]

What this is

The follow-up to #14 that goes after the conjecture from a different direction than brute-forcing seeds: enumerate every possible highway shape, i.e. every periodic-with-drift orbit of the ant on a white background, up to a given period.

A highway with period P and drift d is a configuration C and a P-step walk such that running the ant on C for P steps yields C translated by d. For fixed (P, d) that is a finite SAT problem.

• highway_catalogue.py: builds the SAT instance (one-hot ant position and heading per step, per-cell colour epochs, the read/flip/move rules, and the periodicity constraint "colour of q+d after the period = colour of q before it, white beyond the window"), enumerates all solutions with CaDiCaL, blocking every cyclic shift of each one found.
• Each solution is re-verified independently of the encoding: from the read sequence alone, the walk determines the only consistent starting configuration (parity of visits along the forward ray q+d, q+2d, …); the plain ant from ant.py must replay the reads and end at d with the same heading. Convexity of the window then guarantees the cycle repeats forever.
• Two scopes: an unrestricted window (any walk returning to d after P steps; feasible to P≈50) and an anchored box window (footprint bounding box ≤ (R+1)×(R+1), period anchored at the footprint's leftmost-bottom cell), which is what makes P≈100 feasible.
• catalogue_summary.py: aggregates runs, checks the (P, d) grid is complete for the stated scope, groups highways by canonical read sequence.

Result

Within the searched scope there is exactly one highway, and it is the classic one.

scope	instances	solve time	highways
every even P ≤ 50, every drift with |d|₁ ≤ 6, unrestricted window	284	35 min	0
every even P ≤ 104, every drift, footprint fitting a 9×9 box	1,754	2.4 h	1: the classic (P=104, d=(2,2), 41 cells, verified)

The (P, d) grid is complete for both scopes, no solution failed verification, and the classic highway appears exactly where it must (P=104, d=(2,2)), which is the encoding's end-to-end check. Consequence: any counterexample to the strong conjecture ("the 104-highway is the unique attractor") must have period > 104, or a one-period footprint wider than 9 cells, or both.

Data: data/catalogue/instances_r8.jsonl, instances_unrestricted.jsonl, summary.json. README has a new section stating the result and its exact scope.

Testing

pytest langtons_highway/tests -o addopts="" → 8 passed (two new: verifier accepts the classic highway and rejects a corrupted copy; a small instance is unsatisfiable). flake8 --isolated --max-line-length=127 langtons_highway clean. build CI fails for the pre-existing .flake8 reason documented on #14.

Note on the commit history

The many "sweep snapshot" commits are append-only checkpoints of the results file taken while the 2.4 h sweep ran; the final commit supersedes them. Squash-merge recommended.

🤖 Generated with Claude Code

https://claude.ai/code/session_01DVvB1dWEhjyBKh95Zojt3F

[CrazyDubya]

CI status: build is red for the pre-existing reason, not this PR's.

Same traceback as every run on main, at the first lint step, before any file is linted:

ValueError: Error code '#' supplied to 'extend-ignore' option does not match '^[A-Z]{1,3}[0-9]{0,3}$'

This PR does not touch .flake8 or the workflow. Diagnosis, evidence that main fails identically, and a proposed patch are in the comment on #14; no fix PR exists to port, and a re-run would reproduce the same deterministic config error.

This PR's own checks: pytest langtons_highway/tests -o addopts="" → 8 passed; flake8 --isolated --max-line-length=127 langtons_highway clean.

---

Generated by Claude Code

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: b50885a5d7

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Include drifts ending just beyond the footprint

For a radius R search, the footprint consists of the P cells read at positions p0..p(P-1), while d=pP is the first position of the next period. The final move can therefore place d at coordinate R+1 even though every cell in the footprint remains within 0..R; for example, the advertised 9×9 scope can contain a candidate ending with drift (9, 1). Restricting both drift components to <= R means those candidates are never submitted, so the README's conclusion that every period-≤104 highway fitting a 9×9 box was searched is not established.

Useful? React with 👍 / 👎.

[chatgpt-codex-connector]

Avoid appending a full rerun to the existing catalogue

The documented reproduction command uses the default output directory, which already contains the committed instances_r8.jsonl, so running it appends another complete set of 1,754 instances rather than regenerating the catalogue. catalogue_summary.py then counts both copies, doubling instance counts and solve time and duplicating each highway's found_in entry. The sweep should overwrite the output for a fresh run or explicitly deduplicate/resume by (P, d).

Useful? React with 👍 / 👎.

[chatgpt-codex-connector]

Exclude unverified SAT models from highway counts

If the SAT encoding produces a model that the independent verifier rejects, it is still included in prim and reported as a primitive highway; the generated summary likewise consumes every stored solution. This is precisely the failure mode the verifier is intended to catch, and future scopes containing any false-positive model would therefore publish an incorrect highway count. Filter on s["verified"] or fail the run when verification is false.

Useful? React with 👍 / 👎.