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.