# The Proving Grounds

Four new games bring the arcade to **55**. Each one is built on a part of Lars Rocha's pytoolz that the arcade had not used before, and each answer it gives comes with its proof: rule 30 run backwards, clock banks whose periods are settled by algebra, primes that arrive with a certificate, and the light-cone edge known a quintillion generations out. Nothing in this wing is fitted or learned; there is no WSRF model here, on purpose, and every claim the games make was re-derived by the Python modules before it shipped.

| Game | Play | What it does | Library |
| --- | --- | --- | --- |
| The Rewind Loom | `games/rewind-loom/` | Read one cell of a rule 30 row's predecessor by uncovering as few cells as possible. Reading 0·1·0 resets the three-state inverse machine, and everything below is forced. | `ntmc`: `inverse`, `preimages`, `cell_sync`, `Inverse3` |
| The Belfry | `games/belfry/` | Twenty bells on one shift-XOR register; every bell's period is a power of two computed with no ticks run. Meet the order with the fewest ropes, then ring the peal. | `driver_lab.spectrum_linear_exact`, `txs`: `synthesize`, `cheapest`, `Bank` |
| Rollball Tower | `games/rollball-tower/` | Climb from M31 = 2³¹−1: N = 2kq + 1 off the prime below, weighed on a wheel of small primes and proved with a Pocklington witness. The climb downloads as a certificate. | `lars_approves_of_pocklington_walk`, `numtools.verify_certificate` |
| Edge Fortune | `games/edge-fortune/` | Call the edge bits at an enormous g: v2(g+1) pins exactly determined_depth(v) bits and the next is open. Stop where knowledge ends. The encore is the centre column, which has no lookup. | `prefixlaw`, `edgelaw_deep`, `edgerandom`'s contrast |

## What was ported

`shared/rule30.js` is a browser port of the rule 30 machinery, with rows as BigInt so that bit i is cell i exactly as in Python:

- **ntmc**: `step`, `evolve`, `row`, `flipstrip`, the reference inverse walk, `preimages` over all four boundary tags, `descend`, `cell_sync` with the synchronizing-word search and its cell count, and the `Inverse3` machine (`RESET = '010'`, found by exhaustive search in both languages).
- **prefixlaw**: the 43-term verified spectrum, one stored table of 2¹⁷ edge generations that answers `depth(j, g)` for any g, `bits`, `prefix`, `run`, `at_phase_zero`, `realised`, and the determination law (`index`, `determined_depth`, `run_at`, `determined`, `surplus`, `law`).
- **edgelaw_deep**: the edge-run table to rung 43, `edge(g)` by lookup, and `measure` by evolving the edge alone.
- **driver_lab / txs**: `pmul`, `spectrum_linear_exact` (Frobenius and Lucas, a few polynomial products), `clock_bank`, `tap`, `synthesize`, `spectrum_classes`, `cheapest`, and a running `Bank` with `verify_period`.

`shared/pocklington.js` is the certificate side: modular exponentiation and gcd on BigInt, a wheel of small primes, `pocklington_witness` with the same witness list as the Python library, and two verifiers because the two Python libraries write certificates differently. `lars_approves_of_pocklington_walk` records `[N, k, a]` with N = 2kq + 1 and k the multiplier (`verify_certificate_json`); `pytoolz.numtools.verify_certificate` records `[N, q, a]` with q the earlier proven rung. The game exports the first and shows the second, and both are replayed in the checks.

Both files are small deliberate ports of selected functions, not the packages themselves. They keep the pytoolz adapter's licensing scope in `NOTICE.md`.

## How it was checked

`tools/proving/fixtures.py` reads the pytoolz checkout and writes `tools/fixtures/proving.json`; `tools/test-proving.cjs` compares the browser code with it and replays the games. Everything below is in that fixture with source hashes.

- **Rule 30**: 28 rows to generation 60, the inverse for every boundary tag against both Python inverses, preimage lists, descent to the seed, the centre column to 32 rows, and 280 `cell_sync` reads with their exact cell counts.
- **Prefix law**: the 43-bit prefix at 52 generations up to 10³⁰, the determined prefix and index at each, the law table, realised counts, and the prefix-law run equal to the edge table on every generation below 4,096.
- **Clock banks**: 158 exact spectra (every rope set over shifts 1–7 at 24 bells, every set over 1–5 at 64), ten synthesis problems, the 13 and 41 spectrum classes, and six running banks with `verify_period`.
- **Certificates**: five `numtools.create_prime` certificates from 40 to 200 bits, a `pocklington_walk` chain from M31, and eight tampered certificates (a changed prime, a wrong rung, a composite seed, a skipped rung, in each convention) rejected by both languages.
- **The games' own claims**: for fixed seeds the games record what they assert, 129 claims in all (36 loom rounds, 36 belfry orders, 3 full climbs, 48 fortunes and 6 encores). Python checks each with `ntmc.cell_sync`, `txs.synthesize`, `verify_certificate` in both libraries, `prefixlaw.determined` and `edgelaw_deep.edge`; every verdict is recorded and the test refuses a change that alters the claims. The three recorded climbs reach the twelfth rung with 316 to 317 digits under a weigh-first strategy.
- **The Rule 30 Oracle**: schur-logic's `Rule30Oracle` was run on all 36 loom rows; each has exactly one valid predecessor (`unanimous`), so the loom never needs to disambiguate a tag. This is recorded, not bundled; the Python package stays in its checkout.

The browser check (`npm run test:proving:browser`) starts, plays and finishes all four games at 1280 and 390 pixels wide, verifies a certificate in the page, and checks the landing section, search and the music shelf.

## Limits, said plainly

- The loom's rows are woven from a single seed, which is why each has one predecessor; rows with several predecessors exist and are what the schur-logic oracle is for.
- The belfry's twenty bells stop at coordinate 19, and the spectrum is a coarse invariant: many rope sets meet one order, and the par is the cheapest, not a unique answer.
- The tower proves primality outright but keeps its multipliers below q/2 so that q > √N; leaps stop at 512 bits so a proof stays well under a second in the browser. Coins are a game rule, not a mathematical one.
- Edge Fortune looks up bits with `prefixlaw.depth`, which is exact to depth 42; the centre column encore is simulated because no lookup for it is known, which is the point.

## Reproduce

```sh
/home/wiliamrocha/.spenv/bin/python -B tools/proving/fixtures.py     # rewrites tools/fixtures/proving.json from the real modules
npm run test:proving
npm run build
ARCADE_URL=http://127.0.0.1:8002/dist/ CDP_PORT=9223 npm run test:proving:browser
```

Normal builds use the committed fixture and need no Python. The published arcade is `dist/`.

## Integrated into the current arcade

Imported from `range-arcade_clause` on September 15, 2026. Existing game pages,
IndexinPreview, the three shader rooms, and Rosegold’s 36 controls are retained.
The homepage and return links now count 55 games. Belfry is on the Music shelf;
all four games have their Comfort & Help entries, search, and favorites.

Rollball Tower’s finish screen now offers **Keep this certificate** and
**Review my climb**. The browser suite completes twelve rungs at desktop and
phone sizes, captures the actual downloaded JSON, verifies all thirteen
certificate entries, and returns to the complete receipt.

Original imported file hashes and local changes are recorded in
`tools/proving/import-receipt.json`. The Python fixture is included in the
Netlify folder at `tools/fixtures/proving.json`. No library installation or
existing saved-game key was changed by this import.