# code/ — zero forcing in P(n,5)

Run from the run root with `PYTHONPATH=.pydeps:code python3 code/<script>.py` (every script also sets this up itself through `common.py`). Dependencies: `requirements.txt` (wheels archived in `wheels/`, installed into `.pydeps` by step 0 of `reproduce.sh` or by `python3 -m pip install --no-index --target .pydeps code/wheels/*.whl`; `.pydeps/` itself is not shipped because it contains compiled extension modules), `tools/drat-trim/` (external DRAT checker, built from source), `brute_force.c` (C oracle). No compiled binaries are shipped: step 0 of `reproduce.sh` builds `drat-trim`, `brute_force`, `robustness/ff_brute` and `robustness/beta_brute` with `gcc -O2` (`brute_force.py` also builds its binary on demand).

| module | role |
|---|---|
| `common.py` | paths, UTC timestamps, SHA-256, experiment log |
| `graph_constructor.py` | two independent constructors of P(n,k) (edge formula; block-circulant matrix), canonical labels u_i -> i, v_i -> n+i, SHA-256 of edge lists, dihedral maps, invariant tests T1, isomorphism check P6 |
| `closure_oracle.py` | closure with full chronology, random-order test T2, replay, bitmask closure |
| `brute_force.c` / `brute_force.py` | exhaustive oracle with D_n orbit reduction (P3); gold standard lower bounds (every smaller size exhausted) |
| `sat_or_ilp_solver.py` | round-based SAT (P4), fort-cover SAT with lazy minimal forts, dihedral fort images and first-force normalisation (P2, Lemma 3.5), boundary formulas (Lemma 3.4), proof-logging re-solve + drat-trim |
| `run_exact.py` | exact-value driver: witnesses (replayed), fort-cover DRAT certificates, round-encoding second path |
| `run_boundary_table.py` | beta_p(n) table (obstruction search, CS2/L4) |
| `run_boundary_window.py` | certified window: UNSAT + DRAT + drat-trim per n (Lemma 3.3) |
| `verify_upper_bounds.py` | independent replay of every witness and of the P7 construction (no solver imports) |
| `verify_lower_bounds.py` | independent rebuild of every certified CNF from the definition, fort validity check, hash check, drat-trim rerun |
| `verify_lemmas.py` | CS6 boundary identity, T8 deletion map, sympy checks |
| `build_tables.py` | exact_values.csv, known_vs_new.csv, metrics |
| `reproduce.sh` | reproduction in three modes, all run in a working copy under `results/reproduction/work/` so that the shipped artifacts are never modified: `QUICK=1` (checks only, ~10 min), default (bounded regeneration, ~25 min: exhaustive oracle n <= 22, boundary table p = 16..20, certified window n = 26..40 with fresh proofs, fort-cover certificates n <= 21) and `FULL=1` (everything: oracle n = 23..27, complete table and window, fort-cover certificate n = 22, re-check of every shipped proof incl. the 4.0 GB n = 23 fort-cover proof, proof-logging re-solves at n = 23, 25 and a drat-trim check of the stored n = 25 proof file, the second enumerator through n = 40, exhaustive encoding checks; several hours). The header of the script states which table rows each mode regenerates; the comparison with the shipped files is written to `results/reproduction/summary.json` |
| `regen_fortcover_proof.py` | proof-logging re-solve of a stored fort-cover CNF (used for n = 22, 23, 25) with drat-trim check and record |
| `check_fortcover_proof.py` | drat-trim check (plain subprocess, exit code captured) of a stored fort-cover proof whose producing process ended before the record was written (n = 23, 25; revision, referee F1) |
| `tools/logrun.py` | runs one command and appends `{name, command, startedAt, endedAt, exitCode}` to `results/experiment-log.jsonl` (or `$AUTOSCHOLAR_EXPLOG`) |
| `tools/compare_reproduction.py` | compares a reproduction working copy with the shipped artifacts (exact values, regenerated certificate digests and verdicts, checker verdicts) |
| `tools/make_checksums.py` | writes/verifies `provenance/checksums.sha256` over the artifact directories |
| `tools/run_fortcover_checks.sh` | runs `check_fortcover_proof.py` for n = 23 and 25 in parallel |
| `check_exceptional_automorphisms.py` | revision check (referee F2): the layer-swapping map is an automorphism of P(n,5) exactly for n = 12, 13, 24, 26 (n <= 60) |
| `proofs/handwritten/` | proof sources (mirrors results/derivations.md) |
| `proofs/certificates/` | DIMACS CNFs, DRAT proofs, fort lists, with SHA-256 in the result records |
| `prelim_check_*.py` | Stage B/3 throwaway checks, superseded |

Certification vocabulary (fixed in plan/research-plan.md §5): *fully certified* = replayed witness + exhaustive brute force or externally checked DRAT proof combined with a proved lemma; *solver-supported* = two agreeing solver paths without external certificate; *candidate* = upper bound only; *unknown*.

Execution records (`results/experiment-log.jsonl`, written by `code/tools/logrun.py`: name, command, startedAt, endedAt, exitCode) are kept separate from the milestone events of the original run (`results/experiment-events.jsonl`: conjecture registration, window start/end, stage completion), which are not executions and carry no exit code.