1# Robustness and falsification23Run 951263fc · Stage 5 (2026-10-30). Goal: break Theorem 5.1 (results/derivations.md) and every proposition it rests on. This file records what was tested, what held, what weakened or overturned the contribution, and what it means for the claims. All numbers come from the artifacts in results/robustness/ (summary: results/robustness/summary.json, mirrored under `robustness` in results/metrics.json). Code: code/robustness/. Stage 4's sensitivity notes are kept at the end (§9) for reference.45## 0. Verdict in one paragraph67Nothing was overturned and nothing was weakened. Every proof step of P1–P9, Lemmas 3.1–3.5 and Theorem 5.1 was re-derived by hand (§1) and holds as written. Four independent falsification attempts failed to find a counterexample (§3–§4), and the three machine-trusted ingredients were each cross-checked by a second, independently written path (§2, §5, §6). The attempts also *strengthened* the evidence: the values Z(P(23,5)) = Z(P(25,5)) = 12, which in Stage 4 rested on a single C program, now have a second exhaustive proof by a different reduction principle and a different closure algorithm; the same program independently re-establishes Z ≥ 12 for every n from 23 to 40 (so holdouts 32, 35, 37 are now doubly certified); the independent certificate checker now covers the fort-cover proofs for n = 21, 22 as well. Two facts of interest were learned: the boundary lower bound has *zero slack* (β₁₈(n) = 12 exactly for 26 ≤ n ≤ 40, §4), and the k = 4 parameter p = 16 provably never works for k = 5 (β₁₆(n) ≤ 11 for all n ≥ 22, §6), which closes the question left open in derivations.md §7.89## 1. Re-derivation of every step (by hand, no code)1011| Step | Re-checked claim | Outcome |12|---|---|---|13| P1 | monotone rule → least fixed point → order independence | holds; the argument is the standard one and does not use the graph |14| P2 | fort ⇔ characterisation, both directions | holds; the (⇐) direction produces the white remainder as a fort, which is what the lazy fort generator relies on |15| P3 | orbit representatives suffice | holds; the C code tests exactly the orbit minima (`canonical`), i.e. one per orbit; D_n = {i ↦ i+a, i ↦ a−i} on both layers, all automorphisms |16| P4 | round encoding sound/complete, T = 2n − s | holds (not used for any certified value beyond n = 17) |17| P5 | simple cubic, 3n edges, gcd(n,5) inner cycles | holds for n ≥ 11 (uses 10 ≢ 0 mod n) |18| P6 | ψ(v_{jk}) = u_j, ψ(u_{jk}) = v_j is an isomorphism; partners ≤ 4 exactly at n ∈ {11,14,16,19,21} | holds: n divides 5l′∓1 ∈ {4,6,9,11,14,16,19,21}; KMZ hypotheses (n ≥ 13 for k = 3, n ≥ 18 for k = 4) are met at 14, 16 and 19, 21 |19| P7 | 12 consecutive outer vertices force P(n,5), n ≥ 12 | holds for every n ≥ 13 (the only index facts used are j−5 ≥ 7 and j−10 ≥ 2); replayed independently for 12 ≤ n ≤ 300 (§2) |20| P8 | first-p-forces boundary bound | holds; |B| = |S|+p and N[X] ⊆ B |21| P9 | column deletion preserves |X| and |∂X| when columns 0..10 are empty | holds; both inclusions f(N[X]) ⊆ N[X′] and ⊇ were re-derived (offsets ±1, ±5, q ∈ [6, n+4]); stress-tested in §6, and the hypothesis is shown to be necessary (§6, D2) |22| L3.1 | β_p(n) ≥ 12 ⇒ Z ≥ 12 when 2n−11 ≥ p | holds; for p = 18 this is n ≥ 15 |23| L3.2 | c ≤ ⌊(p+11)/2⌋, gap ≥ 11 when n > 11c_max, reduce by P9 | holds; the count of singly occupied columns is exactly 2c−p and each contributes a spoke neighbour to ∂X; pigeonhole n−c > 10c; for p = 18: c_max = 14, N_max = 154 |24| L3.3 | finite window ⇒ all n ≥ n₁ | holds given n₁ ≤ N_max (26 ≤ 154) |25| L3.4 | F(n,p) SAT ⇔ β_p(n) ≤ 11 | holds; the direction the proof needs (β ≤ 11 ⇒ SAT) uses only rotation and completeness of the sequential counter; cross-checked in §5 |26| L3.5 | fort-cover CNF SAT if Z ≤ b; four directed-edge orbits | holds; the four orbits (outer edges both directions, spokes out, spokes in, inner edges both directions) are correct because the reflection reverses direction within each class |27| Thm 5.1 | assembly | holds; step 2 needs only size Z−1 exhausted (a smaller forcing set would extend to one of size Z−1 by monotonicity of cl); for n = 27 only sizes 4..11 were run, which is sufficient for this reason |2829Two presentational points found and recorded: (a) results/upper_bound_witnesses.jsonl contains, besides a size-Z witness for every n ≤ 25 with Z < 12 (and n = 23, 25 at size 12), the intermediate larger witnesses of the fort-cover descent (sizes 11, 12 at n = 18–22); all are valid forcing sets and none is smaller than Z, so nothing is contradicted, but a table built from that file must select the minimum size. (b) The proof volume is 37 GiB (du) = 39 GB decimal; derivations.md says 39.0 GB.3031## 2. Independent second path for the exhaustive values (code/robustness/ff_brute.c)3233A new C program, written without reference to code/brute_force.c, uses a different reduction principle — first-force normalisation (any zero-forcing S of size s < 2n has a first force x → y with x ∈ S, y ∉ S and N(x)∖{y} ⊆ S; by D_n-transitivity on the four directed-edge orbits, x → y may be taken to be u₀→v₀, u₀→u₁, v₀→u₀ or v₀→v₅), so it enumerates 4·C(2n−4, s−3) sets instead of orbit minima — and a different closure algorithm (counter/worklist instead of pass-based bitmask scanning). Enumerated counts equal 4·C(2n−4, s−3) in every run.3435| n | s | sets tested | forcing sets | conclusion |36|---|---|---|---|---|37| 11–22 | Z−1 | see summary.json | 0 | Z ≥ table value |38| 11–22 | Z | see summary.json | > 0 | Z ≤ table value; witness printed |39| 23 | 11 | 472,120,740 | 0 | Z(P(23,5)) ≥ 12 (second proof) |40| 24 | 11 | 708,930,508 | 0 | ≥ 12 (third path, with DRAT) |41| 25 | 11 | 1,043,731,260 | 0 | Z(P(25,5)) ≥ 12 (second proof) |42| 23 | 12 | 1,783,567,240 | 16,179,916 | positive control |43| 26–40 | 11 | 1,509,395,976 – 75,423,534,300 | 0 | ≥ 12; second path for 28 ≤ n ≤ 40, incl. holdouts 32, 35, 37 |4445All 12 values for 11 ≤ n ≤ 22 are reproduced on both sides (no forcing set at Z−1, forcing sets at Z). Total 344,080,112,924 sets in 2,345.7 s wall-clock (23,516.5 CPU-s, 16 threads). Output: results/robustness/ff_brute_stdout*.txt, timing in ff_brute_time*.txt.4647Audit of the original oracle from its own records (code/robustness/check_counts.py): in all 162 (n, s) rows of results/tables/brute_force.csv the number of enumerated subsets equals C(2n, s) and the number of representatives tested equals the Burnside count of D_n-orbits on s-subsets, so the Gosper enumeration with m₀-splitting missed nothing and the canonical filter kept exactly one set per orbit.4849Independent witness replay (code/robustness/check_witness_replay.py): all 35 stored witnesses replay legally force by force and close to V under a from-scratch closure; the P7 chronology generated from the text of the proof replays for every 12 ≤ n ≤ 300.5051## 3. Direct attacks on the theorem (code/robustness/attack_local_search.py, seed 20261030)5253Attack A: simulated annealing over 11-subsets maximising |cl(S)| for every n from 23 to 60 and n ∈ {70, 80, 96, 120, 154, 155, 200} (4 restarts × 15,000 swap moves each). Positive controls (n, s) = (11, 6), (13, 9), (21, 10), (22, 11), where forcing sets exist, were all found. No 11-set forced any P(n,5) with n ≥ 23; the largest closure reached was 30 of 46 vertices at n = 23, 34 of 50 at n = 25 and 28 at every n ≥ 26. This is heuristic evidence only; the proof does not depend on it.5455## 4. Attacks on the lower-bound certificates5657Attack B (same script): annealing over 18-subsets minimising |∂X| for 26 ≤ n ≤ 60 and n ∈ {70, 80, 96, 120, 154, 155, 160, 200} (5 restarts × 40,000 moves). Controls reached the table values β₁₈(22) = 10, β₁₈(23) = 11, β₁₈(25) = 10, β₂₀(24) = 11 and the certified "≥ 12" at (24, 18). No 18-set with boundary ≤ 11 was found at any n ≥ 26; the best boundary was 12 at every n, including n = 155, 160, 200 beyond the certified window (where Lemma 3.2, not a certificate, carries the proof).5859Slack (code/robustness/check_margin.py): the exact value β₁₈(n), found by solving F(n,18,b) upward from b = 12 and recounting each model, is **12 for every n from 26 to 40**. The certificates therefore have margin zero: an 18-set with boundary 12 exists at every n, and the lower bound 12 is the best this method can give with p = 18. This is consistent with the attack results above and makes the independent enumeration of §2 the decisive cross-check for the encoding.6061## 5. Soundness of the boundary encoding (code/robustness/beta_brute.c, check_boundary_encoding.py)6263An exhaustive enumeration of all p-subsets (no SAT, no symmetry) tabulated the full distribution of |∂X| for n = 13, 14, 15 (all p) and n = 16 (10 ≤ p ≤ 22), 94 (n, p) pairs. For each pair the project's CNF F(n,p,b) was solved at b = β−1 (must be UNSAT) and b = β (must be SAT, model recounted here): all 94 behaved correctly, and all 50 cells shared with results/tables/boundary_table.csv agree. Since the UNSAT side at b = β−1 is exercised on every instance, an over-constrained "exactly p" or "at most b" encoding — the one failure mode that could produce a false certificate — would have been detected.6465## 6. The deletion lemma under stress (code/robustness/check_deletion_lemma.py)6667- D1: for 13 ≤ n ≤ 30 and every X with |X| ≤ 2 (|X| = 3 for n ≤ 20) supported on columns 11..n−1, the strong form f(N[X]) = N[X′] and f(∂X) = ∂X′ holds in all 7,287 cases.68- D2 (negative control): if X is allowed to meet column 10 (only 10 empty columns), the deleted column 5 lies in N[X] in 414 of 810 cases and the boundary size actually changes in 18 of them (e.g. n = 13, X = {v₁₀, v₁₂}: 6 → 5). The hypothesis "11 empty columns" is therefore necessary, and the test can detect violations.69- D3 (pipeline on near-extremal sets): from boundary-11 sets with a 10-column gap (found with the project encoder plus explicit emptiness clauses, recounted here), the inverse map (column insertion at position 5) was applied 25 times and then P9 25 times; the boundary stayed equal at every one of the 50 steps and the original set was recovered, for p = 16 at n₀ = 22, 26, 30. For p = 18 at n₀ = 22, 23, 25 and p = 20 at n₀ = 24 no boundary-≤11 set with a 10-column gap exists (UNSAT), consistent with β₁₈(n) ≥ 12 for n ≥ 26.7071**Consequence (new, proved).** Since P9 is an equality of boundaries in both directions, a 16-set with boundary 11 and ten consecutive empty columns at n = 22 yields β₁₆(n) ≤ 11 for every n ≥ 22. The question "does p = 16 fail for infinitely many n?" (derivations.md §7) is thus answered: p = 16 fails for all n ≥ 22, so the k = 4 parameter cannot be transplanted to k = 5 and p = 18 is genuinely needed.7273## 7. Trust in the checker (code/robustness/check_drat_negative_controls.py)7475drat-trim rejected (exit 1, "s NOT VERIFIED") the P(26,5) proof truncated to its first half, the same proof run against the CNF for n = 27, and the same proof run against the weaker formula F(26,18,12), which is satisfiable (β₁₈(26) = 12); the original pair still verifies. The independent checker code/verify_lower_bounds.py was re-run on every certificate: 135 boundary and 14 fort-cover certificates (now including n = 21, 22, which were produced after the Stage 4 checker pass), all 149 verified; each CNF was rebuilt from the graph definition and compared clause-by-clause with the stored file before drat-trim ran.7677## 8. What weakened, what did not, and the implications7879- **Overturned:** nothing.80- **Weakened:** nothing. No proposition had to be restated; no value changed; the holdout record stands.81- **Qualified (unchanged from Stage 4, restated):** for n > 40 the lower bound rests on one certified path (DRAT + Lemmas 3.1–3.3); the fort-cover second path exists only for n ≤ 22, the enumeration path now for n ≤ 40. Z(P(24r,5)) = 12 is still cited second-hand (Alameda et al. not fetched). Local search is evidence of absence only in the heuristic sense.82- **Strengthened:** two independent exhaustive proofs for n = 23 and 25; enumeration cross-check extended to n = 40; checker negative controls; encoder cross-check on UNSAT instances; β₁₆ question closed.83- **Implication for the manuscript:** Theorem 5.1 can be stated as in derivations.md. The paper should (i) describe the first-force enumeration as the second path for 23 ≤ n ≤ 40, (ii) report the zero slack β₁₈(n) = 12 and the resulting necessity of an exact encoding, (iii) add the p = 16 result to the negative-results section, (iv) build its witness table from the minimum-size witnesses only, (v) state the proof volume in one unit.8485Reported values affected: none of the Stage 4 values changed; the new numbers above are registered via record_reported_value and traceable to results/metrics.json → robustness.8687## 9. Stage 4 sensitivity notes (kept)8889Independent paths that must agree: exhaustive (C, orbit reduction) for 11 ≤ n ≤ 27; fort-cover SAT + DRAT for 11 ≤ n ≤ 22; round SAT (Glucose) UNSAT at Z−1 for 11 ≤ n ≤ 17; boundary DRAT (p = 18) + Lemma 3.1 for n = 24 and 26 ≤ n ≤ 154. No disagreement anywhere; timeouts recorded as unknown. Varied: force order (1200/1200 identical closures), graph construction (two constructors plus independent rebuilds in each verifier), solver (CaDiCaL / Glucose, drat-trim external), parameter p (18 chosen by rule L4; 20 cross-checked on 26..30; 16, 17 fail at every n ≤ 30; 24 fails at 26), orbit reduction (validated against an unreduced Python enumeration on P(5,2) and P(11,5)), exceptional symmetric n (12, 24 handled with the D_n subgroup only, sound by P3). Not tested: anything about k ≥ 6; round-based SAT beyond n = 17.90