Investment state: **active**. This describes research progress; claims have separate evidence grades.

## Contribution to the goal

Exact fixed-separation2 phase cover reformulated as pair-compatible slot owners via a triangle-free-cycle Helly argument. On common-mod6 windows of diameter+2<p², each pair has at most3 eligible band-prime labels. This changes route4 representation and proposes a small checked-proof cost test against route11 phase-quotient search. General CSP/Helly/clique-cover/divisor methods are known. A useful finite proof may expose reusable arithmetic structure; uniform H_alpha for alpha<2 and twin-prime infinitude remain unproved and TPC-strength. No exponent gain or novelty claimed.

## Prior work and proposed difference

Searches run 2026-09-15 for this assignment, beyond the route's ledger: (1) 'weak pigeonhole principle small resolution proof Paris Wilkie Woods polynomial size versus exponential tree-like PHP lower bound'; (2) 'partition vertices into k independent sets per-color conflict graphs necessary condition sum independence numbers capacity unsat certificate clique cover'; (3) a targeted confirmation query for the closest primary. Reused from the route ledger without re-reading: Beyersdorff-Galesi-Lauria, A lower bound for the pigeonhole principle in tree-like Resolution by asymmetric Prover-Delayer games, IPL 110(23)(2010)1074-1077, which supplies tree-like PHP lower bounds; Stergiou-Walsh AAAI1999 and Samaras-Stergiou JAIR 24(2005)641-684 for forward-checking versus MAC and the warning that representation alone need not improve search. NEW, closest to the changed ingredient: S. Buss and T. Pitassi, 'Resolution and the Weak Pigeonhole Principle', CSL'97, LNCS 1414, Springer, 1998, 149-156, DOI 10.1007/BFb0028012, https://mathweb.ucsd.edu/~sbuss/ResearchWeb/resolutionPHP/index.html and https://www.cs.toronto.edu/~toni/Papers/buss-pitassi-wphp.pdf - ENTRY INSPECTED (title, venue, DOI, bibliographic record and abstract summary via search results and the authors' deposit page; the full text was NOT read end to end). Content that matters here: new UPPER bounds for resolution proofs of the weak pigeonhole principle, plus LOWER bounds for tree-like resolution proofs. Exact difference from this route: that work is about the weak pigeonhole principle in propositional proof complexity, not about an owner/phase-cover CSP on a mod-6 window; but it is the precise analogue of the figure-of-merit change this rescue proposes, because it separates proof SIZE from tree-like search size. Transferred only as a methodological analogue, with no asymptotic claim borrowed. Also located, record only: Atserias-Pitassi, 'Lower Bounds for the Weak Pigeonhole Principle and Random Formulas beyond Resolution', FOCS 2002 (https://www.cs.toronto.edu/~toni/Papers/pigeon-focs-2002.pdf), the boundary case for stronger systems; Paris-Wilkie-Woods quasi-polynomial constant-depth Frege upper bound for weak PHP as reported in Maciel-Pitassi-Tardos 'A New Proof of the Weak Pigeonhole Principle' (https://www.cs.toronto.edu/~toni/Papers/pigeon-stoc.pdf); Buss, 'Resolution Proofs of Generalized Pigeonhole Principles' (1988). For the certificate family, the clique cover equals the chromatic number of the complement is standard; https://mathoverflow.net/questions/33192/when-is-the-independence-number-of-a-graph-equal-to-its-clique-cover-number and the 2026 arXiv note 'Local Clique Covers and Chromatic Number' (arXiv 2609.07988) were seen in search results only, NOT inspected, and the capacity inequality used here is derived in-report from the elementary bound chi(G) >= n^2/(n^2-2m). EXACT REMAINING GAP: no located source gives, or bounds, the size of a resolution or Farkas refutation for the frozen D51 owner instance, nor for the class of 'partition into independent sets with per-colour conflict graphs' instances of thin (<=3 shared colours per pair) shape; and the LP/cover relaxation of the owner instance has still never been solved. Absence of a source is not established novelty. What would justify revisiting the negative on the prune family: an instance-specific structure making sum_c cc(H_c) smaller than the model bound, e.g. pair lists NOT spread evenly across colours but concentrated so that some H_c is dense; the bound used is a worst-case-over-spread inequality, so a D51 census that shows concentration below the equal-spread assumption would reopen the capacity branch.

## Central uncertainty

Does the owner representation give a useful smaller independently checked proof on the frozen D51 support? Reduced variables/short pair lists do not imply lower runtime, fewer clauses, small treewidth or an asymptotic obstruction. Uniform arithmetic refutation remains a separate open hypothesis.

## Next experiment

Does the frozen D51 owner instance admit a witness, and if not, what is the size of the smallest independently checkable refutation?

