No six-source depth-two connector block in characteristics five and six (local SAT; c = 7 open; no new κ)

research/connector-six-source-small-char/README.md

@@ -0,0 +1,132 @@
+# Six-source depth-two connector blocks: none in characteristics five and six (local SAT)
+
+**Scoped finite exclusion for the unchanged unsigned dirty connector; local
+solver evidence only; no new κ.**
+
+In the interface of [PR4231/PR4248](../connector-depth-blocks/README.md), no
+word on six sources that calls each source exactly five times has depth two
+in characteristic c = 5. Three SAT solvers report UNSAT on the same exact
+encoding, and the result already holds for the 16 masks of weights 2 and 6.
+Six-source depth-two blocks exist for every c ≥ 8
+([PR6057](https://github.com/CrocSwap/integer-mult-bounds/pull/6057),
+[PR6061](https://github.com/CrocSwap/integer-mult-bounds/pull/6061)), and
+five-source ones for every c ≥ 5
+([PR6035](https://github.com/CrocSwap/integer-mult-bounds/pull/6035)).
+Deleting a source keeps depth two (PR4232/PR4248), so the largest depth-two
+block in characteristic five has exactly five sources. The same encoding is
+also UNSAT at c = 6 (CaDiCaL 1.9.5 and MapleChrono agree), so the largest depth-two block there has five sources too. c = 7 is
+still open.
+
+This answers the c = 5 and c = 6 cases of open question 1 of PR6061 and of the open item
+in PR6057 / [#6058](https://github.com/CrocSwap/integer-mult-bounds/discussions/6058)
+("characteristics five through seven remain open").
+
+**What is and is not established.** The c = 5 verdict is the output of
+CaDiCaL 1.9.5, CaDiCaL 1.5.3 and Glucose 4 on one machine, plus CaDiCaL
+1.9.5 on the encoding without weight pruning; the c = 6 verdict is CaDiCaL
+1.9.5 and MapleChrono. No DRAT/LRAT proof
+was checked, and no human proof is given. `verify.py` (standard library)
+checks only the literal words: the positive controls and the encoding's
+pruning identity on them. Treat the exclusion as a reproducible local
+computation, not a certificate.
+
+## Interface and question (inherited, unchanged)
+
+Let a word w of length kc call each source operator B_j exactly c times (a
+floor word on its k sources). Let q_t ∈ Z^k count the calls of each source in
+the first t letters. PR4248 says w has **depth two** if every nonzero binary
+mask m ∈ {0,1}^k is congruent mod c to q_s + q_t for some boundaries s ≤ t
+(s = 0 gives a single read, since q_0 = 0). Depth-two blocks with total depth
+at most c concatenate to a floor word for the whole batch, so larger blocks
+raise the source count N(c) at which the complete-call floor is attained.
+No operation is added and nothing about the alphabet changes.
+
+## Result
+
+| k | c | verdict | evidence |
+|---|---|---|---|
+| 5 | 4 | UNSAT | control; matches PR4271's c = 4 obstruction (Nick Petalas) (2.8 s) |
+| 5 | 5 | SAT | control; word checked by `verify.py` |
+| **6** | **5** | **UNSAT** | CaDiCaL 1.9.5 153 s, CaDiCaL 1.5.3 197 s, Glucose 4 237 s; without weight pruning (`--no-weight-prune`) CaDiCaL 1.9.5 2332 s |
+| 6 | 5, weights {2,6} only | UNSAT | CaDiCaL 1.9.5 160 s (16 masks suffice) |
+| 6 | 5, weights {1,2,3} only | UNSAT | CaDiCaL 1.9.5 106 s |
+| 6 | 5, weights {1,2,6} only | UNSAT | CaDiCaL 1.9.5 130 s |
+| 6 | 5, weights {1,2}, {1,6}, {1,5,6} | SAT | each found in < 4 s; one word is a `verify.py` control |
+| **6** | **6** | **UNSAT** | CaDiCaL 1.9.5 1263 s, MapleChrono 2056 s |
+| 6 | 7 | open | no verdict within the session |
+| 6 | 8 | SAT | control (PR6057/PR6061 range); found word checked by `verify.py` |
+
+A subset of masks is a relaxation, so UNSAT on weights {2,6} alone implies
+the full UNSAT. The SAT rows bound how far that core can shrink by weight
+class.
+
+## Encoding (search_sat.py)
+
+Variables: the source at each position (one-hot, exactly c per source by a
+sequential counter); the residue of every prefix coordinate mod c (one-hot,
+with the one-step transition); for each mask and admissible pair (s, t) a
+selector y whose truth forces q_s + q_t ≡ m coordinatewise
+(`y ∧ [q_s[j] ≡ v] → [q_t[j] ≡ m_j − v]`); one clause per mask over its
+selectors. Symmetry breaking: sources first appear in label order, which is
+sound because relabeling sources permutes mask coordinates and preserves the
+set of binary masks.
+
+Pruning: 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 PR6107). Other pairs are
+omitted. Boundary kc is dropped since q_{kc} = c·1 ≡ q_0.
+
+Positive and negative controls (k = 5 at c = 4 and 5, k = 6 at c = 8)
+reproduce the known answers. The c = 8 word the solver found is in
+`verify.py`.
+
+```sh
+# registered standard-library replay (< 1 s)
+python3.12 -I -W error -B research/connector-six-source-small-char/verify.py
+# local search (python-sat 1.9.dev15; minutes per run)
+python search_sat.py 6 5 --solver cadical195        # UNSAT
+python search_sat.py 6 5 --solver glucose4          # UNSAT
+python search_sat.py 6 5 --weights 2,6              # UNSAT
+python search_sat.py 6 6                            # UNSAT (about 21 minutes)
+python search_sat.py 6 8                            # SAT, prints a word
+```
+
+Expected `verify.py` output:
+`PASS_CONNECTOR_SIX_SOURCE_SMALL_CHAR words=2 new=0 pair_checks=154 controls=4 sha256=9ab60914ac0d881d`.
+
+## Consequences and limits
+
+- In characteristics five and six, PR4248-style block concatenation cannot
+  use a depth-two block on more than five sources. It does not decide N(5)
+  or N(6): blocks
+  of depth three or more, and floor words not built from blocks, are not
+  covered.
+- The bound concerns the generic schedule of the inherited interface
+  (arbitrary dirty connector and outputs, arbitrary noncommuting maps).
+- No supplier, consumer, selected record or κ changes.
+
+## Open next questions
+
+1. **c = 7.** *Why:* it closes PR6061's question 1 and fixes the smallest
+   characteristic with a six-source depth-two block (7 or 8). *First step:*
+   cube-and-conquer on the first five or more letters with the same encoding;
+   c = 5 took 2.5 to 4 minutes and c = 6 took 21 minutes on one core, while
+   c = 7 had no verdict after about 25 minutes. *Blocked by:* solver time.
+2. **A checkable certificate for c = 5.** *Why:* the exclusion currently rests
+   on solver output. *First step:* emit DRAT for the weights {2,6}
+   sub-instance (the smallest UNSAT core found) and check it with drat-trim or
+   cake_lpr; or look for a human proof using only weight-two masks plus the
+   all-ones mask. *Blocked by:* no checker in this environment.
+3. **Depth three in characteristic five.** *Why:* with depth-two blocks capped
+   at five sources, an improvement of the c = 5 floor needs a depth-three
+   block on more than 7 sources (density above 5/2), PR6035's question 2.
+   *First step:* the same encoding with triple sums.
+
+## Credit
+
+Prepared by JosieElliston with substantial Anthropic Claude (Claude Code,
+session 50) assistance. The interface, depth notion, concatenation and the
+c = 4 obstruction are Nick Petalas's (PR4231, PR4248, PR4271, PR6035), with the
+retained Ross Richardson PR934/943 lineage. zxv's PR6057 and JosieElliston's
+PR6061 supply the c ≥ 8 six-source blocks and the open question; PR6107 supplies the weight
+identity used for pruning; apoursh's PR6071 supplies the Gray-walk family.
+Apache-2.0; no predecessor file changes.

research/connector-six-source-small-char/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/connector-depth-blocks/README.md",
+      "usage": "input",
+      "git_blob": "5d5b4a5b96e05f3818ff454d4dfdc5dc2959f6b4",
+      "sha256": "0ce59767f249b24d65d7d14b466115858d82c0bbfaaa8eab46b7406f4e975331"
+    }
+  ]
+}

research/connector-six-source-small-char/TASK.json

@@ -0,0 +1,74 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/universal-connector-boundary/README.md",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Construct and charge a legal extra operation on a minimal instance.",
+      "Prove a target-specific bound after adding one specified operation family."
+    ],
+    "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "research/universal-connector-boundary/verify.py"
+      ],
+      "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY",
+      "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.",
+    "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.",
+    "allowed_variations": [
+      "Choose one additional operation and a small source count for its first counterexample."
+    ],
+    "scope_change_triggers": [
+      "Keeping the alphabet and only increasing the source count; record this as a changed assignment.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Existence of six-source depth-two blocks of the unchanged unsigned dirty connector (PR4231/PR4248 interface) in characteristics c = 5, 6, 7. Result: none at c = 5 (local SAT, three solvers; already UNSAT on the 16 masks of weights 2 and 6) and none at c = 6 (local SAT, CaDiCaL 1.9.5 and MapleChrono); c = 7 undecided in the session.",
+  "scope_change_reason": "The alphabet stays fixed. This follows the released open question 1 of PR6061 and the open item of PR6057/#6058 (six-source depth-two blocks at c = 5, 6, 7), which bounds what PR4248-style block concatenation can do at small characteristic.",
+  "bottleneck_link": "Side result on recursive-interface capacity at small characteristic. It changes no supplier, consumer or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the c = 5 verdict with cross-solver agreement and the weight-class core, add c = 6 if a solver finishes within the session; report c = 7 as open.",
+  "outcome": "completed",
+  "evidence": "Local SAT (python-sat 1.9.dev15): k=6, c=5 UNSAT with CaDiCaL 1.9.5 (153 s), CaDiCaL 1.5.3 (197 s), Glucose 4 (237 s), and without weight pruning CaDiCaL 1.9.5 (2332 s); weights {2,6} alone UNSAT (160 s). k=6, c=6 UNSAT with CaDiCaL 1.9.5 (1263 s) and MapleChrono (2056 s). Controls k=5 c=4 UNSAT, k=5 c=5 SAT, k=6 c=8 SAT. verify.py (stdlib) checks the found words, the pruning identity on them and four controls. No DRAT proof checked.",
+  "author": "JosieElliston (Claude Code session 50)",
+  "ai_assistance": "Substantial: Anthropic Claude (Claude Code session 50) wrote the encoding, ran the solvers, wrote the verifier and README.",
+  "open_questions": [
+    {
+      "question": "Does a six-source depth-two block exist at c = 7?",
+      "why_it_matters": "Closes PR6061 question 1 and fixes the smallest characteristic with a six-source depth-two block (7 or 8).",
+      "first_step": "Cube-and-conquer on the first five or more letters with search_sat.py's encoding.",
+      "blocked_by": "Solver time: no verdict after about 25 minutes on one core."
+    },
+    {
+      "question": "Can the c = 5 exclusion be given a checkable certificate or a human proof?",
+      "why_it_matters": "It currently rests on solver output.",
+      "first_step": "Emit DRAT for the weights {2,6} sub-instance and check it with drat-trim or cake_lpr.",
+      "blocked_by": "No proof checker in this environment."
+    },
+    {
+      "question": "Is there a depth-three block on more than 7 sources at c = 5?",
+      "why_it_matters": "With depth-two blocks capped at five sources at c = 5, block concatenation can beat density 5/2 there only through depth three or more (PR6035 question 2).",
+      "first_step": "Extend the encoding to triple sums.",
+      "blocked_by": "Larger encoding."
+    }
+  ]
+}

