diff --git a/research/five-source-arity-four-bound/OVERLAP.json b/research/five-source-arity-four-bound/OVERLAP.json new file mode 100644 index 000000000..6dd76bcf0 --- /dev/null +++ b/research/five-source-arity-four-bound/OVERLAP.json @@ -0,0 +1,85 @@ +{ + "task_id": "connector-alphabet-change", + "checked_on_utc": "2026-10-19", + "canonical_main_refresh": { + "command": "git fetch --no-tags https://github.com/CrocSwap/integer-mult-bounds.git main", + "commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "relevant_guidance_and_selected_record_diff_from_launch_base": "none" + }, + "offline_search": { + "command": "python3 scripts/find_overlap.py --task connector-alphabet-change --offline --cache /home/user/int-bounds-pass/20261018-luna-xhigh/overlap.json --limit 8", + "cache_report": "/home/user/int-bounds-pass/20261018-luna-xhigh/overlap-intake.json", + "cache_searched_at_utc": "2026-10-19T02:10:06Z", + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "coverage": { + "open_prs": 586, + "discussions_and_comments": 2536, + "complete_pagination": true, + "freshness_warning": "offline cache; refresh relevant live heads before submission" + }, + "possible_matches": 46, + "relevant_hits": [ + { + "number": 2249, + "title": "Research: high-arity connector toggle cost floor", + "state": "OPEN", + "head": "0c6ed7958433b2cbc0beaa331ff882aa08221a0d", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2249", + "declared_scope": "Six sources; arity-four through arity-six source calls, charged one dispatch plus each constituent source addition." + }, + { + "number": 2134, + "title": "Six-source one-TRIO path misses full paired coverage at 14 calls", + "state": "OPEN", + "head": "388a63c83cf24c3355be9798bde5a381188dadb3", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2134", + "declared_scope": "Six sources; one atomic TRIO plus thirteen singleton source calls." + }, + { + "number": 3586, + "title": "Charge one direct connector call on the one-by-one instance", + "state": "OPEN", + "head": "cde0d3c3a3be86de0c051dc1d2f270ff0f5ae2cd", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3586", + "declared_scope": "One source and one output; a direct product call is compared with the four-call B-A-B-A word." + }, + { + "number": 1930, + "title": "Construction: three-stage persistent prefix shear chain (no new kappa)", + "state": "OPEN", + "head": "11cb2266f7e99279c440a301ea4b862587a9afa2", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1930", + "declared_scope": "Changes the boundary to a target-to-source prefix chain without a dirty connector; not the arity-four source call." + } + ] + }, + "live_discussions": { + "start_here_1163": { + "updated_at_utc": "2026-10-16T02:54:20Z", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1163", + "relevant_guidance": "Claims are advisory; state object, question and bounded domain; check overlap; distinguish provisional evidence from established results." + }, + "handoffs_1166": { + "updated_at_utc": "2026-10-19T00:48:29Z", + "recent_comment_window": 100, + "recent_connector_match_count": 0, + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166", + "bounded_snapshot": "/home/user/int-bounds-pass/20261018-luna-xhigh/handoffs.json", + "decision": "No direct connector match was identified in the recent bounded snapshot or live recent-comment window. This is not a novelty certificate; older DUO/TRIO and pair-source records remain scope evidence, not current reservations." + } + }, + "live_open_pr_search": { + "query": "gh pr list --repo CrocSwap/integer-mult-bounds --state open --search connector --limit 100", + "results": [ + {"number": 3779, "title": "Record the six-window connector gate bill", "head": "14aaaff18dbb8c2860108046e051921305c32224", "updated_at_utc": "2026-10-18T20:36:35Z"}, + {"number": 2249, "title": "Research: high-arity connector toggle cost floor", "head": "0c6ed7958433b2cbc0beaa331ff882aa08221a0d", "updated_at_utc": "2026-10-15T18:21:03Z"}, + {"number": 3586, "title": "Charge one direct connector call on the one-by-one instance", "head": "cde0d3c3a3be86de0c051dc1d2f270ff0f5ae2cd", "updated_at_utc": "2026-10-18T07:03:17Z"}, + {"number": 3778, "title": "Research: exact dirty-connector cost with overlapping write windows (no kappa)", "head": "cc841651682e076fa8d4f2cec9b2055a8c91c5b1", "updated_at_utc": "2026-10-18T20:32:56Z"}, + {"number": 1930, "title": "Construction: three-stage persistent prefix shear chain (no new kappa)", "head": "11cb2266f7e99279c440a301ea4b862587a9afa2", "updated_at_utc": "2026-10-14T17:28:27Z"}, + {"number": 2134, "title": "Six-source one-TRIO path misses full paired coverage at 14 calls", "head": "388a63c83cf24c3355be9798bde5a381188dadb3", "updated_at_utc": "2026-10-15T17:59:07Z"}, + {"number": 3728, "title": "Audit the 20-prefix confinement step of the length-22 exclusion (no new kappa)", "head": "0f000bb4aac86fa667906d8092eb36e49a76944a", "updated_at_utc": "2026-10-18T18:59:07Z"} + ], + "limits": "Search is by connector text in open PR title/body, not code diff; it does not certify novelty." + } +} diff --git a/research/five-source-arity-four-bound/README.md b/research/five-source-arity-four-bound/README.md new file mode 100644 index 000000000..156317bd9 --- /dev/null +++ b/research/five-source-arity-four-bound/README.md @@ -0,0 +1,127 @@ +# Five-source arity-four connector bound + +**Scoped negative result; no supplier or kappa change.** Add one operation +family to the five-source paired-readout connector: a call + +```text +Q_r: z += sum_{j != r} B_j x_j (r in {0,1,2,3,4}) +``` + +Each `Q_r` is one dispatched connector event, and its four source-map additions +are charged individually. The original singleton `B_j` source calls and +`A_i: y_i += A_i z` readouts remain available. Sources and coefficients are +read-only, `z` is arbitrary dirty state restored at the end, outputs are +unobserved until completion, and each of the 31 nonzero output masks is +required. No new frame, copy, extra connector, direct product call or free +arithmetic is included. + +Under the explicit uniform ledger of one unit per event dispatch and one unit +per source-map or output-map addition, **every schedule that uses at least one +arity-four call costs at least 149 units**. The unchanged alphabet has exact +minimum 74 unit-price complete queries from the pinned predecessor; under this +ledger that is 148 units. Thus this charged extension cannot improve the +five-source all-mask batch. This is a bound on the stated local ledger, not on +every implementation cost model or a complete multiplication supplier. + +## Proof + +Project the source-side events of a schedule to vectors in `F_2^5`. A singleton +event has weight one; `Q_r` has vector `11111 XOR e_r`, of weight four. Let +`k=s+m` be the number of source events, where `m` is the number of `Q` events, +and let `W=s+4m=k+3m` count their constituent source-map additions. Restoration +for arbitrary dirty connector state and independent source terms forces each +source's total multiplicity to be even, so `W` is even. + +Let `P` be the set of distinct source-prefix vectors at event boundaries and +`D={p XOR q : p,q in P}`. A pair of output readouts realizes only a mask in +`D`. Every nonzero output row needs an even positive number of readouts. If a +mask is missing from `D`, its row needs at least four readouts. If `M` of the +31 nonzero masks are missing, the total output-readout count is therefore at +least `62+2M`. Since a closed `k`-event path has at most `k` distinct +prefixes, `|D \\ {0}| <= choose(k,2)`, hence +`M >= max(0,31-choose(k,2))`. + +The charged total is + +```text +C = (k dispatches + W source additions) + 2 R output-readout units + >= 124 + 2k + 3m + 4M. +``` + +The only delicate case is `m=1, k=9`. Here `W=12`, and the exact finite +census below gives `|D| <= 26`, so `M >= 6` and `C >= 169`. For `m=1` and +`k>=11`, parity gives odd `k`, so `C >= 124+2*11+3 = 149`. For `m=2`, `W` +even forces even `k`; the pair-count bound gives `k>=10`, so `C>=150`. For +`m>=3, k>=9` gives `C>=151`. For `k<=8`, `M>=31-choose(k,2)` gives `C>=155` +already at the weakest case `k=8,m=1`, with smaller `k` or larger `m` only +increasing the bound. Therefore every schedule using the new family costs +at least 149. + +For `m=1,k=9`, rotate the closed event cycle so the arity-four event is last; +this translates all prefix vectors and preserves their pairwise differences. +Relabel the five sources so that event toggles `01111`. The eight singleton +events before it must then have XOR `01111`. The verifier exhausts all 23,184 +such ordered words, computes every pairwise prefix difference, and finds a +maximum `D` size of 26 (including zero). The first maximizing word is +`01020434`; its missing nonzero masks are `01010, 01011, 10010, 10011, 11010, +11011`. Its histogram and ordered-census SHA-256 are pinned by the verifier. +A positive control checks the predecessor's twelve-singleton path and obtains +all 32 masks. + +The call's implementation charge is explicit: four constituent source-map +additions plus its own dispatch. Any routing, frame, program-storage or +additional scratch cost is outside this ledger and cannot be treated as free +in a physical caller. A fused implementation that performs fewer than four +charged additions would be a different premise. + +## Reproduce + +From the repository root: + +```sh +python3 -I -O -B research/five-source-arity-four-bound/verify.py +python3 scripts/research_package.py --package research/five-source-arity-four-bound --check-only +``` + +The first card control was also run from the pinned base: + +```sh +python3 -B research/universal-connector-boundary/verify.py +``` + +## Scope and overlap + +The broad card is refined to the five-source arity-four family. Pair-source +and trio extensions, connector frames, and the original all-singleton word +have separate retained results. Open PR [#2249](https://github.com/CrocSwap/integer-mult-bounds/pull/2249) +claims a charged arity-four-through-six floor for six sources; this result is +the five-source complement case. Open PR [#3586](https://github.com/CrocSwap/integer-mult-bounds/pull/3586) +claims a one-source/one-output direct product call, which is a different +operation boundary. These open PR claims were not independently verified here. +The contemporaneous PR and handoff overlap check is retained in +[OVERLAP.json](OVERLAP.json); it is not a novelty certificate. + +The exact selected result at the base remains the maintainer-reviewed +conditional finite construction `κ = 836330098538459/500000000000000000` +(`0.001672660197076918`), reproduced by `make frontier1094-verify`. This work +does not depend on that cold replay and did not rerun it. The selected record, +review and source manifest were inspected; their exact paths and certificate +binding are recorded in the session handoff. + +## Open next questions + +Does this family improve the complete bill for a concrete five-source caller +with nonuniform source-map and dispatch costs? The answer could change which +four-source subset is worth fusing. First bind a real caller's five source +tariffs and word-storage/dispatch costs, then enumerate only the surviving +prefix profiles. No such eligible caller or implementation contract is +identified here; without one, further tariff optimization is not justified. + +## Credit + +This scope is based on Ross Richardson's five-source universal connector +boundary (#943/#934 lineage) and Cinna Davis's six-source high-arity connector +floor (#2249). Their source claims and limits are preserved above. Prepared by +OpenAI Codex (macbook-09) with substantial AI assistance. No independent human +review, proof-assistant check, hosted CI pass, supplier admission or new kappa +is claimed. New package content is Apache-2.0. diff --git a/research/five-source-arity-four-bound/SOURCES.json b/research/five-source-arity-four-bound/SOURCES.json new file mode 100644 index 000000000..e40e4fabb --- /dev/null +++ b/research/five-source-arity-four-bound/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "input", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/universal-connector-boundary/CERTIFICATE.json", + "usage": "input", + "git_blob": "079e3e1441dc07c2f0536e9527acf290e51ea9c0", + "sha256": "e733746ba3e5151c829b4e8728bfff5ae3ed24d8d203eb77c735d20758e8266a" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "input", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + }, + { + "path": "research/universal-connector-boundary/verify.py", + "usage": "input", + "git_blob": "de6483bb7ff51940dbbb76c18f91af4c907e07da", + "sha256": "e4fa4700f9e1ae6ca09c3c76ebc569e8361b89b699425a67839d999d8812e42d" + } + ] +} diff --git a/research/five-source-arity-four-bound/TASK.json b/research/five-source-arity-four-bound/TASK.json new file mode 100644 index 000000000..243b2c830 --- /dev/null +++ b/research/five-source-arity-four-bound/TASK.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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": "refined", + "actual_scope": "For five sources and all 31 nonzero paired-readout masks, does adding the arity-four source call Q_r: z += sum_{j != r} B_j x_j lower the complete ledger when each Q_r pays one dispatch and four source-map additions?", + "scope_change_reason": "Refines the broad card to the five-source complement arity-four call, disjoint from the retained pair/trio/frame results and complementary to open PR #2249, whose high-arity floor is for six sources.", + "bottleneck_link": "docs/research/research-family-status.md: New coding, geometry and recursive boundaries / retain exploration; the result tests whether a paid connector alphabet change removes any cost in the all-mask caller.", + "budget_minutes": 60, + "stop_rule": "Stop this family at the five-source uniform charged ledger unless an actual caller supplies nonuniform source tariffs or a cheaper legal fused implementation. Do not infer a supplier or global obstruction from this local result.", + "outcome": "negative-result", + "evidence": "The original 945-pairing verifier passes. A dirty two-dimensional four-source call control passes. The exact normalized one-Q/eight-singleton branch contains 23,184 words with maximum prefix-difference set size 26/32. Pair-count and parity bounds cover all remaining event-count cases and prove every schedule using Q costs at least 149 ledger units, versus the predecessor's exact 148-unit baseline.", + "author": "OpenAI Codex (macbook-09)", + "ai_assistance": "Substantial OpenAI Codex assistance in proof design, verifier implementation, source inspection and writing. No independent human or proof-assistant review is claimed.", + "open_questions": [ + { + "question": "For an actual five-source caller with nonuniform B-map prices, can the complement arity-four family beat the complete caller bill?", + "why_it_matters": "The present bound uses one uniform unit per source-map addition and dispatch. A real caller might price source subsets differently, which could change whether this operation saves anything.", + "first_step": "Bind a concrete caller's five complete B-map prices, dispatch cost and program-storage cost, then enumerate only event profiles that survive those prices.", + "blocked_by": "No eligible five-source caller or legal implementation boundary for Q_r is identified in this checkout; further enumeration has no supplier decision to change until that contract exists." + } + ] +} diff --git a/research/five-source-arity-four-bound/VERIFY.json b/research/five-source-arity-four-bound/VERIFY.json new file mode 100644 index 000000000..e146bb869 --- /dev/null +++ b/research/five-source-arity-four-bound/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json", + "research/universal-connector-boundary/CERTIFICATE.json", + "research/universal-connector-boundary/README.md", + "research/universal-connector-boundary/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Dirty connector semantics and restoration; exact normalized one-Q/eight-singleton coverage census and histogram; cyclic/source-label symmetry controls; twelve-singleton positive coverage control" + } + ] +} diff --git a/research/five-source-arity-four-bound/verify.py b/research/five-source-arity-four-bound/verify.py new file mode 100644 index 000000000..a148e772e --- /dev/null +++ b/research/five-source-arity-four-bound/verify.py @@ -0,0 +1,168 @@ +#!/usr/bin/env python3 +"""Exact finite check for the five-source arity-four connector boundary.""" + +from hashlib import sha256 +from itertools import product + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def matvec(matrix, vector): + return tuple(sum(a * b for a, b in zip(row, vector)) % 2 for row in matrix) + + +def matmul(left, right): + return tuple( + tuple(sum(left[i][k] * right[k][j] for k in range(2)) % 2 for j in range(2)) + for i in range(2) + ) + + +def fused_four(z, matrices, sources): + out = list(z) + for matrix, source in zip(matrices, sources): + term = matvec(matrix, source) + out = [a ^ b for a, b in zip(out, term)] + return tuple(out) + + +def prefix_differences(events): + prefixes = [0] + current = 0 + for event in events: + current ^= event + prefixes.append(current) + if current != 0: + raise ValueError("source event word is not restored") + differences = {0} + for i, left in enumerate(prefixes): + for right in prefixes[:i]: + differences.add(left ^ right) + return differences + + +def tiny_dirty_control(): + # B0 and B1 do not commute; all four inputs and z are dirty. + matrices = ( + ((1, 1), (0, 1)), + ((1, 0), (1, 1)), + ((0, 1), (1, 0)), + ((1, 0), (0, 1)), + ) + sources = ((1, 0), (0, 1), (1, 1), (1, 0)) + z_in = (1, 1) + require( + matmul(matrices[0], matrices[1]) != matmul(matrices[1], matrices[0]), + "noncommuting-map control failed", + ) + z_out = fused_four(z_in, matrices, sources) + require(z_out == (0, 1), "dirty four-source output mismatch") + require(fused_four(z_out, matrices, sources) == z_in, "two calls did not restore dirty z") + require(sources == ((1, 0), (0, 1), (1, 1), (1, 0)), "source rows changed") + return z_out + + +def normalized_census(): + # By source permutation fix the four-toggle as 01111. By cyclic rotation + # of a closed event word, put that toggle last. The 8 singleton labels + # before it must XOR to 01111. This enumerates every normalized word. + quad = 0b01111 + valid = 0 + histogram = {} + records = [] + maximum = 0 + maximum_word = None + maximum_differences = None + + for word in product(range(5), repeat=8): + end = 0 + prefixes = [0] + for label in word: + end ^= 1 << label + prefixes.append(end) + if end != quad: + continue + + valid += 1 + differences = {0} + for i, left in enumerate(prefixes): + for right in prefixes[:i]: + differences.add(left ^ right) + + size = len(differences) + histogram[size] = histogram.get(size, 0) + 1 + encoded_differences = bytes(sorted(differences)) + records.append(bytes(word) + b":" + encoded_differences + b"\n") + if size > maximum: + maximum = size + maximum_word = word + maximum_differences = differences + + digest = sha256(b"".join(records)).hexdigest() + return valid, histogram, maximum, maximum_word, maximum_differences, digest + + +def symmetry_control(word, canonical_differences): + # Check all 5 choices of omitted source and all 9 cyclic rotations of the + # complete closed event cycle on a maximizing word. Label permutations + # and cycle rotations preserve the difference-set cardinality. + for omitted in range(5): + labels = [j for j in range(5) if j != omitted] + permutation = {j: labels[j] for j in range(4)} + permutation[4] = omitted + events = [1 << permutation[j] for j in word] + events.append(0b11111 ^ (1 << omitted)) + for shift in range(9): + rotated = events[shift:] + events[:shift] + differences = prefix_differences(rotated) + require( + len(differences) == len(canonical_differences), + "cyclic or label symmetry changed coverage cardinality", + ) + + +def singleton_positive_control(): + # Twelve-event all-singleton repair from the pinned predecessor. + word = (2, 0, 2, 1, 2, 0, 3, 1, 4, 2, 3, 4) + differences = prefix_differences(tuple(1 << label for label in word)) + require(len(differences) == 32, "twelve-event positive control lost masks") + return len(differences) + + +def main(): + dirty_out = tiny_dirty_control() + valid, histogram, maximum, max_word, max_differences, digest = normalized_census() + require(valid == 23184, "normalized branch size changed") + require(histogram == { + 11: 312, + 13: 2160, + 14: 2976, + 15: 576, + 16: 2832, + 19: 4464, + 21: 3984, + 22: 408, + 23: 3168, + 24: 1728, + 26: 576, + }, "coverage histogram changed") + require(maximum == 26, "maximum difference-set size changed") + require(max_word == (0, 1, 0, 2, 0, 4, 3, 4), "maximizing word changed") + require(len(max_differences) == 26, "maximum witness has wrong coverage") + symmetry_control(max_word, max_differences) + baseline_masks = singleton_positive_control() + missing = tuple(mask for mask in range(1, 32) if mask not in max_differences) + print( + "PASS_FIVE_SOURCE_ARITY4_BOUND " + f"dirty_out={dirty_out} normalized_words={valid} " + f"max_D={maximum}/32 max_word={''.join(map(str, max_word))} " + f"missing={','.join(f'{mask:05b}' for mask in missing)} " + f"baseline_D={baseline_masks}/32 sha256={digest}" + ) + + +if __name__ == "__main__": + main()