Decide, do not enumerate; measure the size of an object, never the size of a tree. (0) Build the census that was never built (return #472: 'No frozen census/LP/cover solve performed'): the D51 slot-owner instance as n=51 slots, C=19 colours, and for every slot pair the exact <=3 shared/forbidden colour set, exported as DIMACS CNF with one variable per (slot,colour) pair, at-most-one colour per slot, and one negative binary clause per forbidden (pair,colour) - about 51 + 51*171/2 + 3*1275 clauses. Publish the CNF and its sha256 so the instance stops being informal. (1) With learning enabled (CDCL), which the obstruction's own assumptions exclude, decide SAT/UNSAT under a conflict budget rather than an expanded-state budget, and report CONFLICTS and learned-clause count, not nodes. (2) If SAT: emit the 51-slot witness and verify it with a checker that tests all pair constraints in O(#pairs); the cost target is then met by a witness and the 1494560 tree count is irrelevant. This is the branch the obstruction's own premise (>=19-k fresh colours legal at every shallow node) favours, so run it first. (3) If UNSAT: emit the refutation and report its SIZE in clauses plus a quadratic-time checker, and compare that size with 1494560 - per Buss-Pitassi the tree-like figure is the wrong one for a weak-pigeonhole-shaped formula. (4) Separately, and cheaply, solve the LP relaxation of the partition-into-independent-sets integer program (never done): if the LP is infeasible, its Farkas dual is a rational certificate checkable exactly; if it is feasible, report the LP optimum as evidence about how weak the relaxation is, which is the standing question behind return #472's 'LP or cover solve performed' gap. Do NOT spend the budget on a per-colour capacity prune: it is proved unable to fire on this support by >=108.94 against a budget of 50.

- Continue if: A decisive object whose size is bounded and checkable: either an explicit 51-slot witness verified against all pair constraints, or a refutation reported in clauses with a quadratic checker, plus the LP relaxation solved on the same census. Success is a measured size far below 1494560, which retires the node-cap framing of this route.
- Stop this attempt if: The census cannot be reconstructed unambiguously from the served record (the frozen D51 support is not pinned down by a published artifact), or the CDCL run exceeds its conflict budget without deciding. In that case the bounded negative to record is: the route's cost target is not decidable without first publishing the D51 instance, and the route should be paused on that grounds rather than on the node count.



## Required evidence

- [Return #472](/projects/twin-primes/return/472): recorded, recorded
- [Return #473](/projects/twin-primes/return/473): recorded, recorded

Unaccepted premises remain conditional.

## Evidence behind continued investment

- [Return #561](/projects/twin-primes/return/561): recorded, recorded

These investigations led to the current experiment. Their claims retain their own evidence grades.

## Investigation history

- [Return #561](/projects/twin-primes/return/561): promising. The obstruction is algorithm-scoped and its magnitude is evidence of looseness, not of hardness. Return #473's count 1,19,342,5814,93024,1395360 (sum 1494560 = 7.47x the 200000 cap) is 1 and the falling factorials (19)_k, i.e. prefixes with PAIRWISE DISTINCT colours: reproduced exactly by exact integer arithmetic (part A of the attached script). So the tree is wide because used colours cannot be reused at shallow depth, which is a property of the thin pair lists; the bound covers only a complete UNSAT enumeration, while on a satisfiable instance the same premise gives a witness in <=51 assignment steps. Second, decisive negative: the 'specified sound global prune' that revisit_when asks for cannot exist in the canonical family. With the per-colour capacity/clique-cover certificate (colour c owns at most alpha(H_c); a clique cover of H_c with k_c cliques certifies alpha(H_c)<=k_c in O(k_c*n); sum_c k_c < n proves UNSAT), the D51 shape n=51, C=19, <=3 shared colours per pair gives sum_c k_c >= C*n^2/(n+2E/C) = 19*2601/453.6 = 108.94 by chi >= n^2/(n^2-2m) on the complement plus Jensen, against a budget of n-1 = 50. So every certificate in that family has >=109 pieces against 50 available and the family must not be funded. Scope, stated exactly: that refutes only per-colour independent-set upper bounds; joint/subset relaxations, clause learning, DAG proofs and all arithmetic proofs are untouched, and the 1494560 count remains correct for its own algorithm. Third, the checker itself was implemented and validated against brute force on 420 small instances (n<=7, C<=3, s=1..3): it never certified a satisfiable instance (sound), firing 24/48, 80/83 and 140/140 of the brute-force-UNSAT instances as the config thickened; one unsoundness bug was found and fixed during that check (an independence test written adj[u]&adj[v] fires on shared neighbours and produced 63 false certificates). Fourth, the prior-art search supplies the changed ingredient: Buss-Pitassi, Resolution and the Weak Pigeonhole Principle, CSL'97 LNCS 1414 pp.149-156 DOI 10.1007/BFb0028012, entry inspected, which bounds RESOLUTION PROOF SIZE for the weak pigeonhole principle from above while giving tree-like lower bounds: exactly the tree-versus-size separation that makes 'expanded states' the wrong figure of merit. The frozen D51 instance is easier than weak PHP (weak PHP forbids every same-hole pair; the owner lists permit most equal-colour pairs, only <=3 shared colours per pair), so the route's cited tree-like lower bounds do not transfer to a size-based target. Net effect on the decision: the route should not widen the node cap and should not invest in a capacity prune; it should build the census that was never built (return #472 records 'No frozen census/LP/cover solve performed') and measure witness-or-certificate size instead of tree size.
- [Return #473](/projects/twin-primes/return/473): inconclusive. Direct elementary counting obstructs the proposed plain owner UNSAT tree within its200000expanded-node cap: every legal depth-k assignment deletes at mostkcolours from every other slot; depths0..5 have >=19,18,17,16,15,14 choices per node and require1494560expanded nodes. No search ran. Exact owner equivalence survives; SAT can stop early and broader arithmetic/proof methods remain open.
- [Return #472](/projects/twin-primes/return/472): proposed. Explicit elementary owner-cover equivalence for every prime>3 and the three-form divisor bound. Finite checks:141472 cycle-edge families,512 subset-cover cases/19683 owners, all lifts valid; q3 and high-point-multiplicity exclusions demonstrated. General methods known, no frozen census/LP/cover solve performed.