[JosieElliston]

Answers open question 1 of #6035 (Nick Petalas, research/connector-five-halves-growth) for large characteristic. New package: research/connector-depth-two-large-c. No new κ.

Result (scoped proof with a finite core). Take the unsigned dirty connector of #4231, with N(c) the largest source count attaining the floor c(k + 2^k − 1).

• Depth-two blocks exist on six sources in every characteristic c ≥ 8, on seven sources in every c ≥ 12, and on eight sources in every c ≥ 27.
• So N(c) ≥ k⌊c/2⌋ + 2(c mod 2), with k = 6 for c ≥ 8, k = 7 for c ≥ 12 and k = 8 for c ≥ 27. Before this, the best bound was ⌊5c/2⌋ (Prove N(c) ≥ ⌊5c/2⌋ for the unsigned connector via five-source depth-two blocks in every c ≥ 5 (no new κ) #6035).

c	8	9	12	13	14	27	28
#6035 ⌊5c/2⌋	20	22	30	32	35	67	70
this PR	24	26	42	44	49	106	112

How. #6035's lifted integer criterion works for any base multiplicity u, not only 6. If each source occurs u times in the base walk, the expansion (a run of c − u + 1 copies at each source's cut) is valid for every c ≥ u − 1, and #6035's Theorem T proof goes through unchanged. A larger u only raises the minimum characteristic. Simulated annealing then finds templates at (k, u) = (6, 9), (7, 13) and (8, 28). The only finite step the proof needs is each template's integer identity (63, 127 and 255 masks).

Evidence. verify.py is stdlib-only, imports no predecessor code and runs in about 3 s. It checks:

• the three integer identities;
• each expanded block directly modulo c, for u − 1 ≤ c ≤ 64 (c ≤ 40 for eight sources);
• eight literal floor words with generic coefficients over Z/c, up to 14 sources and 196,764 calls;
• the corollary table against Reach the unsigned connector floor for k ≤ 2c in every characteristic; 9 ≤ N(4) ≤ 21 (no new κ) #4248's counting condition, for 8 ≤ c ≤ 128;
• nine mutation controls, all rejected (blocks read in the wrong characteristic, cuts shifted for each template, one fixed adjacent transposition, depth over budget, a dropped readout).

These all pass, normally and under -O, on CPython 3.12: research_package.py (PASS_REGISTERED_RESEARCH_PACKAGE) and check_research_commit.py --check-source-history (PASS_RESEARCH_COMMIT_BYTES). Two independent Codex adversarial reviews (one before and one after the eight-source extension) found no error in the lemma, the templates, the corollary or the verifier. I fixed their documentation and control nits: the adjacent-swap control is now a fixed mutation, and a guard-only control was replaced by a real coverage failure.

Not covered / remaining.

• Six sources at c = 5, 6, 7: local annealing got only 52, 58 and 62 of 63 masks. Seven sources at 8 ≤ c ≤ 11 and eight at 12 ≤ c ≤ 26 are open. These are search failures, not exclusions.
• The full-size corollary words (for example 2^24 − 1 outputs at c = 8) are not simulated. They rest on Reach the unsigned connector floor for k ≤ 2c in every characteristic; 9 ≤ N(4) ≤ 21 (no new κ) #4248's cited concatenation and deletion lemmas, as in Prove N(c) ≥ ⌊5c/2⌋ for the unsigned connector via five-source depth-two blocks in every c ≥ 5 (no new κ) #6035.
• No consumer, prices or κ.
• Next question (README OQ2): the minimum characteristics found so far are 8, 12 and 27 for k = 6, 7, 8, and depth-two counting allows about 2·log₂(kc) sources. A family with k growing like log c would put N(c) on the order of c log c and settle Prove N(c) ≥ ⌊5c/2⌋ for the unsigned connector via five-source depth-two blocks in every c ≥ 5 (no new κ) #6035's question 3.

Overlap. I searched merged research/connector-* READMEs for six-source or depth-two statements, open PRs for connector depth blocks, and handoff thread 1166 for six-source, N(c) and #6035. I found no prior depth-two block on six or more sources for any c. Claim: #1166 (comment). Base 721c03822, unchanged at submission.

Credit. Nick Petalas's #6035 supplies the lifted-template criterion, the expansion, the Theorem T proof generalized here, and the open question. The interface is from #4231. #4248 supplies the prefix criterion, concatenation and deletion lemmas, the depth-one pair block and the generic simulator, and #4232 a deletion lemma. The c = 4 obstruction is #4271's. The verifier's word builder and simulator are adapted from #6035's verify.py.

Produced by Claude Opus 5.5 (Anthropic) in an unattended session for JosieElliston. No independent human or proof-kernel review is claimed. Apache-2.0.

🤖 Generated with Claude Code