[JosieElliston]

Change and scope

Adds only research/connector-six-source-small-char/. It is a scoped finite exclusion for the unchanged unsigned dirty connector of #4231/#4248. No operation is added, and there is no new κ or selected-frontier change.

Result (local SAT, not a checked certificate). No word on six sources that calls each source exactly five times has depth two in characteristic c = 5: some nonzero mask in {0,1}^6 is never q_s + q_t mod 5. Three SAT solvers agree on the same exact encoding:

run	verdict	time
CaDiCaL 1.9.5	UNSAT	153 s
CaDiCaL 1.5.3	UNSAT	197 s
Glucose 4	UNSAT	237 s
CaDiCaL 1.9.5, masks of weight 2 and 6 only (16 masks)	UNSAT	160 s

Characteristic six. The same encoding at k = 6, c = 6 is also UNSAT with CaDiCaL 1.9.5 (1263 s) and MapleChrono (2056 s). The c = 5 verdict is also confirmed by the encoding without weight pruning (CaDiCaL 1.9.5, 2332 s).

Since deleting a source keeps depth two (#4232/#4248), the largest depth-two block at c = 5, and also at c = 6, has exactly five sources (#6035 supplies five). This answers the c = 5 and c = 6 cases of #6061's open question 1 and of the open item in #6057 / #6058. c = 7 had no verdict within the session and stays open. It does not decide N(5) or N(6): depth-three blocks and non-block floor words are not covered.

Controls reproduce known answers: k = 5 at c = 4 is UNSAT (#4271), k = 5 at c = 5 and k = 6 at c = 8 are SAT, and the found words pass the stdlib verifier. Weight subsets {1,2}, {1,6} and {1,5,6} are SAT at c = 5, so the core needs the weight-two masks together with something more; {1,2,3}, {1,2,6} and {2,6} are each UNSAT.

Encoding

search_sat.py (python-sat; local only, not in the registered replay): one-hot source per position with exactly c calls per source, one-hot prefix residues mod c with their transitions, and a selector per (mask, pair) forcing q_s + q_t ≡ m coordinatewise. Two reductions, both sound: sources first appear in label order (relabeling permutes coordinates and preserves the binary mask set), and a pair can realize m only if s + t ≡ |m| (mod c), because the coordinate sum of q_t is t (the weight identity of #6107). Boundary kc is dropped since q_kc ≡ q_0. Repeated boundaries (s = t) are allowed, as in #4248's multiset readouts.

Task and overlap

Base 721c03822c421b7f7fcbb2598993b947c4d88419, priority revision 8. Chooser seed 7697fac81dbeda13c228b2dbf7cf55f9 → connector-alphabet-change. Scope changed: the alphabet stays fixed; this follows the released open question of #6061 and #6057/#6058. Reason in TASK.json. Local interface side result; it passes no supplier budget gate.

Claim. scripts/find_overlap.py --task connector-alphabet-change, searches for "six-source depth-two" and "depth-two block", open PRs and #6058 found the question still open at submission. That is not a novelty certificate.

Validation

CPython 3.12, macOS arm64:

python3.12 -I -W error -B research/connector-six-source-small-char/verify.py
python3.12 -I -O -W error -B research/connector-six-source-small-char/verify.py
python3.12 -B scripts/research_package.py --package research/connector-six-source-small-char
python3.12 -B scripts/check_research_commit.py --package research/connector-six-source-small-char --check-source-history --check-modes

All pass. verify.py (standard library, < 1 s) checks the literal words (floor shape, depth two, the weight identity on every realizing pair) and four rejected controls. It does not replay the UNSAT verdicts. No DRAT/LRAT proof was produced or checked, and no human proof is given.

Review. A separate OpenAI Codex read-only adversarial review of the encoding against #4248's definition found no clause that excludes a genuine depth-two block (boundary 0, repeated reads, dropped boundary kc, symmetry breaking, transitions, exact counts and weight pruning all checked). It found one count error (the weights {2,6} instance has 16 masks, not 21), fixed at the current head. It did not run a solver. This is an AI review, not human or proof-kernel review.

Open next questions

1. c = 7: cube-and-conquer with the same encoding (no verdict after about 25 minutes on one core).
2. A checkable certificate for c = 5: DRAT for the weights {2,6} sub-instance, or a human proof from weight-two masks plus the all-ones mask.
3. Depth three at c = 5: a block on more than 7 sources would beat density 5/2 there (Prove N(c) ≥ ⌊5c/2⌋ for the unsigned connector via five-source depth-two blocks in every c ≥ 5 (no new κ) #6035 question 2).

Credit

Prepared by JosieElliston with substantial Anthropic Claude (Claude Code, session 50) assistance. Nick Petalas supplies the interface, depth notion, concatenation/deletion and the c = 4 obstruction (#4231, #4248, #4271, #6035), with the retained Ross Richardson #934/#943 lineage; zxv's #6057 and JosieElliston's #6061 supply the c ≥ 8 six-source blocks and the open question; #6107 supplies the weight identity; apoursh's #6071 supplies the Gray-walk family. Apache-2.0; no predecessor file changes.

🤖 Generated with Claude Code

[JosieElliston]

Update (head d192172): two more local SAT runs have finished. k = 6, c = 6 is UNSAT with MapleChrono (2056 s), which agrees with CaDiCaL 1.9.5, so the c = 6 verdict now rests on two solvers. k = 6, c = 5 is UNSAT on the encoding without weight pruning (--no-weight-prune, CaDiCaL 1.9.5, 2332 s), which confirms that the pruning does not drive the c = 5 result. The README table and TASK.json are updated. c = 7 is still open, and the evidence level is unchanged: local solver output, with no DRAT check.