{"id":564,"job_id":1285,"problem_id":1,"lane_id":5,"type":"explore","user_id":1,"model":"deepseek-v4-flash","provider":"deepseek","report_md":"# Route 19 rescue: the Hall generator was the binding constraint, not the Hall rule\n\nJob #1285, rescue of route 19 (*Prime-labelled partition branching with clique Hall\ncertificates*), revision 3. Direction: general project research.\n\n## 1. What the obstruction actually says, and what it does not\n\nReturn #477 recorded a measured failure of *one implementation*: a frozen D51 list, Q19,\nthe equal-first minimum-common-prime selector, ascending greedy clique candidates,\nidentical optimized full tuple binary propagation, and a cap of 54 CPU s / 200000\ndecisions / 2 MB proof per arm. Both arms returned **identical** counts —\n1821 decisions, 3631 nodes, 1810 cardinality leaves, 110816 deleted values, no final\nproof — with **0 Hall leaves**, and the Hall arm cost **7.17 s against 3.95 s** for its\nablation.\n\nTwo readings of that receipt are available. The route took the pessimistic one (\"the\nclique Hall certificate does not pay\"). The receipt supports a different one:\n\n- the Hall arm's tree was **identical** to its ablation's, so the Hall test pruned\n  nothing at any node the ablation had not already cut; and\n- an extra test that costs 81 % more wall time while changing no node count is not\n  evidence that the rule is weak — it is evidence that the test never fired *before* the\n  ordinary cut.\n\n\"0 Hall leaves\" therefore needs a mechanical explanation, and there is one.\n\n## 2. Finding: the candidate generator, not the Hall rule, produced the zero\n\nHall's condition for a sub-collection W of the blocks is `|N(W)| < |W|`. The canonical\nobject is a *Hall violator*, and its standard construction is: take a maximum matching,\nthen the set of X-vertices reachable from an unmatched X-vertex by M-alternating paths.\nThat set is **inclusion-minimal** by construction, and it exists whenever the instance is\ninfeasible (Hall's theorem, both directions).\n\n#477's candidate generator was the opposite shape. \"Ascending greedy clique candidates\"\nbuilds **maximal** cliques: for each seed it adds every vertex adjacent to all current\nmembers. Maximality grows `|W|` and grows `N(W)` with it, which is precisely how a\ndeficient sub-collection stops looking deficient.\n\nLocal measurement (`work/rescue19_probe.py`, experiment E1), on 400 random instances of\nthe route's shape (blocks forced to distinct owner primes; infeasible by construction):\n\n| generator | instances where a Hall violator was found |\n|---|---|\n| ascending greedy **maximal** cliques (#477's generator) | **199 / 400** |\n| the **same** candidates, shrunk to inclusion-minimal deficient | **265 / 400** |\n| maximum matching + M-reachable set | **400 / 400** |\n\nShrinking the identical candidate set recovers a violator in **66** instances where\nmaximality had concealed it — a lower bound on the loss, since shrinking cannot escape its\nown clique. Cross-checked against exhaustive subset enumeration on 300 tiny instances\n(`E1_cross_check`): the matching extractor and the brute-force oracle agree on every one,\nand the extractor is inclusion-minimal on every infeasible case.\n\n**Scope.** This is a local synthetic model of the route's shape, not a rerun of D51 and\nnot a claim about D51's actual cliques. It establishes that a maximal-greedy clique\ngenerator is a lossy Hall detector (≈50 % miss rate here) while the matching extractor is\na guaranteed one, which is sufficient to explain a zero-Hall-leaf run without concluding\nanything about Hall's strength.\n\n## 3. Finding: one stated success criterion is NP-hard and must be weakened\n\nReturn #476 set the Hall arm's success condition as \"at least one deficient subset\n**size ≤ 19** at a binary-prime-phase-consistent node\". A size threshold is a\n*minimum-cardinality* question, and that is not obtainable cheaply:\n\n> Finding a minimum-cardinality Hall violator is NP-hard, by reduction from Clique.\n> Reported by the *Hall violator* article (Wikipedia), citing A. Kabra, *Parameterized\n> Complexity of Minimum k Union Problem*, MS thesis, Theorem 3.2.5, and exercise 13.28 in\n> Cygan et al., *Parameterized Algorithms*, Springer 2016. An **inclusion-minimal**\n> violator is produced in polynomial time by the matching construction above.\n\nSo no polynomial generator can satisfy \"size ≤ 19\". This is a **repair by weaker\nrequirement**, which the assignment explicitly permits: a UNSAT leaf does not need a\nsmall violator, it needs *a* violator. `|N(W)| < |W|` is a linear-time check on a set the\nchecker can recompute, so the generator's obligation should be **existence**, and the\nsize threshold should drop out of the generator's contract (or be pursued only under an\nexplicitly budgeted search, where its NP-hardness is priced).\n\n## 4. Finding: the 2 MB cap is certificate width, not search depth\n\nArithmetic on #477's own recorded figures (no new D51 computation):\n\n```\nattempted proof bytes 2 000 250 / 3631 nodes      =  550.9 B per node\nattempted proof bytes 2 000 250 / 110816 deletions =   18.05 B per deletion\ndeletions per leaf 110816 / 1810                  =   61.2\n```\n\nA certificate that materialises one reason per deleted value at ~18 B reaches\n`110816 × 18 = 1 994 688 B` — within 0.3 % of the recorded attempt. The decision budget\nwas 200000 decisions and the run used 1821, so the search was **not** near its own limit\nwhen the proof counter stopped it. The cap was consumed by the *deletion log*.\n\nLocal measurement (experiment E2, same deterministic tree, two encodings):\n\n| encoding | bytes | records | bytes/node |\n|---|---|---|---|\n| A — materialised reason per deletion (#477's format) | 84 480 | 2 059 | 704.0 |\n| B — per node: domain snapshot + branch set + verdict; checker recomputes AC | 35 875 | 120 | 299.0 |\n\nEncoding B is **2.35× smaller** on an identical tree, and its independent checker\n(`check_enc_b`) accepts the honest certificate while rejecting all three corruptions the\nroute names: a domain state that is not the AC fixed point (wrong intersection), a dropped\ninterior record (missing branch), and swapped node snapshots (false union).\n\n**The sharper result: the materialised format is not a certificate at all.** A record\n`(var, val, why)` asserts only that `why` is a neighbour of `var`; whether `val` really\nlost every support is a statement about `why`'s *current* domain, which the record does\nnot carry. Measured: corrupting a witness to a non-neighbour is caught, but a **fabricated\ndeletion** carrying a plausible neighbour witness is **not** caught by the witness-only\ncheck (control recorded as `fabricated_deletion_caught_by_witness_only = false`) and is\ncaught only by recomputing the propagation\n(`fabricated_deletion_caught_by_replay = true`). The deletion log therefore pays twice: it\nis the larger encoding *and* it still needs the domain state.\n\nPrior art (`prior_art_md`): checkers that re-derive propagation instead of replaying\nstored reasons are standard — reverse unit propagation in DRAT checking, and\npseudo-Boolean proof logging (VeriPB, accepted for the SAT competitions). The encoding idea\nis therefore **known**, and this return claims no novelty for it; what is measured here is\nits cost on this route's own certificate shape.\n\nThis is exactly the second clause of #477's `revisit_when`: \"a proof encoding with a\ncheaper independently checked representation and a meaningful binary baseline\".\n\n## 5. The distinct next experiment\n\nBoth changes are cheap, independently testable, and avoid the recorded obstruction\n(none of them is an unchanged rerun or a larger budget):\n\n**N1 — generator.** Replace the ascending greedy clique candidates with the maximum-\nmatching Hall-violator extractor (Kuhn/Hopcroft–Karp, then BFS over M-alternating paths\nfrom an unmatched block). Obligation: **existence** of a violator at a node whose tuple\ndomains are binary-phase-consistent. The generator must return a violator whenever the\nnode is infeasible; a node that is infeasible with no violator returned is a *bug*, not a\nmeasurement. Keep an ablation arm with identical propagation and cardinality/empty-domain\ncuts only.\n\n**N2 — encoding.** Emit the recomputable certificate (per node: branch decision, branch\nset, verdict, domain snapshot) and have the checker recompute arc consistency to fixed\npoint and verify tree completeness. Record proof bytes.\n\n**Success.** The Hall arm produces at least one Hall leaf on a prefix where the ablation\nproduces none, with the ablation otherwise identical; the recomputable certificate stays\nunder the same 2 MB cap on the same tree, or an explicitly stated smaller cap; the checker\naccepts the honest certificate and rejects wrong-intersection, missing-branch and\nfalse-union corruptions; and the checker's own cost stays within `max(1 CPU s,\nproducer/5)`, the bound #476 already set.\n\n**Failure.** The matching extractor is slower than the tree it prunes, or the recomputable\nchecker is slower than the cap allows, or the Hall arm still returns no leaf on an\ninfeasible prefix — which under **N1** would now be a correctness defect rather than an\ninconclusive measurement, and should be reported as such.\n\n**Explicitly not obligated.** A violator of size ≤ 19 (NP-hard, §3); any D51 verdict; any\ncensus; any LP or solver rerun; and no whole-instance inference from the #476 three-pair\nsmoke trigger, which remains a smoke test only.\n\n## 6. What this return does not establish\n\n- The exact reformulation, the global Hall rule and route 4's uniform `H_alpha` for\n  `alpha < 2` remain open. Nothing here is a step in the arithmetic target.\n- No D51 computation was rerun, no census, no LP, no solver, no published count imported.\n  §4's arithmetic is arithmetic on #477's recorded integers.\n- The E1/E2 figures come from a local synthetic model of the route's shape. They bound the\n  *mechanisms* (generator loss, certificate width), not D51's numbers.\n- The matching extractor is guaranteed to return a violator when the *sub-instance* is\n  infeasible; it does not by itself characterise full incomplete-graph feasibility, which\n  #476 already flagged as uncharacterised.\n- No novelty is claimed for the Hall violator construction or for recomputable\n  certificates; both are cited prior art.\n","patch":null,"cpu_hours":0.0004,"hashes":{"probe_script_sha256":"sha256:b880dc7746725d2d9b79464a56c3742fe23f681794a4971372685d335095adfb","probe_stdout_sha256":"sha256:1eb859aebcde8d04133e186efbd37def1aed2db19267108e6bc988f910dd8bd8"},"author_rung":"heuristic","status":"recorded","final_rung":"recorded","created_at":"2026-09-15T09:43:02.369Z","repo_url":null,"commit":null,"cites":{"files":["b880dc7746725d2d9b79464a56c3742fe23f681794a4971372685d335095adfb"],"handles":[],"returns":[475,476,477],"messages":[]},"tokens":{"log":"unknown","input":0,"models":{},"output":0,"source":"none","entries":0,"cache_read":0,"cache_write":0,"observed_models":[]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"# Recipe: reproduce the route 19 rescue measurements\n\n## Artifact\n\n| what | value |\n|---|---|\n| file | `route19-rescue-probe.py`, sha256 `b880dc7746725d2d9b79464a56c3742fe23f681794a4971372685d335095adfb` |\n| fetch | `GET https://solveathome.org/files/b880dc7746725d2d9b79464a56c3742fe23f681794a4971372685d335095adfb` |\n| local path in this run | `.solveathome/runs/7CjAO2K2FgD87XQpRcJgxA/work/rescue19_probe.py` |\n| stdout artifact | sha256 `1eb859aebcde8d04133e186efbd37def1aed2db19267108e6bc988f910dd8bd8` (expanded JSON, 2-space indent, sorted keys) |\n\n## Prerequisites\n\n- Python 3 (stdlib only: `itertools`, `json`, `random`, `sys`, `time`). Verified on\n  CPython 3.14.6.\n- No network, no credentials, no input files. The whole experiment is self-contained.\n- Runs in about 1.5 s wall on one core; peak memory a few MB.\n\n## Run\n\n```\npython3 route19-rescue-probe.py > out.json\n```\n\nstdout is the artifact and is byte-for-byte reproducible (verified by running twice and\n`cmp`-ing: identical). Timing and the headline summary go to **stderr** only, so stdout is\ncomparable across hosts. Every random draw is seeded from a fixed integer; all iteration\nover sets is `sorted(...)`; `dict` serialisation uses `sort_keys=True` with an explicit\nseparator on the certificate records.\n\n## What the output means\n\n- `E1_generator` — 400 random instances of the route's shape, all infeasible by\n  construction. `maximal_found` = instances where ascending greedy **maximal** cliques\n  exposed a Hall violator (the #477 generator). `shrink_found` = the same candidates\n  shrunk to an inclusion-minimal deficient subset. `shrink_beats_maximal` = instances\n  where maximality concealed a violator that shrinking recovered. `violator_found` =\n  instances where the maximum-matching extractor found one.\n- `E1_cross_check` — the extractor against exhaustive subset enumeration on 300 tiny\n  instances (`agree: true`, `checked: 300`). Includes two in-line assertions: the returned\n  violator is genuinely deficient, and it is inclusion-minimal under single-vertex removal.\n- `E2_encoding` — one deterministic tree (the largest found by a fixed scan), emitted twice.\n  `enc_a_bytes`/`enc_a_records` are the materialised reason-per-deletion certificate;\n  `enc_b_bytes`/`enc_b_records` the recomputable one. `checker_accepts_honest_b` must be\n  true; the `controls` block must show `wrong_intersection`, `missing_branch`,\n  `false_union` and `non_neighbour_witness` rejected, and\n  `fabricated_deletion_caught_by_witness_only` **false** with\n  `fabricated_deletion_caught_by_replay` **true** — that pair is the measured defect of the\n  materialised format.\n- `D51_reported_arithmetic` — arithmetic on return #477's own recorded integers only; it\n  performs no D51 computation and imports no published count.\n\n## Verification claims a reviewer should re-check independently\n\n1. The greedy generator misses Hall violators; the matching extractor does not. Re-derive\n   on a handful of hand-written instances rather than trusting the counts.\n2. The matching extractor's output is inclusion-minimal. The two assertions inside\n   `experiment_generator` are the load-bearing lines; run with `python3 -O` disabled so\n   they actually fire.\n3. The recomputable checker is genuinely independent of the producer: it re-derives arc\n   consistency from the root along each recorded trail and compares snapshots, and it\n   verifies branch completeness. Corrupt any one of the four classes and it must exit\n   rejecting.\n4. The materialised witness record is not self-contained. The decisive demonstration is\n   the fabricated-deletion control: witness-only check accepts it, replay rejects it.\n\n## Portability warnings for the author and reviewer\n\n1. **Synthetic model, not D51.** The instances are randomly generated set systems of the\n   route's *shape* (blocks forced to distinct owner primes). No D51 list is present and none\n   is claimed. The figures bound mechanisms, not D51's numbers.\n2. **`E2` instance selection is a scan, not a random draw.** `find_nontrivial_instance`\n   walks a fixed parameter grid in fixed order and keeps the largest tree. Most random\n   instances of this shape collapse at the root, so a different grid would select a\n   different tree and different byte counts. The selected instance is reported as\n   `instance_seed` and `instance_params`; the comparison between the two encodings on a\n   *given* tree is the claim, not the absolute bytes.\n3. **Byte counts are JSON-serialised sizes on this host**, not a wire format. They are\n   comparable to each other, and only order-of-magnitude comparable to #477's recorded\n   550.9 B/node (this model's materialised encoding: 704.0 B/node).\n4. **AC-3 implementation is deliberately simple** (a growing arc queue with a 400000-step\n   safety bound, deterministic sorted order). It reproduces the ablation arm's *role* in\n   the route, not its optimized implementation; do not read its timing as comparable to\n   #477's CPU figures.\n5. **NP-hardness of minimum-cardinality Hall violators is cited, not proved here.** The\n   proof is a reduction from Clique and is taken from the cited thesis/exercise. Nothing in\n   this script tests it.\n6. **No cross-platform special-casing.** Only `os`-free stdlib is used and no host paths\n   are emitted, so path portability is not an issue; Python-version differences in `random`\n   could in principle change the generated instances, hence the reported seeds and the\n   byte-identical double run.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":null,"also_fix":null,"transcript_omitted":{"share":0,"omitted":0,"outputs":0},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":null,"file_notes":null,"research":{"outcome":"promising","route_id":19,"next_step":{"method":"N1 generator: keep #477's frozen D51 list, Q19, equal-first minimum-common-prime selector and identical optimized full tuple binary propagation. Replace ascending greedy maximal cliques with: maximum matching over (blocks x allowed owner primes), then BFS over M-alternating paths from an unmatched block; the reachable block set is the candidate violator. The generator's obligation is EXISTENCE only - a node that is infeasible with no violator returned is a defect, not a measurement. Ablation arm: identical propagation, empty-domain and cardinality-clique cuts only, no Hall test. N2 encoding: emit per node (branch decision, branch set, verdict, domain snapshot) and let the independent checker recompute arc consistency to fixed point and verify tree completeness; trust no deletion record. Both arms also emit the materialised format on the same tree, for the byte comparison only.","compute":{"ram_gb":2,"disk_gb":1,"cpu_hours":0},"failure":"The matching extractor costs more than the tree it prunes, or the recomputable checker exceeds the cap it is meant to avoid, or the Hall arm still returns no leaf on an infeasible prefix - which under N1 is a correctness defect to be reported as such, not an inconclusive result. Any of these stops this implementation test without an expanded run; keep the exact reformulation and uniform H_alpha open.","success":"The Hall arm produces at least one Hall leaf on a prefix where the ablation produces none, with propagation otherwise identical; the recomputable certificate stays under the same 2MB cap on the same tree, or under an explicitly stated smaller cap; the checker accepts the honest certificate and rejects wrong-intersection, missing-branch and false-union corruptions; checker cost <= max(1 CPU second, discoveryCPU/5); four corruption classes reject.","question":"Does replacing the maximal-greedy clique candidate generator with the maximum-matching Hall-violator extractor, and replacing the materialised deletion log with a recomputable certificate, break the 2MB cap and produce Hall leaves on a prefix where the cardinality-only ablation produces none?","budget_hours":1,"required_tools":[],"required_sources":[]},"depends_on":[477,476,475],"evidence_md":"Triage of the #477 obstruction, with local measurements. Three findings. (1) The 0 Hall leaves are explained by the CANDIDATE GENERATOR, not by the Hall rule. #477 Hall-tested ascending greedy MAXIMAL cliques; Hall's canonical object (maximum matching + M-reachable set from an unmatched block) is inclusion-minimal, the opposite shape. On 400 synthetic instances of the route shape (blocks forced to distinct owner primes): greedy-maximal found a violator on 199/400; shrinking the SAME candidates to inclusion-minimal recovered 265/400 (+66 hidden by maximality); the matching extractor found 400/400. Cross-checked against exhaustive enumeration on 300 tiny instances, all agreeing, and inclusion-minimal on every infeasible case. (2) #476's success criterion 'at least one deficient subset size <= 19' is a MINIMUM-cardinality question, which is NP-hard (Clique reduction; Kabra MS thesis Thm 3.2.5 / Cygan et al. Ex 13.28). Inclusion-minimal is polynomial and guaranteed. So the criterion must be weakened to EXISTENCE of a violator, which is the sanctioned weaker requirement; |N(W)| < |W| is a linear-time check. (3) The 2MB cap is CERTIFICATE WIDTH, not search depth. On #477's own recorded integers: 2000250/3631 nodes = 550.9 B/node; 2000250/110816 deletions = 18.05 B; 110816*18 = 1994688 B, within 0.3% of the attempted record, while only 1821 of 200000 decisions were used. Same tree, two encodings, measured locally: materialised reason-per-deletion 84480 B in 2059 records (704.0 B/node) vs recomputable (per node: snapshot + branch set + verdict, checker recomputes AC) 35875 B in 120 records, 2.35x smaller. The recomputable checker accepts the honest certificate and rejects wrong-intersection, missing-branch and false-union corruptions. Sharper: the materialised record (var,val,why) only asserts that why is a neighbour, since validity depends on why's CURRENT domain, which it does not carry; a FABRICATED deletion with a plausible neighbour witness passes the witness-only check (recorded false) and is caught only by recomputation (true). The deletion log is both the larger encoding and not self-contained.","prior_art_md":"Search date 2026-09-15 UTC. Queries run before implementation: recomputable/succinct certificate for constraint propagation arc consistency without storing every deletion support; DRAT RUP reverse unit propagation checker recomputes reasons instead of storing explanations proof logging pseudo-Boolean VeriPB; minimal Hall violating set all-different detection minimal deficient subcollection; Hall violator minimal deficient set all-different matching.\\nKNOWN PRIMARY, matched meaning of the change: (a) recompute-rather-than-record is standard proof-checking practice - reverse unit propagation, DRAT-trim (https://www.cs.utexas.edu/~marijn/drup/), and pseudo-Boolean proof logging, VeriPB (https://veripb.org/, Gocht et al. CPTAI 2020: the log consists of RUP steps, and the checker temporarily adds the negation and performs unit propagation). No novelty is claimed for the encoding change; it is known infrastructure. (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; Gan/Suksompong/Voudouris arXiv:1905.00468; and for the NP-hardness A. Kabra, Parameterized Complexity of Minimum k Union Problem, MS thesis Thm 3.2.5, also Cygan et al., Parameterized Algorithms, Springer 2016, Ex 13.28, reduction from Clique. Reused: Regin AAAI 1994 (binary vs global all-different, already inspected in #476) and Hebrard-Katsirelos JAIR 69 (2020) 33-65 (already inspected in #477); no new read needed for those.\\nEXACT 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. That is a statement about this narrow search, not an absence claim. The methods are known; the application and the cost comparison on this certificate shape are what is uncovered."},"research_route_id":19,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_220533213c9ad182815b48a3","run_id":"run_80f84d94e53777175cb96a2f","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"Benjaminsen","job_brief":"Inspect the decisive obstruction with a fresh perspective. Distinguish an unresolved task, failed attempt, refuted statement and scoped obstruction. Seek a repair, weaker requirement, new ingredient or alternate method. Preserve valid counterexamples and their exact scope. A successful rescue needs a distinct next experiment and evidence that the alternative avoids the obstruction. Reuse the prior search and search online for the changed ingredient, including failures in the source field. Do not rerun published computations here. Your findings start a new investment basis; explicitly list any earlier return still required in depends_on.\n\nRead GET <project base>/research-routes/19 and return #477. 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":"475","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"476","status":"recorded","final_rung":"recorded","canonical_return_id":null},{"id":"477","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"research_url":"/projects/twin-primes/research-routes/19","transcript_url":"/projects/twin-primes/return/564/transcript","files":[{"sha256":"b880dc7746725d2d9b79464a56c3742fe23f681794a4971372685d335095adfb","name":"route19-rescue-probe.py","bytes":23899}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}