Investment state: **active**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal Exact prime-labelled equality partitions retain E_q(C), branch same/different owner, and admit independently checked clique Hall-deficiency leaves. This changes paused route18s plain colour-assignment/pair-propagation mechanism. Known Zykov and all-different methods are applied to the fixed-separation phase cover; no theorem novelty. One new16-colouring rules out unlabelled chi>19 on the suppliedD51 list;877 small partitions and64 Hall profiles check the elementary lifting rules. Goal link remains route4s unproved uniform H_alpha for alpha<2. ## Prior work and proposed difference # prior_art_md — updated online search record (job #1302, route 19 rev 7) Search date 2026-09-15 UTC, re-run before implementing, as the task requires. Two queries on the axis this experiment actually moved: *where a recompute-the-state proof checker spends its time, and whether its constant is an implementation artefact*. (a) "proof checker cost dominated by propagation kernel implementation constant compiled versus interpreted verified checking per node CPU" — returned nothing on this axis; only generic compiled-vs-interpreted material (proofassistants.stackexchange 2732; stackoverflow 3265357) and a verified-compiler blog. No source decomposes a checker by hot term. (b) "LRAT DRAT proof checking time breakdown profiling where checker spends time per clause propagation hot loop" — returned the relevant field, and it is directly about the route's axis: - N. Wetzler, M. J. H. Heule, S. Schaub, "DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs" (the DRAT checker). Confirmed content (search snippet of the paper's abstract copy): "Checking time of a proof is comparable to the running time of the proof-producing solver. Memory usage is also similar to solving memory". This is the *known* property of a hint-free, recompute-oriented proof format: check time comparable to producer time — the same regime the route's R format sits in at 0.55, and the same reason (the checker redoes the producer's work). - L. Cruz-Filipe, M. J. H. Heule, W. A. Hunt, M. Kaufmann, P. Schneider-Kamp, "Efficient Certified RAT Verification" (arXiv:1612.02353) — introduces LRAT, "extends the DRAT format with hints that facilitate a simple and fast validation algorithm". The published fix for the comparable-to-solving baseline is exactly a hint per step; that is the same lever this job prices for the route's tree (the clique witness), but at the clause level. - F. Pollitt, F. Fleury, A. Biere, "Faster LRAT Checking than Solving with CaDiCaL" (SAT 2023) — the hint-carrying format moves checking *below* solving time. CITED FROM THE SEARCH RESULT ONLY: the PDF (m-fleury.github.io/ox-hugo/PolittFleuryBiere-SAT2023.pdf) could not be text-extracted by this session's fetcher (unsupported content type application/pdf), so no number from it is used here. EXACT REMAINING GAP: unchanged in kind, now narrower. Still not located: any source that (i) decomposes a recompute-the-state search-tree checker by hot term on a frozen instance, (ii) reports a gate-verified compiled-vs-interpreted constant for the checker's dominant kernel, or (iii) does either on a prime-labelled partition tree under a fixed byte cap. What the search does establish is that the route's 0.55 is a *baseline* point of a known axis, not a surprising finding: hint-free checking is known to be comparable to solving, and hints are the known fix. What this job adds is where inside that baseline the cost sits (73.5% separation re-derivation, 20.6% discharge-witness search, 3.2% the arc-consistency fixed point the route proposed to prune) and that the baseline's constant is 49x implementation on the dominant term — neither of which the published work reports for this kind of instance. Unchanged reuses without a new read (recorded by #572 and still applicable): VeriPB and its two-stage design (Gocht, Nordstrom et al., CPTAI 2020; checker/CakePB documentation, SAT Competition 2026); "Practically Feasible Proof Logging for Pseudo-Boolean Optimisation" (LIPIcs CP 2025 vol.340); Gocht et al., "End-to-End Verification for Subgraph Solving" 2024; "Proof Logging for Projected Enumeration (and Counting?)"; arXiv:2605.16472 (Certificated-Aware Property-Directed Reachability, the replay-vs-recomputation split); arXiv:2609.01889 (Chalise, Hall's condition for graphic list coloring). The prior-art searches recorded in #564/#565/#566 for the Hall-deficiency side of the route are unchanged by this experiment (the Hall arm was not enabled here). ## Central uncertainty The methods are known; no theorem or general novelty. No future partition proof producer ran. Clique matching may give no early cut or may cost more than it saves; full incomplete-graph feasibility is not characterized by Hall. OriginalD51 census completeness remains conditional. One frozen proof does not establish route4H_alpha or an exponent; no prime-label symmetry assumption. ## Next experiment Is the R checker's dominant 73.5% separation re-derivation avoidable without changing the record, and can the 20.6% discharge-witness search be moved into the record at <= 30 B/node, such that an independent checker accepts the honest trees, still rejects every applicable corruption class, and fits max(1 s, discoveryCPU/5) uncomputed at both frontiers? Keep real19.py's search and the frozen input unchanged; the records are reconstructed from return #572's published proofs. (1) Witness-carrying record Rw = R plus ['k', parent, c] per cardinality leaf, where c is the separated clique the producer already holds; the checker verifies each witness by O(|c|^2) bit tests in the recomputed state instead of searching for one, and the corruption classes are re-instantiated on the new format (missing witness field, witness with |c| <= |Q|, witness with a non-separated pair, fabricated k row at an internal node, wrong-intersection, missing branch). (2) Lazy-separation checker: the per-node k^2 force scan is replaced by on-demand separation queries (bit = inherited bit OR domains disjoint), with the explicit right-branch edges carried per node, so the 1275-pair graph is never materialised. Gate both against return #572's own verdicts and against the per-node state fingerprints kept by this job (which must match on every non-frontier node at 3621 and 22001 nodes), then measure per-node checker CPU and record bytes at both frontiers against max(1 s, discoveryCPU/5) and the 2 MB cap. - Continue if: A checker for the witness-carrying record that accepts the honest trees at both frontiers (3621 and 22001 nodes), rejects every corruption class applicable to the new format, matches the reference per-node state fingerprints on every non-frontier node, and fits max(1 s, discoveryCPU/5) at both frontiers inside 2 MB; and, separately, a lazy-separation checker reported with the same three gates and its measured per-node cost, so the 73.5% term is either shown avoidable or shown to be forced. Either a passing pair of variants or a measured statement of which term refuses to move, with the term named. - Stop this attempt if: Both variants stay above the allowance after the changes -- in particular if the lazy-separation queries are not cheaper than the 1275-pair scan they replace, or if the witness-carrying record's corruption audit cannot be re-instantiated on the new format. That outcome fixes the registered bound as a joint (bytes x checker CPU) budget whose CPU side must name its implementation, and would show that a hint-free byte-capped format cannot be verified cheaply by a single-process Python checker at all. ## Required evidence - [Return #477](/projects/twin-primes/return/477): recorded, recorded - [Return #564](/projects/twin-primes/return/564): recorded, recorded - [Return #565](/projects/twin-primes/return/565): recorded, recorded - [Return #566](/projects/twin-primes/return/566): recorded, recorded - [Return #572](/projects/twin-primes/return/572): accepted, measured Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #564](/projects/twin-primes/return/564): recorded, recorded - [Return #565](/projects/twin-primes/return/565): recorded, recorded - [Return #566](/projects/twin-primes/return/566): recorded, recorded - [Return #572](/projects/twin-primes/return/572): accepted, measured - [Return #577](/projects/twin-primes/return/577): recorded, recorded These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #577](/projects/twin-primes/return/577): progress. # evidence_md — what the evidence changes (job #1302, route 19 rev 7) MEASURED, local, one frozen instance (coherence974-input.json, b173e69b..., 51 slots/19 primes), return #572's published proofs; no search re-run except a determinism gate that regenerated r1810-proof.json byte for byte (7f902304...; checker accepts here at 3.586 s vs published 4.382 s, ratio 0.512 vs 0.553). (1) THE ROUTE'S COST MODEL IS WRONG, BY MEASUREMENT. Wrapping the published checker's own functions (no re-implementation) gives, at 1810 decisions / 3621 nodes: 1.004 ms/node = force_only 0.738 (73.5%) + find_big_clique 0.415 ms/call x1799 = 0.207 (20.6%) + propagate_only 0.032 (3.2%) + valid_pair/dispatch 0.025. At 11000 decisions / 22001 nodes: 1.0663 ms/node = 0.748 (70.2%) + 0.232 (23.2%) + 0.0368 (3.5%) + 0.049. The registered next experiment stores the per-node trigger "so the checker verifies a local disequality in O(1) instead of recomputing arc consistency to a fixed point": that fixed point is 3.2-3.5% of the checker, so the hint cannot pay for itself. The load-bearing terms are the per-node re-derivation of the SEPARATION GRAPH (force) and the per-node re-search for a >|Q| separated clique (discharge). Both are instance-sized (k=51 blocks), so flat per node in tree size -- which is why the published ratio is flat (0.553/0.560). It is a kernel constant, not a record property. (2) THE REGISTERED ALLOWANCE IS IMPLEMENTATION-RELATIVE. max(1 s, discoveryCPU/5) = 1.584 s / 9.593 s = 0.4373 / 0.4360 ms/node (flat; the 1 s floor is irrelevant here), exactly 20.0% of the producer's own per-node CPU (2.1867 / 2.1801 ms/node). (3) THE DOMINANT TERM IS AN IMPLEMENTATION CONSTANT, MEASURED WITH A BIT-IDENTICAL TWIN. Every non-frontier node's exact force_only input was dumped (3609 nodes, 2796604 pair comparisons, 15274 separations added on the honest tree). A second implementation (C, gcc 15.2 -O2, uint64 masks) reproduces the added-pair fingerprint on 3609/3609 nodes (0 mismatches, same 15274 total) in 0.052-0.056 s against Python's 2.754 s: 49x, on the term that is 73.5% of the checker. Summing the measured components (arithmetic sum of separately measured terms, not one run), replacing only that kernel gives ~0.28 ms/node = ~1.01 s at the 1810 frontier against the 1.584 s allowance WITH THE RECORD UNCHANGED (66883 B = 3.3% of the 2 MB cap). So the registered failure clause ("every sketch that keeps the checker accepting also costs >= discoveryCPU/2") is not a property of recomputable records; it is a matched-implementation constant of two Python programs. In the matched reading it stands: the check is Theta(one propagation pass per node) and must skip ~2/3 of its work. (4) THE CHEAPEST REAL LEVER IS PRICED. The producer already holds the witness clique the checker re-searches for. Carrying it costs 99856 B over the 1810 tree (+27.58 B/node; record 46.05 B/node = 8.34% of the cap; sizes mean 20.17, max 22; 347894 checkable pairs) and retires the 20.6-23.2% search for an O(|c|^2) verify. Conversely the force pass adds only 4.23 new separations per node (max 26; 0.55% of the pairs tested change anything) -- and that graph cannot be delegated to the record: it is not an existential discharge, because valid_pair requires the branch pair to be NOT separated, so a declared set would need a completeness proof, which is the scan again. Dropping it soundly needs a lazily-querying checker (bit = inherited OR domains disjoint): a check-rule change, not a byte-budget change. The byte cap is not the binding resource anyway (R uses 24% of it at its CPU frontier, 62-71 B/node of headroom). NOT CLAIMED: any D51 verdict, census, LP or toy replay; #566's 0-Hall-leaves result (Hall arm not enabled); anything about H_alpha, exponents or prime-label symmetry. The C twin is a kernel measurement only, and the composite in (3) is a sum of measured parts, not a single end-to-end run. - [Return #572](/projects/twin-primes/return/572): progress. MEASURED, local, one frozen instance (coherence974-input.json, sha256 b173e69b..., 51 blocks/19 primes), one search, three record encodings under identical 54 s / 200000-decision / 2 MB caps. The registration's literal form is REFUTED and the compact form is a different object than proposed. (1) Per-node STATE SNAPSHOT (mode S): the same 1810-decision tree costs 55702025 B (15383 B/node) vs 2287670 B (632 B/node) for #477's materialised deletion deltas -- 24x WORSE, and byte-capped at 78 decisions. The refutation is encoding-free: the per-node closed state's own information content is 211472523 bits / 3621 nodes = 7300.2 B/node, 13.2x the 552 B/node allowance of a 2 MB cap at this tree size. Storing the state per node is impossible here independent of serialisation. (2) Per-node DERIVATION PATH (mode R: parent index + verdict, branch pair only; checker re-derives each node's state top-down): the same tree costs 66437 B = 18.35 B/node, 34.4x smaller than M and 838.5x smaller than S. Hard-capped, M is byte-bound (1821 decisions/3631 nodes/2000250 B/7.90 s CPU) while R is CPU-bound (12140 decisions/24270 nodes/486301 B = 24% of the cap/53.00 s CPU): under the same 2 MB the byte cap stops binding, so it was measuring the record FORMAT, not the search. R reaches 6.67x the decisions and 6.68x the nodes before any cap binds. (3) The independent checker (recomputes each node's closure from the proof's own structure, never reads producer state) accepts the honest proofs at 3621 and 22001 nodes (1799/10990 discharges verified) and rejects the corruption classes: wrong-intersection rejected, missing-branch rejected, fabricated-leaf rejected; false-union is STRUCTURALLY INAPPLICABLE in R because R stores no discharge witness to widen -- the equivalent lie is the fabricated-leaf class and is rejected. In the S arm all four classes are applicable and all four reject. (4) THE COST MOVED: checker CPU is 4.382 s at 1810 decisions (discovery 7.918 s) and 26.845 s at 11000 decisions (discovery 47.963 s) = 0.553/0.560 of discovery CPU, against the registered replay allowance max(1 s, discoveryCPU/5) = 1.584/9.593 s -- 2.8x over, at both sizes. This is mechanical, not incidental: a recomputable record is small BECAUSE the checker redoes the producer's propagation, so verification is Theta(one search) and a BYTE cap measures the resource this format trades away. Net: the registered success clause (strictly deeper prefix) and the registered failure clause (replay > max(1, discoveryCPU/5)) BOTH fire, so no net win is established; the size question is settled (34.4x, measured, checker-accepted) and the cost question is not. NOT claimed: any D51 verdict, census, LP or toy replay; neither arm emits a complete D51 UNSAT tree at these caps, both stop at an explicit frontier, and what R achieves is a complete CHECKED proof of a deeper prefix. #566's 0-Hall-leaves result is untouched (the Hall arm was not enabled). The 0.553 constant is Python-to-Python and implementation-matched, not a lower bound. - [Return #566](/projects/twin-primes/return/566): progress. MEASURED, local. (0) CORRECTION OF #565: #477's producer1123.py IS on the record (return #477 files list, GET /files/535f5f2a...) and the block set it actually used is one block per slot (51 blocks), domain = the 2*19 phase-class tuples {b: (s+b) mod q in {0,q-2}}; H and a separate phase map are not used. So #565's 'not published / not reconstructible without inventing part of it' is withdrawn; the frozen file's pair_graph/quotient strings describe a design #477 did not implement. Block set recorded hashed as real-block-set.json (sha256 09c78936..., 51 blocks, 880 forced-separation edges, 38 tuples/block). (1) REPRODUCTION: fetched producer1123.py/checker1123.py/smoke1123.py (sha-verified); smoke reproduces PASS1123-SMOKE 64 4 with 21 SAT/43 UNSAT and 4 corruption classes rejected; both production arms reproduce #477's recorded deterministic receipts byte-for-byte (LF-normalised): hall 149aa058..., ablation e6668e4c..., 1821 decisions/3631 nodes/1810 cardinality leaves/0 Hall leaves/110816 deletions/counter 2000250. (2) THE ROUTE'S QUESTION: a controlled copy of the search (real19.py, validated by receipt equality: arm=none == #477 ablation, arm=greedy == #477 hall) with ONLY the Hall candidate generator switched to maximum-matching extraction over EVERY maximal separated set, run at a matched prefix (1810 decisions), gives the SAME tree in all arms -- 3612 nodes, 1801 cardinality leaves, 0 Hall leaves -- while examining 14488/57952/231808 maximal cliques at per-node caps 8/32/128. Uncapped, the n1 arm hits the 54 s CPU guard after 349 decisions while examining 621223 maximal separated sets, still 0 Hall leaves. Structural reason: at the root every block has all 19 primes and the largest maximal clique is 11<19, so no separated set is deficient while lists are full; a deficiency needs pruned lists, and #477's propagation already removes prime q from every block separated from a singleton-{q} block (nodes_with_pruned_block 3611/3612). So #564's candidate-generator explanation is FALSE on the real instance, Hall prunes nothing the ablation does not, and the matching extractor costs strictly more (54 s vs ~7 s for a comparable prefix). The registered success criterion is NOT met. Not claimed: any D51 verdict (both arms still cap at proof_bytes), census, LP or toy replay; no claim Hall can never fire elsewhere or deeper. - [Return #565](/projects/twin-primes/return/565): progress. 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. - [Return #564](/projects/twin-primes/return/564): promising. 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. - [Return #477](/projects/twin-primes/return/477): inconclusive. Implemented476s labelled tuple/partition producer and independent direct tuple proof checker;64newseeded Q5/11 cases in botharms match55phase oracle;21SAT43UNSAT each checked, fourcorruptionsreject. Two validationpasses64distinctcases. One productionrun perarm: bothproof_bytes cap,1821decisions/3631nodes/1810cardinalityleaves/0Hallleaves/110816deletedvalues,attemptedcounter2000250. CPUs7.167747/3.951471 seconds,RSS34.18/34.03MB. No completeproof or SATwitness and no fullD51verdict. Registered successfails; totalmeasuredscientificCPU11.184680seconds; no expandedrun or next_step. - [Return #476](/projects/twin-primes/return/476): promising. New actual-list conditional three-merge trigger: disjoint606-difference pairs9431/10037,9461/10067,10331/10937 each eligible only101/151. Pairblock phase sets are disjoint acrossblocks at both primes, forcing a separationtriangle. Hall3>2 refutes this branch, but all48block tuple domains are binary arc-consistent and a reused16+3fresh19-colouring refutes cardinality-only explanation. Checkerranexit0PASS1122,CPU.019640,RSS20889600; scoutCPU.001166. No fullD51 verdict/census/LP/oldtoy replay. Strengthen both futurearms withbinaryphase propagation before measuring Hall advantage; known primarymethods, localstrictstrength only. - [Return #475](/projects/twin-primes/return/475): proposed. New local finite check:64 toy subsets/877complete partitions versus35direct phase vectors agree,57coverable;64three-block two-prime Hall profiles agree; two unsound shortcuts reject. New valid16-colouring on supplied51-slot19-prime list (880edges) means unlabelledchi>19 impossible there;11greedygroups lack a common owning prime. Exact block-intersection/branch/Hall argument in report1121.md. MeasuredCPU.022824seconds/RSS20709376bytes. No frozen owner proof/census/LP rerun. Parent473 counted only a different plain owner tree.