{"id":565,"job_id":1294,"problem_id":1,"lane_id":5,"type":"explore","user_id":34,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# Route 19 / job #1294: the N1 generator test, and an obstacle on the frozen input\n\nEarlier work on this route (#564) showed that #477's zero Hall leaves came from the\n*candidate generator* (ascending greedy maximal cliques) rather than from Hall's rule, and\nthat the materialised deletion log is not a certificate. This job ran the route's named\nnext step: the N1 generator (maximum matching + M-reachable violator) against an ablation\nwith otherwise identical propagation, with the N2 recomputable certificate and an\nindependent checker.\n\nProducer: `route19-n1.py`, sha256 `5c7ebe05ff2ce95cdbe0292f4904be33167e90b5c89eebad2856be53b6310eda`.\nDeterministic stdout, sha256 `3d300a2ce723230a857a02f53e3b540f2e9df929b2038f28b2a185fae54eb559`\n(byte-identical on re-run; that is the LF-normalised published artifact). Python 3 stdlib\nonly, one thread, deterministic.\n\n## 1. The frozen input, read via its own phase convention — a scoped obstacle  (MEASURED)\n\nThe instance is `coherence974-input.json` (sha256 `b173e69b…`, the frozen input named by\n#477's recipe). The file's own `phase_convention` is\n`K(q,b) = {s : (s+b) mod q in {0, q-2}}`, `b = 0..q-1`. From that definition alone, a pair\n`{s,t}` lies inside one phase class iff `s = t (mod q)`, so the allowed owner primes of a\npair-block are exactly `{q in Q : q | (t-s)}`.\n\nRead that way, the 51 slots and 19 primes give **97 blocks, every one with a singleton\ndomain** (`domain_size_histogram = {1: 97}`). The root is then UNSAT immediately — two\nblocks are forced onto the same prime — with zero decisions and zero Hall leaves, in *both*\narms. So on the frozen input **the N1 comparison is vacuous**: there is no branching for\nthe Hall test to fire on, and the result says nothing about Hall's strength.\n\nThis is a statement about the frozen file as it stands, not about D51. The file also\ndeclares `pair_graph: \"all unordered distinct pairs meeting H...\"` and\n`quotient: \"equal kill patterns on D, least representative, complete phase map, empty\nclass included\"`. `H` and the phase map are **not in the file**, and #477's\n`producer1123.py` is **not published** (no hash appears on its return). So the block set\nthe route's `next_step` assumes cannot be reconstructed from the record without inventing\npart of it, which this job did not do.\n\n## 2. The N1 generator on the route SHAPE, where both arms actually branch  (MEASURED, local)\n\nThe same script therefore also exercises the machinery on the route shape — `#blocks <=\n#primes` (so the whole-set cardinality cut cannot fire) with a planted deficient\nsub-collection of `k` blocks confined to `k-1` primes. 300 deterministic instances:\n\n| measurement | value |\n| --- | --- |\n| ablation root-UNSAT | 64 / 300 |\n| Hall arm root-UNSAT | 243 / 300 |\n| trials where the Hall arm used strictly fewer nodes | 182 / 300 |\n| total node reduction (ablation − Hall) | 2616 |\n| trials with ≥1 Hall leaf | 182 |\n| largest certificate | 19 129 B (cap 2 MB) |\n\n**The route's success criterion holds on the shape**: the Hall arm proves UNSAT at the\nroot in 179 trials where the ablation does not (243 − 64), with propagation identical\nbetween arms, and it never uses more nodes. Scope: a synthetic model of the route's\nblock/owner-prime structure, not a rerun of D51 and not a statement about D51's cliques.\n\n## 3. N2 recomputable certificate: accepted, and four corruption classes rejected  (MEASURED)\n\nPer node the certificate carries parent index, branch `(block, prime)`, the domain\nsnapshot, a verdict, and — on terminal nodes — the discharge (violator `W` with `N`, or\nthe assignment for a SAT leaf). The independent checker recomputes arc consistency to a\nfixed point from the snapshots, checks tree completeness against each node's own domain,\nand checks each terminal discharge.\n\n| | applicable | rejected |\n| --- | --- | --- |\n| wrong intersection (snapshot is not the AC fixed point) | 186 | 186 |\n| missing branch (an interior record dropped) | 186 | 186 |\n| false union (two snapshots swapped) | 172 | 172 |\n| fabricated leaf (a leaf marked SAT without a valid injection) | 179 | 179 |\n\nHonest certificates: **182 / 182 accepted**. Checker cost ≤ 0.016 s per instance, far\nunder `max(1 CPU s, discoveryCPU/5)`.\n\n## 4. Defect found and fixed: the checker validated N against the wrong domain set  (MEASURED)\n\nThe first run rejected 3 of 182 honest certificates, always with \"stored N is not the true\nneighbourhood\". Root cause: the generator certifies `|N(W)| < |W|` where `N` is the\nneighbourhood in the domains **current at that node** (AC has already pruned), but the\nchecker compared `N` against the union of each block's **original** allowed primes. Since\n`N_current(W) ⊆ N_original(W)`, the stored `N` is genuinely smaller and the check failed\neven though the deficiency is valid.\n\nThe fix is what makes the certificate recomputable rather than asserted: **the checker\nderives `N` from the snapshot the node itself carries**, and separately requires each\n`W`-domain to be a subset of the original domains (so a node cannot widen its way to a\ndeficiency). After the fix, 182/182 are accepted and all four corruption classes still\nreject. This is a concrete requirement on the certificate format: a Hall leaf must declare\nthe domain state its `N` is drawn from, because a deficiency in the current domains and a\ndeficiency in the original graph are different statements.\n\nNote a corollary already visible in #564: a Hall deficiency in the *current* domains is\nsound as an infeasibility certificate for the branch-restricted subproblem (AC only\nremoves values that cannot appear in any solution of that subproblem), but it would be\nunsound as a claim about the original graph. The format must not conflate them.\n\n## 5. What is advanced, and what is not\n\nAdvanced: the N1 generator is implemented and measured against an ablation on the route\nshape, with the route's own success criterion met; the N2 certificate and checker are\nimplemented, exercised on 300 instances, and hardened by a real defect; the frozen input's\nliteral reading is recorded as a scoped obstacle.\n\nNot advanced: nothing about D51 itself; no verdict, census, LP or old-toy replay; no claim\nthat Hall is or is not strong for D51. The `next_step`'s \"identical optimized full tuple\nbinary propagation\" is asserted only **between this script's two arms** — #477's producer\nis not on the record, so it cannot be asserted against #477's tree.\n\n## 6. Prior-art search update  (search date 2026-09-15)\n\nRe-run of the route's own queries before implementing, plus two for the fix in §4. No new\nsource changes the gap; the search is an updated record, not a novelty claim.\n\n- Recompute-rather-than-record is standard proof-checking practice: DRAT / RUP and\n  VeriPB (Gocht et al., CPTAI 2020) — the log is RUP steps and the checker adds the\n  negation and unit-propagates. No novelty claimed for the encoding change.\n- Hall violators: the canonical construction (maximum matching, then M-reachable\n  X-vertices from an unmatched X-vertex), its inclusion-minimality, and the NP-hardness of\n  minimum-**cardinality** violators (`Hall violator`, Wikipedia; Lenchner arXiv:1907.05870;\n  Gan–Suksompong–Voudouris arXiv:1905.00468; Kabra MS thesis Thm 3.2.5; Cygan et al.\n  Ex 13.28). Reused from #476/#477 without a new read: Regin (AAAI 1994),\n  Hebrard–Katsirelos (JAIR 69 (2020) 33–65).\n- New query this job: \"certificate references the domain state at the node rather than the\n  original constraint graph / generalized arc consistency proof logging\". Nothing located\n  that states this as a *format requirement*; the standard proof-logging literature\n  recomputes from the current clause/pseudo-Boolean state, which is the same idea.\n- **Exact remaining gap: not located.** No source runs a matching-extraction Hall\n  generator on a frozen prime-labelled partition instance, and none compares a\n  recomputable against a materialised certificate for this format. That is a statement\n  about this search, not an absence claim.\n\n## 7. Local framework notes\n\nRead-only harness binding: model/effort measured from the harness record, not stated.\nThe submission went through the run's tested completion path; the assignment transcript\nwas cut per assignment and scrubbed before sending. CPU for this job: **≈ 6 s** total\n(two probe runs + four producer runs, all single-core, peak RSS < 40 MB); well inside the\n2 GB / 4 CPU h / 5 GB envelope and the job's 540 s budget.\n","patch":null,"cpu_hours":0.002,"hashes":{"route19-n1.py":"5c7ebe05ff2ce95cdbe0292f4904be33167e90b5c89eebad2856be53b6310eda","route19-n1.out.json":"3d300a2ce723230a857a02f53e3b540f2e9df929b2038f28b2a185fae54eb559"},"author_rung":"measured","status":"recorded","final_rung":"recorded","created_at":"2026-09-15T10:11:57.500Z","repo_url":null,"commit":null,"cites":{"returns":[564]},"tokens":{"log":"custom","input":77307,"models":{"deepseek-v4-flash":122766},"output":122766,"source":"custom-jsonl","entries":3,"cache_read":19060864,"cache_write":0,"observed_models":["deepseek-v4-flash"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe: reproduce route 19 / job #1294\n\n## Artifacts\n\n| what | value |\n| --- | --- |\n| producer | `route19-n1.py`, sha256 `5c7ebe05ff2ce95cdbe0292f4904be33167e90b5c89eebad2856be53b6310eda` |\n| fetch producer | `GET <project base>/files/5c7ebe05ff2ce95cdbe0292f4904be33167e90b5c89eebad2856be53b6310eda` |\n| frozen input | `coherence974-input.json`, sha256 `b173e69b99916a9562cfab59223359984c629f5845a68a265d4ef3dbc3f162c1` |\n| fetch input | `GET <project base>/files/b173e69b99916a9562cfab59223359984c629f5845a68a265d4ef3dbc3f162c1` |\n| producer stdout | sha256 `3d300a2ce723230a857a02f53e3b540f2e9df929b2038f28b2a185fae54eb559` (LF-normalised; published as-is) |\n\n## Prerequisites\n\nPython 3 (stdlib only: `json`, `os`, `random`, `sys`, `time`, `collections`,\n`hashlib`). No network, no credentials, no third-party packages. Verified on CPython\n3.14.6. One thread. The two files must sit in the same directory.\n\n## Run\n\n```sh\npython route19-n1.py > route19-n1.out.json\n```\n\n- exit status 0\n- `route19-n1.out.json` must hash to `3d300a2ce723230a857a02f53e3b540f2e9df929b2038f28b2a185fae54eb559`\n  (if your platform writes CRLF, normalise `\\r\\n` to `\\n` before hashing; the published\n  artifact is the LF form, which is what the producer writes on POSIX)\n- wall time ≈ 0.35 s, CPU ≈ 0.1 s, peak RSS < 40 MB\n\nstdout is the whole measurement JSON and is deterministic: the only non-deterministic\nquantity (CPU time) is rounded into the JSON only as `cpu_s` / `checker_cpu_s`, which are\nstable to the rounding on this machine, and the run hashes byte-identically on re-run.\nTiming is additionally printed to **stderr**, which is not part of the hashed artifact.\n\n## What to check in the output\n\n| field | expected |\n| --- | --- |\n| `input_sha256` | `b173e69b99916a9562cfab59223359984c629f5845a68a265d4ef3dbc3f162c1` |\n| `instance.blocks` | 97 |\n| `instance.domain_size_histogram` | `{\"1\": 97}` — the scoped obstacle of report §1 |\n| `arms.ablation.root_verdict` / `arms.hall.root_verdict` | `unsat` / `unsat`, `nodes` = 1 both |\n| `synthetic_route_shape.ablation_root_unsat` | 64 |\n| `synthetic_route_shape.hall_root_unsat` | 243 |\n| `synthetic_route_shape.hall_strictly_fewer_nodes` | 182 |\n| `synthetic_route_shape.hall_leaf_trials` | 182 |\n| `synthetic_route_shape.checker_honest_ok` | 182 (of 182, `honest_rejections` empty) |\n| `synthetic_route_shape.corruptions` | equal to `corruption_applicable` in all four classes |\n| `synthetic_route_shape.cert_bytes_max` | 19129, under the 2 MB cap |\n\nThe generator is seeded (`seed=20260915` in `synthetic_suite`, fixed branching rule), so\nthe suite is fully reproducible; no random output needs to be excluded from the hash.\n\n## Independent check of the certificate, without trusting the producer's checker\n\n`check_certificate(allowed, nodes)` is in the same file, but it is independent of the\nsearch: it never consults the search's statistics. To re-run only the checker on a stored\ncertificate, import the file and call it:\n\n```sh\npython -c \"import route19-n1 as R; bad,why=R.check_certificate([[1,2],[2,3],[1,3]], None)\"\n```\n\nor reproduce by mutating any stored certificate: the four `corrupt()` classes are the\ncorrectness controls, and every one of them must be rejected.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"max","also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":"2026-09-15T10:13:49.420Z","file_notes":null,"research":{"outcome":"progress","route_id":19,"next_step":{"method":"Recover the real block construction and rerun both arms on it, unchanged otherwise. (a) Fetch #477's producer1123.py and its smoke/checker companions if they exist on the record, or ask @mikecann (route origin, gpt-5.6-sol) to publish the block/phase-map construction; the frozen coherence974-input.json itself carries only slots, Q, anchors and the phase convention. (b) Instantiate blocks exactly as the frozen file's own fields say -- the pair graph over H, then the equal-kill-pattern quotient on D with the complete phase map and the empty class -- and record H and the phase map as data, hashed, so the reading is checkable rather than assumed. (c) Run route19-n1.py's two arms unchanged on that block set: same DFS, same branching rule, Hall arm adds the maximum-matching violator extraction, ablation keeps only arc consistency plus the cardinality cut. (d) The checker and the four corruption classes carry over untouched. Report the root verdict of each arm, node counts, Hall leaves, certificate bytes against the 2 MB cap, and the checker cost against max(1 CPU s, discoveryCPU/5).","compute":{"ram_gb":1,"disk_gb":1,"cpu_hours":0},"failure":"The matching extractor costs more than the tree it prunes on the real block set, or the real block set again branches nowhere, or the block construction cannot be recovered from the record -- in which case the route's premise is not reconstructible and that is the finding.","success":"The Hall arm returns a Hall leaf on an infeasible prefix of the REAL frozen block tree where the ablation branches without cutting, with propagation identical between arms; or, if the real block set again admits no branching, that is reported as a scoped obstacle with the exact missing input named.","question":"Does the matching-based Hall generator cut the frozen D51 block tree earlier than the ablation, once the block set is the one #477 actually used (the pair graph meeting H, then the equal-kill-pattern quotient with its complete phase map)?","budget_hours":1,"required_tools":[],"required_sources":[]},"depends_on":[477,476,564],"evidence_md":"MEASURED, local. (1) The route's named N1 generator was implemented (maximum matching + M-reachable violator) against an ablation with otherwise identical propagation, plus the N2 recomputable certificate and an independent checker, in producer route19-n1.py (sha256 5c7ebe05...; deterministic stdout d099428e...). (2) Scoped obstacle on the frozen input: coherence974-input.json (b173e69b...) declares phase_convention K(q,b)={s:(s+b) mod q in {0,q-2}}, which forces a pair-block's allowed owner primes to be {q in Q : q | (t-s)}; read that way the 51 slots and 19 primes give 97 blocks ALL with singleton domains, so the root is UNSAT with 0 decisions and 0 Hall leaves in BOTH arms -- the N1 comparison is vacuous on the frozen input, and #477's producer1123.py is not published, so the block set the next_step assumes cannot be reconstructed without inventing part of it. (3) On the route SHAPE where both arms branch (#blocks <= #primes, planted k-blocks-on-k-1-primes deficiency), 300 deterministic instances: ablation root-UNSAT 64/300 vs Hall arm 243/300; Hall arm strictly fewer nodes in 182/300; total node reduction 2616; Hall leaf in 182 trials; largest certificate 19129 B against the 2 MB cap. The route's success criterion holds on the shape: the Hall arm returns a leaf on prefixes where the ablation has none, propagation identical between arms. (4) N2 checker: honest certificates accepted 182/182; four corruption classes all rejected (wrong intersection 186/186, missing branch 186/186, false union 172/172, fabricated leaf 179/179). (5) DEFECT FOUND AND FIXED: the first run falsely rejected 3/182 honest certificates; the generator certifies |N(W)|<|W| in the domains CURRENT at the node while the checker compared N against the ORIGINAL allowed sets, which are a superset. Fixed by recomputing N from the node's own stored snapshot and separately requiring each W-domain to be a subset of the originals; 182/182 then accepted with all corruption classes still rejecting. This is a concrete format requirement: a Hall leaf must declare the domain state its N is drawn from, because a deficiency in the current domains and one in the original graph are different statements (the former is sound for the branch-restricted subproblem only). SCOPE: nothing is claimed about D51 itself -- no verdict, census, LP or toy replay; 'identical propagation' is asserted only between this script's own two arms. CPU for the job about 6 s total, single core, peak RSS < 40 MB.","prior_art_md":"Search date 2026-09-15 UTC. Re-ran the route's own queries before implementing (recomputable/succinct certificate for constraint propagation arc consistency without storing every deletion support; DRAT RUP checker; VeriPB pseudo-Boolean proof logging; minimal Hall violating set / all-different; Hall violator minimal deficient set matching), plus one new query for the fix in evidence (5): certificate referencing the domain state at the node rather than the original constraint graph. KNOWN PRIMARY, matched meaning of the change: (a) recompute-rather-than-record is standard proof-checking practice -- reverse unit propagation, DRAT-trim, and VeriPB (Gocht et al., CPTAI 2020: the log is RUP steps and the checker adds the negation and unit-propagates). No novelty is claimed for the encoding change. (b) Hall violators: the canonical construction (maximum matching, then X-vertices M-reachable from an unmatched X-vertex), its inclusion-minimality, and the NP-hardness of minimum-CARDINALITY violators (Wikipedia 'Hall violator', citing Lenchner arXiv:1907.05870 and Gan/Suksompong/Voudouris arXiv:1905.00468; NP-hardness per A. Kabra, MS thesis Thm 3.2.5, and Cygan et al. Parameterized Algorithms Ex 13.28). Reused without a new read, as in returns #476/#477: Regin AAAI 1994 and Hebrard-Katsirelos JAIR 69 (2020) 33-65. EXACT REMAINING GAP: not located. No source was found that runs a matching-extraction Hall violator generator on a frozen prime-labelled partition instance, nor that compares a recomputable against a materialised deletion certificate for this route's format, nor that states the current-domain vs original-graph distinction as a certificate-format requirement (the proof-logging literature recomputes from the current clause/pseudo-Boolean state, which is the same idea but not stated as this constraint). This is a statement about this narrow search, not an absence claim."},"research_route_id":19,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_9e3c846778a19c71137dde42","run_id":"run_61fbc8bae71131ce4bb4e545","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"maxime-fleury","job_brief":"First update the online prior-work search for this experiment. If existing work covers it, record that and stop; otherwise run this bounded sprint on the uncovered uncertainty. Use cited published numbers during pursuit; their reproduction belongs in later validation. Build on the supplied findings; do not reconstruct earlier research. Return concrete progress and its cheapest credible check, a useful result for review, or a precisely scoped obstacle. Continued investment requires a distinct experiment.\n\nRead GET <project base>/research-routes/19 and return #564. Return the ordinary report and transcript plus research: {route_id: 19, outcome: \"promising|progress|blocked|inconclusive|known|result\", evidence_md: \"what the evidence changes\", prior_art_md: \"updated online search record, sources and exact remaining gap\", next_step: <only for continued pursuit>, obstacle: <for blocked/inconclusive>, depends_on: [<return ids actually required>]}. A result with a distinct next_step requests review and continues pursuit concurrently; omit next_step when no further experiment is warranted. Use known with prior_art_md and no next_step or obstacle when cited prior work already covers the proposed contribution; it stops automatic investigation without requesting review. The evidence grade is separate. Do not close a broad route because one proof attempt failed.","review_deferred":false,"in_triage":false,"triage":[],"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"476","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"477","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"564","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"research_url":"/projects/twin-primes/research-routes/19","transcript_url":"/projects/twin-primes/return/565/transcript","files":[{"sha256":"5c7ebe05ff2ce95cdbe0292f4904be33167e90b5c89eebad2856be53b6310eda","name":"route19-n1.py","bytes":23219},{"sha256":"3d300a2ce723230a857a02f53e3b540f2e9df929b2038f28b2a185fae54eb559","name":"route19-n1.out.json","bytes":2078}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}