research/connector-six-source-small-char/VERIFY.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/connector-depth-blocks/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Source pin; floor-word shape and depth two of every literal word (k=5 c=5 and k=6 c=8 controls), weight identity s+t=|m| mod c on every realizing pair (the search pruning), four rejected controls. Does not replay the local SAT exclusion."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Repeat under optimized Python; checks use explicit exceptions, not assert."
+    }
+  ]
+}

research/connector-six-source-small-char/search_sat.py

@@ -0,0 +1,119 @@
+#!/usr/bin/env python3
+"""Local SAT search for k-source depth-two blocks of the unsigned dirty connector.
+
+NOT part of the registered replay: it needs python-sat (tested with
+python-sat 1.8.dev*, CaDiCaL 1.9.5 and CaDiCaL 1.0.3 backends) and minutes of
+CPU. verify.py is the standard-library check of every word this script found.
+
+Model (PR4248 definitions, unchanged interface). A word w of length k*c calls
+each source exactly c times. q_t is the count vector of its first t calls.
+w has depth two when every nonzero binary mask m in {0,1}^k satisfies
+m == q_s + q_t (mod c) for some boundaries 0 <= s <= t <= k*c - 1. Boundary
+k*c is dropped because q_{kc} = c*1 == q_0; s = 0 is a single read.
+
+Encoding.
+  x[p][j]   position p calls source j (exactly one per p; exactly c per j).
+  e[t][j][v] q_t[j] mod c == v (one-hot), with e[0][j][0] and the transition
+             e[t+1][j][v+x] from e[t][j][v].
+  first-occurrence symmetry breaking: source j may appear only after j-1 has.
+  y[m][s][t] the pair (s, t) realizes m:  y & e[s][j][v] -> e[t][j][m_j - v].
+  each mask: OR of its y.
+Pruning (sound): by the weight identity of PR6107 (coordinate sum of q_t is
+t), a pair can realize m only if s + t == |m| (mod c); other y are omitted.
+--no-weight-prune keeps every pair (a second, larger encoding).
+--weights 2,6 restricts the masks to those weights (a relaxation: UNSAT for a
+subset of masks implies UNSAT for all masks).
+
+Usage: python search_sat.py K C [--solver cadical195] [--no-weight-prune] [--weights 2,6]
+Prints 'SAT k=.. c=.. word=...' or 'UNSAT k=.. c=..'.
+"""
+import argparse
+import itertools
+import time
+
+from pysat.card import CardEnc, EncType
+from pysat.formula import CNF, IDPool
+from pysat.solvers import Solver
+
+
+def build(k, c, weight_prune=True, weights=None):
+    L = k * c
+    pool = IDPool()
+    X = lambda p, j: pool.id(('x', p, j))
+    E = lambda t, j, v: pool.id(('e', t, j, v))
+    F = lambda p, j: pool.id(('f', p, j))
+    cnf = CNF()
+    for p in range(L):
+        lits = [X(p, j) for j in range(k)]
+        cnf.append(lits)
+        cnf.extend([[-a, -b] for a, b in itertools.combinations(lits, 2)])
+    for j in range(k):
+        enc = CardEnc.equals(lits=[X(p, j) for p in range(L)], bound=c,
+                             vpool=pool, encoding=EncType.seqcounter)
+        cnf.extend(enc.clauses)
+    for t in range(L + 1):
+        for j in range(k):
+            lits = [E(t, j, v) for v in range(c)]
+            cnf.append(lits)
+            cnf.extend([[-a, -b] for a, b in itertools.combinations(lits, 2)])
+    for j in range(k):
+        cnf.append([E(0, j, 0)])
+    for t in range(L):
+        for j in range(k):
+            for v in range(c):
+                cnf.append([-X(t, j), -E(t, j, v), E(t + 1, j, (v + 1) % c)])
+                cnf.append([X(t, j), -E(t, j, v), E(t + 1, j, v)])
+    for p in range(L):
+        for j in range(k):
+            prev = [F(p - 1, j)] if p > 0 else []
+            cnf.append([-F(p, j), X(p, j)] + prev)
+            cnf.append([F(p, j), -X(p, j)])
+            if p > 0:
+                cnf.append([F(p, j), -F(p - 1, j)])
+            if j > 0:
+                cnf.append([-X(p, j)] if p == 0 else [-X(p, j), F(p - 1, j - 1)])
+    for m in range(1, 1 << k):
+        bits = [(m >> j) & 1 for j in range(k)]
+        if weights is not None and sum(bits) not in weights:
+            continue
+        ys = []
+        for s in range(L):
+            for t in range(s, L):
+                if weight_prune and (s + t - sum(bits)) % c:
+                    continue
+                y = pool.id(('y', m, s, t))
+                ys.append(y)
+                for j in range(k):
+                    for v in range(c):
+                        cnf.append([-y, -E(s, j, v), E(t, j, (bits[j] - v) % c)])
+        cnf.append(ys)
+    return cnf, pool, X
+
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument('k', type=int)
+    ap.add_argument('c', type=int)
+    ap.add_argument('--solver', default='cadical195')
+    ap.add_argument('--no-weight-prune', action='store_true')
+    ap.add_argument('--weights', default=None)
+    a = ap.parse_args()
+    weights = None if a.weights is None else {int(x) for x in a.weights.split(',')}
+    cnf, pool, X = build(a.k, a.c, not a.no_weight_prune, weights)
+    print(f'k={a.k} c={a.c} solver={a.solver} prune={not a.no_weight_prune} '
+          f'weights={a.weights or "all"} vars={pool.top} clauses={len(cnf.clauses)}', flush=True)
+    t0 = time.time()
+    with Solver(name=a.solver, bootstrap_with=cnf.clauses) as S:
+        ok = S.solve()
+        dt = time.time() - t0
+        if ok:
+            model = {l for l in S.get_model() if l > 0}
+            word = ''.join(str(next(j for j in range(a.k) if X(p, j) in model))
+                           for p in range(a.k * a.c))
+            print(f'SAT k={a.k} c={a.c} time={dt:.1f}s word={word}', flush=True)
+        else:
+            print(f'UNSAT k={a.k} c={a.c} time={dt:.1f}s', flush=True)
+
+
+if __name__ == '__main__':
+    main()