Stage 5 robustness checks
Run from the run root. Outputs go to results/robustness/; the narrative is results/robustness.md.
| Script | Purpose | Output |
|---|---|---|
ff_brute.c (+ run_ff_brute.sh) |
Independent exhaustive zero-forcing search by first-force normalisation (4·C(2n−4, s−3) sets, counter/worklist closure); no code shared with code/brute_force.c |
ff_brute_stdout*.txt, ff_brute_time*.txt |
beta_brute.c (+ run_beta_brute.sh) |
Exhaustive distribution of |∂X| over all p-subsets, n = 13..16 | beta_brute_stdout.txt |
check_counts.py |
Binomial and Burnside audit of the Stage 4 oracle's recorded counts | enumeration_counts_check.json |
check_witness_replay.py |
From-scratch replay of all stored witnesses and of the P7 chronology for 12 ≤ n ≤ 300 | witness_replay.json |
check_boundary_encoding.py |
F(n,p,b) UNSAT at b = β−1 and SAT at b = β against beta_brute; comparison with results/tables/boundary_table.csv |
boundary_encoding_check.json |
check_deletion_lemma.py |
P9 exhaustive small-set test (D1), negative control (D2), insertion/deletion pipeline on boundary-11 sets (D3) | deletion_lemma.json |
check_drat_negative_controls.py |
drat-trim must reject a truncated proof, a proof against a satisfiable weakening, and a proof against the wrong CNF; also determines β₁₈(26) | drat_negative_controls.json |
check_margin.py |
Exact β₁₈(n) for 26 ≤ n ≤ 40 (slack of the certificates) | margin.json |
attack_local_search.py |
Simulated-annealing attacks: 11-sets that force (A) and 18-sets with boundary ≤ 11 (B), with positive controls; seed 20261030 | local_search_attacks.json |
collect_robustness_metrics.py |
Collects everything into summary.json and results/metrics.json["robustness"] |
summary.json |
Build: gcc -O2 -o code/robustness/ff_brute code/robustness/ff_brute.c -lpthread and likewise for beta_brute. The certificate re-check is the Stage 4 script python3 code/verify_lower_bounds.py 12 (stdout kept in verify_lower_bounds_rerun_stdout.txt).