# Exact invariant covering results

This supplement supports six exact group-restricted covering numbers in the accompanying manuscript.

## Files

- exact_results.json: canonical manifest with six base-block recipes, CP-SAT/SCIP metadata, environment details, reference commands, and SHA-256 hashes of the solver/verifier sources. Treat the uploaded copy as immutable; local solver reruns can choose different optimal recipes and replace their scratch output files.
- verify_all.py: dependency-free reconstruction and exhaustive covering verifier.
- cyclic_exact.py: regular cyclic orbit model solved by CP-SAT.
- cyclic_scip.py: independently rebuilt regular cyclic orbit model solved by SCIP.
- rot1_cpsat.py: one-fixed-point cyclic model solved by CP-SAT.
- rot1_scip.py: independently rebuilt one-fixed-point cyclic model solved by SCIP.
- cyclic_bnb.py: standard-library exhaustive decision search used as a third proof for the regular cyclic (16,5,3) and (13,5,4) cases.

## Fast verification

From this directory run:

    python verify_all.py exact_results.json

Expected: six lines with construction=PASS and recorded_metadata=CONSISTENT, with block counts 80, 75, 169, 171, 238, and 234 in manifest order. The first verdict independently verifies the objects; the second only checks internal consistency of archived solver metadata and is not a proof-certificate checker.

## Re-solving the integer programs

Requires Python 3.10+ and OR-Tools. The reported runs used Python 3.10, OR-Tools 9.11.4210, CP-SAT with 8 workers, and SCIP 9.0.0 through the OR-Tools linear-solver interface (default SCIP threading):

    python cyclic_exact.py 16 5 3 120 8
    python cyclic_scip.py 16 5 3 120
    python rot1_cpsat.py 16 5 3 120 8
    python rot1_scip.py 16 5 3 120

Replace the cell by 13 5 4 or 14 5 4 to reproduce the other rows. A lower bound is claimed only when status is OPTIMAL and objective equals best_bound.

## Third-solver checks

    python cyclic_bnb.py 16 5 3 5 240
    python cyclic_bnb.py 13 5 4 13 300

The fourth argument is the known incumbent number of full regular cyclic block orbits. The solver decides whether one fewer orbit suffices. A result is a proof only when timed_out is false and sat is false.

The custom search for regular cyclic (14,5,4) did not finish and is deliberately excluded as a proof; that optimum is independently certified by CP-SAT and SCIP.

## Actions

Regular cyclic: x maps to x+1 modulo v on all points.

One-fixed-point: point v-1 is fixed and points 0 through v-2 map by x to x+1 modulo v-1.

All points and base blocks are 0-based.