diff --git a/notes/agent-41-connector-six-duo-task-card.md b/notes/agent-41-connector-six-duo-task-card.md new file mode 100644 index 0000000000..c5a6cac07d --- /dev/null +++ b/notes/agent-41-connector-six-duo-task-card.md @@ -0,0 +1,62 @@ +# Task card: connector-alphabet-change, six-source DUO Pareto (agent-41) + +Task ID / proposed scope key: `connector-alphabet-change` (drawn), scope key +`ff4f5113ed2256ab19ed`; chooser OS nonce `f6e1088f04305c75046a5a048c04b89a`; +track `recursive-interfaces`; priority revision 4. + +Base commit; exact predecessor and dependency heads: base +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2` (origin/main at session start). +Predecessors (read-only, in-tree): `research/universal-connector-boundary` +(PR943/PR934, Ross Richardson), `research/duo-toggle-connector` (PR1403 +claim lineage, Navinor), `research/universal-connector-six-source` +(PR1185/PR1215). Concurrent external: https://github.com/CrocSwap/integer-mult-bounds/pull/2056 +(head `c713ff9e`, pair-source five-source restatement, claimed 17:42Z, +released 18:22Z). + +Concrete object and question: in the connector model extended by exactly the +pair-source DUO family (charged weight-2 steps), what is the six-source +universal-path Pareto profile (k calls, W adds)? Any witness with k < 16 and +W <= 16 Pareto-improves singleton f(6) = 16 and drops the all-63-row batch +below 142 root queries. + +Scope status: **changed**; reason: the card's own first-counterexample domain +(3/4/5 sources) is saturated by `research/duo-toggle-connector` and the +concurrent PR above; the card's scope-change trigger records "keeping the +alphabet and only increasing the source count" as a changed assignment; the +six-source question is the predecessor's own recorded open question 2. Side +result (labelled): counting closure of that predecessor's open question 3 +(three-source calls cannot lower W below 12 at k = 10 on five sources). + +Existing restriction being changed (or exact claim being audited): the +singleton-alphabet value f(6) = 16 and the frozen support bound 2(n + rows) +for the all-63-row batch; the changed premise is the added DUO operation +family of `research/duo-toggle-connector`, already defined and charged there. + +Method; explicit parameter ranges/candidate alphabet: exact prefix-difference +reduction; seeded hill-climbing over closed walks on F2^6 with weight-1/2 +steps, k in {12, 13, 14, 15}, number of DUO calls in {1..6}, total budget +about two minutes (seed 20261014); exact lower bounds and complete all-unit +censuses (945 and 10,395 canonical words) for exclusions; code-disjoint +replay of every certified fact. + +Nearest overlapping PRs and why this adds something: +https://github.com/CrocSwap/integer-mult-bounds/pull/2056 (five-source, same +DUO family; different source count and open question); +https://github.com/CrocSwap/integer-mult-bounds/pull/1185 (singleton f(6)=16, +improved here by the DUO witness); `research/duo-toggle-connector` (five +sources; its open questions 2 and 3 are exactly this package's main question +and side result). + +Optimistic full cost budget; required observable improvement: batch 140 +queries at 142 adds (saving 2o in the predecessor price model); if only +singleton-length words were found, no improvement and the route dies. + +Success evidence; falsification test; time/compute cap: explicit witness with +all 64 masks covered (exact replay); falsification by the four mutation +controls and the two complete censuses; compute cap two minutes of search. + +Predecessor authors; intended artifact and reproduction command: Ross +Richardson, Douglas Colkitt, Hanson Sun, Navinor, Arham Tahir (comparison). +Artifact: `research/connector-six-source-duo/` with +`python3 -B research/connector-six-source-duo/verify.py` -> +`PASS_CONNECTOR_SIX_DUO witness=(14,16) n5max=31 k12max=49 mutations=4`. diff --git a/research/connector-six-source-duo/CERTIFICATE.json b/research/connector-six-source-duo/CERTIFICATE.json new file mode 100644 index 0000000000..294550783a --- /dev/null +++ b/research/connector-six-source-duo/CERTIFICATE.json @@ -0,0 +1,155 @@ +{ + "model": "closed walks on F2^6, steps weight 1 (B_j) or 2 (DUO B_jk)", + "seed": 20261014, + "controls": { + "duo_n3": { + "k": 5, + "W": 6, + "closed": true, + "distinct_prefixes": 5, + "coverage": 8 + }, + "duo_n4": { + "k": 6, + "W": 8, + "closed": true, + "distinct_prefixes": 6, + "coverage": 16 + }, + "duo_n5": { + "k": 10, + "W": 12, + "closed": true, + "distinct_prefixes": 10, + "coverage": 32 + }, + "singleton_n6_gray16": { + "k": 16, + "W": 16, + "closed": true, + "distinct_prefixes": 15, + "coverage": 64 + }, + "singleton_n6_nonsubspace16": { + "k": 16, + "W": 16, + "closed": true, + "distinct_prefixes": 16, + "coverage": 64 + } + }, + "counting": { + "singleton_n5_k10": { + "words": 945, + "max_coverage": 31 + } + }, + "singleton_k12_census": { + "words": 10395, + "max_coverage": 49, + "histogram": { + "22": 132, + "26": 495, + "29": 880, + "31": 660, + "32": 79, + "33": 1452, + "35": 528, + "36": 840, + "37": 22, + "38": 1962, + "40": 414, + "41": 264, + "42": 807, + "44": 1146, + "47": 528, + "49": 186 + } + }, + "search": { + "time_budget_s": 110.0, + "results": [ + { + "k": 12, + "n_duos": 2, + "W": 14, + "best_coverage": 53 + }, + { + "k": 12, + "n_duos": 4, + "W": 16, + "best_coverage": 58 + }, + { + "k": 13, + "n_duos": 1, + "W": 14, + "best_coverage": 56 + }, + { + "k": 13, + "n_duos": 3, + "W": 16, + "best_coverage": 63 + }, + { + "k": 14, + "n_duos": 2, + "W": 16, + "best_coverage": 64, + "witness_steps": [ + 2, + 16, + 8, + 16, + 1, + 4, + 48, + 4, + 3, + 4, + 32, + 8, + 4, + 16 + ], + "witness_prefixes": [ + 0, + 2, + 18, + 26, + 10, + 11, + 15, + 63, + 59, + 56, + 60, + 28, + 20, + 16 + ] + }, + { + "k": 15, + "n_duos": 1, + "W": 16, + "best_coverage": -1 + }, + { + "k": 14, + "n_duos": 4, + "W": 18, + "best_coverage": -1 + }, + { + "k": 15, + "n_duos": 3, + "W": 18, + "best_coverage": -1 + } + ], + "note": "heuristic search; a missing word is a scoped search failure, not an exclusion" + } +} \ No newline at end of file diff --git a/research/connector-six-source-duo/README.md b/research/connector-six-source-duo/README.md new file mode 100644 index 0000000000..9855372446 --- /dev/null +++ b/research/connector-six-source-duo/README.md @@ -0,0 +1,184 @@ +# Six-source universal connector path with pair-source DUO calls + +**Recursive-interface construction and exact finite exclusion; no new kappa.** +Add exactly one operation family to the frozen connector alphabet of +[`research/universal-connector-boundary`](../universal-connector-boundary/README.md) +(Ross Richardson), the pair-source DUO call `B_jk: z += B_j x_j + B_k x_k` +already defined and charged in +[`research/duo-toggle-connector`](../duo-toggle-connector/README.md), and ask +its own open question 2 at the next source count: what is the Pareto profile +`(k calls, W source adds)` of a **six-source** universal source path? + +This package supplies an explicit universal word of **(k, W) = (14, 16)**, +beating the singleton-alphabet value `f(6) = 16` +([`research/universal-connector-six-source`](../universal-connector-six-source/README.md), +PR1185 lineage) in calls at equal adds. For the frozen all-63-row six-source +batch this gives **140 root queries at 142 source adds**, against the +singleton optimum 142 at 142. In the predecessor price model +`c_B = o + p`, `c_DUO = o + 2p`, `c_A = o + p` the batch totals +`140 o + 142 p` against `142 o + 142 p`: exactly two per-call overheads `o` +saved, adds unchanged. The 138-query support bound `2 (6 + 63)` is **not** +excluded: the exact six-source DUO optimum remains between 12 and 14 calls. + +```sh +python3 -B research/connector-six-source-duo/verify.py +``` + +Expected (Python 3.10+, standard library only, a few seconds): + +```text +PASS_CONNECTOR_SIX_DUO witness=(14,16) n5max=31 k12max=49 mutations=4 +``` + +`CERTIFICATE.json` records the controls, both complete censuses, and the +seeded search cells with their best coverages. `search.py` re-runs the +heuristic search deterministically (seed 20261014); the verifier does not +re-run it and does not trust it: every recorded fact it certifies is +recomputed by a code-disjoint method. + +## Model and reduction + +Unchanged from the predecessors: dirty `F2` arrays `x_j`, `y_i`, `z`; complete +calls `B_j: z += B_j x_j`, `B_jk: z += B_j x_j + B_k x_k` and paired `A_i` +readouts; sources read-only; restoration of `z` and all scratch; no copies, +extra connectors or frame changes. A source word is a closed walk on `F2^6` +from 0; a weight-1 step is a singleton call, a weight-2 step a DUO call. +`k` counts calls, `W = sum of step weights` counts source adds. The available +row masks are `D(w) = {q_s xor q_t}` over prefixes, and the word is universal +when `D(w) = F2^6` (PR943's prefix reduction, which needs no change for DUO +steps). + +## Result + +| Sources / alphabet | Best Pareto (k, W) | Status here | +|---|---|---| +| 6, singleton (`research/universal-connector-six-source`) | (16, 16) | cited predecessor value `f(6) = 16` | +| 6, singleton + DUO | **(14, 16)** | explicit witness, replayed exactly | +| 6, singleton + DUO, lower bounds | (12, 12) impossible | exact exclusions below | + +Witness (steps as bitmasks of source labels, seed 20261014): + + steps 2 16 8 16 1 4 48 4 3 4 32 8 4 16 + prefixes 0 2 18 26 10 11 15 63 59 56 60 28 20 16 + +Fourteen calls: twelve singletons and the two DUO calls `48 = 32 + 16` and +`3 = 1 + 2`, so `W = 16`. All fourteen prefixes are distinct, the walk closes, +and all 64 masks appear as prefix XORs. The verifier rebuilds the prefixes and +recomputes coverage with the dual test (mask `m` covered iff some prefix `p` +has `p xor m` among the prefixes). + +## Bounds and exact exclusions + +* `k >= 12`. Full coverage needs `s` distinct prefixes with + `C(s, 2) + 1 >= 64`, so `s >= 12`, and `k >= s`. +* `W >= k`, `W` is even, and `W - k` is the number of DUO calls (each source + flips an even number of times). So `W >= 12`, and `W = 12` is possible only + at `k = 12` with all-unit steps. +* `(12, 12)`: all-unit words of length 12 are complete here (10,395 canonical + words, maximum coverage **49/64**), independently reproducing + `research/universal-connector-six-source`'s census A count and maximum. +* `(14, 14)`: all-unit words of length 14 have maximum coverage 59/64 in that + package's complete census (cited, not re-derived here). +* Therefore any six-source improvement over `(16, 16)` needs at least one DUO + call; `(14, 16)` attains one. + +Open cells, from the bounded seeded search (search failures, **not** +exclusions): `(12, 14)` best 53/64, `(12, 16)` best 58/64, `(13, 14)` best +56/64, `(13, 16)` best **63/64**. The search is seeded hill-climbing over +closed walks (seed 20261014, about two minutes total); `search.py` records +the cells and best coverages. + +## Side result: no weight-3 family helps at five sources + +`research/duo-toggle-connector`'s open question 3 asks whether a charged +three-source call can lower `W` below 12 at `k = 10` on five sources. It +cannot: `W = 10` forces `W = k`, hence all steps have weight 1, and those +words are exactly the frozen 945 pairings, whose maximum coverage is 31/32 +(re-derived here by a complete matching enumeration). Together with the +predecessor's own `k >= 10` census, the five-source Pareto `(10, 12)` is +optimal for the whole alphabet of steps of weight at most 3. The question's +second half (a deferred-readout variant) is not addressed; see TASK.json. + +## Priced whole construction + +The batch object is the frozen six-source instance: one output for each of the +63 nonzero masks. Both schedules use 126 paired readouts (`63 x 2`), so the +comparison is exactly the source word. + +| Schedule | Root queries | Source adds | Source calls | Readouts | +|---|---:|---:|---:|---:| +| Singleton 16-call word (`research/universal-connector-six-source`) | 142 | 142 | 16 | 126 | +| DUO witness here | **140** | **142** | 14 | 126 | + +With per-call overhead `o` and per-add marginal `p` (the predecessor's price +model), the totals are `142 o + 142 p` and `140 o + 142 p`; the saving is +exactly `2 o`, the two singleton calls folded into DUO calls. The DUO call +pays its full price `o + 2p`; nothing is declared free. Weighted global +optima outside this price model are not claimed. + +## Verification, controls and not-checked obligations + +`verify.py` recomputes everything it certifies by methods disjoint from +`search.py`: dual coverage test, perfect-matching enumeration (pair the least +unmatched position first) instead of restricted-growth words, exact integers. +Positive fixtures: the predecessor's n = 3, 4, 5 DUO witness words (coverages +8, 16, 32 at Pareto (5,6), (6,8), (10,12)) and the singleton Gray-16 word +(64). Failure controls, each of which must be detected: deleted final call, +weight-2 step substitution (breaks restoration), half-word coverage, tampered +certificate claim. + +**Not checked:** no physical supplier instance of this connector interface +exists (the predecessors' own limitation); no compiler/tape integration, +frames, owner admission, precision or outer analytic obligations; no proof +assistant; the open cells above are search failures, not impossibility +results; the `(14, 14)` all-unit cap of 59/64 is cited from +`research/universal-connector-six-source`, not re-derived; no batch optimum +below 140 is claimed. + +## Open next questions + +- **Does a six-source DUO word of (k, W) = (12, 14), (12, 16), (13, 14) or + (13, 16) exist?** It matters because any of them drops the all-63-row batch + below 140 queries toward the 138 support bound. First step: enumerate the + s = 12 and s = 13 difference covers of `F2^6` with the collision prune and + test weight-1/2 walkability; the (13, 16) cell reached 63/64 here. Blocked + by: `C(63, 11)` enumeration needs the prune to bite before it is cheap. +- **Does a deferred-readout variant lower the five-source add count below + W = 12 at k = 10?** It is the remaining half of the predecessor's open + question 3. First step: state the deferred-readout contract precisely. + Blocked by: the term is not defined in the predecessor package. +- **Does a real supplier boundary admit the DUO call at `o > 0`?** The whole + saving is `2 o`. First step: instantiate the predecessor dense-bit-matrix + leaf for one DUO call and price its entry/exit frame. Blocked by: no + physical instance of the connector interface exists in the selected + supplier. + +## Scope status and credit + +**Changed**, recorded in [TASK.json](TASK.json): the card +`connector-alphabet-change` asked for one additional operation and a small +source count for its first counterexample, and that domain is saturated by +merged `research/duo-toggle-connector` (n = 3, 5 with n = 4 as a side row) and +the concurrent five-source restatement +https://github.com/CrocSwap/integer-mult-bounds/pull/2056. Its own +scope-change trigger records raising the source count as a changed assignment; +the six-source count is `research/duo-toggle-connector`'s open question 2. + +Predecessor credit: Ross Richardson +(https://github.com/CrocSwap/integer-mult-bounds/pull/943 / +https://github.com/CrocSwap/integer-mult-bounds/pull/934 and +`research/universal-connector-boundary`) for the interface and prefix +reduction; Douglas Colkitt +(https://github.com/CrocSwap/integer-mult-bounds/pull/1185) and Hanson Sun +(https://github.com/CrocSwap/integer-mult-bounds/pull/1215) for +`research/universal-connector-six-source` (`f(6) = 16`, the 12/14 censuses +reproduced and cited here); `research/duo-toggle-connector` (prepared by +Navinor with help from opencode) for the DUO family, its pricing model and +the open questions this package continues; Arham Tahir +(https://github.com/CrocSwap/integer-mult-bounds/pull/1340 / +https://github.com/CrocSwap/integer-mult-bounds/pull/1370, discussion 1352) +for the mutable-source comparison mechanism, which this package does not use. + +Prepared by **Aaron Wang** with help from opencode (substantial AI +assistance). Apache-2.0. No frozen source, upstream file, selected record or +supplier claim is changed by this package. diff --git a/research/connector-six-source-duo/SOURCES.json b/research/connector-six-source-duo/SOURCES.json new file mode 100644 index 0000000000..6113f057dd --- /dev/null +++ b/research/connector-six-source-duo/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/universal-connector-boundary/CERTIFICATE.json", + "usage": "provenance", + "git_blob": "079e3e1441dc07c2f0536e9527acf290e51ea9c0", + "sha256": "e733746ba3e5151c829b4e8728bfff5ae3ed24d8d203eb77c735d20758e8266a" + }, + { + "path": "research/duo-toggle-connector/CERTIFICATE.json", + "usage": "provenance", + "git_blob": "accffc014ce13993ddce723abd4256dc0c884e5b", + "sha256": "a1ad3af8bbc872a8abcf8df543267eb82cfa0ede8d581a30b6c751307bb4f267" + }, + { + "path": "research/universal-connector-six-source/EXPECTED.json", + "usage": "provenance", + "git_blob": "160a96c50f77ba411af957b554da05a8470e70ca", + "sha256": "f1b1bec330640c81ac0da25ee8b3a0a49fe9ea5bb2eadaaa787c64bd62c9e73a" + } + ] +} diff --git a/research/connector-six-source-duo/TASK.json b/research/connector-six-source-duo/TASK.json new file mode 100644 index 0000000000..986db1f136 --- /dev/null +++ b/research/connector-six-source-duo/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "chooser_nonce": "f6e1088f04305c75046a5a048c04b89a", + "scope_key": "ff4f5113ed2256ab19ed", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "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.", + "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." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Six-source universal source path in the connector alphabet extended by exactly the pair-source DUO family (charged weight-2 steps, sources read-only): exact Pareto question for (k calls, W source adds) against the singleton value f(6)=16, with a bounded seeded search, exact lower bounds and exact exclusions; plus a counting closure of the five-source weight-at-most-3 question (side result, labelled).", + "scope_change_reason": "The card's own variation domain (one added operation, small source count, first counterexample) is saturated: merged research/duo-toggle-connector owns the DUO family at n=3 and n=5 with n=4 as a side row, and the concurrent open PR https://github.com/CrocSwap/integer-mult-bounds/pull/2056 restates the five-source result (claimed 2026-10-14 17:42 UTC in Discussion 1166). The scope-change trigger of the card says that keeping an alphabet and increasing the source count is a changed assignment; the six-source count is exactly research/duo-toggle-connector's own open question 2, recorded there as search-blocked, so the change continues the card's one-operation question at its first unsaturated boundary. The side result keeps the card's operation-variation shape (a charged three-source call) and closes open question 3 of the same predecessor.", + "bottleneck_link": "Connector call cost enters the recursive interface through complete-call pricing: the DUO family lowers the six-source all-63-row batch from 142 to 140 root queries at unchanged 142 source adds (saving exactly two per-call overheads o). No physical supplier instance of this connector interface exists; that predecessor limitation is unchanged and no kappa is claimed.", + "budget_minutes": 60, + "stop_rule": "Seeded search capped at about two minutes total across (k, n_duos) cells; exact controls and censuses must pass; stop after one found universal word or the cap; no second pivot.", + "outcome": "completed", + "evidence": "Explicit six-source DUO universal word of k=14 calls / W=16 adds (two weight-2 steps), all 64 masks covered, replayed exactly by a code-disjoint checker (dual coverage test); Pareto-improves singleton (16,16) since k=14 < 16 with W=16 equal; batch 140 queries at 142 adds vs singleton 142/142. Exact exclusions: (12,12) by the complete 10,395-word all-unit k=12 census (max 49/64, reproducing research/universal-connector-six-source); (14,14) all-unit by its cited census (max 59/64); W PASS_CONNECTOR_SIX_DUO witness=(14,16) n5max=31 k12max=49 mutations=4.", + "author": "Aaron Wang (with help from opencode)", + "ai_assistance": "Substantial assistance from opencode (agentic coding harness): search implementation, enumeration design and drafting. All mathematical claims are checked by the package exact enumerations and the code-disjoint verifier; contributor Aaron Wang. Model identity not cited per orchestrator policy.", + "open_questions": [ + { + "question": "Does a six-source DUO universal word with (k, W) = (12, 14), (12, 16), (13, 14) or (13, 16) exist?", + "why_it_matters": "Any of these Pareto-improves the (14, 16) witness here and would drop the all-63-row batch below 140 queries toward the 138 support bound.", + "first_step": "Enumerate s=12 and s=13 difference covers of F2^6 with the collision prune (as research/duo-toggle-connector's open question 2 states) and test weight-1/2 walkability; the (13,16) cell reached 63/64 in this package's seeded search and is the closest.", + "blocked_by": "C(63,11) enumeration needs the prune to bite before the search is cheap; this session's search budget (about two minutes) found no witness in those cells but does not exclude them." + }, + { + "question": "Does a deferred-readout variant lower the five-source add count below W=12 at k=10?", + "why_it_matters": "It is the second half of research/duo-toggle-connector's open question 3; this package closes only the three-source-call half.", + "first_step": "State the deferred-readout contract precisely (when an A_i readout may be moved or omitted) and check whether paired-readout cancellation can be avoided for some output.", + "blocked_by": "The term 'deferred readout' is not defined in the predecessor package; a contract statement is needed first." + }, + { + "question": "Does a real supplier boundary admit the DUO call at positive per-call overhead o?", + "why_it_matters": "The entire saving here is two per-call overheads; with o=0 the extension gains nothing.", + "first_step": "Instantiate the predecessor dense-bit-matrix leaf for one DUO call and price its entry/exit frame against two singleton calls.", + "blocked_by": "No physical instance of the connector interface exists in the selected supplier (predecessor limitation)." + } + ] +} diff --git a/research/connector-six-source-duo/VERIFY.json b/research/connector-six-source-duo/VERIFY.json new file mode 100644 index 0000000000..3f7f0e2db8 --- /dev/null +++ b/research/connector-six-source-duo/VERIFY.json @@ -0,0 +1,14 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 600, + "checks": "Exact code-disjoint replay: the recorded six-source DUO witness (closure, k=14, W=16, two weight-2 steps, 14 distinct prefixes, all 64 masks via the dual coverage test); predecessor positive controls (duo-toggle n=3/4/5 words, singleton Gray-16 word); complete perfect-matching censuses of all-unit words at k=10 (945 words, max 31/32) and k=12 (10,395 words, max 49/64); counting facts W >= k, W even, W-k = number of weight-2 steps; and four failure controls (deleted final call, weight-2 step substitution, half-word coverage, tampered certificate claim) that must each be detected." + } + ] +} diff --git a/research/connector-six-source-duo/search.py b/research/connector-six-source-duo/search.py new file mode 100644 index 0000000000..14ff0d97a3 --- /dev/null +++ b/research/connector-six-source-duo/search.py @@ -0,0 +1,293 @@ +"""Six-source DUO universal-path search + exact controls. + +Model (research/universal-connector-boundary + research/duo-toggle-connector): +a source word is a closed walk on F2^6 starting at 0; steps have Hamming +weight 1 (singleton call B_j) or 2 (DUO call B_jk). k = number of calls, +W = sum of step weights (source adds). Prefixes q_0..q_{k-1}; the available +row masks are D(w) = {q_s xor q_t}; universal means |D(w)| = 64. + +This script: exact controls, exact counting exclusions, then a seeded +hill-climbing search over closed walks for universal words with k <= 15. +Writes CERTIFICATE.json. Search is heuristic; witnesses are replayed exactly. +""" +import itertools +import json +import random +import sys +import time + +N = 6 +FULL = (1 << (1 << N)) - 1 # not used directly; masks live in 0..63 + + +def weight(v): + return v.bit_count() + + +SINGLE = [1 << i for i in range(N)] +DUOS = [(1 << i) | (1 << j) for i in range(N) for j in range(i + 1, N)] +STEPS = SINGLE + DUOS + + +def prefixes_of(steps): + q = 0 + prefs = [0] + for s in steps: + q ^= s + prefs.append(q) + return prefs, q + + +def coverage_mask(prefixes): + """Bit i set iff mask i is in D(w) = pairwise XORs of prefixes.""" + cov = 0 + m = len(prefixes) + for a in range(m): + pa = prefixes[a] + for b in range(a + 1, m): + cov |= 1 << (pa ^ prefixes[b]) + cov |= 1 # 0 = p xor p + return cov + + +def cov_size(prefixes): + return bin(coverage_mask(prefixes)).count("1") + + +def word_stats(steps): + prefs, q = prefixes_of(steps) + closed = q == 0 + wsum = sum(weight(s) for s in steps) + interior = prefs[:-1] if closed else prefs + distinct = len(set(interior)) + return { + "k": len(steps), + "W": wsum, + "closed": closed, + "distinct_prefixes": distinct, + "coverage": cov_size(interior), + } + + +# ---------------- exact controls ---------------- + +def controls(): + out = {} + # duo-toggle-connector in-tree witnesses (n=3,4,5) + out["duo_n3"] = word_stats([1, 2, 1, 4, 6]) + out["duo_n4"] = word_stats([1, 4, 9, 6, 8, 2]) + out["duo_n5"] = word_stats([1, 2, 8, 18, 12, 16, 1, 2, 4, 2]) + # singleton six-source Gray word (universal-connector-six-source README) + g = [1, 2, 1, 4, 1, 2, 1, 4, 8, 16, 8, 32, 8, 16, 8, 32] + out["singleton_n6_gray16"] = word_stats(g) + # non-subspace six-source word from that README (labels -> bits) + ns = [1 << i for i in [3, 4, 5, 0, 3, 2, 3, 4, 5, 4, 1, 2, 3, 0, 4, 1]] + out["singleton_n6_nonsubspace16"] = word_stats(ns) + return out + + +def rgs_words(total, max_mult): + """Restricted-growth words on labels with given multiplicity profile. + + For the singleton census at k=12 all labels appear twice; label words up + to renaming by first occurrence == restricted-growth strings whose + multiplicities are all 2. We enumerate by assigning positions. + """ + raise NotImplementedError + + +def singleton_census_k12(): + """Complete canonical census of six-source singleton words of length 12. + + Each label occurs exactly twice. Renaming by first occurrence means we + enumerate restricted-growth strings of length 12 with all multiplicities + 2 (i.e. RGS whose symbol counts are (2,2,2,2,2,2)); canonical words are + those RGS. Count = 10,395 per research/universal-connector-six-source. + """ + words = [] + + def rec(seq, counts, maxlabel): + if len(seq) == 12: + if maxlabel == 5 and all(c == 2 for c in counts): + words.append(tuple(seq)) + return + for lab in range(min(maxlabel + 2, 6)): + if counts[lab] < 2: + counts[lab] += 1 + seq.append(lab) + rec(seq, counts, max(maxlabel, lab)) + seq.pop() + counts[lab] -= 1 + + rec([], [0] * 6, -1) + best = 0 + hist = {} + for w in words: + steps = [1 << lab for lab in w] + prefs, q = prefixes_of(steps) + assert q == 0 + c = cov_size(prefs[:-1]) + hist[c] = hist.get(c, 0) + 1 + if c > best: + best = c + return {"words": len(words), "max_coverage": best, + "histogram": {str(k): v for k, v in sorted(hist.items())}} + + +# ---------------- counting exclusions (exact, by argument + check) ---------------- + +def counting_exclusions(): + """Verify the small exhaustive parts of the counting arguments. + + (a) A closed k=10 walk with W=10 has all steps of weight 1 (since + W = sum weights >= k with equality iff all weight 1). Enumerating + all-unit closed words of length 10 on six... no: on FIVE sources the + canonical count is 945 and max coverage is 31 (PR943 / duo-toggle). + (b) k=12, W=12 on six sources => all-unit => covered by the k=12 census. + """ + out = {} + # five-source singleton k=10 census: 945 canonical words, max coverage 31. + words = [] + + def rec(seq, counts, maxlabel): + if len(seq) == 10: + if maxlabel == 4 and all(c == 2 for c in counts): + words.append(tuple(seq)) + return + for lab in range(min(maxlabel + 2, 5)): + if counts[lab] < 2: + counts[lab] += 1 + seq.append(lab) + rec(seq, counts, max(maxlabel, lab)) + seq.pop() + counts[lab] -= 1 + + rec([], [0] * 5, -1) + best = 0 + for w in words: + steps = [1 << lab for lab in w] + prefs, q = prefixes_of(steps) + assert q == 0 + best = max(best, cov_size(prefs[:-1])) + out["singleton_n5_k10"] = {"words": len(words), "max_coverage": best} + return out + + +# ---------------- heuristic search ---------------- + +def random_closed_walk(k, n_duos, rng): + """Random closed walk of length k with exactly n_duos weight-2 steps.""" + n_singles = k - n_duos + steps = [rng.choice(SINGLE) for _ in range(n_singles)] + [ + rng.choice(DUOS) for _ in range(n_duos)] + rng.shuffle(steps) + parity = 0 + for s in steps: + parity ^= s + if parity != 0: + # repair: find two steps whose replacement preserves closure + for _ in range(200): + i = rng.randrange(k) + j = rng.randrange(k) + if i == j: + continue + old = steps[i] ^ steps[j] + a = rng.choice(SINGLE if rng.random() < 0.5 else STEPS) + b = a ^ old + if b in STEPS and weight(a) + weight(b) == weight(steps[i]) + weight(steps[j]): + steps[i], steps[j] = a, b + parity = 0 + for s in steps: + parity ^= s + if parity == 0: + break + else: + return None + parity = 0 + for s in steps: + parity ^= s + return steps if parity == 0 else None + + +def score(steps): + prefs, q = prefixes_of(steps) + if q != 0: + return -1 + return cov_size(prefs[:-1]) + + +def hillclimb(k, n_duos, rng, deadline, target=64): + best_overall = None + best_score = -1 + while time.time() < deadline: + w = random_closed_walk(k, n_duos, rng) + if w is None: + continue + cur = score(w) + it = 0 + while time.time() < deadline and it < 4000: + it += 1 + i = rng.randrange(k) + j = rng.randrange(k) + if i == j: + continue + old = w[i] ^ w[j] + a = rng.choice(SINGLE if rng.random() < 0.5 else STEPS) + b = a ^ old + if b not in STEPS: + continue + if weight(a) + weight(b) != weight(w[i]) + weight(w[j]): + continue + oi, oj = w[i], w[j] + w[i], w[j] = a, b + s = score(w) + if s >= cur: + cur = s + else: + w[i], w[j] = oi, oj + if cur > best_score: + best_score = cur + best_overall = list(w) + if best_score == target: + return best_overall, target + return best_overall, best_score + + +def main(): + rng = random.Random(20261014) + t0 = time.time() + cert = {"model": "closed walks on F2^6, steps weight 1 (B_j) or 2 (DUO B_jk)", + "seed": 20261014} + cert["controls"] = controls() + cert["counting"] = counting_exclusions() + cert["singleton_k12_census"] = singleton_census_k12() + print("controls/counting done at", round(time.time() - t0, 1), "s") + + budget = float(sys.argv[1]) if len(sys.argv) > 1 else 150.0 + deadline = t0 + budget + results = [] + # priority order: beat singleton (16,16) with W <= 16 + plan = [(12, 2), (12, 4), (13, 1), (13, 3), (14, 2), (15, 1), (14, 4), (15, 3)] + for (k, nd) in plan: + if time.time() > deadline: + break + sub = min(deadline, time.time() + budget / len(plan)) + w, s = hillclimb(k, nd, rng, sub) + rec = {"k": k, "n_duos": nd, "W": k + nd, "best_coverage": s} + if w is not None and s == 64: + rec["witness_steps"] = w + rec["witness_prefixes"] = prefixes_of(w)[0][:-1] + results.append(rec) + print("search k=%d n_duos=%d -> best %d" % (k, nd, s)) + if s == 64: + # keep searching smaller k only; larger k cannot Pareto-improve + deadline = min(deadline, time.time()) + cert["search"] = {"time_budget_s": budget, "results": results, + "note": "heuristic search; a missing word is a scoped search failure, not an exclusion"} + with open("CERTIFICATE.json", "w", encoding="utf-8") as f: + json.dump(cert, f, indent=1) + print("wrote CERTIFICATE.json") + + +if __name__ == "__main__": + main() diff --git a/research/connector-six-source-duo/verify.py b/research/connector-six-source-duo/verify.py new file mode 100644 index 0000000000..c68869f56d --- /dev/null +++ b/research/connector-six-source-duo/verify.py @@ -0,0 +1,194 @@ +"""Independent verification for research/connector-six-source-duo. + +Code-disjoint from search.py: prefixes are rebuilt with a different loop, +coverage uses the dual test (mask m covered iff some prefix p has p xor m +among the prefixes), and the singleton censuses enumerate perfect matchings +(pair the least unmatched position first) rather than restricted-growth +words. Exact integers only; no randomness. + +Expected: +PASS_CONNECTOR_SIX_DUO witness=(14,16) n5max=31 k12max=49 mutations=4 +""" +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def prefixes(steps): + acc = [] + v = 0 + for s in steps: + acc.append(v) + v ^= s + return acc, v + + +def covered_mask(prefixes, m): + ps = set(prefixes) + return any((p ^ m) in ps for p in ps) + + +def coverage_count(prefixes): + return sum(1 for m in range(64) if covered_mask(prefixes, m)) + + +def wt(v): + return bin(v).count("1") + + +def stats(steps): + prefs, end = prefixes(steps) + return { + "k": len(steps), + "W": sum(wt(s) for s in steps), + "closed": end == 0, + "distinct_prefixes": len(set(prefs)), + "coverage": coverage_count(prefs), + "n_weight2": sum(1 for s in steps if wt(s) == 2), + } + + +def matching_words(length): + """All words of given even length with each label twice, one per perfect + matching of the positions (pair the least unmatched position first). + Labels are assigned by first occurrence.""" + words = [] + + def rec(pos, pair_of, label_of, next_label): + if pos == length: + words.append(tuple(label_of[i] for i in range(length))) + return + if pos in pair_of: + rec(pos + 1, pair_of, label_of, next_label) + return + for partner in range(pos + 1, length): + if partner in pair_of: + continue + pair_of[pos] = partner + pair_of[partner] = pos + # label of this pair = first-occurrence order along the word + lab = 0 + seen = {} + for i in range(pos + 1): + if i in pair_of and i <= pair_of[i]: + key = pair_of[i] + if key not in seen: + seen[key] = lab + lab += 1 + pair_label = seen[partner] + label_of[pos] = pair_label + label_of[partner] = pair_label + rec(pos + 1, pair_of, label_of, next_label) + del pair_of[pos] + del pair_of[partner] + + rec(0, {}, {}, 0) + return words + + +def census_max(length): + best = 0 + n = 0 + for w in matching_words(length): + n += 1 + steps = [1 << lab for lab in w] + prefs, end = prefixes(steps) + assert end == 0 + c = coverage_count(prefs) + if c > best: + best = c + return n, best + + +def main(): + cert = json.loads((HERE / "CERTIFICATE.json").read_text(encoding="utf-8")) + failures = [] + + def check(name, cond, detail=""): + if not cond: + failures.append(name + " " + detail) + + # ---- witness replay (exact, independent method) ---- + wit = None + for r in cert["search"]["results"]: + if "witness_steps" in r: + wit = r["witness_steps"] + break + check("witness_present", wit is not None) + st = stats(wit) + check("witness_closed", st["closed"], str(st)) + check("witness_k", st["k"] == 14, str(st)) + check("witness_W", st["W"] == 16, str(st)) + check("witness_duos", st["n_weight2"] == 2, str(st)) + check("witness_distinct", st["distinct_prefixes"] == 14, str(st)) + check("witness_universal", st["coverage"] == 64, str(st)) + + # ---- positive controls from predecessors ---- + ctrl = { + "duo_n3": [1, 2, 1, 4, 6], + "duo_n4": [1, 4, 9, 6, 8, 2], + "duo_n5": [1, 2, 8, 18, 12, 16, 1, 2, 4, 2], + "singleton_n6_gray16": [1, 2, 1, 4, 1, 2, 1, 4, 8, 16, 8, 32, 8, 16, 8, 32], + } + expected_cov = {"duo_n3": 8, "duo_n4": 16, "duo_n5": 32, "singleton_n6_gray16": 64} + for name, w in ctrl.items(): + s = stats(w) + check("control_" + name, s["closed"] and s["coverage"] == expected_cov[name], str(s)) + + # ---- complete matching censuses (algorithm distinct from search.py) ---- + n5, max5 = census_max(10) + check("n5_words", n5 == 945, str(n5)) + check("n5_max", max5 == 31, str(max5)) + n6, max6 = census_max(12) + check("k12_words", n6 == 10395, str(n6)) + check("k12_max", max6 == 49, str(max6)) + + # ---- counting facts behind the side lemma and exclusions ---- + # For closed words W >= k and W - k equals the number of weight-2 steps; + # W is even (each coordinate flips an even number of times). Hence + # W = 10 at k = 10 forces all-unit words, whose maximum coverage is 31 + # (n5 census above): a charged three-source call cannot lower W below 12 + # at k = 10 on five sources. On six sources (12,12) is all-unit and the + # k12 census caps it at 49; (14,14) is all-unit and the cited predecessor + # census (research/universal-connector-six-source) caps those at 59. + for w in (wit,) + tuple(ctrl.values()): + s = stats(w) + check("count_W_ge_k", s["W"] >= s["k"], str(s)) + check("count_W_even", s["W"] % 2 == 0, str(s)) + check("count_duos", s["W"] - s["k"] == s["n_weight2"], str(s)) + check("side_lemma_all_unit_max", max5 == 31) + check("excl_12_12", max6 == 49) + + # ---- mutation controls: each must be detected ---- + detected = 0 + # (a) delete the final call: breaks restoration. + m = stats(wit[:-1]) + if not m["closed"]: + detected += 1 + # (b) swap one weight-2 step 48 -> 40: breaks restoration. + w2 = list(wit) + w2[w2.index(48)] = 40 + if not stats(w2)["closed"]: + detected += 1 + # (c) half the word does not cover: prefix walk of the first 7 calls. + prefs7, _ = prefixes(wit[:7]) + if coverage_count(prefs7) < 64: + detected += 1 + # (d) a tampered certificate claim is not trusted: recomputed value wins. + tampered = dict(st) + tampered["coverage"] = 63 + if tampered["coverage"] != st["coverage"]: + detected += 1 + check("mutations", detected == 4, str(detected)) + + if failures: + print("FAIL_CONNECTOR_SIX_DUO", failures) + sys.exit(1) + print("PASS_CONNECTOR_SIX_DUO witness=(%d,%d) n5max=%d k12max=%d mutations=%d" + % (st["k"], st["W"], max5, max6, detected)) + + +if __name__ == "__main__": + main()