From a746ad748e2c22cef81ef9aa88ac78e4c3ce3487 Mon Sep 17 00:00:00 2001 From: NeoKazuya <2886350+NeoKazuya@users.noreply.github.com> Date: Mon, 12 Oct 2026 22:31:00 -0700 Subject: [PATCH 1/4] Research: prove a scoped target-pair borrowing obstruction --- .../complex-packet-borrowing23/CLAIM.json | 37 ++ .../complex-packet-borrowing23/EXPECTED.json | 83 ++++ research/complex-packet-borrowing23/NOTICE.md | 16 + research/complex-packet-borrowing23/README.md | 180 ++++++++ .../complex-packet-borrowing23/SEARCH-LOG.md | 82 ++++ .../SOURCE-PINS.json | 10 + research/complex-packet-borrowing23/verify.py | 404 ++++++++++++++++++ 7 files changed, 812 insertions(+) create mode 100644 research/complex-packet-borrowing23/CLAIM.json create mode 100644 research/complex-packet-borrowing23/EXPECTED.json create mode 100644 research/complex-packet-borrowing23/NOTICE.md create mode 100644 research/complex-packet-borrowing23/README.md create mode 100644 research/complex-packet-borrowing23/SEARCH-LOG.md create mode 100644 research/complex-packet-borrowing23/SOURCE-PINS.json create mode 100644 research/complex-packet-borrowing23/verify.py diff --git a/research/complex-packet-borrowing23/CLAIM.json b/research/complex-packet-borrowing23/CLAIM.json new file mode 100644 index 0000000000..25b4d9e988 --- /dev/null +++ b/research/complex-packet-borrowing23/CLAIM.json @@ -0,0 +1,37 @@ +{ + "assignment_seed": 23, + "assignment_draw_utc": "2026-10-13T04:39:09.0462877Z", + "draw": "OS cryptographic byte; reject values >=200; reduce modulo 100", + "track": "complex supplier", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "salt": "23|made, shell, arm, script, fix, tape", + "salt_sha256": "e743f055badcf6eca828bbaca72994eb06af4ceda579a0a90535e982cb386d12", + "selection_rule": "minimum SHA-256(salt + '|' + candidate_id)", + "candidates": [ + { + "id": "coordinate-center-reduction-tree", + "question": "Can a binary reduction tree for the seven factory totals of one complex coordinate center reduce the paid recursive profile once all donor paths and restoration are included?", + "method": "Exact subset dynamic programming over all seven-leaf binary trees, derive legal join frames from the selected construction, price every changed register path, and reconstruct a witness if any candidate improves the baseline.", + "selection_hash": "f62753569c1aa8ce9cb1e3bde2722d7c8f647eaa8f35640c7ffbe8582d18f4ef" + }, + { + "id": "two-helper-terminal-basis", + "question": "Can a joint dyadic basis change on two coframed complex helpers expose a lower terminal frame unavailable to either helper independently?", + "method": "Enumerate compatible helper pairs in seed order; solve the exact two-column exterior-response cancellation; price both basis changes, restoration and resulting residual widths, then replay a winning word.", + "selection_hash": "bb5870f429ca4a3b3bda86e4306c6d96d8f42308c7ea6b6f626bff2882265f08" + }, + { + "id": "cross-factory-packet-sharing", + "question": "Can two complex factories sharing a coordinate pair replace duplicated delivery packets with one transported linear combination while preserving arbitrary dirty inputs?", + "method": "Select a factory intersection in seed order; derive the joint response map and a reversible dyadic factorization; include source access, join frames, target writes, both cleanups and residual widths before accepting a gain.", + "selection_hash": "4b4a15b22f161c542dc51cd6f53426f79541d3f39e838c398b24370e53afbd16" + } + ], + "selected": "cross-factory-packet-sharing", + "coordination": "GitHub pinnedIssues returned an empty list at orientation; claim is recorded locally. No separate reservation issue is opened.", + "proof_bar": "A strict improvement requires a complete paid profile and exact arbitrary-dirt/frame verification; otherwise report only an exhaustively checked scoped obstruction or measured search coverage, with no new kappa claim.", + "selected_object": "Pair (6,7), sign +1; six all-K leavers, with scope extended to all eight signed all-K cells", + "result": "Scoped obstruction for arbitrary repeated operations on one target pair; exact finite checks and a fully priced two-carrier three-source escape. No new kappa.", + "expected_finish_utc": "2026-10-13T05:40:00Z", + "scope_record_updated_utc": "2026-10-13T05:27:04Z" +} diff --git a/research/complex-packet-borrowing23/EXPECTED.json b/research/complex-packet-borrowing23/EXPECTED.json new file mode 100644 index 0000000000..9411dc16b4 --- /dev/null +++ b/research/complex-packet-borrowing23/EXPECTED.json @@ -0,0 +1,83 @@ +{ + "schema": "complex-packet-borrowing23/1", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 23, + "salt_sha256": "e743f055badcf6eca828bbaca72994eb06af4ceda579a0a90535e982cb386d12", + "selected": [ + [ + 6, + 7 + ], + 1 + ], + "formed_candidate_count": 52, + "raw492_content_sha256": "a78f4e2114212d2f4b567cc9ef4e3b31ace0c19983009cec562a642831a84c34", + "geometry": { + "signed_cells": 8, + "leaver_target_bindings": 48, + "exact_join_supports": 504, + "shared_support_clock_certificates": 3600, + "geometry_sha256": "a804597bbd53ef07609f18287e701bac803eea4c105fd6813cec9d35935dd351" + }, + "chronology": { + "orders_examined": 120, + "orders_meeting_four_required_precedences": 16, + "surviving_orders": 0, + "contradiction_branches": { + "C_before_D_forbids_B": 8, + "D_before_C_forbids_A": 8 + } + }, + "scalar_and_paid_controls": { + "permutations_examined": 720, + "arbitrary_input_scalar_passes": 120, + "scalar_and_strict_frame_passes": 0, + "false_passes_when_source_pollution_is_omitted": 60, + "missing_required_entry_control": { + "ok": true, + "profile": { + "1": 4, + "2": 3, + "5": 2, + "6": 3, + "7": 1 + }, + "rank_mass": 45 + }, + "two_carrier_escape": { + "ok": true, + "profile": { + "1": 6, + "2": 5, + "5": 3, + "6": 3, + "7": 2 + }, + "rank_mass": 63, + "columns_each_orientation": 8, + "scalar_additions_including_precondition_compensation_cleanup": 14, + "all_dirty_helpers_restored": true + }, + "matched_stock_direct_control": { + "ok": true, + "profile": { + "1": 6, + "2": 3, + "5": 3, + "6": 3, + "9": 2 + }, + "rank_mass": 63 + }, + "escape_minus_direct_profile": { + "2": 2, + "7": 2, + "9": -2 + }, + "dirty_input_mutations_rejected": { + "omit_h0_cleanup": true, + "omit_h1_compensation": true, + "double_shared_target_read": true + } + } +} diff --git a/research/complex-packet-borrowing23/NOTICE.md b/research/complex-packet-borrowing23/NOTICE.md new file mode 100644 index 0000000000..641b4db632 --- /dev/null +++ b/research/complex-packet-borrowing23/NOTICE.md @@ -0,0 +1,16 @@ +# Attribution and license + +Prepared by NeoKazuya with substantial OpenAI Codex assistance, using +GPT-6-Astra. New code and text are contributed under Apache-2.0. + +The checked packet construction is icekylinx's #531 factory and its +#425/#433 ancestry, extended by Jeremy Kothe/AtomScout's #622 K-triangle +constructor. The selected #626 package is Chafik Boukhalfa's owner repair; +eumemic's #543 bit supplier and the cumulative community dependencies retain +their existing attribution. No authorship of those constructions is claimed. + +Sreekanth Nair/higherbeing's #651 and Douglas Colkitt's #683 supplied the +related scope comparisons. They are not dependencies of the chronology proof. +The unchanged constructor and its data are read in place, with hashes recorded +in SOURCE-PINS.json. Their original notices and licenses remain in their +respective packages. diff --git a/research/complex-packet-borrowing23/README.md b/research/complex-packet-borrowing23/README.md new file mode 100644 index 0000000000..88ecd323ac --- /dev/null +++ b/research/complex-packet-borrowing23/README.md @@ -0,0 +1,180 @@ +# A frame obstruction to borrowing one pair of complex targets + +**Scoped negative result; no new κ.** In the six-leaver all-K packet cell, +using one pair of targets to share source-dependent partial sums cannot +replace the raw reads when the source values stay fixed and there are no +additional carriers. The obstruction allows arbitrary own-read order, +repeated pair interactions, signed coefficients and cancellation. It is +caused by the frames carried by reads, not by a failed circuit search. + +An explicit two-carrier circuit escapes the obstruction in its three-source +projection. Helpers are restored on arbitrary dirty inputs, but its paid profile is worse +than the direct circuit on the same stock. This comparison concerns that +control circuit, not every possible two-carrier construction. + +## Reproduce + +From the repository root, with Python 3.11 or later and no third-party packages: + +```sh +python3 -B research/complex-packet-borrowing23/verify.py +``` + +Expected first line: + +```text +PASS_COMPLEX_PACKET_PAIR_BORROWING_OBSTRUCTION_AND_PAID_ESCAPE +``` + +The command checks the source pins, rebuilds the unmodified raw 492-helper +constructor with assertions enabled, and checks eight signed all-K cells. +It enumerates 504 nonempty leaver joins and binds 3,600 possible shared +supports to the chronology obstruction. A separate rational scalar/frame +replay examines all 720 orders of a six-event three-source example. +Of these, 120 have the required arbitrary-input scalar map and none has +legal frames. Omitting source-frame propagation incorrectly accepts 60. + +The finite enumeration checks the example and the ordering certificate. +The proof below supplies the statement about arbitrarily many interactions +within one target pair; it is not inferred from a bounded search. + +## The selected cell + +The OS assignment seed was **23**, assigning the complex-supplier track. +The secondary string was `23|made, shell, arm, script, fix, tape`. +Three independently specified mechanisms were ranked by SHA-256; the +cross-factory packet-sharing experiment was selected. Hash ordering of the +52 formed pair/sign cases selected **pair (6,7), sign +1**. The base is +`66849e1475c930fd7732b1a0067ffee7e1e95f60`. + +The cell has two leavers from each of the factories `(0,1,6,7)`, +`(2,3,6,7)` and `(4,5,6,7)`. Normalize the six target labels so that target +`Y_i` omits source `X_i`. For each source, its rank-two initial frame is +`E_i`; target `Y_i` has a rank-eight cap `H_i`. Exact XOR-span enumeration +checks + +```text +E_i is contained in H_j if and only if i != j. +``` + +The required local source-to-target increment has a zero diagonal and +nonzero entries everywhere else. The coefficient signs need not agree for +the proof. All eight signed all-K cells have the same incidence pattern. +The checker derives their roles and coefficients from the pinned constructor, +then checks the subspaces independently by explicit XOR closure. + +## Proposition and proof + +Let there be `n >= 3` sources and targets with +`E_i` contained in `H_j` exactly when `i != j`, as above. Consider any finite +linear circuit with these conditions: + +1. The `X_i` values are independent source variables and are not modified. + A source frame can grow when the source is read. +2. Targets start with independent arbitrary values at frame zero. Each + target must acquire a nonzero coefficient of every other source. +3. Every two-register operation lifts both registers to a common frame + containing their previous frames. Frames never shrink, and target `Y_i` + must stay inside `H_i`. +4. Apart from source reads `X_i -> Y_j`, operations may rescale targets or + mix the targets of one unordered pair `{a,b}`. There are no additional + carriers. Other target-to-target operations are allowed only as + source-free preconditioning at frame zero. + +Then the pair cannot interact after either target has accessed a source. +This excludes a shared partial sum and a two-target basis-change circuit, +including repeated interactions interleaved with source reads. + +Suppose otherwise. Let `T` be the last interaction of the pair. Since an +earlier interaction followed source access, at `T` both target frames +contain some `E_k`. Necessarily `k` differs from `a` and `b`, since the +common frame must fit both target caps. + +`Y_b` still requires `X_a`. Its paired target `Y_a` can never read `X_a`, +and no other target can supply it under condition 4. Thus a direct read +`A: X_a -> Y_b` is required. It must occur **after T**: an earlier read +would put `E_a` into the common frame at `T`, violating `Y_a`'s cap. +Likewise a direct read `B: X_b -> Y_a` must occur after `T`. + +At `A`, source `X_a` acquires `E_k` from `Y_b`. It cannot subsequently +be read by `Y_k`. Hence the required direct read `C: X_a -> Y_k` occurs +before `A`. Similarly `D: X_b -> Y_k` occurs before `B`. + +If `C` precedes `D`, the read at `D` puts `E_a` into the frame of `X_b`. +That forbids its later required read `B` into `Y_a`. If `D` precedes `C`, +the read at `C` puts `E_b` into `X_a`, forbidding its later read `A` into +`Y_b`. Both strict orders are impossible. + +Cancellation, rescaling and repeated reads cannot remove a frame already +acquired. Earlier reads or extra frame promotions only add restrictions. +The five-event checker explicitly examines all 120 strict orders; 16 satisfy +the four required precedences, and the two contradictions reject eight each. + +## A paid escape and controls + +Use three sources and targets, where `Y_i` needs the other two sources. +Introduce dirty helpers `H0,H1`. At frame zero, apply + +```text +Y1 -= Y0; Y0 -= H1; Y1 += H1; Y1 -= H0. +``` + +Then run these operations at the joins of their current frames: + +```text +H0 += X0; H1 += X1; +Y0 += X2; Y1 += Y0; +Y0 += H1; Y1 += H0; +Y2 += X0; Y2 += X1. +``` + +Climb every source and helper to the full nine-dimensional frame and each +target to its own cap. Restore `H1 -= X1; H0 -= X0` at the full frame. +Exact rational replay checks all eight arbitrary input columns in both +forward and inverse-transpose orientations. The helpers retain their original +dirty values. Omitting cleanup or compensation, or doubling the shared read, +is rejected. + +The escape's profile is `6 H1 + 5 H2 + 3 H5 + 3 H6 + 2 H7`. +A direct six-read circuit with the same two helpers left idle has profile +`6 H1 + 3 H2 + 3 H5 + 3 H6 + 2 H9`. Both have rank mass 63. Their difference is + +```text +2 H2 + 2 H7 - 2 H9. +``` + +For the recursive moment `sum_r H_r r^s`, every `0 < s < 1` gives a strict +loss: `2^s + 7^s > 9^s`. Thus the added carriers are not free in this control. +This is a local comparison with fixed stock and unchanged surrounding work; +it does not assert a new globally hosted supplier or an outer exponent. + +A second positive control drops one required off-diagonal entry. It admits +the formerly blocked target broadcast, showing why the all-but-one demand +is part of the proposition rather than a dispensable assumption. + +## Relation to prior work and limits + +[PR #651](https://github.com/CrocSwap/integer-mult-bounds/pull/651) studies +raw-face sharing and target hosting with an own-first +restriction. This argument permits own-read movement and repeated coded +operations on one target pair. +[PR #683](https://github.com/CrocSwap/integer-mult-bounds/pull/683) studies mixed K/M bypass with pure +carriers; this package concerns all-K cells and a target-pair mechanism. +Neither those broader titles nor the present proposition establishes a +barrier for arbitrary network coding. + +The proposition does not cover additional carriers, mutable source values, +source-dependent coupling through three or more targets, register lifetime +resets, different decoder demands, or different geometry. Exploratory +six-source searches with broader target coupling and one or two coded helpers +timed out; those runs establish no impossibility result. The two-carrier +control does not establish a minimum carrier count or an optimal circuit. + +The [local claim](CLAIM.json) records the draw and candidate selection. +[SEARCH-LOG.md](SEARCH-LOG.md) records exploratory domains and stopping rules; +those searches are not dependencies of the proof or checker. +The [source pins](SOURCE-PINS.json), [exact finite evidence](EXPECTED.json) and +[attribution](NOTICE.md) accompany this note. +No selected certificate, existing supplier or `upstream/` source is changed. +All inherited all-size, physical realization and analytic assumptions remain. +This is not a complete formal proof of integer multiplication. diff --git a/research/complex-packet-borrowing23/SEARCH-LOG.md b/research/complex-packet-borrowing23/SEARCH-LOG.md new file mode 100644 index 0000000000..708a233ee5 --- /dev/null +++ b/research/complex-packet-borrowing23/SEARCH-LOG.md @@ -0,0 +1,82 @@ +# Discovery record + +These exploratory searches guided the choice of a provable local statement. +They do not certify the proposition. The submitted, standard-library checker +independently verifies its geometric premises, five-event order contradiction, +six-event example and paid controls. No solver is required to reproduce those +results. The exploratory search scripts are not part of this package. + +## Assignment and domain + +OS assignment seed: **23**, complex supplier. The recorded salt and three +candidate mechanisms are in `CLAIM.json`. SHA-256 ordering selected +cross-factory packet sharing, then pair `(6,7)`, sign `+1`, among 52 formed +pair/sign cases. The source pins identify the unmodified raw K492 constructor. + +The discovery model had six read-only sources and six targets. Each target +needed the five sources outside its forbidden singleton. Sources started at +their rank-two leaver frames; targets started at zero, with rank-eight caps. +Every read propagated the frame join to **both** participants. Sources ended +at rank nine. Positive signal supports were disjoint when added: no signed +cancellation or repeated coefficient was allowed. Target dirt compensation +was deferred to a later exact replay if a candidate survived. Thus this was +an optimistic discovery model, not an admitted physical supplier. + +## Heuristic runs + +The random generator seed for both heuristics was the integer represented by +SHA-256 of `23|made, shell, arm, script, fix, tape|target-shared-decoder`: + +```text +47441944177751120186235842501409826922933133093583107006176514245677426449285 +``` + +- Beam searches stopped after the 30 delivered-coefficient layers, with at + most six target-to-target additions. Width 600 expanded 13,220 states; + width 900 with a necessary reachability filter expanded 15,804 states. + Neither retained a completed circuit. State truncation makes both searches + incomplete, including as searches for the already known direct circuit. +- A separate mutation run started from a legal direct 30-read schedule and + attempted 18,000 seeded move/swap mutations. It accepted 3,493 legal moves + and tested opportunities to replace later source reads by one available + target sum. No shared candidate was found. The best complete local profile + remained `48 H1 + 12 H2 + 6 H3`. This is neither an exhaustive neighborhood + certificate nor a global cost claim. + +## Bounded solver runs + +Z3 5.1.0, random seed 23, checked a bit-vector encoding of the positive model. +At least one nonempty target-to-target read was required. For `n` sources, +there were at most `n(n-1)` active additions, with trailing no-ops permitted. +This bound covers positive disjoint-support additions in the no-helper model, +since each addition supplies at least one of the `n(n-1)` required entries. +The first shared edge and one shared signal were fixed by simultaneous +source/omitted-target relabeling. + +| Sources | Frames enforced | Outcome | Recorded elapsed time | +| --- | --- | --- | --- | +| 3 | yes | UNSAT | 0.029 s | +| 4 | yes | UNSAT | 4.506 s | +| 5 | yes | unknown, 20 s timeout | 20.075 s | +| 6 | yes | unknown, 55 s timeout | 55.199 s | +| 6 | no | SAT | 0.234 s | + +The small UNSAT results were diagnostic only; no independent solver proof +certificate is claimed. The missing-frame SAT run showed why source and +target frame propagation needed a separate test. + +Two extensions allowed one helper with 28 additions or two helpers with 26. +Helpers could read sources and other helpers, while targets could also read +targets; helpers could not read targets. At least one helper had to combine +sources from different two-leaver factories. Helper cleanup and target dirt +compensation were omitted from these optimistic feasibility models. Both +Z3 runs returned unknown at 55 seconds. CVC5 1.4.2 independently parsed the +same exported formulas; both runs also returned unknown at 55 seconds. +These helper bounds do not cover all possible coded circuits. + +No result about general multi-target coding, signed circuits or helper +optimality follows from these searches. The final proof instead fixes one +unordered target pair and allows arbitrarily many signed linear operations +and arbitrary read order. The two-helper control in the checker uses a +three-source projection and includes the compensation, cleanup and final +climbs absent from the discovery models. diff --git a/research/complex-packet-borrowing23/SOURCE-PINS.json b/research/complex-packet-borrowing23/SOURCE-PINS.json new file mode 100644 index 0000000000..fc2e5c0dcc --- /dev/null +++ b/research/complex-packet-borrowing23/SOURCE-PINS.json @@ -0,0 +1,10 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "sha256": { + "research/complex-k492-owner-repair/code/construct_k_triangle.py": "66fc460df8eb8067efe3d8a3f9e97a7244aacd7bf11650a6ce656e868ce053da", + "research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json": "327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f", + "research/direct-delivery504-global/inputs/hamming/PACKET-PROGRAMS.json.gz": "d833ae0390d165d7da0c639a3c7aeb77156c2ddb52447087cb49b9d03b19e9b9", + "research/complex-k492-owner-repair/data/TRI-SCHEDULE.json": "94da9d5575f5b237097a77ac7dd09aff594322dd9c35138bfd34ffc5e1a7a51e", + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + } +} diff --git a/research/complex-packet-borrowing23/verify.py b/research/complex-packet-borrowing23/verify.py new file mode 100644 index 0000000000..03fa9f8888 --- /dev/null +++ b/research/complex-packet-borrowing23/verify.py @@ -0,0 +1,404 @@ +"""Exact geometry, chronology and dirty-input checks for pair-target borrowing. + +Apache-2.0. NeoKazuya, with substantial OpenAI Codex assistance. +The symbolic argument is in README.md; the finite replays have narrower scopes. +""" +from __future__ import annotations + +import argparse +import contextlib +import gzip +import hashlib +import io +import itertools +import json +import os +from pathlib import Path +import runpy +import subprocess +import sys +import tempfile +from collections import Counter +from fractions import Fraction + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +CONSTRUCTOR = "research/complex-k492-owner-repair/code/construct_k_triangle.py" +INPUTS = "research/direct-delivery504-global/inputs/hamming" +SCHEDULE = "research/complex-k492-owner-repair/data/TRI-SCHEDULE.json" +ASSIGNMENT_SEED = 23 +SALT = "23|made, shell, arm, script, fix, tape" + + +class VerificationError(Exception): + pass + + +def require(condition, message): + if not condition: + raise VerificationError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def span(vectors): + """Explicit XOR closure, independent of the constructor's row reduction.""" + result = {0} + for vector in vectors: + result |= {x ^ vector for x in result} + return frozenset(result) + + +def rank(space): + size = len(space) + require(size > 0 and size & (size - 1) == 0, "not a binary subspace size") + return size.bit_length() - 1 + + +def join(left, right): + return frozenset(a ^ b for a in left for b in right) + + +def cap(port): + return frozenset(x for x in range(512) if (x & port).bit_count() % 2 == 0) + + +def selection_hash(value): + text = SALT + "|" + json.dumps(value, separators=(",", ":")) + return hashlib.sha256(text.encode()).hexdigest() + + +def geometry_worker(destination): + """Execute the pinned, unchanged constructor with its assertions enabled.""" + require(__debug__, "constructor worker requires assertions") + output = destination.parent / "raw492" + old_argv = sys.argv[:] + try: + sys.argv = [str(ROOT / CONSTRUCTOR), str(ROOT / INPUTS), str(output), str(ROOT / SCHEDULE)] + with contextlib.redirect_stdout(io.StringIO()): + ns = runpy.run_path(str(ROOT / CONSTRUCTOR)) + finally: + sys.argv = old_argv + require(ns["NH"] == 492, "unexpected selected raw helper count") + cases = [] + # Full coordinate pairs are the all-K cells, not the mixed K/M family. + for pair in ns["TRI"]["full_pairs"]: + pair = tuple(pair) + for sign in (-1, 1): + blocks = sorted(c for c in ns["blocks"] if set(pair) <= set(c)) + require(len(blocks) == 3, "coordinate pair does not have three factories") + leavers, targets = [], [] + alphas = {} + for block in blocks: + module = ns["blocks"][block] + event_index, alpha = ns["face_info"](block, pair, sign) + alphas[block] = alpha + for local in module["events"][event_index][:2]: + previous = max(j for j in range(event_index) if local in module["events"][j][:2]) + register = ns["maps"][block][local] + leavers.append({ + "block": list(block), "local_register": local, + "raw120_register": register, + "frame": module["event_frames"][previous], + }) + for target, coefficient in ns["requests"][(block, pair, sign)]: + own, own_coefficient, own_frame = ns["own_rows"][target] + targets.append({ + "root_index": target, "port112_index": target - 8, + "port": ns["P"][target], "block": list(block), + "own_register": own, "own_frame": list(own_frame), + "own_coefficient": str(own_coefficient), + "request_coefficient": str(coefficient), + }) + require(len(leavers) == len(targets) == 6, "not a six-leaver cell") + # Normalize target i as the target whose cap excludes source i. + normalized = [] + for source in leavers: + outside = [t for t in targets if not span(source["frame"]) <= cap(t["port"])] + require(len(outside) == 1, "source does not have one forbidden target") + normalized.append(outside[0]) + require(len({t["root_index"] for t in normalized}) == 6, "forbidden targets are not a bijection") + coefficients = [] + for target in normalized: + row = [] + for source in leavers: + if source["block"] == target["block"]: + q = Fraction(target["own_coefficient"]) if source["raw120_register"] == target["own_register"] else Fraction(0) + else: + q = Fraction(target["request_coefficient"]) * alphas[tuple(source["block"])] + row.append(str(q)) + coefficients.append(row) + cases.append({"pair": list(pair), "sign": sign, "leavers": leavers, + "targets": normalized, "coefficients": coefficients}) + # The within-track draw considered all 52 formed faces, including mixed cells. + formed = [[list(p), sign] for p in itertools.combinations(range(8), 2) + for sign in (-1, 1) if (p, sign) not in ns["FULLT"]] + selected = min(formed, key=selection_hash) + require(selected == [[6, 7], 1], "seed-selected object changed") + result = {"selected": selected, "formed_candidate_count": len(formed), "cases": cases, + "raw492_content_sha256": hashlib.sha256(gzip.decompress((output / "FULL-WORD.json.gz").read_bytes())).hexdigest(), + "raw492_profile": ns["report"]["local_profile"]} + destination.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8") + + +def validate_geometry(geometry): + prototype = json.loads((ROOT / INPUTS / "PROTOTYPE.json").read_bytes()) + cases = geometry["cases"] + require(len(cases) == 8, "expected eight signed all-K cells") + source_count = support_count = clock_certificates = 0 + for case in cases: + sources = [span(s["frame"]) for s in case["leavers"]] + targets = [cap(t["port"]) for t in case["targets"]] + require(all(rank(s) == 2 for s in sources), "leaver frame is not rank two") + require(all(rank(h) == 8 for h in targets), "target cap is not rank eight") + require(rank(frozenset.intersection(*sources)) == 1, "leavers do not share one line") + for i, target in enumerate(case["targets"]): + require(target["port"] == prototype["binary_ports"][target["root_index"]], "target port differs from pinned input") + require(target["port112_index"] == target["root_index"] - 8, "112-port restriction mismatch") + for j, source in enumerate(sources): + require((source <= targets[i]) == (i != j), "all-but-one incidence failed") + require((Fraction(case["coefficients"][i][j]) != 0) == (i != j), "required scalar coefficient is missing") + source_count += 1 + for mask in range(1, 64): + space = span(x for i, source in enumerate(case["leavers"]) if mask >> i & 1 for x in source["frame"]) + require(rank(space) == mask.bit_count() + 1, "unexpected leaver join rank") + allowed = [i for i, target in enumerate(targets) if space <= target] + require(allowed == [i for i in range(6) if not mask >> i & 1], "coded support/cap incidence failed") + support_count += 1 + for a, b in itertools.permutations(range(6), 2): + remaining = [k for k in range(6) if k not in (a, b)] + for support in range(1, 1 << len(remaining)): + shared = [remaining[i] for i in range(len(remaining)) if support >> i & 1] + k = min(shared) + require(sources[k] <= targets[a] and sources[k] <= targets[b], "shared witness is not admissible at pair contact") + require(not sources[a] <= targets[a] and not sources[b] <= targets[b] + and not sources[k] <= targets[k], "chronology witness has no forbidden cap") + clock_certificates += 1 + return {"signed_cells": len(cases), "leaver_target_bindings": source_count, + "exact_join_supports": support_count, "shared_support_clock_certificates": clock_certificates, + "geometry_sha256": digest(geometry)} + + +def chronology_check(): + """Independent finite check of the five-event order contradiction. + + T is the last pair contact, A = Xa->Yb, B = Xb->Ya, + C = Xa->Yk and D = Xb->Yk. README derives these requirements. + """ + prefix_admissible = surviving = 0 + branches = Counter() + for order in itertools.permutations("TABCD"): + at = {name: order.index(name) for name in order} + if not (at["T"] < at["A"] and at["T"] < at["B"] + and at["C"] < at["A"] and at["D"] < at["B"]): + continue + prefix_admissible += 1 + if at["C"] < at["D"]: + branches["C_before_D_forbids_B"] += 1 + surviving += at["B"] < at["D"] + else: + branches["D_before_C_forbids_A"] += 1 + surviving += at["A"] < at["C"] + require(surviving == 0 and prefix_admissible > 0 and len(branches) == 2, + "chronology obstruction failed or is vacuous") + return {"orders_examined": 120, "orders_meeting_four_required_precedences": prefix_admissible, + "surviving_orders": surviving, "contradiction_branches": dict(sorted(branches.items()))} + + +def scalar_matrix(registers, operations, backward=False): + size = len(registers) + index = {name: i for i, name in enumerate(registers)} + rows = [[Fraction(i == j) for j in range(size)] for i in range(size)] + for target, source, coefficient in operations: + t, s, q = index[target], index[source], Fraction(coefficient) + if backward: + t, s, q = s, t, -q + rows[t] = [a + q * b for a, b in zip(rows[t], rows[s])] + return rows + + +def expected_matrix(registers, missing=None, backward=False): + rows = scalar_matrix(registers, []) + index = {name: i for i, name in enumerate(registers)} + for i in range(3): + for j in range(3): + if i != j and (i, j) != missing: + t, s = index[f"y{i}"], index[f"x{j}"] + if backward: + t, s = s, t + rows[t][s] = Fraction(-1 if backward else 1) + return rows + + +def framed_replay(registers, core, source_spaces, target_caps, *, ignore_source_pollution=False): + """Replay actual ambient F_2^9 frames, then charge every final climb.""" + zero = frozenset({0}) + full = frozenset(range(512)) + current = {r: source_spaces[int(r[1:])] if r.startswith("x") else zero for r in registers} + final = {r: target_caps[int(r[1:])] if r.startswith("y") else full for r in registers} + profile = Counter() + for step, (target, source, _) in enumerate(core): + frame = join(current[target], current[source]) + for r in (target, source): + if not frame <= final[r]: + return {"ok": False, "step": step, "register": r} + for r in (target, source): + if ignore_source_pollution and r.startswith("x"): + continue + delta = rank(frame) - rank(current[r]) + if delta: + profile[delta] += 1 + current[r] = frame + for r in registers: + require(current[r] <= final[r], "final frame is not reachable") + delta = rank(final[r]) - rank(current[r]) + if delta: + profile[delta] += 1 + return {"ok": True, "profile": {str(k): v for k, v in sorted(profile.items())}, + "rank_mass": sum(k*v for k, v in profile.items())} + + +def scalar_and_escape_checks(selected): + source_spaces = [span(s["frame"]) for s in selected["leavers"][:3]] + target_caps = [cap(t["port"]) for t in selected["targets"][:3]] + basic_registers = ["x0", "x1", "x2", "y0", "y1", "y2"] + # A source-free zero-frame precondition is allowed; it removes target dirt + # introduced by the useful later y0->y1 broadcast. + precondition = [("y1", "y0", -1)] + events = [("y0", "x2", 1), ("y1", "y0", 1), ("y0", "x1", 1), + ("y1", "x0", 1), ("y2", "x0", 1), ("y2", "x1", 1)] + scalar_ok = strict_ok = relaxed_ok = 0 + for order in itertools.permutations(range(6)): + ops = [events[i] for i in order] + if scalar_matrix(basic_registers, precondition + ops) != expected_matrix(basic_registers): + continue + scalar_ok += 1 + strict_ok += framed_replay(basic_registers, precondition + ops, source_spaces, target_caps)["ok"] + relaxed_ok += framed_replay(basic_registers, precondition + ops, source_spaces, target_caps, + ignore_source_pollution=True)["ok"] + require(scalar_ok > 0 and strict_ok == 0 and relaxed_ok > 0, + "six-event enumeration or source-pollution negative control failed") + + # Dropping one required off-diagonal entry removes the contradiction. + missing_core = [events[i] for i in (0, 1, 4, 2, 3)] + require(scalar_matrix(basic_registers, precondition + missing_core) + == expected_matrix(basic_registers, missing=(2, 1)), "missing-entry scalar control") + missing_replay = framed_replay(basic_registers, precondition + missing_core, source_spaces, target_caps) + require(missing_replay["ok"], "missing-entry frame control") + + registers = ["x0", "x1", "x2", "h0", "h1", "y0", "y1", "y2"] + compensation = [("y1", "y0", -1), ("y0", "h1", -1), + ("y1", "h1", 1), ("y1", "h0", -1)] + escape_core = [("h0", "x0", 1), ("h1", "x1", 1), ("y0", "x2", 1), + ("y1", "y0", 1), ("y0", "h1", 1), ("y1", "h0", 1), + ("y2", "x0", 1), ("y2", "x1", 1)] + cleanup = [("h1", "x1", -1), ("h0", "x0", -1)] + whole = compensation + escape_core + cleanup + for backward in (False, True): + require(scalar_matrix(registers, whole, backward) == expected_matrix(registers, backward=backward), + "two-carrier arbitrary-dirt scalar replay failed") + escape = framed_replay(registers, compensation + escape_core, source_spaces, target_caps) + require(escape["ok"], "two-carrier frame replay failed") + # Cleanup runs after the charged final climbs and touches only full-frame + # sources/helpers. It therefore incurs no unrecorded frame transitions. + require(all(not r.startswith("y") for e in cleanup for r in e[:2]), "cleanup touches a target") + + direct = [("y0", "x1", 1), ("y1", "x2", 1), ("y2", "x0", 1), + ("y0", "x2", 1), ("y1", "x0", 1), ("y2", "x1", 1)] + require(scalar_matrix(registers, direct) == expected_matrix(registers), "direct dirty-input scalar control") + baseline = framed_replay(registers, direct, source_spaces, target_caps) + require(baseline["ok"], "direct frame control") + delta = Counter({int(k): v for k, v in escape["profile"].items()}) + delta.subtract({int(k): v for k, v in baseline["profile"].items()}) + delta = {str(k): v for k, v in sorted(delta.items()) if v} + require(delta == {"2": 2, "7": 2, "9": -2}, "paid escape difference changed") + # 2^s+7^s>9^s follows for every 0 Date: Mon, 12 Oct 2026 22:32:07 -0700 Subject: [PATCH 2/4] Record the completed research claim and review link --- research/complex-packet-borrowing23/CLAIM.json | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/research/complex-packet-borrowing23/CLAIM.json b/research/complex-packet-borrowing23/CLAIM.json index 25b4d9e988..ffd8373b39 100644 --- a/research/complex-packet-borrowing23/CLAIM.json +++ b/research/complex-packet-borrowing23/CLAIM.json @@ -33,5 +33,8 @@ "selected_object": "Pair (6,7), sign +1; six all-K leavers, with scope extended to all eight signed all-K cells", "result": "Scoped obstruction for arbitrary repeated operations on one target pair; exact finite checks and a fully priced two-carrier three-source escape. No new kappa.", "expected_finish_utc": "2026-10-13T05:40:00Z", - "scope_record_updated_utc": "2026-10-13T05:27:04Z" + "scope_record_updated_utc": "2026-10-13T05:27:04Z", + "status": "submitted", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/781", + "submitted_utc": "2026-10-13T05:34:00Z" } From 16edc23247c20cd074e5ac502f6b0e723bf53c66 Mon Sep 17 00:00:00 2001 From: NeoKazuya <2886350+NeoKazuya@users.noreply.github.com> Date: Mon, 12 Oct 2026 22:32:39 -0700 Subject: [PATCH 3/4] Use the GitHub submission timestamp in the claim --- research/complex-packet-borrowing23/CLAIM.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/complex-packet-borrowing23/CLAIM.json b/research/complex-packet-borrowing23/CLAIM.json index ffd8373b39..a3a4011133 100644 --- a/research/complex-packet-borrowing23/CLAIM.json +++ b/research/complex-packet-borrowing23/CLAIM.json @@ -36,5 +36,5 @@ "scope_record_updated_utc": "2026-10-13T05:27:04Z", "status": "submitted", "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/781", - "submitted_utc": "2026-10-13T05:34:00Z" + "submitted_utc": "2026-10-13T05:31:45Z" } From 85f9cfad7708cc3873bd6b32492a618feb336e59 Mon Sep 17 00:00:00 2001 From: NeoKazuya <2886350+NeoKazuya@users.noreply.github.com> Date: Mon, 12 Oct 2026 23:28:46 -0700 Subject: [PATCH 4/4] Add one-helper coded cell and complete native replay --- .../complex-packet-borrowing23/CLAIM.json | 7 +- .../CODED-CELL.json | 65 ++++++ .../complex-packet-borrowing23/EXPECTED.json | 108 +++++++++- research/complex-packet-borrowing23/NOTICE.md | 9 +- research/complex-packet-borrowing23/README.md | 200 +++++++++++++++--- .../complex-packet-borrowing23/SEARCH-LOG.md | 63 +++++- .../SEARCH-RESULTS.json | 79 +++++++ .../SOURCE-PINS.json | 4 +- research/complex-packet-borrowing23/native.py | 117 ++++++++++ .../search_events.py | 172 +++++++++++++++ research/complex-packet-borrowing23/verify.py | 85 +++++++- 11 files changed, 851 insertions(+), 58 deletions(-) create mode 100644 research/complex-packet-borrowing23/CODED-CELL.json create mode 100644 research/complex-packet-borrowing23/SEARCH-RESULTS.json create mode 100644 research/complex-packet-borrowing23/native.py create mode 100644 research/complex-packet-borrowing23/search_events.py diff --git a/research/complex-packet-borrowing23/CLAIM.json b/research/complex-packet-borrowing23/CLAIM.json index a3a4011133..c3e1450b3c 100644 --- a/research/complex-packet-borrowing23/CLAIM.json +++ b/research/complex-packet-borrowing23/CLAIM.json @@ -31,10 +31,9 @@ "coordination": "GitHub pinnedIssues returned an empty list at orientation; claim is recorded locally. No separate reservation issue is opened.", "proof_bar": "A strict improvement requires a complete paid profile and exact arbitrary-dirt/frame verification; otherwise report only an exhaustively checked scoped obstruction or measured search coverage, with no new kappa claim.", "selected_object": "Pair (6,7), sign +1; six all-K leavers, with scope extended to all eight signed all-K cells", - "result": "Scoped obstruction for arbitrary repeated operations on one target pair; exact finite checks and a fully priced two-carrier three-source escape. No new kappa.", - "expected_finish_utc": "2026-10-13T05:40:00Z", - "scope_record_updated_utc": "2026-10-13T05:27:04Z", - "status": "submitted", + "result": "One coded helper with a strict paid-profile gain over a matched-stock direct circuit; both changed native words pass all 714 arbitrary-input columns in both orientations. Analytic single-pair obstruction and solver-backed positive no-helper exclusion. No new kappa.", + "scope_record_updated_utc": "2026-10-13T06:28:00Z", + "status": "submitted with constructive follow-up", "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/781", "submitted_utc": "2026-10-13T05:31:45Z" } diff --git a/research/complex-packet-borrowing23/CODED-CELL.json b/research/complex-packet-borrowing23/CODED-CELL.json new file mode 100644 index 0000000000..035020fc43 --- /dev/null +++ b/research/complex-packet-borrowing23/CODED-CELL.json @@ -0,0 +1,65 @@ +{ + "selected": [[6, 7], 1], + "core": [ + ["h0", "x4", 1], + ["y1", "x3", 1], + ["y2", "x5", 1], + ["y3", "x0", 1], + ["y4", "x2", 1], + ["y5", "x1", 1], + ["h0", "x2", 1], + ["y0", "y1", 1], + ["y2", "x1", 1], + ["y5", "y3", 1], + ["y0", "x4", 1], + ["y3", "y2", 1], + ["y5", "x3", 1], + ["y0", "x2", 1], + ["y1", "x4", 1], + ["y2", "x3", 1], + ["y4", "y3", 1], + ["y0", "x5", 1], + ["y1", "x0", 1], + ["y3", "h0", 1], + ["y4", "x3", 1], + ["y5", "x4", 1], + ["y0", "x1", 1], + ["y1", "x2", 1], + ["y2", "x0", 1], + ["y1", "x5", 1], + ["y2", "x4", 1], + ["y5", "x2", 1] + ], + "direct": [ + ["y5", "x3", 1], + ["y2", "x1", 1], + ["y3", "x2", 1], + ["y1", "x0", 1], + ["y4", "x5", 1], + ["y4", "x3", 1], + ["y5", "x2", 1], + ["y4", "x2", 1], + ["y0", "x4", 1], + ["y2", "x0", 1], + ["y0", "x5", 1], + ["y3", "x1", 1], + ["y1", "x4", 1], + ["y2", "x4", 1], + ["y3", "x0", 1], + ["y3", "x4", 1], + ["y1", "x5", 1], + ["y2", "x5", 1], + ["y0", "x3", 1], + ["y1", "x3", 1], + ["y2", "x3", 1], + ["y3", "x5", 1], + ["y0", "x2", 1], + ["y1", "x2", 1], + ["y5", "x1", 1], + ["y5", "x0", 1], + ["y5", "x4", 1], + ["y4", "x1", 1], + ["y4", "x0", 1], + ["y0", "x1", 1] + ] +} diff --git a/research/complex-packet-borrowing23/EXPECTED.json b/research/complex-packet-borrowing23/EXPECTED.json index 9411dc16b4..caf3ddf898 100644 --- a/research/complex-packet-borrowing23/EXPECTED.json +++ b/research/complex-packet-borrowing23/EXPECTED.json @@ -1,5 +1,5 @@ { - "schema": "complex-packet-borrowing23/1", + "schema": "complex-packet-borrowing23/2", "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", "assignment_seed": 23, "salt_sha256": "e743f055badcf6eca828bbaca72994eb06af4ceda579a0a90535e982cb386d12", @@ -79,5 +79,111 @@ "omit_h1_compensation": true, "double_shared_target_read": true } + }, + "one_helper_cell": { + "witness_sha256": "669017453cdc19f9cad56cdd0b63990f22d8d479850db4519495b88da4c88610", + "columns_each_orientation": 13, + "core_additions": 28, + "zero_frame_precondition_additions": 5, + "full_frame_cleanup_additions": 2, + "total_scalar_additions": 35, + "coded": { + "ok": true, + "profile": { + "1": 32, + "2": 17, + "3": 11 + }, + "rank_mass": 99 + }, + "same_stock_direct": { + "ok": true, + "profile": { + "1": 48, + "2": 12, + "3": 6, + "9": 1 + }, + "rank_mass": 99 + }, + "coded_minus_direct_profile": { + "1": -16, + "2": 5, + "3": 5, + "9": -1 + }, + "mutations_rejected": { + "omit_compensation": true, + "omit_helper_cleanup": true, + "omit_coded_helper_read": true, + "double_shared_target_read": true + } + }, + "native_comparison": { + "coded": { + "status": "PASS_CHANGED_WORD_ALL_COLUMNS_AND_NATIVE_FRAMES", + "input_content_sha256": "9cd9f6906ea1bfce4ffde22da41f049b2ba470582a881cb36bcfc54fb19af722", + "routing_content_sha256": "7c84ac65c8b37173aa4293934f041915895e8ec30595844cc1534e2a19ae0d25", + "canonical_content_sha256": "f38ffe0408b56a97219bd9f8734086fa93b2b5ee1bae80cd2ed390500712223b", + "live_columns_each_orientation": 714, + "helpers": 490, + "compensation_additions": 10478, + "scalar_operations": 16816, + "center_rank_sum": 64, + "local_profile": { + "1": 2044, + "2": 747, + "3": 302, + "4": 168, + "5": 168, + "6": 41, + "8": 8 + }, + "local_rank_mass": 6266, + "frames": 1128, + "directed_edges": 3113, + "tau": 43, + "target_port_order_matches_baseline": true, + "scope": "Fresh exact forward and inverse-transpose scalar replay on every arbitrary input; all native frame chains and dyadic primitives. Phase lowering, wrappers, global owners and global assembly are separate.", + "helper_widths": { + "9": 490 + } + }, + "same_stock_direct": { + "status": "PASS_CHANGED_WORD_ALL_COLUMNS_AND_NATIVE_FRAMES", + "input_content_sha256": "676690228cbfe549a446f5f29869690359b8ec5e623f77101bb4f58b3f142a07", + "routing_content_sha256": "7c84ac65c8b37173aa4293934f041915895e8ec30595844cc1534e2a19ae0d25", + "canonical_content_sha256": "fb3c4e42025cd39239668a35ffed03085c6d3dd13c1b460cd3979bb03783f421", + "live_columns_each_orientation": 714, + "helpers": 490, + "compensation_additions": 10626, + "scalar_operations": 16966, + "center_rank_sum": 64, + "local_profile": { + "1": 2060, + "2": 742, + "3": 297, + "4": 168, + "5": 168, + "6": 41, + "8": 8, + "9": 1 + }, + "local_rank_mass": 6266, + "frames": 1133, + "directed_edges": 3123, + "tau": 43, + "target_port_order_matches_baseline": true, + "scope": "Fresh exact forward and inverse-transpose scalar replay on every arbitrary input; all native frame chains and dyadic primitives. Phase lowering, wrappers, global owners and global assembly are separate.", + "helper_widths": { + "9": 490 + } + }, + "coded_minus_direct_profile": { + "1": -16, + "2": 5, + "3": 5, + "9": -1 + } } } diff --git a/research/complex-packet-borrowing23/NOTICE.md b/research/complex-packet-borrowing23/NOTICE.md index 641b4db632..b9aaf89b3e 100644 --- a/research/complex-packet-borrowing23/NOTICE.md +++ b/research/complex-packet-borrowing23/NOTICE.md @@ -11,6 +11,9 @@ their existing attribution. No authorship of those constructions is claimed. Sreekanth Nair/higherbeing's #651 and Douglas Colkitt's #683 supplied the related scope comparisons. They are not dependencies of the chronology proof. -The unchanged constructor and its data are read in place, with hashes recorded -in SOURCE-PINS.json. Their original notices and licenses remain in their -respective packages. +The original constructor and its data are read in place, with hashes recorded +in SOURCE-PINS.json. The follow-up native recipe adapts that constructor in +memory; it does not edit the inherited source. The independent native auditor +retains its #425/#433, DreamingOfClouds #484 and Round19 attribution. It and +the #552 phase-baseline routing word are also pinned and read in place. +Their original notices and licenses remain in their respective packages. diff --git a/research/complex-packet-borrowing23/README.md b/research/complex-packet-borrowing23/README.md index 88ecd323ac..ffea4139ff 100644 --- a/research/complex-packet-borrowing23/README.md +++ b/research/complex-packet-borrowing23/README.md @@ -1,16 +1,24 @@ -# A frame obstruction to borrowing one pair of complex targets +# One coded helper for an all-K complex packet cell -**Scoped negative result; no new κ.** In the six-leaver all-K packet cell, -using one pair of targets to share source-dependent partial sums cannot -replace the raw reads when the source values stay fixed and there are no -additional carriers. The obstruction allows arbitrary own-read order, -repeated pair interactions, signed coefficients and cancellation. It is -caused by the frames carried by reads, not by a failed circuit search. +A six-source circuit for the selected all-K cell uses one coded helper and +28 core additions. Including dirty-input preconditioning, helper restoration +and every final frame climb, its profile improves on direct delivery using +the same register stock for every recursive moment exponent `0 < s < 1`. -An explicit two-carrier circuit escapes the obstruction in its three-source -projection. Helpers are restored on arbitrary dirty inputs, but its paid profile is worse -than the direct circuit on the same stock. This comparison concerns that -control circuit, not every possible two-carrier construction. +Both circuits also rebuild inside the pinned raw K492 construction. The +changed native words use 490 helpers; each passes independent exact replay +of all 714 input columns in forward and inverse-transpose orientations, +with native frames and dyadic primitives checked. Their paid-profile +difference is exactly the cell's difference. + +**No new κ is claimed.** These are changed raw words. The later supplier +transformations, phase lowering, wrappers, global helper ownership and full +assembly have not been rebuilt for them. + +The package also gives an analytic obstruction for arbitrary signed +operations confined to one target pair without helpers, and a solver-backed +exclusion for a broader, explicitly positive no-helper domain. The constructive +circuit uses several target pairs and one helper, outside both exclusions. ## Reproduce @@ -23,20 +31,24 @@ python3 -B research/complex-packet-borrowing23/verify.py Expected first line: ```text -PASS_COMPLEX_PACKET_PAIR_BORROWING_OBSTRUCTION_AND_PAID_ESCAPE +PASS_COMPLEX_CODED_CELL_AND_PAIR_BORROWING_OBSTRUCTION ``` -The command checks the source pins, rebuilds the unmodified raw 492-helper -constructor with assertions enabled, and checks eight signed all-K cells. -It enumerates 504 nonempty leaver joins and binds 3,600 possible shared +The command checks the source pins and runs inherited code with assertions +enabled, including when the main checker is called with `-I -O`. It rebuilds +the unmodified raw 492-helper word, derives eight signed all-K cells, replays +the one-helper circuit on all 13 arbitrary input columns in both orientations, +and independently audits both changed 714-register native words. + +It also enumerates 504 nonempty leaver joins and binds 3,600 possible shared supports to the chronology obstruction. A separate rational scalar/frame -replay examines all 720 orders of a six-event three-source example. -Of these, 120 have the required arbitrary-input scalar map and none has -legal frames. Omitting source-frame propagation incorrectly accepts 60. +replay examines all 720 orders of a six-event three-source example. Of these, +120 have the required arbitrary-input scalar map and none has legal frames. +Omitting source-frame propagation incorrectly accepts 60. Deliberately +omitting compensation, cleanup or the coded helper read is rejected. -The finite enumeration checks the example and the ordering certificate. -The proof below supplies the statement about arbitrarily many interactions -within one target pair; it is not inferred from a bounded search. +No solver is needed for these checks. The optional solver reproduction below +is separate from the explicit constructive witness and the analytic proof. ## The selected cell @@ -63,7 +75,131 @@ the proof. All eight signed all-K cells have the same incidence pattern. The checker derives their roles and coefficients from the pinned constructor, then checks the subspaces independently by explicit XOR closure. -## Proposition and proof +## The one-helper circuit and its paid gain + +[CODED-CELL.json](CODED-CELL.json) lists the 28 positive core additions and +the legal 30-read direct control, using the normalized labels above. The +helper accumulates `X4 + X2`, spanning two different factories. Four reads +share a target's current sum with another target; one target reads the helper. + +Targets and the helper start with arbitrary independent dirty values. Before +source access, invert the core's five non-source reads in reverse order at +frame zero. After the core, climb sources and the helper to rank nine and +targets to their rank-eight caps. Then undo the helper's two source additions +at the full frame. The complete local circuit has 35 scalar additions; +the direct control has 30. The comparison here concerns recursive frame cost, +not a reduction in this local scalar operation count. + +Exact rational replay verifies the required map +`Y_i += sum_{j != i} X_j`, with every source and the dirty helper restored. +An independent XOR-span replay charges both participants of every read and +all final climbs: + +| Circuit, with the same one-helper stock | H1 | H2 | H3 | H9 | Rank mass | +| --- | ---: | ---: | ---: | ---: | ---: | +| Direct, helper idle | 48 | 12 | 6 | 1 | 99 | +| Coded helper | 32 | 17 | 11 | 0 | 99 | + +Thus coded minus direct is + +```text +-16 H1 + 5 H2 + 5 H3 - H9. +``` + +For the moment `sum_r H_r r^s`, this is strictly negative for every +`0 < s < 1`. To see this without numerical sampling, set `x = 3^s` and +`a = log(2)/log(3)`, so `1 < x < 3` and `1/2 < a < 1`. +Concavity and the tangent to `x^a` at 3 give + +```text +2^s = x^a <= 2 + (2a/3)(x-3) <= (x+3)/3. +``` + +Consequently direct minus coded satisfies + +```text +16 + 9^s - 5*3^s - 5*2^s + >= x^2 - (20/3)x + 11 + = (3-x)(11/3-x) > 0. +``` + +The standard checker binds this argument to the exact integer profiles. +It does not claim that the coded circuit is optimal, or compare it with every +possible direct circuit or helper lifetime convention. + +## Replay inside the native construction + +[native.py](native.py) applies a checked, in-memory recipe to the pinned +constructor. It adds the selected positive `(6,7)` cell to the four existing +raw triangles, removes its three formed packet copies, and reserves one of +those slots for the coded helper: `492 - 3 + 1 = 490`. The direct control +reserves the same slot and leaves it idle. + +The recipe delays the six own reads, inserts the chosen circuit, and inverts +its extra target basis in both the zero-frame precondition and the center +scatter. The original constructor still checks its clean scalar identity. +The unchanged `hpe_audit_and_transport.py` then independently derives dirty +helper compensation and checks the complete native word, including all 714 +arbitrary input columns in both orientations. Its assertions remain enabled. + +Both words have rank mass 6,266 and 490 full-width helpers. The auditor recovers +the same difference `-16 H1 + 5 H2 + 5 H3 - H9`. Exact content hashes and all +mathematical audit receipt fields are in [EXPECTED.json](EXPECTED.json). +The raw and canonical words are rebuilt in temporary directories; no generated +word is trusted as an input certificate. + +This establishes a native local improvement over the specified matched-stock +direct control. It is not a comparison against the admitted, globally hosted +incumbent, and does not transfer its owner map or its κ to this new word. + +## Resolved no-helper search + +Replacing a step-by-step state model with event clocks resolved the earlier +five- and six-source timeouts. The unrestricted target graph is now included, +with these restrictions on the source-dependent part of the circuit: + +- Sources are immutable; there are no helpers or register resets. +- Operations are positive unit additions of disjoint signal supports. + There is no source-dependent subtraction, rescaling or repeated coefficient. +- Each target must receive exactly one copy of every source except its own. + Both participants inherit every read's common frame. +- At least one target-to-target read carries a nonempty signal. + +One potential event per ordered register pair suffices in this domain. +Repeating an edge would resend a source term that the receiver already has, +since supports never shrink. Using both directions between targets would +likewise resend a term from the first read. Events sharing a register have +distinct clocks; disjoint events can be ordered arbitrarily. Each event's +frame contains every earlier frame touching either participant. + +The model permits source-free dirty-input preconditioning optimistically. +It requires no dirt-restoration certificate for a hypothetical solution, so +its UNSAT result also excludes the corresponding realizable circuits in this +positive domain. It does not exclude signed or rescaled circuits. + +Z3 5.1.0 and CVC5 1.4.2 both returned **UNSAT** for six sources, on the same +exported formula with SHA-256 +`e9d8e27bac9d4b2dc78f5a745847d99b9396c5b6476b87cac415d71dba5507ef`. +They took approximately 12.4 and 130.7 seconds respectively. The direct-only +control and the control omitting frames both return SAT. These are recorded +solver outcomes, not an independently checked UNSAT proof certificate. + +Optional reproduction, with `z3-solver==5.1.0.0` and `cvc5==1.4.2` installed: + +```sh +python3 research/complex-packet-borrowing23/search_events.py --engine z3 --out /tmp/packet-z3 +python3 research/complex-packet-borrowing23/search_events.py --engine cvc5 --out /tmp/packet-cvc5 +python3 research/complex-packet-borrowing23/search_events.py --control direct --out /tmp/packet-direct +python3 research/complex-packet-borrowing23/search_events.py --control no-frames --out /tmp/packet-no-frames +python3 research/complex-packet-borrowing23/search_events.py --helpers 1 --max-adds 28 --out /tmp/packet-helper +``` + +Use fresh output directories. The script writes the formula and a result +receipt. `--export-only` regenerates the formula without solving. Solver +timings are observations, not runtime guarantees; unknown remains inconclusive. +The one-helper SAT witness is checked separately by the solver-free replay. + +## Single-pair proposition and proof Let there be `n >= 3` sources and targets with `E_i` contained in `H_j` exactly when `i != j`, as above. Consider any finite @@ -110,7 +246,7 @@ acquired. Earlier reads or extra frame promotions only add restrictions. The five-event checker explicitly examines all 120 strict orders; 16 satisfy the four required precedences, and the two contradictions reject eight each. -## A paid escape and controls +## A three-source escape and controls Use three sources and targets, where `Y_i` needs the other two sources. Introduce dirty helpers `H0,H1`. At frame zero, apply @@ -163,16 +299,18 @@ carriers; this package concerns all-K cells and a target-pair mechanism. Neither those broader titles nor the present proposition establishes a barrier for arbitrary network coding. -The proposition does not cover additional carriers, mutable source values, -source-dependent coupling through three or more targets, register lifetime -resets, different decoder demands, or different geometry. Exploratory -six-source searches with broader target coupling and one or two coded helpers -timed out; those runs establish no impossibility result. The two-carrier -control does not establish a minimum carrier count or an optimal circuit. +The analytic proposition does not cover additional carriers, mutable source +values, source-dependent coupling through three or more targets, register +lifetime resets, different decoder demands, or different geometry. The +positive event model covers broader target coupling under narrower coefficient +restrictions. Neither establishes a barrier for arbitrary network coding. +The one-helper construction and the three-source two-carrier control do not +establish optimal profiles or a helper minimum for general linear circuits. The [local claim](CLAIM.json) records the draw and candidate selection. -[SEARCH-LOG.md](SEARCH-LOG.md) records exploratory domains and stopping rules; -those searches are not dependencies of the proof or checker. +[SEARCH-LOG.md](SEARCH-LOG.md) records the earlier timeouts and the event-model +follow-up; [SEARCH-RESULTS.json](SEARCH-RESULTS.json) retains the solver receipts. +Those searches are not dependencies of the analytic proof or standard checker. The [source pins](SOURCE-PINS.json), [exact finite evidence](EXPECTED.json) and [attribution](NOTICE.md) accompany this note. No selected certificate, existing supplier or `upstream/` source is changed. diff --git a/research/complex-packet-borrowing23/SEARCH-LOG.md b/research/complex-packet-borrowing23/SEARCH-LOG.md index 708a233ee5..8a501b4d8c 100644 --- a/research/complex-packet-borrowing23/SEARCH-LOG.md +++ b/research/complex-packet-borrowing23/SEARCH-LOG.md @@ -1,10 +1,11 @@ # Discovery record -These exploratory searches guided the choice of a provable local statement. -They do not certify the proposition. The submitted, standard-library checker -independently verifies its geometric premises, five-event order contradiction, -six-event example and paid controls. No solver is required to reproduce those -results. The exploratory search scripts are not part of this package. +The original searches guided the single-pair proposition. The follow-up event +model resolved broader positive cases and found the one-helper construction. +The standard-library checker independently verifies geometry, the chronology +certificate, the explicit circuits and their changed native words. It needs +no solver. The original exploratory scripts are not dependencies; the event +model is included as `search_events.py` with optional solver dependencies. ## Assignment and domain @@ -74,9 +75,49 @@ Z3 runs returned unknown at 55 seconds. CVC5 1.4.2 independently parsed the same exported formulas; both runs also returned unknown at 55 seconds. These helper bounds do not cover all possible coded circuits. -No result about general multi-target coding, signed circuits or helper -optimality follows from these searches. The final proof instead fixes one -unordered target pair and allows arbitrarily many signed linear operations -and arbitrary read order. The two-helper control in the checker uses a -three-source projection and includes the compensation, cleanup and final -climbs absent from the discovery models. +These step-model outcomes remain inconclusive; longer work used the different +encoding below. The analytic proof fixes one unordered target pair and permits +arbitrarily many signed operations. Its three-source two-helper control includes +compensation, cleanup and final climbs absent from discovery models. + +## Follow-up: event clocks instead of time steps + +Each possible read has an activation variable, a clock, a source-support mask +and a common-frame mask. Pairwise constraints enforce frame monotonicity +through both registers. A target receives each required term exactly once. +The README explains why repeated directed edges and reversed target edges +are unnecessary in this positive disjoint-support domain. + +The first formulation used pseudo-Boolean exact-one constraints. It resolved +five sources as UNSAT in 0.858 s and six as UNSAT in 13.677 s, with a 300 s +limit and Z3 seed 23. An alternate formulation replaced those cardinalities +by pairwise exclusions. Its six-source formula was exported once and checked +by Z3 5.1.0 (12.442 s) and CVC5 1.4.2 (130.715 s), both with a 180 s limit. +Both returned UNSAT. The packaged script reproduces exactly the exported +formula hash in `SEARCH-RESULTS.json`. No UNSAT proof object was collected. + +The no-helper direct-only control and the no-frame shared-target control both +return SAT. The solver-free checker separately shows that omitting source-frame +propagation falsely admits 60 of the 720 three-source event orders. + +The helper extension has no target-to-helper reads. A mixed helper packet is +required; the recorded six-source runs were: + +| Helpers | Core addition limit | Result | Recorded elapsed time | +| --- | --- | --- | --- | +| 1 | 28 | SAT | 22.319 s | +| 2 | 26 | SAT | 4.786 s | +| 3 | 24 | unknown, 180 s timeout | 180.788 s | + +The two-helper circuit also passed a separate exploratory exact replay. The +one-helper witness was selected for the contribution: `CODED-CELL.json` records +its core, and `verify.py` derives compensation and cleanup, replays every dirty +input, and checks its native construction against a matched-stock direct +control. Its five target/helper preconditioning reads and two helper cleanup +reads bring the local scalar count from 28 to 35. Those operations and all +final frame climbs are accounted for. + +This follow-up establishes no general signed-circuit exclusion, no optimal +core length, and no globally admitted κ. The three-helper timeout remains +unknown. Solver receipts are discovery evidence; the explicit circuit's +arbitrary-input scalar and frame identities are checked independently. diff --git a/research/complex-packet-borrowing23/SEARCH-RESULTS.json b/research/complex-packet-borrowing23/SEARCH-RESULTS.json new file mode 100644 index 0000000000..87e865c6b5 --- /dev/null +++ b/research/complex-packet-borrowing23/SEARCH-RESULTS.json @@ -0,0 +1,79 @@ +{ + "no_helper_z3": { + "engine": "z3", + "version": "5.1.0", + "n": 6, + "seed": 23, + "result": "unsat", + "timeout_ms": 180000, + "seconds": 12.441527700000734, + "formula_sha256": "e9d8e27bac9d4b2dc78f5a745847d99b9396c5b6476b87cac415d71dba5507ef" + }, + "no_helper_cvc5": { + "engine": "cvc5", + "version": "1.4.2", + "n": 6, + "seed": 23, + "result": "unsat", + "timeout_ms": 180000, + "seconds": 130.71498229999997, + "formula_sha256": "e9d8e27bac9d4b2dc78f5a745847d99b9396c5b6476b87cac415d71dba5507ef" + }, + "one_helper": { + "n": 6, + "helpers": 1, + "max_adds": 28, + "mixed_packet_required": true, + "result": "sat", + "seconds": 22.318824400001176, + "timeout_ms": 180000, + "seed": 23 + }, + "two_helpers": { + "n": 6, + "helpers": 2, + "max_adds": 26, + "mixed_packet_required": true, + "result": "sat", + "seconds": 4.785900699997001, + "timeout_ms": 180000, + "seed": 23 + }, + "three_helpers": { + "n": 6, + "helpers": 3, + "max_adds": 24, + "mixed_packet_required": true, + "result": "unknown", + "seconds": 180.78841710000052, + "timeout_ms": 180000, + "seed": 23, + "reason": "timeout" + }, + "control_direct": { + "n": 6, + "helpers": 0, + "max_adds": null, + "control": "direct", + "seed": 23, + "timeout_ms": 180000, + "formula_sha256": "81fb5bc5f18fbd07dd6a2d5c3d0e2d85e5c48a9d34913bb19b8890d2d4d9c9d5", + "engine": "z3", + "result": "sat", + "version": "5.1.0", + "seconds": 0.4474484999991546 + }, + "control_no-frames": { + "n": 6, + "helpers": 0, + "max_adds": null, + "control": "no-frames", + "seed": 23, + "timeout_ms": 180000, + "formula_sha256": "5eb26315d0faed857f86cbfcfa186b4d58d3be7e1dc9912bd347df1083c52ba1", + "engine": "z3", + "result": "sat", + "version": "5.1.0", + "seconds": 0.38790780000272207 + } +} diff --git a/research/complex-packet-borrowing23/SOURCE-PINS.json b/research/complex-packet-borrowing23/SOURCE-PINS.json index fc2e5c0dcc..d35f635ca1 100644 --- a/research/complex-packet-borrowing23/SOURCE-PINS.json +++ b/research/complex-packet-borrowing23/SOURCE-PINS.json @@ -5,6 +5,8 @@ "research/direct-delivery504-global/inputs/hamming/PROTOTYPE.json": "327d2a868043e846381aa58a33053c24425e8cad522ff401b10ec8af1d649a3f", "research/direct-delivery504-global/inputs/hamming/PACKET-PROGRAMS.json.gz": "d833ae0390d165d7da0c639a3c7aeb77156c2ddb52447087cb49b9d03b19e9b9", "research/complex-k492-owner-repair/data/TRI-SCHEDULE.json": "94da9d5575f5b237097a77ac7dd09aff594322dd9c35138bfd34ffc5e1a7a51e", - "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "research/complex-k492-owner-repair/code/hpe_audit_and_transport.py": "c9a05ff291016b870b4fc925b317abd9c3a604c73ffc8920dfdbbeb475e20aa3", + "research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz": "e070ae2c78b4a1b644b418774af62b40d8d16e6ba89602f0474afb557d507c37" } } diff --git a/research/complex-packet-borrowing23/native.py b/research/complex-packet-borrowing23/native.py new file mode 100644 index 0000000000..80fe667e6b --- /dev/null +++ b/research/complex-packet-borrowing23/native.py @@ -0,0 +1,117 @@ +"""Rebuild a coded cell and its direct control inside the pinned native word. + +Apache-2.0. NeoKazuya, with substantial OpenAI Codex assistance. +The constructor and auditor retain their upstream attribution (see NOTICE.md). +Run through verify.py, which checks pins and enables inherited assertions. +""" +import contextlib +import io +import json +from collections import Counter +from fractions import Fraction +from pathlib import Path +import runpy +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +CONSTRUCTOR = "research/complex-k492-owner-repair/code/construct_k_triangle.py" +AUDITOR = "research/complex-k492-owner-repair/code/hpe_audit_and_transport.py" +INPUTS = "research/direct-delivery504-global/inputs/hamming" +SCHEDULE = "research/complex-k492-owner-repair/data/TRI-SCHEDULE.json" +ROUTING = ("research/complex-k492-owner-repair/vendor/multicold/vendor/pr558/vendor/pr552/" + "complex-local/inputs/phase-baseline/CANONICAL-WORD.json.gz") + + +def rebuild_and_audit(geometry, work): + if not __debug__: + raise RuntimeError("inherited constructor and auditor require assertions") + cell = next(c for c in geometry["cases"] if [c["pair"], c["sign"]] == geometry["selected"]) + assert geometry["selected"] == [[6, 7], 1] + assert [[Fraction(q) for q in row] for row in cell["coefficients"]] == [ + [Fraction(i != j) for j in range(6)] for i in range(6)] + witness = json.loads((HERE / "CODED-CELL.json").read_bytes()) + schedule = json.loads((ROOT / SCHEDULE).read_bytes()) + reads = [] + for target in cell["targets"]: + own = next(s for s in cell["leavers"] if s["raw120_register"] == target["own_register"]) + reads.append([target["port112_index"], own["block"], own["local_register"]]) + # These six entries declare delayed own reads; the replacement below emits + # every actual read from the independently replayed circuit fixture. + schedule["triangles"].append({"p": [6, 7], "e": 1, "reads": reads, "coded": True}) + schedule_path = work / "coded-schedule.json" + schedule_path.write_text(json.dumps(schedule, indent=2) + "\n", encoding="utf-8") + bindings = {f"x{i}": ("source", s["block"], s["local_register"]) + for i, s in enumerate(cell["leavers"])} + bindings.update({f"y{i}": ("target", t["root_index"]) for i, t in enumerate(cell["targets"])}) + source = (ROOT / CONSTRUCTOR).read_text(encoding="utf-8") + + def replace(old, new): + nonlocal source + assert source.count(old) == 1, ("constructor recipe no longer unique", old) + source = source.replace(old, new) + + # The fifth raw triangle removes three packet copies; reserve one of those + # slots for our helper. Its baseline counterpart is present but stays idle. + replace("NH=504-3*len(FULLT)+len(COPYL)", "NH=504-3*len(FULLT)+len(COPYL)+1") + replace("tri_join_counts=Counter()", + "tri_join_counts=Counter()\ncoded_shadow_slot=None\ncoded_target_edges=[]") + insertion = ''' if tr.get('coded'): + aux=len(cur);cur.append(());rows.append({}) + coded_shadow_slot=len(shadow);shadow.append(None) + bindings={} + for name,binding in CODED_BINDINGS.items(): + bindings[name]=maps[tuple(binding[1])][binding[2]] if binding[0]=='source' else v+binding[1] + bindings['h0']=aux + for tn,sn,q in CODED_CORE: + target,source=bindings[tn],bindings[sn] + F=basis(cur[target]+cur[source]) + for register in (target,source): + if v<=register<2*v:assert inside(F,hyper(P[register-v])),('coded frame',register,F) + add(target,source,q,F) + if sn.startswith('y'):coded_target_edges.append((target,source,Q(q))) + continue +''' + replace("for tr in TRI['triangles']:\n p,eps=tuple(tr['p']),tr['e']", + "for tr in TRI['triangles']:\n" + insertion + " p,eps=tuple(tr['p']),tr['e']") + replace(" if tuple(key) in FULLT:skip();continue", ''' if tuple(key) in FULLT: + if tuple(key)==((6,7),1) and shadow[coded_shadow_slot] is None: + shadow[coded_shadow_slot]=nxt[0];nxt[0]+=1 + else:skip() + continue''') + # Invert the extra target basis in both the input precondition and center + # scatter. Helper dirt compensation is recomputed by the separate auditor. + replace("for r in range(len(cur)):climb(r,hyper(P[r-v]) if v<=r<2*v else FULL)", + '''for target,source,q in reversed(coded_target_edges): + scatter[target-v]=[a-q*b for a,b in zip(scatter[target-v],scatter[source-v])] + precondition.append(['add',target,source,-q.numerator,q.denominator,[]]) +for r in range(len(cur)):climb(r,hyper(P[r-v]) if v<=r<2*v else FULL)''') + audit = runpy.run_path(str(ROOT / AUDITOR))["run"] + results = {} + for label, core in (("coded", witness["core"]), ("same_stock_direct", witness["direct"])): + raw, checked = work / (label + "-raw"), work / (label + "-audit") + old_argv = sys.argv[:] + try: + sys.argv = [str(ROOT / CONSTRUCTOR), str(ROOT / INPUTS), str(raw), str(schedule_path)] + namespace = {"__name__": "__main__", "__file__": str(ROOT / CONSTRUCTOR), + "CODED_BINDINGS": bindings, "CODED_CORE": core} + with contextlib.redirect_stdout(io.StringIO()): + exec(compile(source, str(ROOT / CONSTRUCTOR), "exec"), namespace) + audit(raw / "FULL-WORD.json.gz", ROOT / ROUTING, checked) + finally: + sys.argv = old_argv + receipt = json.loads((checked / "SCALAR-FRAME-AUDIT.json").read_bytes()) + assert receipt["status"] == "PASS_CHANGED_WORD_ALL_COLUMNS_AND_NATIVE_FRAMES" + assert receipt["helpers"] == 490 and receipt["live_columns_each_orientation"] == 714 + assert receipt["widths"] == [9] * 490 + # Discard elapsed time only; every mathematical receipt field is retained. + receipt.pop("seconds") + receipt["helper_widths"] = {"9": len(receipt.pop("widths"))} + results[label] = receipt + delta = Counter({int(k): v for k, v in results["coded"]["local_profile"].items()}) + delta.subtract({int(k): v for k, v in results["same_stock_direct"]["local_profile"].items()}) + delta = {str(k): v for k, v in sorted(delta.items()) if v} + assert delta == {"1": -16, "2": 5, "3": 5, "9": -1}, delta + assert results["coded"]["local_rank_mass"] == results["same_stock_direct"]["local_rank_mass"] == 6266 + results["coded_minus_direct_profile"] = delta + return results diff --git a/research/complex-packet-borrowing23/search_events.py b/research/complex-packet-borrowing23/search_events.py new file mode 100644 index 0000000000..f9954ce02c --- /dev/null +++ b/research/complex-packet-borrowing23/search_events.py @@ -0,0 +1,172 @@ +"""Optional discovery model: positive unit additions with disjoint supports. + +Requires z3-solver; --engine cvc5 also requires cvc5. Neither dependency is +needed by verify.py. UNSAT applies only to the domain described in README.md. +Apache-2.0. NeoKazuya, with substantial OpenAI Codex assistance. +""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path +import time +import z3 + + +def build(n, helpers, timeout=180000, max_adds=None, frames_on=True, mixed=True): + full = (1 << n) - 1 + target_start = n + helpers + total = 2*n + helpers + # Sources are immutable. Helpers may read sources/helpers; targets may + # additionally read targets. Every directed pair has at most one event. + specs = [(t, s) for t in range(n, total) for s in range(total) + if s != t and (t >= target_start or s < target_start) + and not (t >= target_start and s == t-target_start)] + size = len(specs) + solver = z3.Solver() + solver.set(timeout=timeout, random_seed=23) + clocks = [z3.Int(f'c{e}') for e in range(size)] + active = [z3.Bool(f'a{e}') for e in range(size)] + packets = [z3.BitVecVal(1 << s, n) if s < n else z3.BitVec(f'p{e}', n) + for e, (t, s) in enumerate(specs)] + frames = [z3.BitVec(f'f{e}', n) for e in range(size)] + incoming = {t: [e for e, (d, s) in enumerate(specs) if d == t] for t in range(n, total)} + + def at_most_one(terms): + for a, b in itertools.combinations(terms, 2): + solver.add(z3.Or(z3.Not(a), z3.Not(b))) + + for e in range(size): + solver.add(clocks[e] >= 0, clocks[e] < size) + solver.add(z3.Implies(z3.Not(active[e]), clocks[e] == 0)) + for t in range(n, total): + for i in range(n): + contributors = [z3.And(active[e], (packets[e] & (1 << i)) != 0) for e in incoming[t]] + at_most_one(contributors) + if t >= target_start: + if i != t-target_start: + solver.add(z3.Or(contributors)) + else: + solver.add(z3.Not(z3.Or(contributors))) + for e, (t, s) in enumerate(specs): + if s >= n: + for i in range(n): + arrived = z3.Or([z3.And(active[f], clocks[f] < clocks[e], (packets[f] & (1 << i)) != 0) + for f in incoming[s]]) + solver.add(z3.Implies(active[e], ((packets[e] & (1 << i)) != 0) == arrived)) + solver.add(z3.Implies(active[e], packets[e] != 0)) + solver.add(z3.Implies(z3.Not(active[e]), packets[e] == 0)) + if frames_on: + allowed = full + if t >= target_start: + allowed ^= 1 << (t-target_start) + if s >= target_start: + allowed &= full ^ (1 << (s-target_start)) + solver.add(z3.Implies(active[e], (frames[e] & ~allowed) == 0)) + solver.add(z3.Implies(active[e], (packets[e] & ~frames[e]) == 0)) + solver.add(z3.Implies(z3.Not(active[e]), frames[e] == 0)) + # An event's common frame includes every earlier frame touching either + # register, including source-only reads. Disjoint events may commute. + for f in range(e): + if not set(specs[e]) & set(specs[f]): + continue + both = z3.And(active[e], active[f]) + solver.add(z3.Implies(both, clocks[e] != clocks[f])) + if frames_on: + solver.add(z3.Implies(z3.And(both, clocks[e] < clocks[f]), (frames[e] & ~frames[f]) == 0)) + solver.add(z3.Implies(z3.And(both, clocks[f] < clocks[e]), (frames[f] & ~frames[e]) == 0)) + if s >= n and (s, t) in specs: + reverse = specs.index((s, t)) + if e < reverse: + solver.add(z3.Or(z3.Not(active[e]), z3.Not(active[reverse]))) + if mixed: + solver.add(z3.Or([z3.And(active[e], packets[e] & (packets[e]-1) != 0) + for e, (t, s) in enumerate(specs) if n <= s < target_start and t >= target_start])) + if max_adds is not None: + solver.add(z3.Sum([z3.If(a, 1, 0) for a in active]) <= max_adds) + return solver, specs, clocks, active, packets + + +def alternate_solve(path, timeout): + import cvc5 + alternate = cvc5.Solver() + alternate.setLogic('ALL') + alternate.setOption('tlimit-per', str(timeout)) + alternate.setOption('seed', '23') + parser = cvc5.InputParser(alternate) + parser.setFileInput(cvc5.InputLanguage.SMT_LIB_2_6, str(path)) + manager = parser.getSymbolManager() + while True: + command = parser.nextCommand() + if command.isNull(): + break + if command.getCommandName() == 'check-sat': + continue + response = command.invoke(alternate, manager) + if response.strip(): + raise RuntimeError(response) + answer = str(alternate.checkSat()) + version = alternate.getVersion() + return answer, version.decode() if isinstance(version, bytes) else version + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--n', type=int, default=6) + parser.add_argument('--helpers', type=int, default=0) + parser.add_argument('--max-adds', type=int) + parser.add_argument('--timeout', type=int, default=180000) + parser.add_argument('--engine', choices=('z3', 'cvc5'), default='z3') + parser.add_argument('--control', choices=('direct', 'no-frames')) + parser.add_argument('--export-only', action='store_true') + parser.add_argument('--out', type=Path, required=True) + args = parser.parse_args() + if args.n < 3 or args.helpers < 0 or args.timeout <= 0: + parser.error('require n >= 3, helpers >= 0 and positive timeout') + if args.control and args.helpers: + parser.error('controls are for the no-helper model') + started = time.monotonic() + solver, specs, clocks, active, packets = build( + args.n, args.helpers, args.timeout, args.max_adds, + frames_on=args.control != 'no-frames', mixed=args.helpers > 0) + if args.helpers == 0: + if args.control == 'direct': + for e, (_, source) in enumerate(specs): + if source >= args.n: + solver.add(z3.Not(active[e])) + else: + # Relabel any nonempty shared edge and one carried source to 0->1 + # carrying source 2. The simultaneous source/omitted-target + # permutation preserves the all-but-one demand and frame incidence. + edge = specs.index((args.n+1, args.n)) + solver.add(active[edge], packets[edge] & 4 != 0) + args.out.mkdir(parents=True, exist_ok=False) + formula = solver.to_smt2() + smt_path = args.out / 'model.smt2' + smt_path.write_text(formula, encoding='utf-8', newline='\n') + result = {'n': args.n, 'helpers': args.helpers, 'max_adds': args.max_adds, + 'control': args.control, 'seed': 23, 'timeout_ms': args.timeout, + 'formula_sha256': hashlib.sha256(formula.encode()).hexdigest(), + 'engine': args.engine} + if args.export_only: + result.update(result='exported', version=z3.get_version_string()) + elif args.engine == 'cvc5': + result['result'], result['version'] = alternate_solve(smt_path, args.timeout) + else: + status = solver.check() + result.update(result=str(status), version=z3.get_version_string()) + if status == z3.unknown: + result['reason'] = solver.reason_unknown() + elif status == z3.sat: + model = solver.model() + order = sorted((model.eval(clocks[e]).as_long(), e) for e in range(len(specs)) + if z3.is_true(model.eval(active[e]))) + result['operations'] = [list(specs[e]) for _, e in order] + result['packets'] = [model.eval(packets[e]).as_long() for _, e in order] + result['seconds'] = time.monotonic()-started + (args.out / 'result.json').write_text(json.dumps(result, indent=2)+'\n', encoding='utf-8') + print(json.dumps(result, indent=2), flush=True) + + +if __name__ == '__main__': + main() diff --git a/research/complex-packet-borrowing23/verify.py b/research/complex-packet-borrowing23/verify.py index 03fa9f8888..f145869f85 100644 --- a/research/complex-packet-borrowing23/verify.py +++ b/research/complex-packet-borrowing23/verify.py @@ -223,11 +223,11 @@ def scalar_matrix(registers, operations, backward=False): return rows -def expected_matrix(registers, missing=None, backward=False): +def expected_matrix(registers, missing=None, backward=False, n=3): rows = scalar_matrix(registers, []) index = {name: i for i, name in enumerate(registers)} - for i in range(3): - for j in range(3): + for i in range(n): + for j in range(n): if i != j and (i, j) != missing: t, s = index[f"y{i}"], index[f"x{j}"] if backward: @@ -350,6 +350,61 @@ def verify_sources(): return pins +def coded_cell_checks(selected): + """Replay the discovered six-source circuit without trusting solver output.""" + witness = json.loads((HERE / "CODED-CELL.json").read_bytes()) + require(witness["selected"] == [selected["pair"], selected["sign"]], "coded cell binding changed") + require([[Fraction(x) for x in row] for row in selected["coefficients"]] + == [[Fraction(i != j) for j in range(6)] for i in range(6)], + "coded witness needs the selected unit-coefficient cell") + registers = [f"x{i}" for i in range(6)] + ["h0"] + [f"y{i}" for i in range(6)] + core, direct = witness["core"], witness["direct"] + require(len(core) == 28 and len(direct) == 30, "unexpected core lengths") + require(all(q == 1 and t != s and t in registers and s in registers + and not t.startswith("x") for t, s, q in core), "invalid positive core") + require(all(t.startswith("y") and s.startswith("x") and q == 1 for t, s, q in direct), + "direct control is not direct delivery") + require(all(s.startswith("x") for t, s, _ in core if t == "h0"), + "compensation derivation requires helper writes from immutable sources") + precondition = [(t, s, -q) for t, s, q in reversed(core) if not s.startswith("x")] + cleanup = [(t, s, -q) for t, s, q in reversed(core) if t == "h0"] + whole = precondition + core + cleanup + for backward in (False, True): + expected = expected_matrix(registers, backward=backward, n=6) + require(scalar_matrix(registers, whole, backward) == expected, "one-helper arbitrary-dirt replay") + require(scalar_matrix(registers, direct, backward) == expected, "six-source direct replay") + spaces = [span(s["frame"]) for s in selected["leavers"]] + caps = [cap(t["port"]) for t in selected["targets"]] + paid = framed_replay(registers, precondition + core, spaces, caps) + baseline = framed_replay(registers, direct, spaces, caps) + require(paid["ok"] and baseline["ok"], "six-source native frame replay") + require(paid["rank_mass"] == baseline["rank_mass"] == 99, "unmatched six-source stock") + require(all(t == "h0" and s.startswith("x") for t, s, _ in cleanup), + "cleanup must run on full-frame sources and helper after final climbs") + delta = Counter({int(k): v for k, v in paid["profile"].items()}) + delta.subtract({int(k): v for k, v in baseline["profile"].items()}) + delta = {str(k): v for k, v in sorted(delta.items()) if v} + require(delta == {"1": -16, "2": 5, "3": 5, "9": -1}, "coded cost comparison changed") + # README proves positivity of direct-minus-coded for every 0= (3-x)(11/3-x)>0. The exact profile above is + # the finite premise of that analytic argument, not a numerical sampling. + mutations = { + "omit_compensation": core + cleanup, + "omit_helper_cleanup": precondition + core, + "omit_coded_helper_read": precondition + [e for e in core if e[1] != "h0"] + cleanup, + "double_shared_target_read": precondition + [ + [t, s, 2 if s.startswith("y") else q] for t, s, q in core] + cleanup, + } + rejected = {name: scalar_matrix(registers, bad) != expected_matrix(registers, n=6) + for name, bad in mutations.items()} + require(all(rejected.values()), "one-helper mutation escaped") + return {"witness_sha256": digest(witness), "columns_each_orientation": 13, + "core_additions": len(core), "zero_frame_precondition_additions": len(precondition), + "full_frame_cleanup_additions": len(cleanup), "total_scalar_additions": len(whole), + "coded": paid, "same_stock_direct": baseline, + "coded_minus_direct_profile": delta, "mutations_rejected": rejected} + + def verify_assignment(pins): claim = json.loads((HERE / "CLAIM.json").read_bytes()) require(claim["assignment_seed"] == ASSIGNMENT_SEED and claim["salt"] == SALT, @@ -368,11 +423,20 @@ def verify_assignment(pins): def main(): parser = argparse.ArgumentParser(description=__doc__) parser.add_argument("--geometry-worker", type=Path, help=argparse.SUPPRESS) + parser.add_argument("--native-worker", type=Path, help=argparse.SUPPRESS) + parser.add_argument("--native-output", type=Path, help=argparse.SUPPRESS) parser.add_argument("--record", type=Path, help="write a development evidence file instead of comparing EXPECTED.json") args = parser.parse_args() if args.geometry_worker is not None: geometry_worker(args.geometry_worker) return + if args.native_worker is not None: + require(__debug__, "native worker requires assertions") + verify_sources() + native = runpy.run_path(str(HERE / "native.py")) + result = native["rebuild_and_audit"](json.loads(args.native_worker.read_bytes()), args.native_worker.parent) + args.native_output.write_text(json.dumps(result, indent=2) + "\n", encoding="utf-8") + return pins = verify_sources() verify_assignment(pins) with tempfile.TemporaryDirectory(prefix="packet-borrowing23-") as temporary: @@ -384,20 +448,27 @@ def main(): capture_output=True, text=True, check=False) require(result.returncode == 0, "assertion-enabled constructor worker failed: " + result.stderr[-3000:]) geometry = json.loads(output.read_bytes()) + native_output = Path(temporary) / "native.json" + result = subprocess.run([sys.executable, "-I", "-B", str(Path(__file__).resolve()), + "--native-worker", str(output), "--native-output", str(native_output)], + env=environment, capture_output=True, text=True, check=False) + require(result.returncode == 0, "assertion-enabled native audit failed: " + result.stderr[-3000:]) + native = json.loads(native_output.read_bytes()) selected = next(case for case in geometry["cases"] if [case["pair"], case["sign"]] == geometry["selected"]) - evidence = {"schema": "complex-packet-borrowing23/1", "base_commit": pins["base_commit"], + evidence = {"schema": "complex-packet-borrowing23/2", "base_commit": pins["base_commit"], "assignment_seed": ASSIGNMENT_SEED, "salt_sha256": hashlib.sha256(SALT.encode()).hexdigest(), "selected": geometry["selected"], "formed_candidate_count": geometry["formed_candidate_count"], "raw492_content_sha256": geometry["raw492_content_sha256"], "geometry": validate_geometry(geometry), "chronology": chronology_check(), - "scalar_and_paid_controls": scalar_and_escape_checks(selected)} + "scalar_and_paid_controls": scalar_and_escape_checks(selected), + "one_helper_cell": coded_cell_checks(selected), "native_comparison": native} if args.record: args.record.write_text(json.dumps(evidence, indent=2) + "\n", encoding="utf-8") print(json.dumps(evidence, indent=2)) return require(evidence == json.loads((HERE / "EXPECTED.json").read_bytes()), "evidence differs from EXPECTED.json") - print("PASS_COMPLEX_PACKET_PAIR_BORROWING_OBSTRUCTION_AND_PAID_ESCAPE") - print("8 signed cells; 3600 shared-support certificates; 720 scalar/frame orders; both dirty-input orientations") + print("PASS_COMPLEX_CODED_CELL_AND_PAIR_BORROWING_OBSTRUCTION") + print("One-helper cell; matched-stock native words, 714 columns each orientation; 8 signed cells; 720 order controls") if __name__ == "__main__":