diff --git a/research/connector-trio-cycle25-seed1b82df/CERTIFICATE.json b/research/connector-trio-cycle25-seed1b82df/CERTIFICATE.json new file mode 100644 index 0000000000..ebda889cce --- /dev/null +++ b/research/connector-trio-cycle25-seed1b82df/CERTIFICATE.json @@ -0,0 +1,122 @@ +{ + "schema_version": 1, + "claim": "No normalized simple 12-vertex F2^6 path with eleven unit edges and a closing weight-three edge has all 63 nonzero pairwise differences.", + "normalization": { + "dimension": 6, + "initial_prefixes": [ + 0, + 1, + 3 + ], + "reason": "Translate q0 to 0; rotate the unique weight-three edge to closing; permute coordinates so the first two distinct unit edges are 1 and 2.", + "remaining_unit_edges": 9, + "raw_upper_bound": 1953125 + }, + "profile": { + "vertices": 12, + "unit_edges": 11, + "weight_three_closing_edges": 1, + "calls": 12, + "source_adds": 14, + "required_nonzero_differences": 63 + }, + "counts": { + "normalized_simple_walks": 1098204, + "closing_weight_three_candidates": 709812, + "coverage_histogram": { + "15": 4188, + "25": 3072, + "26": 22272, + "27": 40368, + "29": 49632, + "30": 70800, + "31": 50112, + "36": 24768, + "37": 8640, + "38": 70560, + "39": 4608, + "40": 50976, + "41": 86400, + "42": 44856, + "43": 70896, + "44": 4608, + "45": 52992, + "46": 13824, + "47": 31248, + "49": 4992 + }, + "maximum_coverage": 49, + "full_cover_witnesses": 0 + }, + "maximum_example_prefixes": [ + 0, + 1, + 3, + 7, + 6, + 14, + 15, + 31, + 29, + 61, + 57, + 41 + ], + "maximum_example_missing_masks": [ + 10, + 11, + 21, + 22, + 23, + 33, + 35, + 37, + 43, + 44, + 45, + 48, + 49, + 53 + ], + "endpoint_records_sha256": "e3035dbb174381d4ecfb35088dfdacd614b93cc14dde0f238bcbd7e509d201eb", + "positive_control_pr2128": { + "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 + ], + "calls": 14, + "source_adds": 16, + "readouts": 126, + "root_queries": 140, + "source": "CrocSwap/integer-mult-bounds PR #2128, head 697369a971eed02c0fbcd75ebefec9f59945f08e" + }, + "scope_limit": "This excludes only the stated normalized profile. It does not exclude other arities, other step-weight profiles, repeated boundary prefixes, deferred readout, or other interfaces." +} diff --git a/research/connector-trio-cycle25-seed1b82df/OVERLAP.json b/research/connector-trio-cycle25-seed1b82df/OVERLAP.json new file mode 100644 index 0000000000..87000c67ba --- /dev/null +++ b/research/connector-trio-cycle25-seed1b82df/OVERLAP.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "refreshed_utc": "2026-10-14T20:54:54Z", + "command": "python3 scripts/find_overlap.py --refresh --all-terms 'six-source' 'TRIO' '12-call' 'weight-3' --limit 20", + "coverage": { + "open_pull_requests": { + "fetched_at_utc": "2026-10-14T20:52:59Z", + "complete_pagination": true, + "records": 399 + }, + "discussions": { + "fetched_at_utc": "2026-10-14T20:54:54Z", + "complete_pagination": true, + "records": 816 + } + }, + "exact_all_terms_matches": 0, + "warnings": [], + "nearest_distinct_open_work": [ + { + "reference": "https://github.com/CrocSwap/integer-mult-bounds/pull/2128", + "head": "697369a971eed02c0fbcd75ebefec9f59945f08e", + "difference": "Uses two charged weight-two DUO calls at six sources, with (k,W)=(14,16). This census tests one charged weight-three TRIO call and the distinct (12,14) profile." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2141", + "hub_pointer": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18933826", + "claim_expiry_utc": "2026-10-14T22:45:00Z", + "status": "active" + }, + "limits": "The overlap utility searched open pull requests, discussion claims, and local task/readme records for the exact conjunction. It is not a novelty certificate and did not inspect closed code diffs or arbitrary package files." +} diff --git a/research/connector-trio-cycle25-seed1b82df/PR-BODY.md b/research/connector-trio-cycle25-seed1b82df/PR-BODY.md new file mode 100644 index 0000000000..5367aeefc9 --- /dev/null +++ b/research/connector-trio-cycle25-seed1b82df/PR-BODY.md @@ -0,0 +1,51 @@ +## Contribution + +Adds an exact scoped census for a six-source connector alphabet with one +charged three-source call. For a closed 12-call word with eleven singleton +steps and one weight-three step, no path covers all 63 nonzero pairwise +prefix differences. After symmetry normalization, the complete exact search +contains 1,098,204 simple paths and 709,812 eligible closing-edge candidates; +maximum coverage is 49, and no candidate covers 63 masks. This excludes only +the stated call and source-add profile. No supplier, recursive bound, or +`kappa` change is claimed. + +The fully charged hypothetical bill would be `138 o + 140 p`, including 126 +output readouts, versus PR #2128's `140 o + 142 p`. The TRIO call is charged +`o + 3p`, and any additional implementation surcharge must be below +`2o + 2p` for the modeled saving to survive. The complete census shows that +this profile does not realize the saving. + +## Verification + +Run: + +```sh +python3 -I -B research/connector-trio-cycle25-seed1b82df/verify.py +python3 scripts/research_package.py --package research/connector-trio-cycle25-seed1b82df --check-only +``` + +The verifier independently scans all normalized paths by a product iterator, +recomputes difference sets from scratch, checks the exact histogram and +endpoint-record digest, confirms the PR #2128 full-cover fixture, and runs +three negative controls. Direct local output under Python 3.14.7: + +```text +PASS_TRIO_CYCLE_VERIFY walks=1098204 endpoints=709812 max=49 full=0 pr2128=63/63 controls=3 +``` + +The metadata-and-source-pin check passes locally. The registered replay is +configured for Python 3.12; it was not run locally because Python 3.12 is not +installed. + +## Provenance and disclosure + +Seed `1b82dfd0673536e282d9d9e7adcb1a04`, track `recursive-interfaces`, task +`connector-alphabet-change`, priority revision 4. Exact base: +`0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. Selected record SHA-256: +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +All pins and the refined scope are in `TASK.json` and `SOURCES.json`. + +Nearest positive comparator and fixture: Aaron Wang, [PR #2128](https://github.com/CrocSwap/integer-mult-bounds/pull/2128), +head `697369a971eed02c0fbcd75ebefec9f59945f08e`. The current result uses a +different alphabet extension: exactly one charged TRIO call. Substantial +OpenAI Codex assistance was used; no independent human review is claimed. diff --git a/research/connector-trio-cycle25-seed1b82df/README.md b/research/connector-trio-cycle25-seed1b82df/README.md new file mode 100644 index 0000000000..01ad9283dd --- /dev/null +++ b/research/connector-trio-cycle25-seed1b82df/README.md @@ -0,0 +1,104 @@ +# Six-source connector with one charged TRIO call: exact scoped exclusion + +**Scoped negative result; no supplier, assembled bound, or new `kappa`.** On +the six-source connector over `F_2^6`, a closed source path with twelve calls, +eleven singleton calls, and one weight-three call cannot produce all 63 +nonzero pairwise prefix differences. The complete normalized census contains +1,098,204 simple paths; 709,812 have the required weight-three closing edge. +Their maximum coverage is 49/63, attained by 4,992 candidates, with no full +cover. This excludes only this exact call and source-add profile. + +The operation family is the universal connector's singleton source call +extended by `TRIO_{jkl}: z += B_j x_j + B_k x_k + B_l x_l`. It reads three +source rows and charges all three source additions; the rows stay read-only. +For a closed source word, the prefix states are distinct elements of `F_2^6`, +and each output mask must occur as a difference of two prefixes. The pairwise +difference test is the connector endpoint condition for arbitrary dirty +inputs. + +## Exact search and result + +There are twelve prefix vertices in a twelve-call closed word; the last call +returns from the twelfth vertex to the first. Full coverage of 63 nonzero +masks needs at least twelve distinct vertices because `binom(11,2) = 55`. +Thus twelve calls meet the counting floor. In the tested profile, the eleven +singleton edges form a simple path and the TRIO edge closes it. + +Normalize any candidate by translating its first vertex to zero, rotating the +unique TRIO edge to the closing position, and permuting coordinates so the +first two singleton edges are `1` and `2`. The vertices then start +`(0, 1, 3)`. A self-avoiding unit walk adds nine more vertices, and its last +vertex must have Hamming weight three so the closing TRIO returns to zero. +This is a complete orbit representative: simplicity forces the first two +unit edges to use distinct coordinates, and coordinate permutations act +transitively on those ordered pairs. + +[`search.py`](search.py) uses a depth-first walk and incrementally packs the +pairwise differences into an integer. [`verify.py`](verify.py) independently +enumerates all `6^9` coordinate suffixes, filters repeated vertices, and +recomputes each eligible difference set from scratch. Both exact methods +agree on the census and a SHA-256 digest over all 709,812 endpoint records. +The coverage histogram, maximal example, and exact census counts are in +[`CERTIFICATE.json`](CERTIFICATE.json). + +The maximum example has prefixes +`0, 1, 3, 7, 6, 14, 15, 31, 29, 61, 57, 41` and misses the fourteen masks +listed in the certificate. A positive control replays the 14-call, 16-source- +add witness in [PR #2128](https://github.com/CrocSwap/integer-mult-bounds/pull/2128), +which covers all 63 nonzero masks under the same pair-difference test. + +## Fully charged comparison + +Both schedules use two readouts for each of 63 outputs, so each has 126 +readouts. Let `o` be the complete cost of each root call and `p` the cost of +each source addition. The PR #2128 schedule has fourteen source calls and +sixteen source additions: `140 o + 142 p` including readouts. A hypothetical +schedule in this profile would have twelve source calls and fourteen source +additions: `138 o + 140 p`. The TRIO is charged as `o + 3p`; it is not a free +three-source operation. If an implementation adds a further TRIO surcharge +`tau`, the modeled saving survives only when `tau < 2o + 2p`. + +This profile has no full-coverage path, so that favorable completed budget +does not materialize here. Other arities, other weight profiles, mixed TRIO +and DUO paths, implementation surcharges, and supplier availability remain +open. No connector supplier is currently supplied by this experiment, so it +does not establish a recursive saving or change the selected frontier. + +## Reproduction + +From the repository root: + +```sh +python3 -I -B research/connector-trio-cycle25-seed1b82df/verify.py +python3 scripts/research_package.py --package research/connector-trio-cycle25-seed1b82df --check-only +``` + +Expected verifier output: + +```text +PASS_TRIO_CYCLE_VERIFY walks=1098204 endpoints=709812 max=49 full=0 pr2128=63/63 controls=3 +``` + +The repository's registered replay runtime is Python 3.12. The local runtime +used for this handoff is Python 3.14.7; Python 3.12 is not installed in the +research environment. + +## Open next questions + +- Does a twelve-call six-source cycle with ten singleton edges and two + charged TRIO edges attain all 63 nonzero differences? Its source-add count + is sixteen, so a witness would match PR #2128's add count while saving two + complete calls before any TRIO-specific surcharge. First step: normalize + both weight-three edges under cyclic rotation and coordinate permutation, + then enumerate only simple paths whose total XOR is zero. Stop at a full + exact census of that fixed `10×weight-1 + 2×weight-3` profile. Blocked by: + no complete covering word has been identified. + +## Attribution + +The source-call operation and pair-difference endpoint follow the universal +connector in `research/universal-connector-boundary/`. The cost comparator +and positive witness are from Aaron Wang's [PR #2128](https://github.com/CrocSwap/integer-mult-bounds/pull/2128). +Substantial OpenAI Codex assistance was used for the mathematical modeling, +search implementation, and verification. No independent human review is +claimed. diff --git a/research/connector-trio-cycle25-seed1b82df/SOURCES.json b/research/connector-trio-cycle25-seed1b82df/SOURCES.json new file mode 100644 index 0000000000..e0d8a87507 --- /dev/null +++ b/research/connector-trio-cycle25-seed1b82df/SOURCES.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "provenance", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + }, + { + "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" + } + ], + "external_references": [ + { + "name": "PR #2128 positive comparator and fixture", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2128", + "head": "697369a971eed02c0fbcd75ebefec9f59945f08e" + } + ] +} diff --git a/research/connector-trio-cycle25-seed1b82df/TASK.json b/research/connector-trio-cycle25-seed1b82df/TASK.json new file mode 100644 index 0000000000..8ed86f6936 --- /dev/null +++ b/research/connector-trio-cycle25-seed1b82df/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "track": "recursive-interfaces", + "seed": "1b82dfd0673536e282d9d9e7adcb1a04", + "selector_scope_key": "ff4f5113ed2256ab19ed", + "priority_revision": 4, + "catalogue_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "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": "For six sources over F2^6, exhaust the normalized closed 12-call source paths with eleven weight-one transitions and one charged weight-three closing TRIO; determine whether the 12 distinct prefix vertices cover all 63 nonzero pairwise differences.", + "scope_change_reason": "The selected card asks for one priced alphabet extension on a small instance. The preceding six-source result PR #2128 settles the nearby pair-source DUO schedule at (k,W)=(14,16), while its remaining (12,14) cells use a different alphabet. This contribution changes the extension to a charged three-source TRIO and tests the exact counting-floor profile (12 calls,14 source additions), a distinct full-mask cycle question.", + "bottleneck_link": "A positive path would lower the six-source connector bill from 140 o + 142 p to 138 o + 140 p before any TRIO surcharge. The exact census excludes only this profile; it creates no concrete supplier or kappa change.", + "optimistic_fully_charged_cost": "Both schedules require 126 output readouts. PR #2128 costs 140 o + 142 p including readouts. The tested profile would cost 138 o + 140 p, with the TRIO charged as o + 3p. Any extra TRIO surcharge tau must be less than 2o + 2p. No path in the tested profile exists.", + "method": "Normalize q0=0, rotate the unique weight-three edge to the closing edge, and use coordinate permutations to set q1=1,q2=3. Enumerate every simple 12-vertex unit path from that prefix whose final vertex has weight three; compute exact pairwise XOR coverage.", + "domain": "All normalized self-avoiding walks with 11 singleton edges and a closing weight-three edge on F2^6. The complete DFS has 1,098,204 simple walks, of which 709,812 have eligible closing endpoint; the independent checker scans the full 6^9 suffix product.", + "stop_rule": "Stop after the complete normalized domain is enumerated by the incremental packed-mask engine and independently reproduced by the product/set engine, including exact coverage histogram, maximum witness, positive predecessor fixture, and failure controls. Do not widen to other call or step-weight profiles in this task.", + "outcome": "negative-result", + "evidence": "Complete census: 1,098,204 normalized simple paths; 709,812 eligible closing-edge candidates; maximum coverage 49 of 63 (4,992 candidates); zero full covers. The independent set-based verifier reproduces every histogram bin and the SHA-256 digest of all endpoint records. PR #2128 positive fixture covers all 63 masks.", + "author": "OpenAI Codex research agent", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical modeling, exact search implementation, independent verification, and packaging. No independent human review is claimed.", + "open_questions": [ + { + "question": "Does a twelve-call six-source cycle with ten singleton edges and two charged TRIO edges cover all 63 nonzero differences?", + "why_it_matters": "A witness would match PR #2128 source-add count W=16 while saving two complete source calls before any additional TRIO implementation surcharge.", + "first_step": "Normalize the pair of weight-three edges under cyclic rotation and coordinate permutation, then enumerate only simple twelve-vertex cycles with total XOR zero and exact 63-mask difference coverage.", + "blocked_by": "No full-cover witness or complete normalized domain count has yet been obtained." + } + ] +} diff --git a/research/connector-trio-cycle25-seed1b82df/TASK.md b/research/connector-trio-cycle25-seed1b82df/TASK.md new file mode 100644 index 0000000000..2a4beee7c9 --- /dev/null +++ b/research/connector-trio-cycle25-seed1b82df/TASK.md @@ -0,0 +1,19 @@ +Task ID / scope key: `connector-alphabet-change` / `F2^6-full-mask-cycle-k12-W14-single-TRIO` +Track and accepted seed: `recursive-interfaces` / `1b82dfd0673536e282d9d9e7adcb1a04` +Priority revision / catalogue SHA-256: 4 / `d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7` +Exact base / selected-record SHA-256: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2` / `10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32` +Scope status: **changed** from the pair-source DUO handoff. Fix the source group to `F2^6`, use exactly twelve complete source calls with eleven singleton steps and one charged weight-three step, and require all 63 nonzero prefix differences. The new operation is `B_jkl: z += B_j x_j + B_k x_k + B_l x_l` with source rows read-only. + +Question: can a closed 12-step source path with exactly one weight-three step and eleven weight-one steps cover every nonzero mask of `F2^6` as a pairwise difference of its twelve distinct boundary prefixes? + +Predecessors / nearest work: `research/universal-connector-boundary/` proves the exact five-source boundary and provides the paired-readout interface. `research/duo-toggle-connector/` adds a fully charged weight-two DUO operation; its n=6 successor is PR #2128, head `697369a971eed02c0fbcd75ebefec9f59945f08e`, with a 14-call, 16-add universal path. Its five-source weight-three question is answered in the PR body. This cycle changes both the operation arity and the n=6 parameter domain; it seeks a 12-call path, which is the counting lower bound because 11 prefixes yield at most 55 differences. + +Optimistic complete budget: the 63 outputs require two readouts each, for 126 A calls in either schedule. PR #2128 uses 14 source calls and 16 source additions (140 total root calls). A positive path here uses 12 source calls and 14 source additions (138 root calls). With complete source-call overhead `o` and per-add cost `p`, the modeled saving is `2o + 2p`; the TRIO itself is charged `o + 3p`, never as one free addition. Any extra implementation surcharge for a three-source call must be below `2o + 2p` to retain the modeled advantage. No native supplier/controller/hosting instance currently exists, so no supplier or kappa claim is possible. + +Method / bounded domain: translate each path to a simple 12-vertex cycle in the 6-cube with eleven Hamming-distance-one edges and one closing distance-three edge. Translation and coordinate-permutation symmetries set the start and first two singleton edges to `0, 1, 3`. Enumerate every self-avoiding unit walk under that normalization (at most `5^9 = 1,953,125` paths), retain endpoints of weight three, and test the exact full difference set. A complete negative covers only this call/weight profile; a positive witness is checked against the universal connector endpoint for arbitrary dirty inputs through the paired-prefix-difference identity. + +Success evidence: exact twelve-call path and full 63-mask difference certificate, or complete census of the stated profile. Include the 12-call counting floor, direct source/add/query bill, PR #2128 benchmark, source restoration and one omitted/altered-step negative control. Stop after the complete normalized domain; do not widen to other weight profiles in this cycle. + +Claim venue: new canonical Discussion thread in the Ideas category; short pointer to #1167. Fresh overlap snapshot: 396 open PRs and 807 Discussion records, complete pagination with no warnings; exact all-term query for six-source / TRIO / 12-call / weight-three returned zero matches. + +Reproduction target: `python3 -I -B research/connector-trio-cycle25-seed1b82df/verify.py`. Substantial OpenAI Codex assistance; no independent human review claimed. diff --git a/research/connector-trio-cycle25-seed1b82df/VERIFY.json b/research/connector-trio-cycle25-seed1b82df/VERIFY.json new file mode 100644 index 0000000000..991e4111b1 --- /dev/null +++ b/research/connector-trio-cycle25-seed1b82df/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "An independent 6^9 product iterator recomputes every normalized simple walk and eligible endpoint difference set from scratch; it matches the pinned complete histogram and endpoint digest, finds maximum coverage 49 and no 63-mask cover, replays PR #2128's positive fixture, and checks three failure controls." + } + ] +} diff --git a/research/connector-trio-cycle25-seed1b82df/search.py b/research/connector-trio-cycle25-seed1b82df/search.py new file mode 100644 index 0000000000..e720b4c8b6 --- /dev/null +++ b/research/connector-trio-cycle25-seed1b82df/search.py @@ -0,0 +1,133 @@ +#!/usr/bin/env python3 +"""Exact normalized census for one weight-three closing call on F_2^6.""" + +from __future__ import annotations + +import hashlib +import json +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent +DIM = 6 +START = (0, 1, 3) +POINT_COUNT = 12 + + +def weight(x: int) -> int: + return x.bit_count() + + +def initial_cover(points: list[int]) -> int: + cover = 0 + for i, x in enumerate(points): + for y in points[i + 1 :]: + cover |= 1 << (x ^ y) + return cover + + +def main() -> dict: + points = list(START) + visited = set(points) + counts = Counter() + digest = hashlib.sha256() + max_coverage = -1 + max_prefixes = None + full_witnesses = [] + + def visit(cover: int) -> None: + nonlocal max_coverage, max_prefixes + if len(points) == POINT_COUNT: + counts["simple_walks"] += 1 + if weight(points[-1]) != 3: + return + counts["trio_endpoints"] += 1 + coverage = cover.bit_count() + counts[str(coverage)] += 1 + row = bytes(points) + cover.to_bytes(8, "big") + digest.update(row) + if coverage > max_coverage: + max_coverage = coverage + max_prefixes = points.copy() + if coverage == 63: + full_witnesses.append(points.copy()) + return + + current = points[-1] + for coordinate in range(DIM): + nxt = current ^ (1 << coordinate) + if nxt in visited: + continue + new_cover = cover + for old in points: + new_cover |= 1 << (old ^ nxt) + points.append(nxt) + visited.add(nxt) + visit(new_cover) + visited.remove(nxt) + points.pop() + + visit(initial_cover(points)) + histogram = { + str(k): counts[str(k)] + for k in range(64) + if counts[str(k)] + } + missing_at_max = sorted( + set(range(1, 64)) + - { + max_prefixes[i] ^ max_prefixes[j] + for i in range(len(max_prefixes)) + for j in range(i + 1, len(max_prefixes)) + } + ) + result = { + "schema_version": 1, + "claim": "No normalized simple 12-vertex F2^6 path with eleven unit edges and a closing weight-three edge has all 63 nonzero pairwise differences.", + "normalization": { + "dimension": DIM, + "initial_prefixes": list(START), + "reason": "Translate q0 to 0; rotate the unique weight-three edge to closing; permute coordinates so the first two distinct unit edges are 1 and 2.", + "remaining_unit_edges": 9, + "raw_upper_bound": 5**9, + }, + "profile": { + "vertices": POINT_COUNT, + "unit_edges": 11, + "weight_three_closing_edges": 1, + "calls": 12, + "source_adds": 14, + "required_nonzero_differences": 63, + }, + "counts": { + "normalized_simple_walks": counts["simple_walks"], + "closing_weight_three_candidates": counts["trio_endpoints"], + "coverage_histogram": histogram, + "maximum_coverage": max_coverage, + "full_cover_witnesses": len(full_witnesses), + }, + "maximum_example_prefixes": max_prefixes, + "maximum_example_missing_masks": missing_at_max, + "endpoint_records_sha256": digest.hexdigest(), + "positive_control_pr2128": { + "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], + "calls": 14, + "source_adds": 16, + "readouts": 126, + "root_queries": 140, + "source": "CrocSwap/integer-mult-bounds PR #2128, head 697369a971eed02c0fbcd75ebefec9f59945f08e", + }, + "scope_limit": "This excludes only the stated normalized profile. It does not exclude other arities, other step-weight profiles, repeated boundary prefixes, deferred readout, or other interfaces.", + } + (HERE / "CERTIFICATE.json").write_text(json.dumps(result, indent=2) + "\n") + print( + "PASS_TRIO_CYCLE_CENSUS " + f"walks={counts['simple_walks']} endpoints={counts['trio_endpoints']} " + f"max={max_coverage} full={len(full_witnesses)}" + ) + return result + + +if __name__ == "__main__": + main() diff --git a/research/connector-trio-cycle25-seed1b82df/verify.py b/research/connector-trio-cycle25-seed1b82df/verify.py new file mode 100644 index 0000000000..3ac2f5adb9 --- /dev/null +++ b/research/connector-trio-cycle25-seed1b82df/verify.py @@ -0,0 +1,143 @@ +#!/usr/bin/env python3 +"""Independent product-enumeration verifier for the TRIO-cycle certificate.""" + +from __future__ import annotations + +import hashlib +import itertools +import json +from collections import Counter +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def differences(points: tuple[int, ...]) -> set[int]: + # Deliberately recompute from scratch instead of sharing search.py's + # incrementally accumulated packed difference mask. + return { + points[i] ^ points[j] + for i in range(len(points)) + for j in range(i + 1, len(points)) + } + + +def enumerate_certificate() -> dict: + walks = 0 + endpoints = 0 + histogram = Counter() + maximum = -1 + maximum_prefixes = None + full = 0 + digest = hashlib.sha256() + + # With q0=0, q1=1, q2=3 fixed, each of the next nine steps has six + # coordinate choices. Reject collisions only; there is no coverage prune. + for flips in itertools.product(range(6), repeat=9): + points = [0, 1, 3] + seen = {0, 1, 3} + for coordinate in flips: + nxt = points[-1] ^ (1 << coordinate) + if nxt in seen: + break + points.append(nxt) + seen.add(nxt) + else: + walks += 1 + if points[-1].bit_count() != 3: + continue + endpoints += 1 + pts = tuple(points) + diff = differences(pts) + size = len(diff) + histogram[str(size)] += 1 + packed = sum(1 << mask for mask in diff) + digest.update(bytes(pts) + packed.to_bytes(8, "big")) + if size > maximum: + maximum = size + maximum_prefixes = list(pts) + if len(diff) == 63 and diff == set(range(1, 64)): + full += 1 + + return { + "normalized_simple_walks": walks, + "closing_weight_three_candidates": endpoints, + "coverage_histogram": dict(sorted(histogram.items(), key=lambda kv: int(kv[0]))), + "maximum_coverage": maximum, + "full_cover_witnesses": full, + "maximum_example_prefixes": maximum_prefixes, + "endpoint_records_sha256": digest.hexdigest(), + } + + +def main() -> None: + certificate = json.loads((HERE / "CERTIFICATE.json").read_text()) + observed = enumerate_certificate() + expected = { + key: certificate["counts"][key] + for key in ( + "normalized_simple_walks", + "closing_weight_three_candidates", + "coverage_histogram", + "maximum_coverage", + "full_cover_witnesses", + ) + } + expected["maximum_example_prefixes"] = certificate["maximum_example_prefixes"] + expected["maximum_example_missing_masks"] = certificate["maximum_example_missing_masks"] + expected["endpoint_records_sha256"] = certificate["endpoint_records_sha256"] + observed["maximum_example_missing_masks"] = sorted( + set(range(1, 64)) + - differences(tuple(observed["maximum_example_prefixes"])) + ) + if observed != expected: + raise SystemExit(f"certificate mismatch\nobserved={observed}\nexpected={expected}") + if observed["normalized_simple_walks"] != 1_098_204: + raise SystemExit("unexpected normalized domain size") + if observed["closing_weight_three_candidates"] != 709_812: + raise SystemExit("unexpected closing-edge candidate count") + if observed["maximum_coverage"] != 49 or observed["full_cover_witnesses"] != 0: + raise SystemExit("unexpected coverage endpoint") + + # Predecessor positive control from PR #2128: its 14 boundary prefixes + # realize all 63 nonzero masks under the same pair-difference criterion. + control = certificate["positive_control_pr2128"] + prefixes = tuple(control["prefixes"]) + steps = control["steps"] + if len(prefixes) != 14 or len(set(prefixes)) != 14: + raise SystemExit("PR #2128 control prefixes are not 14 distinct vertices") + if [prefixes[0]] + [prefixes[i - 1] ^ steps[i - 1] for i in range(1, 14)] != list(prefixes): + raise SystemExit("PR #2128 control prefix replay mismatch") + if prefixes[-1] ^ steps[-1] != prefixes[0]: + raise SystemExit("PR #2128 control does not close") + if sum(x.bit_count() for x in steps) != control["source_adds"]: + raise SystemExit("PR #2128 source-add bill mismatch") + diff = differences(prefixes) + if diff != set(range(1, 64)): + raise SystemExit("PR #2128 positive control misses a required mask") + if control["calls"] + control["readouts"] != control["root_queries"]: + raise SystemExit("PR #2128 root-query bill mismatch") + + # Negative controls: the maximal example misses masks; deleting one of + # its points cannot cover all 63 masks; a weight-one closing edge violates + # the claimed operation profile. + max_prefixes = tuple(certificate["maximum_example_prefixes"]) + max_diff = differences(max_prefixes) + if len(max_diff) != 49 or len(set(range(1, 64)) - max_diff) != 14: + raise SystemExit("maximal example negative control changed") + if len(differences(max_prefixes[:-1])) >= 63: + raise SystemExit("deleted-point negative control failed") + if (max_prefixes[-1] ^ max_prefixes[0]).bit_count() != 3: + raise SystemExit("closing-edge profile control failed") + print( + "PASS_TRIO_CYCLE_VERIFY " + f"walks={observed['normalized_simple_walks']} " + f"endpoints={observed['closing_weight_three_candidates']} " + f"max={observed['maximum_coverage']} " + f"full={observed['full_cover_witnesses']} " + "pr2128=63/63 controls=3" + ) + + +if __name__ == "__main__": + main()