From c804e7d79ac524723aa8c2d0d6a59d5e662763b3 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:10:52 +0530 Subject: [PATCH 1/2] Research: factor R420 compensation through disjoint target pairs --- research/r420-target-pairs/CLAIM.md | 29 ++ research/r420-target-pairs/README.md | 211 ++++++++++++++ research/r420-target-pairs/certificate.json | 38 +++ research/r420-target-pairs/native.py | 172 ++++++++++++ research/r420-target-pairs/recipe.json | 17 ++ research/r420-target-pairs/verify.py | 288 ++++++++++++++++++++ 6 files changed, 755 insertions(+) create mode 100644 research/r420-target-pairs/CLAIM.md create mode 100644 research/r420-target-pairs/README.md create mode 100644 research/r420-target-pairs/certificate.json create mode 100644 research/r420-target-pairs/native.py create mode 100644 research/r420-target-pairs/recipe.json create mode 100644 research/r420-target-pairs/verify.py diff --git a/research/r420-target-pairs/CLAIM.md b/research/r420-target-pairs/CLAIM.md new file mode 100644 index 0000000000..8b4d4b521f --- /dev/null +++ b/research/r420-target-pairs/CLAIM.md @@ -0,0 +1,29 @@ +# R420 target-pair compensation claim + +- Track: bit supplier. Assignment seed: **13**, drawn from OS randomness on + 2026-10-13 at 04:23:54 UTC. +- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Object: the 120 target rows of the frame-zero D compensation matrix in + eumemic's PR543 R420 word, source commit + `2065fe4f72a914d907f1046603f5a36f17018535`. +- Method: score all 120 × 119 oriented target pairs, then use seed 13 to + break ties in one greedy disjoint matching. Restore the target basis inside + D and charge both target-to-target gates per pair. Check the full dirty-input + operator, unchanged frame paths, scalar counts and positive-prefix growth. +- Deliverable: one frozen finite circuit, exact reproducible checker, mutation + controls and a scoped research note. No new kappa or hosted invoice claim. +- Finish target: 2026-10-13 05:04 UTC. Verification and handoff begin by 04:54. + +The three candidates were fixed-order phase-B frame optimization, phase-A quad +synthesis, and target-row compensation factoring. PR661 already closes the +first class; PR691 and PR670/674/688 cover quad/block circuit synthesis. +PR686/694 factor helper columns in D. This claim factors target rows while +leaving every helper untouched. Older target-factoring work, including PR476, +is checked for relevant precedent and credited in the final note. + +At selection, GitHub reported no pinned issues. An overlap refresh inspected +all 520 open PRs and searched their titles and bodies for target-pair, target +basis and row-factoring work. The claim is local because no pinned coordination +issue exists. Delegated work stays within this D-stage construction. + +Contributor: Sagar Thakrar, with substantial OpenAI Codex assistance. diff --git a/research/r420-target-pairs/README.md b/research/r420-target-pairs/README.md new file mode 100644 index 0000000000..5864b0c8f0 --- /dev/null +++ b/research/r420-target-pairs/README.md @@ -0,0 +1,211 @@ +# R420 compensation with disjoint target pairs + +**Finite circuit improvement; no new kappa.** On eumemic's PR543 R420 word, +57 disjoint target pairs reduce the frame-zero D compensation from **19,922 +to 16,772 binary XOR additions**. The complete local word drops from **26,916 +to 23,766 additions**, a saving of 3,150, including preparation and restoration. +Every source and helper keeps its original value at the D boundary. + +The complete physical frame paths, 420 helpers, nine retained copies and paid +rank mass 5,112 are unchanged. The reverse positive-prefix bound grows, so this +is not a free substitution into a previously certified hosted invoice. + +| Local quantity | PR543 source | Target-pair word | +| --- | ---: | ---: | +| D binary additions | 19,922 | 16,772 | +| All binary additions | 26,916 | 23,766 | +| Forward positive-prefix bound | 144,651 | 144,651 | +| Reverse positive-prefix bound | 2,270,064 | 3,703,810 | +| Local native payload bits | 100 | 102 | +| Paid rank mass | 5,112 | 5,112 | + +The local native payload expression is `64 F^3 B^2`. For the changed word it is +`2657306775507971405724759110400 < 2^104`. This is the inherited local payload +test used by the native cohort checker, not a new proof of global hosted +prefix bounds at nine or eleven stages. + +## Reproduce + +From the repository root, with Python 3.11 or later and its standard library: + +```sh +python3 -B research/r420-target-pairs/verify.py +``` + +Expected output: + +```text +PASS_R420_TARGET_PAIRS D=19922->16772 ADDs=26916->23766 saved=3150 columns=660 rank_mass=5112 +``` + +`--report` prints the exact receipt, which must match `certificate.json`. +The recipe and pinned source reconstruct the entire changed word in memory; +its canonical JSON SHA-256 is +`309cf1688f1027ec5ec182f5f6ccb8e5752e74ccd3ce017ced8bd45dfd7ff010`. +No generated word or changes to predecessor files are needed. + +To also run the unchanged native exporter, legality checker and five-, nine- +and eleven-stage formal-column checkers, provide a C++17 compiler and Boost +headers. These are the predecessor checkers' existing dependencies. + +```sh +BOOST_INCLUDE=/path/containing/boost python3 -B research/r420-target-pairs/verify.py --native +``` + +`CXX` selects the compiler. With system Boost headers, omit `BOOST_INCLUDE`. +Native checks cover 900, 1,380 and 1,620 formal columns, respectively, and 6, +18 and 24 omitted-bridge rejection controls. Two additional corruptions, +missing target restoration and an incorrect helper read, pass frame legality +but fail the formal-column checker at all three stage counts. The native +receipt also compares exact prefix bounds from an independent binary-record +parser against each C++ result. Temporary streams are removed after the run. + +## The identity and its complete local cost + +Let `K_a` and `K_b` be sets of helper indices in two original D rows. Addition +is over F2. The target inputs `u,v` and all helper contents `s` are arbitrary. +Write `A = K_a s`, `B = K_b s`. Replace the two direct helper sums by + +```text +y_a += y_b +y_b += K_b s +y_a += (K_a symmetric_difference K_b) s +y_a += y_b +``` + +The successive target states are + +```text +(u,v) -> (u+v,v) -> (u+v,v+B) -> (u+v+A+B,v+B) -> (u+A,v+B). +``` + +Thus the endpoint is exactly the original two-row operator. Helpers are only +read and never modified. There is no clean-register assumption. All operands +start and remain at frame zero throughout D, so there are no additional frame +changes, copies, source accesses or recursive children. Both target-to-target +additions are charged. The cost is `|K_b| + |K_a symmetric_difference K_b| + 2`, +instead of `|K_a| + |K_b|`. Disjoint target pairs cannot interfere, and the six +unpaired target rows retain their original operations. + +The changed D has more multi-input rows, 234 instead of 120. Counts in this +note are binary additions, after expanding every source operand. Neither a +multi-input row nor a restored target mixing operation is charged for free. + +## Explicit interface extension + +The original PR543 checker rejects the changed word at +`H2_D_frame0_targets_from_helpers` and `K_equals_D`. H2 forbids target sources +in D, and the literal K extractor assumes each D source is a helper input. +`verify.py` requires these two rejections to occur. It does not patch the +predecessor or report that its original H1–H5 contract accepts the new D. + +Replace only that syntactic D condition and literal extraction with the +following semantic condition, H2'. D executes first; every operand is a target +or helper at frame zero; D writes only targets; and its complete operator is +`(x,s,y) -> (x,s,y+Ks)`, with exactly the K of the original D. The independent +set-valued replay checks this on all 660 input columns. In particular, its +target-to-target endpoint block is the identity. H1's prohibition on target +feedback into sources or helpers is retained, even for F2-neutral feedback. + +The original raw word `W0 = A, scatter, B` and cleanup C are unchanged. +The pinned source audit proves their finite decomposition as +`(z,y) -> (Uz,y+Jx+Ks)`, with `J=I`, and C restores z. Substituting a D with +the same complete operator therefore leaves the complete scalar map +`(x,s,y) -> (x,s,y+x)` unchanged. The existing exact frame/scalar replay also +checks the changed word directly on all 660 columns. Its remaining interface +hypotheses and conclusions pass. Every frame path is compared exactly, and +the retained-copy frames are checked at the actual scatter boundary. + +This is a finite endpoint substitution and a written algebraic argument. It +does not formalize the all-size multiplication theorem or establish that a +downstream tool accepts H2'. + +## Search domain, scope and controls + +The OS assignment seed was **13**. All `120 × 119 = 14,280` oriented target +pairs were scored; 4,544 had positive complete local savings. One seed-13 +shuffle breaks ties before descending-gain greedy disjoint selection. That +single pass selected the 57 pairs in `recipe.json`; there were no restarts or +continuation searches. The verifier reproduces the nomination and freezes its +exact endpoint and cost. No maximum-matching or circuit-optimality claim is +made. Applying a known identity to D changes the compensation interface and +its measured cost; seed diversity alone is not the contribution. + +Nine negative controls reject removed initial mixing, removed final recovery, +a missing helper term, a nonzero D frame, target feedback into a helper, +F2-neutral feedback into a helper, source access at frame zero, an edit outside +D, and overlapping pairs. Every mutation must change the object and fail for +the expected reason. A positive F2-neutral target-pair control passes the +operator check but must pay two additional additions. These are finite tests, +not impossibility proofs or a formal proof of the full theorem. + +## Pins, predecessor credit and remaining work + +Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +The selected certificate at that base identifies **#626 with #543**, with +conditional `kappa = 51110230636731/31250000000000000`, approximately +`0.001635527380375392`. See the +[selected review](../../docs/research/community-k492-review.md). +Historical numbers in the R420 README are not the current selected result. + +The input is eumemic's [PR543](https://github.com/CrocSwap/integer-mult-bounds/pull/543), +source commit `2065fe4f72a914d907f1046603f5a36f17018535`. The two source pins in +`certificate.json` cover the decompressed word payload and the exact checker +bytes. `native.py` pins the six exporter, checker and header files it executes +from PR493's package. Gzip container bytes are deliberately not the identity. +PR493, #425 and the retained common-label interface supply the inherited +mutable-source and cleanup construction. + +Dugongue's [PR476](https://github.com/CrocSwap/integer-mult-bounds/pull/476), +head `e850569c33ad1d5771e2f8b1c6dfe7a445396167` at inspection, uses this reversible +target-factoring identity in phase B. DreamingOfClouds' PR450 is earlier +target-mixing precedent. This note claims neither invention of the identity +nor those submissions' bounds. + +Concurrent [PR686](https://github.com/CrocSwap/integer-mult-bounds/pull/686) and +[PR694](https://github.com/CrocSwap/integer-mult-bounds/pull/694) factor helper +columns in D and motivate a semantic D contract. Their inspected heads were +`23dcb610c2b156b76b9d599ea296c3cbde224b2d` and +`9732ac127dd4bef98a846aaa904c20b5a84e72c1`. This package instead factors target +rows, has no helper writes, imports no code from those pending PRs, and does +not combine their circuits. PR670/674/688 optimize phase-B blocks, and PR691 +optimizes a phase-A quad. Those are separate scopes. + +The final overlap refresh covered 528 open PRs. PR708 shares +phase-A decoder operands, while PR707/709 improve verification tooling. None +changes these target-row compensation pairs. No pinned coordination issue +existed at either check, so [the sprint claim](CLAIM.md) is local. + +The recursive profile is unchanged. No larger supplier exponent or kappa is +claimed. Hosted-parent regeneration, whole-owner accounting, finite invoices, +outer assembly and acceptance of H2' remain work for a future integration. +All-size compilation, common-label/mutable-basis realization, whole-call +hosting, normalized residual, precision/tape, exact recovery and analytic +transfer remain inherited assumptions. Local native payload checks do not +discharge them. No practical runtime speedup is claimed. + +## Validation record + +Local replay on 2026-10-13 used Python 3.14.8, macOS 26.5.2 arm64, Apple Clang +21.0.0 and Boost 1.92.0 headers. The standard-library verifier passed normally +and with `python3 -I -O -B`. The final native run also used `-I -O -B`; all +five-, nine- and eleven-stage checks and the two corruption controls passed. +Native records fall from 29,874 to 26,724, while 2,940 nested MOVEs, nine +COPY/ERASE pairs and the paid histogram remain unchanged. + +Gzip recompression with a different timestamp passed the payload pin; changed +decompressed source bytes were rejected. An independent audit reconstructed +the frozen D map without importing this verifier and separately recovered all +672 frame dimensions and the paid histogram. `make selected-record-check` +passed. No selected-frontier, predecessor or upstream file is edited. + +The repository-wide `make verify` target and selected cold supplier replay +were not run: this additive package changes neither selected supplier and +does not regenerate global artifacts. Linux execution, hosted-parent +reconstruction and outer assembly remain unchecked here. Native compiler and +Boost versions are environmental dependencies, not new repository dependencies. + +Contributor: Sagar Thakrar, with substantial OpenAI Codex assistance in the +search, implementation, written argument and review. Independent delegated +checks corroborated the endpoint and paid profile. New material is Apache-2.0; +predecessor sources, notices and `upstream/` are unchanged. diff --git a/research/r420-target-pairs/certificate.json b/research/r420-target-pairs/certificate.json new file mode 100644 index 0000000000..14ca1f99c8 --- /dev/null +++ b/research/r420-target-pairs/certificate.json @@ -0,0 +1,38 @@ +{ + "status": "finite circuit improvement; semantic D interface required; no new kappa", + "seed": 13, + "oriented_pairs_scored": 14280, + "positive_orientations": 4544, + "selected_disjoint_pairs": 57, + "D_additions_before": 19922, + "D_additions_after": 16772, + "total_additions_before": 26916, + "total_additions_after": 23766, + "saved_additions": 3150, + "symbolic_columns": 660, + "helpers": 420, + "copies": 9, + "frame_catalogue": {"labels": 120, "lattice_rank": 8, "gram_det": 1, "frames": 672}, + "paid_histogram": {"1": 1320, "2": 1440, "4": 60, "5": 120, "8": 9}, + "rank_mass": 5112, + "unchanged_frame_paths": 660, + "inherited_checks_rejected": ["H2_D_frame0_targets_from_helpers", "K_equals_D"], + "controls": {"negative": 9, "positive_paid_neutral_pair": 1}, + "positive_prefix_before": { + "forward": 144651, + "reverse": 2270064, + "local_payload_upper": 998206739997057013039187410944, + "local_payload_bits": 100 + }, + "positive_prefix_after": { + "forward": 144651, + "reverse": 3703810, + "local_payload_upper": 2657306775507971405724759110400, + "local_payload_bits": 102 + }, + "changed_word_canonical_sha256": "309cf1688f1027ec5ec182f5f6ccb8e5752e74ccd3ce017ced8bd45dfd7ff010", + "source_pins": { + "data/bitE8mut-r420.json.gz": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", + "code/xcheck.py": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424" + } +} diff --git a/research/r420-target-pairs/native.py b/research/r420-target-pairs/native.py new file mode 100644 index 0000000000..c786ba2efa --- /dev/null +++ b/research/r420-target-pairs/native.py @@ -0,0 +1,172 @@ +"""Unmodified PR493 cohort checkers for the target-pair experiment. + +Prepared by Sagar Thakrar with substantial OpenAI Codex assistance; Apache-2.0. +The checkers and exporter are credited to their authors in the pinned sources. +""" +import copy +import hashlib +import json +import os +from pathlib import Path +import shlex +import struct +import subprocess +import sys +import tempfile + + +SOURCE_HASHES = { + "code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "code/bit/regression/stage_cohort.py": "6c288f6f234b528c1a7c0a4adfb724e91e0fe6b18c8dffad96af3f973de1829a", + "code/bit/checkers/legality_h.cpp": "6c1ef2b24e57781d6951c172a1024fc4300e6fd392c9d6672079a7806ab663b3", + "code/bit/checkers/columns_k.cpp": "1c344d18fcd494eeca93e259f10cafae7705780e6592f6dcb35b34752dab9bc2", + "code/bit/checkers/json.hpp": "aaf127c04cb31c406e5b04a63f1ae89369fccde6d8fa7cdda1ed4f32dfc5de63", + "portable-include/bits/stdc++.h": "420094be2af295eed03a983dd66debbbe9cfb78d8252859f4498a615a0074b99", +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def positive_prefix(records, n): + """Exact integer replay of the cancellation-free local row bounds.""" + events = list(struct.iter_unpack("<6i", records.read_bytes())) + maxima = [] + for reverse in (False, True): + norms = [1] * (n + 1) + maximum = 1 + opened = False + for op, dst, src, coefficient, frame, rank in (reversed(events) if reverse else events): + if op == 0: + continue + if reverse and op in (2, 3): + op = 5 - op + if op == 1: + norms[dst] += abs(coefficient) * norms[src] + maximum = max(maximum, norms[dst]) + elif op == 2: + require(not opened, "nested prefix copy") + norms[n] = norms[dst] + opened = True + else: + require(op == 3 and opened, "invalid prefix erase") + norms[n] = 0 + opened = False + require(not opened, "unclosed prefix copy") + maxima.append(maximum) + forward, backward = maxima + payload = 64 * forward**3 * backward**2 + return { + "forward": str(forward), "reverse": str(backward), + "native_payload_upper": str(payload), "native_payload_bits": payload.bit_length(), + } + + +def verify_native(original_word, changed_word): + """Return fresh official 5/9/11-stage receipts and corruption controls.""" + package = Path(__file__).resolve().parents[1] / "e8-bit-carrier-skeleton" + for relative, expected in SOURCE_HASHES.items(): + require(hashlib.sha256((package / relative).read_bytes()).hexdigest() == expected, + "source hash mismatch: " + relative) + for word in (original_word, changed_word): + require((word["h"], word["v"], word["R"]) == (8, 120, 420), "wrong R420 dimensions") + bit = package / "code/bit" + checkers = bit / "checkers" + + def run(args, rejected=False): + result = subprocess.run(list(map(str, args)), text=True, capture_output=True) + if rejected: + require(result.returncode != 0, "native corruption control was accepted") + require("local defining-decoder full formal column" in result.stderr, + "unexpected native rejection: " + result.stderr) + elif result.returncode: + raise RuntimeError(f"command failed: {shlex.join(map(str, args))}\n{result.stderr}") + return result + + with tempfile.TemporaryDirectory(prefix="r420-target-pairs-") as temporary: + work = Path(temporary) + compiler = shlex.split(os.environ.get("CXX", "c++")) + flags = ["-O2", "-std=c++17", "-DHDIM=8", "-DNCOPY=9", "-DVPORTS=120", "-DRHELP=420", + "-I" + str(package / "portable-include"), "-I" + str(checkers), + "-I" + os.environ.get("BOOST_INCLUDE", "/usr/include")] + run([*compiler, *flags, checkers / "legality_h.cpp", "-o", work / "legality"]) + for pairs in (2, 4, 5): + run([*compiler, *flags, f"-DKPAIRS={pairs}", checkers / "columns_k.cpp", + "-o", work / f"columns-{pairs}"]) + + def export(word, name): + directory = work / name + directory.mkdir() + path = directory / "word.json" + path.write_text(json.dumps(word, separators=(",", ":"))) + run([sys.executable, "-I", "-B", bit / "export_records.py", path, directory / "records"]) + run([sys.executable, "-I", "-B", bit / "regression/stage_cohort.py", + directory / "records", directory / "records", directory / "cin", directory / "cout"]) + run([work / "legality", directory / "cin", directory / "cout", directory / "legality.json"]) + return directory + + def columns(directory, pairs): + output = directory / f"columns-{pairs}.json" + run([work / f"columns-{pairs}", directory / "cout/COHORT249-RECORDS.bin", output]) + receipt = json.loads(output.read_text()) + receipt.pop("seconds") + receipt.pop("local_scalar_stream") + require(receipt["formal_columns_checked"] == 2 * pairs * 120 + 420, "formal column count") + require(len(receipt["stages"]) == 2 * pairs + 1, "native stage count") + require(len(receipt["negative_controls"]) == 6 * (pairs - 1), "omitted bridge control count") + require(all(item["rejected"] for item in receipt["negative_controls"]), "bridge control accepted") + return receipt + + receipts = {} + for name, word in (("baseline", original_word), ("target_pairs", changed_word)): + directory = export(word, name) + prefix = positive_prefix(directory / "cout/COHORT249-RECORDS.bin", 660) + cohorts = {str(2 * pairs + 1): columns(directory, pairs) for pairs in (2, 4, 5)} + for receipt in cohorts.values(): + require([row["cancellation_free_signed_row_l1_upper"] + for row in receipt["signed_lift_prefix"]] == [prefix["forward"], prefix["reverse"]], + "independent positive prefix disagrees") + require(receipt["payload_prefix_upper"] == prefix["native_payload_upper"], "native payload differs") + require(receipt["payload_prefix_bits"] == prefix["native_payload_bits"], "native payload bits differ") + legality = json.loads((directory / "legality.json").read_text()) + receipts[name] = { + "legality": {key: legality[key] for key in ( + "status", "records", "common_frame_ADDs", "nested_MOVEs", "copies", "erasures", + "rank_mass", "paid_histogram", "all_final_frames_pass")}, + "prefix": prefix, + "cohorts": {stage: { + **{key: receipt[key] for key in ( + "status", "formal_columns_checked", "local_scalar_additions", "bridge_additions", + "fresh_center_copies", "reverse_fresh_center_copies", "local_raw_H")}, + "stage_count": len(receipt["stages"]), + "omitted_bridge_controls_rejected": len(receipt["negative_controls"]), + } for stage, receipt in cohorts.items()}, + } + + require(receipts["baseline"]["legality"]["paid_histogram"] == receipts["target_pairs"]["legality"]["paid_histogram"], + "paid histogram changed") + require(receipts["baseline"]["cohorts"]["5"]["local_raw_H"] == receipts["target_pairs"]["cohorts"]["5"]["local_raw_H"], + "local raw histogram changed") + controls = {} + dropped = copy.deepcopy(changed_word) + target_gates = [i for i, (_, dst, sources) in enumerate(dropped["D"]) + if 120 <= dst < 240 and any(120 <= source < 240 for source in sources)] + require(target_gates, "no target-pair gate to mutate") + del dropped["D"][target_gates[-1]] + wrong_helper = copy.deepcopy(changed_word) + for _, _, sources in wrong_helper["D"]: + if any(source >= 240 for source in sources): + index = next(i for i, source in enumerate(sources) if source >= 240) + sources[index] = next(source for source in range(240, 660) if source not in sources) + break + else: + raise AssertionError("no helper read to mutate") + for name, mutant in (("dropped_target_unmix", dropped), ("wrong_helper_read", wrong_helper)): + directory = export(mutant, name) + for pairs in (2, 4, 5): + run([work / f"columns-{pairs}", directory / "cout/COHORT249-RECORDS.bin", + directory / f"columns-{pairs}.json"], rejected=True) + controls[name] = {"legality_passed": True, "formal_columns_rejected_stages": [5, 9, 11]} + return {"source_sha256": SOURCE_HASHES, "receipts": receipts, "negative_controls": controls} diff --git a/research/r420-target-pairs/recipe.json b/research/r420-target-pairs/recipe.json new file mode 100644 index 0000000000..be9c4640b7 --- /dev/null +++ b/research/r420-target-pairs/recipe.json @@ -0,0 +1,17 @@ +{ + "seed": 13, + "pairs": [ + [222,219], [234,236], [239,233], [137,143], [148,145], + [128,134], [200,156], [224,230], [174,173], [193,194], + [131,133], [141,139], [214,208], [181,198], [205,154], + [197,199], [176,182], [191,185], [189,187], [221,216], + [178,170], [209,211], [140,138], [149,144], [232,238], + [237,235], [146,151], [125,123], [218,223], [155,175], + [184,171], [231,225], [142,136], [183,177], [229,227], + [202,126], [196,160], [135,129], [210,212], [195,192], + [122,124], [158,152], [179,213], [220,217], [165,161], + [166,163], [121,127], [168,157], [226,228], [167,159], + [169,188], [206,203], [215,162], [150,190], [186,153], + [132,172], [180,147] + ] +} diff --git a/research/r420-target-pairs/verify.py b/research/r420-target-pairs/verify.py new file mode 100644 index 0000000000..f45dc3682e --- /dev/null +++ b/research/r420-target-pairs/verify.py @@ -0,0 +1,288 @@ +#!/usr/bin/env python3 +"""Exact finite R420 target-row compensation construction. Apache-2.0. + +Sagar Thakrar, with substantial OpenAI Codex assistance. The target-basis +identity follows Dugongue's PR476; the pinned word/checker are eumemic's PR543. +""" +import argparse +import copy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import random +from collections import Counter + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / "research/e8-bit-r420" +PINS = { + "data/bitE8mut-r420.json.gz": + "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", + "code/xcheck.py": + "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424", +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load_source(): + for name, expected in PINS.items(): + data = (SOURCE / name).read_bytes() + if name.endswith(".gz"): + data = gzip.decompress(data) + need(hashlib.sha256(data).hexdigest() == expected, "source pin: " + name) + return json.loads(gzip.decompress((SOURCE / "data/bitE8mut-r420.json.gz").read_bytes())) + + +def rows(word): + need(len(word["D"]) == word["v"], "source must have one D row per target") + result = {d: set(srcs) for _, d, srcs in word["D"]} + need(len(result) == word["v"], "duplicate source D destination") + return result + + +def nominate(word, seed): + """One bounded greedy matching; exhaustive pair scoring is not optimal matching.""" + matrix = rows(word) + candidates = [] + for a in sorted(matrix): + for b in sorted(matrix): + if a != b: + gain = len(matrix[a]) - len(matrix[a] ^ matrix[b]) - 2 + if gain > 0: + candidates.append((gain, a, b)) + random.Random(seed).shuffle(candidates) + candidates.sort(key=lambda item: -item[0]) + used, pairs = set(), [] + for _, a, b in candidates: + if a not in used and b not in used: + pairs.append([a, b]) + used.update((a, b)) + return pairs, len(candidates) + + +def construct(word, pairs): + matrix = rows(word) + zero = word["frames"].index([]) + changed = copy.deepcopy(word) + gates, used = [], set() + for a, b in pairs: + need(a in matrix and b in matrix and a != b, "invalid target pair") + need(a not in used and b not in used, "target pairs overlap") + used.update((a, b)) + gates.append([zero, a, [b]]) + gates.append([zero, b, sorted(matrix[b])]) + difference = sorted(matrix[a] ^ matrix[b]) + if difference: + gates.append([zero, a, difference]) + gates.append([zero, a, [b]]) + gates.extend(copy.deepcopy(g) for g in word["D"] if g[1] not in used) + changed["D"] = gates + return changed + + +def check_prefix(original, changed): + """Independent set-valued D replay, including all arbitrary target inputs.""" + need(original.keys() == changed.keys(), "word fields changed") + need(all(original[k] == changed[k] for k in original if k != "D"), + "field outside D changed") + v, n = original["v"], 2 * original["v"] + original["R"] + zero = original["frames"].index([]) + values = [{r} for r in range(n)] + for frame, dest, sources in changed["D"]: + need(frame == zero, "D must stay at frame zero") + need(v <= dest < 2 * v, "D must write only targets") + need(sources and all(v <= s < n and s != dest for s in sources) + and len(sources) == len(set(sources)), "invalid D operands") + for src in sources: + values[dest].symmetric_difference_update(values[src]) + matrix = rows(original) + for r in range(n): + expected = {r} ^ matrix[r] if r in matrix else {r} + need(values[r] == expected, "D endpoint differs at register " + str(r)) + return n + + +def frame_paths(word): + paths = [[frame] for frame in word["start"]] + for section in ("D", "A", "B", "C"): + for frame, dest, sources in word[section]: + for reg in [dest] + sources: + if paths[reg][-1] != frame: + paths[reg].append(frame) + for reg, frame in enumerate(word["final"]): + if paths[reg][-1] != frame: + paths[reg].append(frame) + return paths + + +def additions(word): + return sum(len(g[2]) for sec in ("D", "A", "B", "C") for g in word[sec]) + sum( + len(row) for row in word["scatter"]) + + +def positive_prefix(word): + """Lower to scalar ADD/COPY events; price the signed lift without cancellation.""" + n, v = 2 * word["v"] + word["R"], word["v"] + events = [] + for section in ("D", "A", "scatter", "B", "C"): + if section == "scatter": + for k, register in enumerate(word["ret"]): + events.append((2, register, 0)) + events.extend((1, v + t, n) for t, row in enumerate(word["scatter"]) if k in row) + events.append((3, register, 0)) + else: + events.extend((1, dest, src) for _, dest, sources in word[section] for src in sources) + peaks = [] + for reverse in (False, True): + values, peak = [1] * (n + 1), 1 + for op, dest, src in reversed(events) if reverse else events: + if reverse and op in (2, 3): + op = 5 - op + if op == 1: + values[dest] += values[src] + peak = max(peak, values[dest]) + elif op == 2: + values[n] = values[dest] + else: + values[n] = 0 + peaks.append(peak) + forward, backward = peaks + payload = 64 * forward ** 3 * backward ** 2 + need(payload < 2 ** 104, "local native payload exceeds inherited cap") + return {"forward": forward, "reverse": backward, + "local_payload_upper": payload, "local_payload_bits": payload.bit_length()} + + +def controls(original, changed, pairs): + cases = [] + mutant = copy.deepcopy(changed) + del mutant["D"][0] + cases.append(("missing initial target mix", mutant, "D endpoint differs")) + mutant = copy.deepcopy(changed) + del mutant["D"][3] + cases.append(("missing final target unmix", mutant, "D endpoint differs")) + mutant = copy.deepcopy(changed) + mutant["D"][2][2].pop() + cases.append(("missing helper contribution", mutant, "D endpoint differs")) + mutant = copy.deepcopy(changed) + mutant["D"][0][0] = original["final"][0] + cases.append(("illegal nonzero D frame", mutant, "D must stay")) + mutant = copy.deepcopy(changed) + mutant["D"][0][1] = 2 * original["v"] + cases.append(("target feeds helper", mutant, "D must write only targets")) + mutant = copy.deepcopy(changed) + forbidden = [original["frames"].index([]), 2 * original["v"], [pairs[0][0]]] + mutant["D"] += [forbidden, copy.deepcopy(forbidden)] + cases.append(("neutral target feedback into helper", mutant, "D must write only targets")) + mutant = copy.deepcopy(changed) + mutant["D"][0][2] = [0] + cases.append(("source access at frame zero", mutant, "invalid D operands")) + mutant = copy.deepcopy(changed) + mutant["A"][0][2].pop() + cases.append(("mutation outside claimed scope", mutant, "field outside D")) + for name, mutant, reason in cases: + need(mutant != changed, "negative control did not mutate: " + name) + try: + check_prefix(original, mutant) + except ValueError as error: + need(reason in str(error), name + " failed for the wrong reason") + else: + raise ValueError("accepted negative control: " + name) + try: + construct(original, pairs + pairs[:1]) + except ValueError as error: + need("overlap" in str(error), "wrong overlapping-pair rejection") + else: + raise ValueError("accepted overlapping pairs") + # An F2-neutral pair is legal but must still pay for both additions. + neutral = copy.deepcopy(changed) + gate = [original["frames"].index([]), pairs[0][0], [pairs[0][1]]] + neutral["D"] += [gate, copy.deepcopy(gate)] + check_prefix(original, neutral) + need(additions(neutral) == additions(changed) + 2, "neutral pair underpriced") + return {"negative": len(cases) + 1, "positive_paid_neutral_pair": 1} + + +def verify(): + original = load_source() + recipe = json.loads((HERE / "recipe.json").read_text()) + pairs, positive = nominate(original, recipe["seed"]) + need(pairs == recipe["pairs"], "frozen recipe differs from bounded nomination") + changed = construct(original, pairs) + columns = check_prefix(original, changed) + spec = importlib.util.spec_from_file_location("r420_source_xcheck", SOURCE / "code/xcheck.py") + checker = importlib.util.module_from_spec(spec) + spec.loader.exec_module(checker) + audited, labels, _, hypotheses, conclusion, _ = checker.check(original) + need(all(hypotheses.values()) and all(conclusion.values()), "source interface failed") + # Geometry is unchanged. Reuse only the exact frame catalogue and its audit. + audited.w = changed + audited.full() + new_hypotheses, new_conclusion, _ = audited.interface() + failed = [key for key, value in {**new_hypotheses, **new_conclusion}.items() if not value] + need(failed == ["H2_D_frame0_targets_from_helpers", "K_equals_D"], + "unexpected inherited interface result: " + str(failed)) + before_paths, after_paths = frame_paths(original), frame_paths(changed) + need(before_paths == after_paths, "physical frame paths changed") + histogram = Counter() + for path in after_paths: + for a, b in zip(path, path[1:]): + histogram[audited.fdim[b] - audited.fdim[a]] += 1 + copy_frames = list(changed["start"]) + for section in ("D", "A"): + for frame, dest, sources in changed[section]: + for reg in [dest] + sources: + copy_frames[reg] = frame + for reg in changed["ret"]: + need(audited.fdim[copy_frames[reg]] == original["h"], "copy is not at full frame") + histogram[audited.fdim[copy_frames[reg]]] += 1 + rank_mass = sum(rank * count for rank, count in histogram.items()) + controls_result = controls(original, changed, pairs) + result = { + "status": "finite circuit improvement; semantic D interface required; no new kappa", + "seed": recipe["seed"], "oriented_pairs_scored": original["v"] * (original["v"] - 1), + "positive_orientations": positive, "selected_disjoint_pairs": len(pairs), + "D_additions_before": sum(len(g[2]) for g in original["D"]), + "D_additions_after": sum(len(g[2]) for g in changed["D"]), + "total_additions_before": additions(original), "total_additions_after": additions(changed), + "saved_additions": additions(original) - additions(changed), + "symbolic_columns": columns, "helpers": original["R"], "copies": len(original["ret"]), + "frame_catalogue": labels, "paid_histogram": dict(sorted(histogram.items())), + "rank_mass": rank_mass, "unchanged_frame_paths": len(after_paths), + "inherited_checks_rejected": failed, "controls": controls_result, + "positive_prefix_before": positive_prefix(original), + "positive_prefix_after": positive_prefix(changed), + "changed_word_canonical_sha256": hashlib.sha256(json.dumps( + changed, sort_keys=True, separators=(",", ":")).encode()).hexdigest(), + "source_pins": PINS, + } + return original, changed, result + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--report", action="store_true", help="print the exact replay receipt") + parser.add_argument("--native", action="store_true", help="also run original C++ cohort checkers") + args = parser.parse_args() + original, changed, receipt = verify() + expected = HERE / "certificate.json" + need(expected.is_file(), "missing frozen certificate") + need(json.loads(json.dumps(receipt)) == json.loads(expected.read_text()), "certificate mismatch") + if args.native: + spec = importlib.util.spec_from_file_location("r420_target_pairs_native", HERE / "native.py") + native = importlib.util.module_from_spec(spec) + spec.loader.exec_module(native) + native_receipt = native.verify_native(original, changed) + print(json.dumps(native_receipt, indent=2, sort_keys=True)) + if args.report: + print(json.dumps(receipt, indent=2, sort_keys=True)) + print("PASS_R420_TARGET_PAIRS D=%d->%d ADDs=%d->%d saved=%d columns=%d rank_mass=%d" % ( + receipt["D_additions_before"], receipt["D_additions_after"], + receipt["total_additions_before"], receipt["total_additions_after"], + receipt["saved_additions"], receipt["symbolic_columns"], receipt["rank_mass"])) From afeb452f58ff0cbf109172335e2ba282aac3dcde Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Tue, 13 Oct 2026 10:19:25 +0530 Subject: [PATCH 2/2] Certify the optimal 3250-addition disjoint target matching --- research/r420-target-pairs/CLAIM.md | 24 +++++ research/r420-target-pairs/README.md | 92 ++++++++++++++----- research/r420-target-pairs/certificate.json | 17 +++- research/r420-target-pairs/matching-dual.json | 11 +++ research/r420-target-pairs/recipe.json | 24 ++--- research/r420-target-pairs/verify.py | 37 +++++++- 6 files changed, 161 insertions(+), 44 deletions(-) create mode 100644 research/r420-target-pairs/matching-dual.json diff --git a/research/r420-target-pairs/CLAIM.md b/research/r420-target-pairs/CLAIM.md index 8b4d4b521f..188fdd108f 100644 --- a/research/r420-target-pairs/CLAIM.md +++ b/research/r420-target-pairs/CLAIM.md @@ -27,3 +27,27 @@ basis and row-factoring work. The claim is local because no pinned coordination issue exists. Delegated work stays within this D-stage construction. Contributor: Sagar Thakrar, with substantial OpenAI Codex assistance. + +## Result + +Completed contribution: [PR716](https://github.com/CrocSwap/integer-mult-bounds/pull/716). +The final circuit uses 60 pairs and saves **3,250 additions**, reducing D from +19,922 to 16,672 and the whole local word from 26,916 to 23,666. An exact +120-vertex price certificate bounds every disjoint pairing by 3,250, proving +optimality only in this four-operation pair-substitution class. + +The immediate submission refresh found Scott Woolsey Biggart's concurrent +PR713, which independently saved 3,150 additions with 57 pairs. One bounded +pivot replaced the greedy pass with a maximum-weight matching nomination. +Independent integer assignment prices supplied the upper bound. PR713 is +credited; this submission adds 100 saved additions and the complete restricted +optimality certificate. The same PR was updated, without opening another. + +The exact 660-column replay, all frame paths, paid histogram and positive +prefixes passed. Fresh native 5/9/11-stage checks passed on both source and +final words, with bridge and corruption controls. The reverse bound is +3,703,810 and local payload allowance 102 bits, below 104. Source pins, +optimized/isolated Python execution and selected-record integrity passed. +Full hosted accounting and acceptance of the semantic D interface remain +open; no new kappa is claimed. No pinned coordination issue existed, so this +is the single local claim update with the result and submission link. diff --git a/research/r420-target-pairs/README.md b/research/r420-target-pairs/README.md index 5864b0c8f0..0f87a399d9 100644 --- a/research/r420-target-pairs/README.md +++ b/research/r420-target-pairs/README.md @@ -1,19 +1,25 @@ # R420 compensation with disjoint target pairs **Finite circuit improvement; no new kappa.** On eumemic's PR543 R420 word, -57 disjoint target pairs reduce the frame-zero D compensation from **19,922 -to 16,772 binary XOR additions**. The complete local word drops from **26,916 -to 23,766 additions**, a saving of 3,150, including preparation and restoration. +60 disjoint target pairs reduce the frame-zero D compensation from **19,922 +to 16,672 binary XOR additions**. The complete local word drops from **26,916 +to 23,666 additions**, a saving of 3,250, including preparation and restoration. Every source and helper keeps its original value at the D boundary. +A small vertex-price certificate proves that **3,250 is optimal within this +disjoint target-pair substitution class**. This adds 100 saved additions beyond +concurrent [PR713](https://github.com/CrocSwap/integer-mult-bounds/pull/713), +which independently found a 3,150-addition saving. Neither result is a new +supplier exponent or a claim about arbitrary compensation circuits. + The complete physical frame paths, 420 helpers, nine retained copies and paid rank mass 5,112 are unchanged. The reverse positive-prefix bound grows, so this is not a free substitution into a previously certified hosted invoice. | Local quantity | PR543 source | Target-pair word | | --- | ---: | ---: | -| D binary additions | 19,922 | 16,772 | -| All binary additions | 26,916 | 23,766 | +| D binary additions | 19,922 | 16,672 | +| All binary additions | 26,916 | 23,666 | | Forward positive-prefix bound | 144,651 | 144,651 | | Reverse positive-prefix bound | 2,270,064 | 3,703,810 | | Local native payload bits | 100 | 102 | @@ -35,13 +41,13 @@ python3 -B research/r420-target-pairs/verify.py Expected output: ```text -PASS_R420_TARGET_PAIRS D=19922->16772 ADDs=26916->23766 saved=3150 columns=660 rank_mass=5112 +PASS_R420_TARGET_PAIRS D=19922->16672 ADDs=26916->23666 saved=3250 columns=660 rank_mass=5112 ``` `--report` prints the exact receipt, which must match `certificate.json`. The recipe and pinned source reconstruct the entire changed word in memory; its canonical JSON SHA-256 is -`309cf1688f1027ec5ec182f5f6ccb8e5752e74ccd3ce017ced8bd45dfd7ff010`. +`814b845afa056f6bce4e566e87494d591c6776092772748b509aead2959e0bff`. No generated word or changes to predecessor files are needed. To also run the unchanged native exporter, legality checker and five-, nine- @@ -84,10 +90,10 @@ read and never modified. There is no clean-register assumption. All operands start and remain at frame zero throughout D, so there are no additional frame changes, copies, source accesses or recursive children. Both target-to-target additions are charged. The cost is `|K_b| + |K_a symmetric_difference K_b| + 2`, -instead of `|K_a| + |K_b|`. Disjoint target pairs cannot interfere, and the six -unpaired target rows retain their original operations. +instead of `|K_a| + |K_b|`. Disjoint target pairs cannot interfere. The final +recipe pairs all 120 targets. -The changed D has more multi-input rows, 234 instead of 120. Counts in this +The changed D has more multi-input rows, 240 instead of 120. Counts in this note are binary additions, after expanding every source operand. Neither a multi-input row nor a restored target mixing operation is charged for free. @@ -120,23 +126,56 @@ This is a finite endpoint substitution and a written algebraic argument. It does not formalize the all-size multiplication theorem or establish that a downstream tool accepts H2'. -## Search domain, scope and controls +## Exact optimum in the disjoint-pair class + +The domain consists of arbitrary disjoint target pairs, either orientation +for each pair, and unchanged D rows for any unpaired targets. Each pair uses +exactly the four-operation identity above with both mixing operations paid. +For distinct targets i,j, let + +```text +w_ij = max(0, max(|K_i|, |K_j|) - |K_i symmetric_difference K_j| - 2). +``` + +This is the best nonnegative saving from that pair. In `matching-dual.json`, +`twice_vertex_prices` gives 120 integers q_i in target order 120 through 239. +The independent, integer-only checker verifies + +```text +q_i >= 0 for all 120 targets +q_i + q_j >= 2*w_ij for all 7,140 unordered pairs +sum_i q_i = 6,500. +``` -The OS assignment seed was **13**. All `120 × 119 = 14,280` oriented target -pairs were scored; 4,544 had positive complete local savings. One seed-13 -shuffle breaks ties before descending-gain greedy disjoint selection. That -single pass selected the 57 pairs in `recipe.json`; there were no restarts or -continuation searches. The verifier reproduces the nomination and freezes its -exact endpoint and cost. No maximum-matching or circuit-optimality claim is -made. Applying a known identity to D changes the compensation interface and -its measured cost; seed diversity alone is not the contribution. +For any disjoint matching M, summing its edge inequalities gives +`2*sum_M w_ij <= sum_used q_i <= sum_all q_i = 6,500`. Thus no matching in +this class saves more than 3,250 additions. The 60-pair recipe has actual +oriented saving exactly 3,250, so it attains the upper bound. This proves the +restricted optimum without trusting a matching solver. It makes no claim +about larger target blocks, overlapping transformations or helper factoring. + +The OS assignment seed was **13**. All `120 × 119 = 14,280` orientations were +scored; 4,544 had positive complete local savings. The original single seed-13 +greedy pass saved 3,150. Concurrent PR713 reported that same saving before +submission, so one bounded pivot replaced greedy selection by a maximum-weight +matching nomination on the 3,280 positive undirected edges. NetworkX 3.5, +with seed-13 shuffled edge insertion, nominated the final matching. A separate +integer Hungarian assignment calculation produced the vertex prices and an +attaining matching independently. Neither solver is imported or required by +the shipped verifier. The exact frozen witness and feasible prices, rather +than a solver's success message, establish the result. The stopping rule was +one matching solve followed by the independent matching-bound certificate; +there was no search beyond this class. + +## Controls Nine negative controls reject removed initial mixing, removed final recovery, a missing helper term, a nonzero D frame, target feedback into a helper, F2-neutral feedback into a helper, source access at frame zero, an edit outside D, and overlapping pairs. Every mutation must change the object and fail for the expected reason. A positive F2-neutral target-pair control passes the -operator check but must pay two additional additions. These are finite tests, +operator check but must pay two additional additions. A tenth negative +control lowers one vertex price and must fail an edge inequality. These are finite tests, not impossibility proofs or a formal proof of the full theorem. ## Pins, predecessor credit and remaining work @@ -171,10 +210,15 @@ rows, has no helper writes, imports no code from those pending PRs, and does not combine their circuits. PR670/674/688 optimize phase-B blocks, and PR691 optimizes a phase-A quad. Those are separate scopes. -The final overlap refresh covered 528 open PRs. PR708 shares +The pre-submission overlap refresh covered 534 open PRs. PR708 shares phase-A decoder operands, while PR707/709 improve verification tooling. None -changes these target-row compensation pairs. No pinned coordination issue -existed at either check, so [the sprint claim](CLAIM.md) is local. +of those changes these target rows. Scott Woolsey Biggart's PR713 appeared +in the final refresh at head `1a19af5c5ddb6de9797a6d085e5df0b90ed6d58b` and +independently constructed 57 target pairs with saving 3,150. The original +version of this package corroborated that value. This final version adds the +60-pair circuit and a solver-independent 3,250 upper bound for the full +disjoint-pair class. It claims no priority for target-row factoring. No pinned +coordination issue existed, so [the sprint claim](CLAIM.md) is local. The recursive profile is unchanged. No larger supplier exponent or kappa is claimed. Hosted-parent regeneration, whole-owner accounting, finite invoices, @@ -190,7 +234,7 @@ Local replay on 2026-10-13 used Python 3.14.8, macOS 26.5.2 arm64, Apple Clang 21.0.0 and Boost 1.92.0 headers. The standard-library verifier passed normally and with `python3 -I -O -B`. The final native run also used `-I -O -B`; all five-, nine- and eleven-stage checks and the two corruption controls passed. -Native records fall from 29,874 to 26,724, while 2,940 nested MOVEs, nine +Native records fall from 29,874 to 26,624, while 2,940 nested MOVEs, nine COPY/ERASE pairs and the paid histogram remain unchanged. Gzip recompression with a different timestamp passed the payload pin; changed diff --git a/research/r420-target-pairs/certificate.json b/research/r420-target-pairs/certificate.json index 14ca1f99c8..0dc3f294f5 100644 --- a/research/r420-target-pairs/certificate.json +++ b/research/r420-target-pairs/certificate.json @@ -3,12 +3,19 @@ "seed": 13, "oriented_pairs_scored": 14280, "positive_orientations": 4544, - "selected_disjoint_pairs": 57, + "selected_disjoint_pairs": 60, + "greedy_saved_additions": 3150, + "matching_optimality": { + "unordered_pairs_covered": 7140, + "twice_upper_bound": 6500, + "optimal_saving_in_disjoint_pair_class": 3250 + }, + "underpriced_dual_rejected": true, "D_additions_before": 19922, - "D_additions_after": 16772, + "D_additions_after": 16672, "total_additions_before": 26916, - "total_additions_after": 23766, - "saved_additions": 3150, + "total_additions_after": 23666, + "saved_additions": 3250, "symbolic_columns": 660, "helpers": 420, "copies": 9, @@ -30,7 +37,7 @@ "local_payload_upper": 2657306775507971405724759110400, "local_payload_bits": 102 }, - "changed_word_canonical_sha256": "309cf1688f1027ec5ec182f5f6ccb8e5752e74ccd3ce017ced8bd45dfd7ff010", + "changed_word_canonical_sha256": "814b845afa056f6bce4e566e87494d591c6776092772748b509aead2959e0bff", "source_pins": { "data/bitE8mut-r420.json.gz": "e597e3885c0a8daa262afa5985ee2930443329126aece76d33159d81882bdcc2", "code/xcheck.py": "5737d18a7826fd51e131035f2d7bebba2e2868af91dd7672a5f11208b036d424" diff --git a/research/r420-target-pairs/matching-dual.json b/research/r420-target-pairs/matching-dual.json new file mode 100644 index 0000000000..3d62a14129 --- /dev/null +++ b/research/r420-target-pairs/matching-dual.json @@ -0,0 +1,11 @@ +{ + "first_target": 120, + "twice_vertex_prices": [ + 34,41,39,42,51,66,48,33,87,38,29,93,27,55,81,65,49,101,62,68, + 58,74,55,81,50,78,59,17,92,64,23,53,44,19,45,67,43,40,44,5, + 57,38,31,32,23,48,52,55,30,39,57,41,5,85,67,41,69,48,65,48, + 16,78,61,52,65,72,31,63,23,63,27,56,38,93,57,54,58,62,58,70, + 115,21,56,33,5,89,26,32,57,63,57,57,45,41,81,34,51,47,54,87, + 41,71,103,54,75,33,43,52,25,48,83,71,64,111,102,51,86,61,50,77 + ] +} diff --git a/research/r420-target-pairs/recipe.json b/research/r420-target-pairs/recipe.json index be9c4640b7..aaade9764d 100644 --- a/research/r420-target-pairs/recipe.json +++ b/research/r420-target-pairs/recipe.json @@ -1,17 +1,17 @@ { "seed": 13, "pairs": [ - [222,219], [234,236], [239,233], [137,143], [148,145], - [128,134], [200,156], [224,230], [174,173], [193,194], - [131,133], [141,139], [214,208], [181,198], [205,154], - [197,199], [176,182], [191,185], [189,187], [221,216], - [178,170], [209,211], [140,138], [149,144], [232,238], - [237,235], [146,151], [125,123], [218,223], [155,175], - [184,171], [231,225], [142,136], [183,177], [229,227], - [202,126], [196,160], [135,129], [210,212], [195,192], - [122,124], [158,152], [179,213], [220,217], [165,161], - [166,163], [121,127], [168,157], [226,228], [167,159], - [169,188], [206,203], [215,162], [150,190], [186,153], - [132,172], [180,147] + [126,120], [121,127], [122,124], [125,123], [128,134], + [206,129], [212,130], [131,133], [132,172], [135,204], + [142,136], [137,143], [140,138], [141,139], [149,144], + [148,145], [146,151], [150,147], [158,152], [186,153], + [205,154], [155,175], [200,156], [168,157], [167,159], + [160,201], [165,161], [162,213], [166,163], [178,164], + [170,169], [184,171], [173,174], [176,182], [183,177], + [215,179], [196,180], [181,198], [191,185], [189,187], + [190,188], [195,192], [193,194], [197,199], [202,207], + [210,203], [214,208], [209,211], [221,216], [220,217], + [218,223], [222,219], [224,230], [231,225], [226,228], + [229,227], [232,238], [239,233], [234,236], [237,235] ] } diff --git a/research/r420-target-pairs/verify.py b/research/r420-target-pairs/verify.py index f45dc3682e..f74a614c9c 100644 --- a/research/r420-target-pairs/verify.py +++ b/research/r420-target-pairs/verify.py @@ -46,7 +46,7 @@ def rows(word): return result -def nominate(word, seed): +def greedy_baseline(word, seed): """One bounded greedy matching; exhaustive pair scoring is not optimal matching.""" matrix = rows(word) candidates = [] @@ -66,6 +66,25 @@ def nominate(word, seed): return pairs, len(candidates) +def check_matching_dual(word, pairs, dual): + """Vertex prices upper-bound every disjoint matching; equality proves this class's optimum.""" + matrix = rows(word) + prices = dual["twice_vertex_prices"] + need(dual["first_target"] == word["v"] and len(prices) == word["v"], "dual target domain") + need(all(type(p) is int and p >= 0 for p in prices), "dual prices must be nonnegative integers") + for a in sorted(matrix): + for b in sorted(matrix): + if a < b: + weight = max(0, max(len(matrix[a]), len(matrix[b])) - len(matrix[a] ^ matrix[b]) - 2) + need(prices[a - word["v"]] + prices[b - word["v"]] >= 2 * weight, + "dual edge inequality failed") + need(len({v for pair in pairs for v in pair}) == 2 * len(pairs), "dual witness pairs overlap") + saving = sum(len(matrix[a]) - len(matrix[a] ^ matrix[b]) - 2 for a, b in pairs) + need(sum(prices) == 2 * saving, "dual objective differs from matching saving") + return {"unordered_pairs_covered": word["v"] * (word["v"] - 1) // 2, + "twice_upper_bound": sum(prices), "optimal_saving_in_disjoint_pair_class": saving} + + def construct(word, pairs): matrix = rows(word) zero = word["frames"].index([]) @@ -212,8 +231,18 @@ def controls(original, changed, pairs): def verify(): original = load_source() recipe = json.loads((HERE / "recipe.json").read_text()) - pairs, positive = nominate(original, recipe["seed"]) - need(pairs == recipe["pairs"], "frozen recipe differs from bounded nomination") + greedy, positive = greedy_baseline(original, recipe["seed"]) + pairs = recipe["pairs"] + dual = json.loads((HERE / "matching-dual.json").read_text()) + matching_proof = check_matching_dual(original, pairs, dual) + corrupted_dual = copy.deepcopy(dual) + corrupted_dual["twice_vertex_prices"][0] -= 1 + try: + check_matching_dual(original, pairs, corrupted_dual) + except ValueError as error: + need("dual edge inequality" in str(error), "wrong underpriced-dual rejection") + else: + raise ValueError("accepted underpriced dual") changed = construct(original, pairs) columns = check_prefix(original, changed) spec = importlib.util.spec_from_file_location("r420_source_xcheck", SOURCE / "code/xcheck.py") @@ -248,6 +277,8 @@ def verify(): "status": "finite circuit improvement; semantic D interface required; no new kappa", "seed": recipe["seed"], "oriented_pairs_scored": original["v"] * (original["v"] - 1), "positive_orientations": positive, "selected_disjoint_pairs": len(pairs), + "greedy_saved_additions": additions(original) - additions(construct(original, greedy)), + "matching_optimality": matching_proof, "underpriced_dual_rejected": True, "D_additions_before": sum(len(g[2]) for g in original["D"]), "D_additions_after": sum(len(g[2]) for g in changed["D"]), "total_additions_before": additions(original), "total_additions_after": additions(changed),