diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). diff --git a/research/historical-selected-replay-gap/README.md b/research/historical-selected-replay-gap/README.md index 55d8cc3b49..36d9a873ca 100644 --- a/research/historical-selected-replay-gap/README.md +++ b/research/historical-selected-replay-gap/README.md @@ -69,7 +69,11 @@ python3 -B scripts/research_package.py --package research/historical-selected-re The direct command prints `PASS_HISTORICAL_SELECTED_REPLAY_GAP`. A registered replay prints `PASS_REGISTERED_RESEARCH_PACKAGE`. Both require Git history -containing the two inspected commits. +containing the two inspected commits and the source and manifest objects at +`2485805a6d47f36ea83ddde6327d453ac82d44dc`. The verifier uses a temporary +sparse checkout of that commit, checks the declared source digests there, and +uses its planner and manifest inventory. The recorded rejections and selection +therefore remain reproducible after later changes to the live Makefile or CI guide. ## Open next questions diff --git a/research/historical-selected-replay-gap/SOURCES.json b/research/historical-selected-replay-gap/SOURCES.json index c1010eec95..62bb8b3950 100644 --- a/research/historical-selected-replay-gap/SOURCES.json +++ b/research/historical-selected-replay-gap/SOURCES.json @@ -4,13 +4,13 @@ "files": [ { "path": "Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "0d683a06b9e7ee162496108ce9a7c5d2ee94fccf", "sha256": "4f2d4f2dcd15139ec82658a975f85ed300897385f85799218539f4c8d60567da" }, { "path": "certificates/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "eccafa830c16170c36faf93045ddf1f638f7bcd4", "sha256": "4c0b9d37e1034b2076e30a70f8e514416298c462d9ee98bc87fe6556b14df786" }, @@ -22,7 +22,7 @@ }, { "path": "docs/ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "63ba3e9aa8bdc5e942b56e34244b92b16f854085", "sha256": "c7d3027e9ad8bcbff68f07aa9576b30fb2f3c76c44d876d40c7fdbf4a3e2228a" }, @@ -34,163 +34,163 @@ }, { "path": "research/clifford-state-performance/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "6f98a0061a5104dfab82c9e806f819b41811f684", "sha256": "396d0f08df24952248140d5c65c51b8c902ef1c580892ff7ea182890530f67ee" }, { "path": "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "5e0f92af463ec12c5e1dcc3effd44081a88af647", "sha256": "07a9daeaf2bda308a92e9a4684f13d5fc766c7772d74801fceb7f4599fdab226" }, { "path": "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "9e13266bf85e627f1b7dc225e9530ea69fd2c7f0", "sha256": "421e1211fb1897c45621dc6801c276e53f2e6f335583c9c9049e535f87c0a3b1" }, { "path": "research/community-batch932-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "cc4d03eb59b9ab3f952735f7e88ff18c2d15d7af", "sha256": "184629cac91a5cfaca50330a88596008b824221433867dcf8117539c913c284a" }, { "path": "research/community-batch970-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8b9f4111badf7de5d97684799560b55110e9da79", "sha256": "23188ed920e38a54006cb883e181585620821c63bf7e8b5e05d32719417cc37e" }, { "path": "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "a5300d4e7a5381a3f443fc54c768ca6f0f236d68", "sha256": "3c820fb30e1b4d9bcfc6a7ab524375e5b2abd66b940af2c509146104f0bcd79c" }, { "path": "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "usage": "input", + "usage": "provenance", "git_blob": "d7ff6d777b01d69b6ce84caf25d3b7e4a4d2f211", "sha256": "6b185a9902652f893f3ebd8ada92d2f11b6de6533a9a4d11718a8a4496101128" }, { "path": "research/community-hyperplane599-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "546f37d326d10a99910ae8f908e71ef768524d98", "sha256": "65099d764bfcc39bda5e4d9966783611b094c3522dbdd1435cd498d657a8ef8e" }, { "path": "research/community-k492-audit/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "e538481e4cb16ed936d3195f2dfb5b5a9ca0a76b", "sha256": "2c0f4fa5bc150d05658af2e7c54c4d2c337dd52b7efd3d69530ae73bcbdf452a" }, { "path": "research/community-reconciliation92-audit/MANIFEST.json", - "usage": "input", + "usage": "provenance", "git_blob": "2a2e93685173d5f13cbb5abe740f5d90352e0228", "sha256": "5f501f3c118131e7d069f30ad77186eb2ad6961f9680a0ef105f4514ed41808a" }, { "path": "research/partial-swap-digest/baseline.py", - "usage": "input", + "usage": "provenance", "git_blob": "a2f0190704db83bd8ef48e46e723c49b925804fe", "sha256": "81e9af92cdf38243a540cdcff2062778e449467848d444da37a9553c12ca4c34" }, { "path": "research/r420-two-sided-basis/SOURCES.json", - "usage": "input", + "usage": "provenance", "git_blob": "5d718e11e62f4bcadecf1e02d6b61f87dbe190b0", "sha256": "d9810b0d139c5a1211fd2c1f0d142187cc1fca30026e1e7bc4f9ecfacf1596d1" }, { "path": "research/skip-clones/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "8d1bb3b9c8189e35e5d8bfdfa632d7473e8be0d5", "sha256": "0b68e63e35a97ce6b0cdb6e291b88ebaa8f2dd4afb70b2498f10ee89428258dc" }, { "path": "research/split-skip/SOURCE.json", - "usage": "input", + "usage": "provenance", "git_blob": "2ab610b6ea2edd2865fda793ef2168b0c76afb4f", "sha256": "7c2b4646a3ecfef6f881da5c43e4bd0fa9a4d1b00548b8ab458d897e16735134" }, { "path": "scripts/historical-ci-inputs/Makefile", - "usage": "input", + "usage": "provenance", "git_blob": "aff68409021c9d401a6f8013b9dfd7dbcc30f2a8", "sha256": "ea8830dd79da493e2d75baf753d733ff7efbcf2b4794afe41fae0ac8f3055646" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "65db599ab0b1dea0312c4ca048e0bd0f44c3736f", "sha256": "96ea543e6c707424afe247e77bd86c82152f90fc76a0773c4232145da5cdf8d1" }, { "path": "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "34820a8f24678f918f4d0e7a35380d8013fc3495", "sha256": "628391b6abfbc8674ceec1751867a4392f2cc0b5b66886243e139af86cf355ac" }, { "path": "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "c755b76e0d44ba4917aa94440ebe54daefce5b2a", "sha256": "d7fd929726b326aeeaf0a3996475adec88eee9aac09ae0bebeeaa0bc1fc8f199" }, { "path": "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "usage": "input", + "usage": "provenance", "git_blob": "7f3c012504187917a728b9fe87043f0fc8cd006a", "sha256": "a854022e0e1d5d4db4d60e586be3ea56005013ef14a1fc06d02bc06e8529c4b0" }, { "path": "scripts/historical-ci-inputs/partial-swap-context.json", - "usage": "input", + "usage": "provenance", "git_blob": "ad65114886bf34a4fd27e79f3be502389e689faa", "sha256": "833a9642f33aeab2ffea17ec9c6b82e0a953f90192b2c82e10bef21538dccba9" }, { "path": "scripts/historical-ci-inputs/partial-swap-network.json", - "usage": "input", + "usage": "provenance", "git_blob": "52075f2463f60af5e16571347f24274fce73a1ea", "sha256": "f3c4be597b2f2136da4ae2cc80c7454f63c90aa01f84e5b8131cee4dd55de815" }, { "path": "scripts/partial_swap/shared.py", - "usage": "input", + "usage": "provenance", "git_blob": "44a0e454c70f9c4b98e258b8443612e6a119904b", "sha256": "5a0646a50b9f3e8ea55168620a78e8853b0ab810517cefc8cfb8696aedee278a" }, { "path": "scripts/replay_historical_check.py", - "usage": "input", + "usage": "provenance", "git_blob": "1e92fff2782970ef71378f594f2350d245a4db26", "sha256": "5467619c78183d3adc82b0cb55af28e5c1a01fca2b0588677816244b53e2bafd" }, { "path": "scripts/research_package.py", - "usage": "input", + "usage": "provenance", "git_blob": "091b4c8f58bac9a9580d76025b887dc5c873d05f", "sha256": "e1256016e7f51827d04fa2179255989f639ae1d97afaa9c16265f85a0c6abd70" }, { "path": "scripts/run_isolated_tests.py", - "usage": "input", + "usage": "provenance", "git_blob": "a96ab35b315ce492e7fbbfd6c5ae211aa066b541", "sha256": "49eb56dd0fc0d8d8ffdb209970a7adf2176223580646f575d5c22e59543b381c" }, { "path": "scripts/verify_selected_result.py", - "usage": "input", + "usage": "provenance", "git_blob": "6882a4700e410dec569b51ae2eaf1a19cc019195", "sha256": "d6b305eac5b9bdb8172c469ad30a1655a60fa0aceac8b1bf610e1b73f51babd8" }, { "path": "tests/test_isolated_test_runner.py", - "usage": "input", + "usage": "provenance", "git_blob": "343b24abf6719b81805eba5a84c74e57634c8288", "sha256": "3a5470d0b139828b90e19bf9583ddeafcd69f8e34f2824664eb3a2958a52e34d" } diff --git a/research/historical-selected-replay-gap/VERIFY.json b/research/historical-selected-replay-gap/VERIFY.json index 98553e72ed..ab7efa3471 100644 --- a/research/historical-selected-replay-gap/VERIFY.json +++ b/research/historical-selected-replay-gap/VERIFY.json @@ -4,36 +4,7 @@ "python": "3.12", "requirements": [], "inputs": [ - "Makefile", - "certificates/partial-swap-network.json", - "docs/ci-verification.md", - "research/clifford-state-performance/SOURCE.json", - "research/community-batch1047-audit/CONTENT-COVERAGE.json", - "research/community-batch1099-audit/CONTENT-COVERAGE.json", - "research/community-batch932-audit/CONTENT-COVERAGE.json", - "research/community-batch970-audit/CONTENT-COVERAGE.json", - "research/community-frontier741-audit/CONTENT-COVERAGE.json", - "research/community-frontier890-audit/CONTENT-COVERAGE.json", - "research/community-hyperplane599-audit/SOURCE.json", - "research/community-k492-audit/SOURCE.json", - "research/community-reconciliation92-audit/MANIFEST.json", - "research/partial-swap-digest/baseline.py", - "research/r420-two-sided-basis/SOURCES.json", - "research/skip-clones/SOURCE.json", - "research/split-skip/SOURCE.json", - "scripts/historical-ci-inputs/Makefile", - "scripts/historical-ci-inputs/ledger-batch932-run_isolated_tests.py", - "scripts/historical-ci-inputs/ledger-batch932-test_isolated_test_runner.py", - "scripts/historical-ci-inputs/ledger-batch970-verify_selected_result.py", - "scripts/historical-ci-inputs/ledger-frontier741-ci-verification.md", - "scripts/historical-ci-inputs/partial-swap-context.json", - "scripts/historical-ci-inputs/partial-swap-network.json", - "scripts/partial_swap/shared.py", - "scripts/replay_historical_check.py", - "scripts/research_package.py", - "scripts/run_isolated_tests.py", - "scripts/verify_selected_result.py", - "tests/test_isolated_test_runner.py" + "scripts/research_package.py" ], "commands": [ { diff --git a/research/historical-selected-replay-gap/verify.py b/research/historical-selected-replay-gap/verify.py index 83b995941a..9d266c5a4e 100644 --- a/research/historical-selected-replay-gap/verify.py +++ b/research/historical-selected-replay-gap/verify.py @@ -6,8 +6,10 @@ """ import hashlib import importlib.util +import json import subprocess import sys +import tempfile from pathlib import Path ROOT = Path(__file__).resolve().parents[2] @@ -61,31 +63,47 @@ def require(ok, message): raise SystemExit(message) -def load_checker(): - path = ROOT / "scripts/replay_historical_check.py" - spec = importlib.util.spec_from_file_location("historical_selected_replay_gap_checker", path) +def load_module(path): + spec = importlib.util.spec_from_file_location(path.stem, path) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module +def checkout_snapshot(snapshot, sources, runner, env): + paths = [runner.canonical_relative_path(row["path"]) for row in sources["files"]] + git = ["git", "-c", "maintenance.auto=false", "-c", "gc.auto=0", + "-c", "core.autocrlf=false"] + subprocess.run([*git, "clone", "--quiet", "--shared", "--no-tags", "--no-checkout", + "--", str(ROOT), str(snapshot)], cwd=ROOT, env=env, check=True) + subprocess.run([*git, "update-ref", "--no-deref", "HEAD", INSPECTED], + cwd=snapshot, env=env, check=True) + # The pinned planner reads omitted manifests from the sparse HEAD/index. + patterns = "".join(f"/{path.as_posix()}\n" for path in paths) + subprocess.run([*git, "sparse-checkout", "set", "--no-cone", "--stdin"], + cwd=snapshot, env=env, input=patterns.encode("utf-8"), check=True) + subprocess.run([*git, "read-tree", "-mu", "HEAD"], cwd=snapshot, env=env, check=True) + for path, row in zip(paths, sources["files"], strict=True): + require(hashlib.sha256((snapshot / path).read_bytes()).hexdigest() == row["sha256"], + "historical checkout source digest changed: " + path.as_posix()) + + def entries(checker): for name, config in checker.CONFIG.items(): for entry in [config, *config.get("additional_inputs", [])]: yield name, entry -def reject(checker, entry): +def reject(root, checker, entry): try: - checker.authenticated_input(ROOT, entry) + checker.authenticated_input(root, entry) except ValueError as exc: return str(exc) raise SystemExit("historical input was admitted: " + entry["path"]) -def main(): - require(not sys.flags.optimize, "assertions must stay enabled") - checker = load_checker() +def check_snapshot(root, env): + checker = load_module(root / "scripts/replay_historical_check.py") selected = [entry for name, entry in entries(checker) if name == "tooling-ledger" and entry["path"] == SELECTED_PATH] require(len(selected) == 1, "selected-result checker overlay is not unique") @@ -94,7 +112,7 @@ def main(): require(entry["accepted_live_sha256"] == [SELECTED_ACCEPTED], "accepted selected-checker successors changed") frozen = (checker.INPUTS / entry["input"]).read_bytes() - live = (ROOT / SELECTED_PATH).read_bytes() + live = (root / SELECTED_PATH).read_bytes() require(hashlib.sha256(frozen).hexdigest() == SELECTED_PIN, "frozen selected checker bytes changed") require(hashlib.sha256(live).hexdigest() == SELECTED_LIVE, "live selected checker digest changed") require(SELECTED_LIVE not in (SELECTED_PIN, SELECTED_ACCEPTED), "live checker was already admitted") @@ -102,7 +120,7 @@ def main(): # live successor, not a broken comparison. require(SELECTED_PIN in (SELECTED_PIN, *entry["accepted_live_sha256"]), "pin membership control failed") - require(reject(checker, entry) == REJECTIONS[SELECTED_PATH][1], + require(reject(root, checker, entry) == REJECTIONS[SELECTED_PATH][1], "selected checker rejection text changed") counts = {path: 0 for path in REJECTIONS} @@ -110,7 +128,7 @@ def main(): for _name, item in entries(checker): if item["path"] not in REJECTIONS: continue - message = reject(checker, item) + message = reject(root, checker, item) counts[item["path"]] += 1 messages.setdefault(item["path"], message) for path, (count, message) in REJECTIONS.items(): @@ -118,20 +136,31 @@ def main(): require(messages[path] == message, "rejection text changed for " + path) require(sum(counts.values()) == 19, "rejection total changed") ci = [item for _name, item in entries(checker) if item["path"] == CI_PATH] - require(len(ci) == 1 and hashlib.sha256((ROOT / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, + require(len(ci) == 1 and hashlib.sha256((root / CI_PATH).read_bytes()).hexdigest() == CI_LIVE, "selected CI note digest changed") diff = subprocess.check_output( - ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=ROOT, text=True) + ["git", "diff", "--name-only", PARENT, INSPECTED], cwd=root, env=env, text=True) changed = sorted(name for name in diff.splitlines() if name) require(changed == CHANGED, "inspected commit diff changed") - sys.path.insert(0, str(ROOT / "scripts")) - from research_package import plan_details - details = plan_details(ROOT, set(changed)) + planner = load_module(root / "scripts/research_package.py") + details = planner.plan_details(root, set(changed)) require([row["package"] for row in details] == PLAN_PACKAGES, "helper plan selection changed") matched = {name for row in details for names in row["causes"].values() for name in names} require(sorted(set(changed) - matched) == UNMATCHED, "unmatched plan paths changed") - require(plan_details(ROOT, set()) == [], "empty change set selected a package") + require(planner.plan_details(root, set()) == [], "empty change set selected a package") + + +def main(): + require(not sys.flags.optimize, "assertions must stay enabled") + sources = json.loads(Path(__file__).with_name("SOURCES.json").read_bytes()) + require(sources["base_commit"] == INSPECTED, "historical checkout base changed") + runner = load_module(ROOT / "scripts/research_package.py") + env = runner.git_source_env() + with tempfile.TemporaryDirectory(prefix="historical-selected-replay-") as temporary: + snapshot = Path(temporary) / "snapshot" + checkout_snapshot(snapshot, sources, runner, env) + check_snapshot(snapshot, env) print("PASS_HISTORICAL_SELECTED_REPLAY_GAP") print("selected_checker_live=" + SELECTED_LIVE) print("rejections=19 distinct_paths=7 plan_packages=9") diff --git a/research/p104-chart1089-split-bound/LOCAL-PINS.json b/research/p104-chart1089-split-bound/LOCAL-PINS.json new file mode 100644 index 0000000000..2bdcd2ee77 --- /dev/null +++ b/research/p104-chart1089-split-bound/LOCAL-PINS.json @@ -0,0 +1,16 @@ +{ + "independent/chart1089.py": "82c448e1a15d436d54dde0a4e673f94a0f755863d28100ae92ad18fb48580aeb", + "inputs/7334-WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "inputs/paired_rank.py": "d1b7c34e6f8c8a7b810414762015e6e300a8292422af66ff671ae09741141f09", + "inputs/paired_support.py": "38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f", + "lead/low_chart.py": "2a0ea8eed4c574a4ebe871099e91d1d24ceb1de1497e88125e6b0db11d8ab0d3", + "price/inputs/ADMITTED.json": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "price/inputs/AFFECTED-CHARTS.json.gz": "e2aaa1db90e883d7d719b44ba49f6c471b1b1d5761f60a58e4f164cc61233cf0", + "price/inputs/IDENTITIES.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "price/inputs/OCCUPANCY.json.gz": "13063dd5cab0fe97daebdda5f83b727c574033b7dfc0dcdfa3d16f646c78e0ee", + "price/inputs/RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "price/inputs/derivative_check.py": "348c8b2de72f1f112cb1337eca9d29ca96c85a7ad903beecafb1a2a1221f408e", + "price/inputs/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "price/quote.py": "3fdf82b2a119df71a60d5d9e8240bf6597272107b2aa86c6659a6e697c6c6e4b", + "receipts/SHA256.json": "003126314870a448df079efc17e36d346a169b0ca0b8651b155573bda20c9d82" +} diff --git a/research/p104-chart1089-split-bound/NOTICE b/research/p104-chart1089-split-bound/NOTICE new file mode 100644 index 0000000000..da56f2e63a --- /dev/null +++ b/research/p104-chart1089-split-bound/NOTICE @@ -0,0 +1,6 @@ +Apache-2.0. + +#7339 supplies exact cohort and pairing methods, #7334 the emitted word, #7113 +the signed caller and #7298 the directed tariff. Credit #5599, #7121, #7130 +and #7332 for related productive split constructions and exclusions. +OpenAI Codex and subagents materially assisted. diff --git a/research/p104-chart1089-split-bound/PROOF.md b/research/p104-chart1089-split-bound/PROOF.md new file mode 100644 index 0000000000..e6ebbf2c98 --- /dev/null +++ b/research/p104-chart1089-split-bound/PROOF.md @@ -0,0 +1,15 @@ +# Exterior prefix obstruction at the chart-1089 entrance + +The original chart-3→127 root has rank nine. Chart 1089 has rank three and is strictly intermediate. The proposed edit preserves every paid MOVE and splits one productive helper at an existing coframe. The full exact filtered endpoint cohort has 615 roles. At each of the twelve pre-event cuts 44588–44599, the full public chart bank is [85,319,1081] and the owned bank is empty. Role 1081 is the affected split pivot. The necessary support check admits every public bank coordinate. + +Let P be the normalized arbitrary-input prefix. For a legal split, some nonzero local functional a must give aP=c supported inside the retained endpoint cohort, as part of the exact identities aP=c, Sb=d and ab=cd=1. In particular, a must annihilate every exterior coordinate of P restricted to the bank. Rank three on the three exterior rows makes that impossible. + +The first implementation propagates the literal prefix over exact rational coefficients, with forward chart and ownership tracking. Its exterior kernel is zero at every key. The independent implementation walks backwards from the final charts and propagates a separate forward prefix modulo 1,000,003. It verifies all scalar denominators used in the replay are units. The minor on exterior coordinates [98,962,1467] is 500001 modulo that prime for every cut. Each rational minor is nonzero because its modular reduction is nonzero. The two engines agree on every bank and rank. The prefix alone resolves the scoped question. + +The exact directed one-root gross ceiling at the comparator crossing is + +```text +3528183420760683542117844246809394802491686063717/10000000000000000000000000000000000000000000000000 +``` + +All twelve cut keys are alternatives to one root edit. The complete signed price changes T by {3:+17,6:+17,9:−17} and keeps P fixed. Paid 110,519, productive 22,478 after the hypothetical edit, rank surplus 1,424 and no empty-root credit. At the incumbent raw upper plus 10⁻⁹, the old complete bill has negative margin and the hypothetical bill has positive margin. With one added paid rank-one position the upper margin is negative at the lower endpoint of the incumbent crossing, and the derivative remains strictly negative through the retained BIT premise. The fixed moonshot remains short by more than 139.37944 raw, even with the one split granted and all ancillary costs free. The literal support result eliminates the price-only credit. diff --git a/research/p104-chart1089-split-bound/PROVENANCE.json b/research/p104-chart1089-split-bound/PROVENANCE.json new file mode 100644 index 0000000000..8649517723 --- /dev/null +++ b/research/p104-chart1089-split-bound/PROVENANCE.json @@ -0,0 +1,67 @@ +{ + "derived_receipts": { + "price/inputs/AFFECTED-CHARTS.json.gz": { + "expected_uncompressed_sha256": "587739d21541e7ffe01af9cb7e51abaa757ee69b580befe8bb768a81b614aa08", + "receipt_manifest": "https://github.com/CrocSwap/integer-mult-bounds/blob/4b958b057e133e92a5c3a07f1fb489c626dc2525/research/p104-retimed-chart207-split-bound/receipts/SHA256.json", + "source_receipt": "REVERSE.json" + }, + "price/inputs/IDENTITIES.json": { + "expected_uncompressed_sha256": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "receipt_manifest": "https://github.com/CrocSwap/integer-mult-bounds/pull/7338", + "source_receipt": "IDENTITIES.json" + }, + "price/inputs/OCCUPANCY.json.gz": { + "expected_uncompressed_sha256": "4c349e06b22bfebb431fab1c9ae04f0e798f398acc6fdd99591b49b1c95ef6ca", + "receipt_manifest": "https://github.com/CrocSwap/integer-mult-bounds/blob/4b958b057e133e92a5c3a07f1fb489c626dc2525/research/p104-retimed-chart207-split-bound/receipts/SHA256.json", + "source_receipt": "OCCUPANCY.json" + }, + "price/inputs/RANK-STOCK.json": { + "expected_uncompressed_sha256": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "receipt_manifest": "https://github.com/CrocSwap/integer-mult-bounds/pull/7338", + "source_receipt": "RANK-STOCK.json" + } + }, + "files": { + "inputs/7334-WORD.json.gz": { + "commit": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd", + "path": "research/p104-helper-319-fused-return/WORD.json.gz", + "sha256": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a", + "source": "https://github.com/Clear1nsight/integer-mult-bounds/blob/aaeec8c0acf01e99a5f331ef363a698d9c084ace/research/p104-helper-319-fused-return/WORD.json.gz", + "uncompress": false + }, + "inputs/paired_rank.py": { + "commit": "4b958b057e133e92a5c3a07f1fb489c626dc2525", + "git_blob": "b712cdb1f8a824086e90a81cf22747aa4b63f918", + "path": "research/p104-retimed-chart207-split-bound/engines/paired_rank.py", + "sha256": "d1b7c34e6f8c8a7b810414762015e6e300a8292422af66ff671ae09741141f09", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/4b958b057e133e92a5c3a07f1fb489c626dc2525/research/p104-retimed-chart207-split-bound/engines/paired_rank.py", + "uncompress": false + }, + "inputs/paired_support.py": { + "commit": "4b958b057e133e92a5c3a07f1fb489c626dc2525", + "git_blob": "46180f7b496c002f1ee216e03fcdc85cf57a14aa", + "path": "research/p104-retimed-chart207-split-bound/engines/paired_support.py", + "sha256": "38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/4b958b057e133e92a5c3a07f1fb489c626dc2525/research/p104-retimed-chart207-split-bound/engines/paired_support.py", + "uncompress": false + }, + "price/inputs/ADMITTED.json": { + "commit": "349996445176e934ffb3c76813adcd230ca8f783", + "git_blob": "464c89e45c4eca230c099e8bac784a90200a5069", + "path": "research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "sha256": "c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/349996445176e934ffb3c76813adcd230ca8f783/research/p104-compensated-fusion-readout-bound/inputs/ADMITTED.json", + "uncompress": false + }, + "price/inputs/pricing.py": { + "commit": "c522451caf287bb3c16eaece72be4c263315dca4", + "git_blob": "40ec194017bda1d524bba4f07b188c53281419d0", + "path": "research/adjacent-owned-add-exchange-bound/pricing.py", + "sha256": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "source": "https://github.com/CrocSwap/integer-mult-bounds/blob/c522451caf287bb3c16eaece72be4c263315dca4/research/adjacent-owned-add-exchange-bound/pricing.py", + "uncompress": false + } + }, + "schema_version": 1 +} diff --git a/research/p104-chart1089-split-bound/README.md b/research/p104-chart1089-split-bound/README.md new file mode 100644 index 0000000000..d00b649feb --- /dev/null +++ b/research/p104-chart1089-split-bound/README.md @@ -0,0 +1,24 @@ +# Fixed-paid P104 chart-1089 split bound + +**NO VERIFIED GAIN. Exact conditional κ change 0%.** On independently reproduced [#7334](https://github.com/CrocSwap/integer-mult-bounds/pull/7334) at `aaeec8c0acf01e99a5f331ef363a698d9c084ace`, test whether one rank-nine helper can split into ranks three and six using the same paid MOVE schedule. The only affected eligible pivot at chart 1089 is role 1081, with endpoints chart 3→127. The twelve tested cuts are immediately before events 44588 through 44599 in the emitted helper-319 block. + +Two independent walks agree that every cut has public bank `[85,319,1081]` and an empty owned bank. The support gate grants the full 615-role endpoint cohort and all three public chart rows, including protected role 319 as a local relaxation. Exact rational elimination gives exterior prefix rank three. The independent replay reconstructs a nonzero 3×3 minor for every key, with all used denominators invertible modulo 1,000,003. Thus no pure prefix exists. All twelve keys are resolved and no suffix or construction is needed. [Proof](PROOF.md). + +The complete signed [#7113](https://github.com/CrocSwap/integer-mult-bounds/pull/7113) price for a hypothetical 3+6 split is `T3+17,T6+17,T9−17`, with all paid stock fixed. The complete comparator remains κ `0.00364665195644`, and the optimistic one-edit credit is about 0.3528183420760684 raw. A single added paid rank-one position eliminates the price through the retained BIT cap. The exact prefix obstruction reduces compatible savings to zero in this scope. + +## Replay + +Use CPython 3.12 with assertions and the standard library. From a clean checkout: + +```sh +python3.12 -I -B research/p104-chart1089-split-bound/replay.py +python3.12 -B scripts/research_package.py --package research/p104-chart1089-split-bound +``` + +Use `--out` with a fresh output path to retain all three receipts. The command authenticates the exact #7334 compressed word and its Git blob, rebuilds the signed directed price, compares exact rational and modular prefix certificates, and rejects changed compressed input. [Source and replay details](VERIFICATION.md). + +## Open next questions + +Can a different cut bank support a fixed-paid split of this exact endpoint cohort? Pin the next chart and scope, reprice the full signed invoice, and test its exterior prefix before exact pairing. This result covers only the affected 1081 pivot in the literal chart-1089 interval. Other pivots, changed paid paths, changed owner contracts and newly installed physical interfaces are open. + +Credit #7339 for the exact cohort, earlier occupancy receipts and pairing code; #7334 for the emitted word; #7113 for the signed caller; #7298 for the directed tariff; and #5599, #7121, #7130 and #7332 for earlier split, basis and cohort methods. OpenAI Codex and subagents materially assisted. diff --git a/research/p104-chart1089-split-bound/SOURCES.json b/research/p104-chart1089-split-bound/SOURCES.json new file mode 100644 index 0000000000..e8c2f265cd --- /dev/null +++ b/research/p104-chart1089-split-bound/SOURCES.json @@ -0,0 +1,18 @@ +{ + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "path": "certificates/selected-result.json", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1", + "usage": "provenance" + }, + { + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "path": "docs/research/agent-task-catalog.json", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "usage": "provenance" + } + ], + "schema_version": 1 +} diff --git a/research/p104-chart1089-split-bound/TASK.json b/research/p104-chart1089-split-bound/TASK.json new file mode 100644 index 0000000000..d425be4707 --- /dev/null +++ b/research/p104-chart1089-split-bound/TASK.json @@ -0,0 +1,117 @@ +{ + "actual_scope": "Exact #7334, pivot 1081 in the fixed 615-role 3\u2192127 endpoint cohort, chart 1089 at all 12 retimed pre-event cuts. Fixed-paid productive rank-nine split into ranks three and six.", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent verification and packaging.", + "author": "Fixed-paid chart-1089 productive-root research", + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "bottleneck_link": "A same-paid productive 3+6 split would improve the binding complete complex moment. The exact exterior-prefix obstruction rules out this stock.", + "budget_minutes": 8, + "evidence": "All 12 cuts exhausted. Full exterior prefix rank three by rational elimination and by 12 explicit nonzero modular minors with unit denominators. No suffix or build needed.", + "open_questions": [ + { + "blocked_by": "The chart-1089 bank has full exterior prefix rank at all 12 cuts.", + "first_step": "Pin the next distinct chart or interval, rebuild the complete price, and test its exact exterior prefix before pairing.", + "question": "Can a different cut bank support a fixed-paid split of this rank-nine endpoint cohort?", + "why_it_matters": "A legal 3+6 split improves the binding complex moment if all paid routes stay fixed." + } + ], + "original_card": { + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "existing_checks": [ + { + "evidence": "research/p104-literal-slot-defect/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4133: literal-slot defect", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "88666f1dee93fbd85b31fd5d6f91a219e111b5f4", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-commutation-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4136: uniform commutation gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "281ce601a8be9db470de630759179c23e1dfaa88", + "status": "author-checked" + }, + { + "evidence": "research/p104-uniform-encoding-gap/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4140: uniform encoding gap", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "de25c6525aa866962309df5d107b32d55e6e5628", + "status": "author-checked" + }, + { + "evidence": "research/p104-source-chart-shortcut/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4153: source-chart shortcut exhausts its optimistic allowance", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "9123241fea53df77e51ffe30d9aca1625d4bf3a8", + "status": "author-checked" + }, + { + "evidence": "research/p104-fiber-tag-seam/README.md", + "remaining": "Independently validate the stated scope or change its producer/consumer premise and pay the complete boundary.", + "scope": "PR #4154: fiber-tag seam mismatch", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "source_commit": "4ffcdaee5d6255a9cea1fe53a5424435068089d0", + "status": "author-checked" + }, + { + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "status": "reviewed" + } + ], + "first_experiment": "Start with the selected #5599 emitted word and review pending #5718 distinct input/output bases plus #5717/#5719 coverage before claiming work. Pick one uncovered source word, helper group and cut region. Prove the arbitrary-input relation and legal entry/exit corrections, then compare full target and paid profiles. Reject if completion, owned lifetimes or consumer costs repay the gain. A static pairing rank alone is not a physical split.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "id": "p104-side-correction", + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "overlap_terms": [ + "P104", + "helper basis", + "helper split", + "5718", + "dyadic capacity" + ], + "question": "Can joint helper bases and a legal causal split improve the complete P104 productive/paid invoice?", + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/p104-helper-subspace-splits/README.md", + "research/dyadic-helper-channel-capacity/README.md" + ] + }, + "outcome": "negative-result", + "priority_revision": 8, + "schema_version": 1, + "scope_change_reason": "Switch from the exhausted chart-207 and chart-240 cuts to the known rank-three entrance of the same retimed block.", + "scope_status": "changed", + "stop_rule": "At most 12 exact prefix keys or 20 runner seconds, then at most 12 exact pairings or 35 runner seconds only if a prefix survives.", + "task_id": "p104-side-correction" +} diff --git a/research/p104-chart1089-split-bound/VERIFICATION.md b/research/p104-chart1089-split-bound/VERIFICATION.md new file mode 100644 index 0000000000..fa45bb64ce --- /dev/null +++ b/research/p104-chart1089-split-bound/VERIFICATION.md @@ -0,0 +1,10 @@ +# Source pins and exact replay + +LOCAL-PINS.json binds package-relative inputs, code and receipt hashes. PROVENANCE.json names the exact #7334 word, #7338 admission, #7298 tariff and #7339 code. Two compressed #7339 geometry outputs are validated by their original uncompressed receipt hashes before the price is computed. The code and outputs from earlier rounds are inputs, and the replay reconstructs the chart-1089 banks directly from the literal word. + +- PRICE.json regenerates the complete 17-copy signed invoice and derivative with one added paid rank-one position. +- LEAD.json checks all twelve banks by forward ownership and exact rational exterior elimination. +- INDEPENDENT.json checks all twelve banks by reverse ownership and independently reconstructs their nonzero exterior minors. The price and both scientific receipts must match their exact SHA-256 values. +- Controls test full and deficient modular rank, a genuine exact unit pair, and a pure pair with no unit pairing. A changed compressed input must reject before decode. + +The bounded prefix gate exhausted all twelve keys. The stronger suffix/pairing gate was reserved only for a prefix survivor and was unnecessary. No physical, ownership or complete changed-bound certification was performed for a new candidate. diff --git a/research/p104-chart1089-split-bound/VERIFY.json b/research/p104-chart1089-split-bound/VERIFY.json new file mode 100644 index 0000000000..5ca0008118 --- /dev/null +++ b/research/p104-chart1089-split-bound/VERIFY.json @@ -0,0 +1,19 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/replay.py" + ], + "checks": "Replay the exact directed 3+6 price, reconstruct all 12 banks with two walks, agree on complete rational and modular exterior rank, and reject changed word bytes.", + "timeout_seconds": 90 + } + ], + "inputs": [], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/p104-chart1089-split-bound/independent/chart1089.py b/research/p104-chart1089-split-bound/independent/chart1089.py new file mode 100644 index 0000000000..b92ac723f0 --- /dev/null +++ b/research/p104-chart1089-split-bound/independent/chart1089.py @@ -0,0 +1,328 @@ +"""Independent reverse bank inventory, modular prefix and exact pairing audit.""" +from argparse import ArgumentParser +from collections import Counter +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from math import isqrt +from pathlib import Path +from time import monotonic + +P = 1000003 +HEAD = "aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD = "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PRICE = "3659931ae9d38e58629ad111c21a97e1e41175bf2e181c7084ed5645892cb146" +COHORT = "4c349e06b22bfebb431fab1c9ae04f0e798f398acc6fdd99591b49b1c95ef6ca" +CHART, PIVOT = 1089, 1081 +CUTS = tuple(range(44588, 44600)) + + +class Capped(Exception): + pass + + +def require(ok, reason): + if not ok: + raise ValueError(reason) + + +def safe(deadline): + if monotonic() >= deadline: + raise Capped + + +def pinned(path, digest): + raw = path.read_bytes() + require(sha256(raw).hexdigest() == digest, "changed pinned input " + path.name) + return raw + + +def reverse_banks(word, deadline): + n = word["public"] + stock = word["final"].copy() + [None] * word["owned_fields"] + out = {} + events = word["program"] + for t in range(len(events), CUTS[0] - 1, -1): + if t % 128 == 0: + safe(deadline) + if t in CUTS: + public = [r for r in range(n) if stock[r] == CHART] + owned = [r for r in range(n, len(stock)) if stock[r] == CHART] + require(PIVOT in public and 319 in public, "sealed affected bank does not match") + out[t] = {"public": public, "owned": owned} + if t == CUTS[0]: + break + op, r, *a = events[t - 1] + if op == "MOVE": + require(stock[r] == a[1] and a[2] == (r >= n), "reverse move chart or owner mismatch") + stock[r] = a[0] + elif op == "INIT": + require(r >= n and stock[r] == a[0], "reverse INIT chart mismatch") + stock[r] = None + elif op == "CLEAR": + require(r >= n and stock[r] is None, "reverse CLEAR chart mismatch") + stock[r] = a[0] + else: + require(op in ("ADD", "SCALE", "COPY"), "unknown native op") + return out + + +@cache +def rational(value): + return Q(value) + + +@cache +def mod_coeff(value): + q = rational(value) + require(q.denominator % P, "observed nonunit denominator") + return q.numerator * pow(q.denominator, -1, P) % P + + +def axpy(dst, src, c, mod): + for j, x in src.items(): + value = dst.get(j, 0) + c * x + if mod: + value %= P + if value: + dst[j] = value + else: + dst.pop(j, None) + + +def scaled(row, c, mod): + if mod: + return {i: z for i, x in row.items() if (z := c * x % P)} + return {i: z for i, x in row.items() if (z := c * x)} + + +def sparse_states(word, banks, deadline, reverse, mod): + n = word["public"] + one = 1 if mod else Q(1) + rows = [{i: one} for i in range(n)] + [{} for _ in range(word["owned_fields"])] + last, first = max(banks), min(banks) + events = word["program"] + cuts = range(len(events), first - 1, -1) if reverse else range(last + 1) + saved = {} + convert = mod_coeff if mod else rational + for t in cuts: + if t % 128 == 0: + safe(deadline) + if t in banks: + saved[t] = [rows[r].copy() for r in banks[t]["public"]] + if (reverse and t == first) or (not reverse and t == last): + break + op, d, *a = events[t - 1 if reverse else t] + if op == "MOVE": + continue + if op in ("INIT", "CLEAR"): + rows[d] = {} + continue + coeff = convert(a[-2]) + if op == "SCALE": + rows[d] = scaled(rows[d], coeff, mod) + elif reverse: + axpy(rows[a[0]], rows[d], coeff, mod) + if op == "COPY": + rows[d] = {} + elif op == "COPY": + rows[d] = scaled(rows[a[0]], coeff, mod) + else: + require(op == "ADD", "unknown scalar operation") + axpy(rows[d], rows[a[0]], coeff, mod) + return saved + + +def modulo_witness(rows, allowed): + pivots = {} + for original in rows: + row = {i: x for i, x in original.items() if i not in allowed} + while row: + j = max(row) + if j not in pivots: + pivots[j] = scaled(row, pow(row[j], -1, P), True) + break + axpy(row, pivots[j], -row[j], True) + columns = sorted(pivots) + if len(columns) != len(rows): + return len(columns), columns, None + dense = [[row.get(j, 0) for j in columns] for row in rows] + det = 1 + for j in range(len(dense)): + r = next(i for i in range(j, len(dense)) if dense[i][j]) + if r != j: + dense[r], dense[j] = dense[j], dense[r] + det = -det + value = dense[j][j] + det = (det * value) % P + inverse = pow(value, -1, P) + for k in range(j + 1, len(dense)): + multiplier = dense[k][j] * inverse % P + dense[k] = [(a - multiplier * b) % P for a, b in zip(dense[k], dense[j], strict=True)] + require(det, "zero modular minor") + return len(columns), columns, det + + +def kernel(matrix, n): + """Dense rational RREF on transposed exterior constraints.""" + matrix = [r.copy() for r in matrix if any(r)] + pivots = [] + for j in range(n): + head = len(pivots) + pivot = next((i for i in range(head, len(matrix)) if matrix[i][j]), None) + if pivot is None: + continue + matrix[head], matrix[pivot] = matrix[pivot], matrix[head] + a = matrix[head][j] + matrix[head] = [x / a for x in matrix[head]] + for i, row in enumerate(matrix): + if i != head and row[j]: + a = row[j] + matrix[i] = [x - a * y for x, y in zip(row, matrix[head], strict=True)] + pivots.append(j) + basis = [] + for j in range(n): + if j not in pivots: + v = [Q(i == j) for i in range(n)] + for i, col in enumerate(pivots): + v[col] = -matrix[i][j] + basis.append(v) + return basis + + +def linear(rows, weights): + target = {} + for row, a in zip(rows, weights, strict=True): + if a: + axpy(target, row, a, False) + return target + + +def pure(rows, allowed): + outside = sorted(set().union(*(row.keys() for row in rows)) - allowed) + exterior = [[row.get(j, Q(0)) for row in rows] for j in outside] + basis = kernel(exterior, len(rows)) + return [(v, linear(rows, v)) for v in basis] + + +def dot(a, b): + return sum((x * y for x, y in zip(a, b, strict=True)), Q(0)) + + +def dot_sparse(a, b): + return sum((x * b.get(i, 0) for i, x in a.items()), Q(0)) + + +def bilinear(A, D): + """Exact witness for xAy=1, xDy=0, or proof none exists.""" + n, m = len(A), len(A[0]) + choices = [[Q(i == j) for i in range(n)] for j in range(n)] + candidates = choices + [[a + b for a, b in zip(choices[i], choices[j], strict=True)] + for i in range(n) for j in range(i)] + candidates += kernel([[row[j] for row in D] for j in range(m)], n) + for x in candidates: + c = [dot(x, [r[j] for r in A]) for j in range(m)] + d = [dot(x, [r[j] for r in D]) for j in range(m)] + y = [Q(0)] * m + if not any(d): + j = next((j for j, a in enumerate(c) if a), None) + if j is None: + continue + y[j] = 1 / c[j] + else: + i = next(j for j, a in enumerate(d) if a) + j = next((j for j in range(m) if c[i] * d[j] != c[j] * d[i]), None) + if j is None: + continue + det = c[i] * d[j] - c[j] * d[i] + y[i], y[j] = d[j] / det, -d[i] / det + require(dot(c, y) == 1 and not dot(d, y), "invalid bilinear certificate") + return x, y + return None + + +def pairing(before, after, allowed, bank): + F, R = pure(before, allowed), pure(after, allowed) + outcome = {"prefix_nullity": len(F), "suffix_nullity": len(R)} + if not any(c for _, c in F): + return outcome | {"status": "no_nonzero_pure_prefix_exact"} + if not any(d for _, d in R): + return outcome | {"status": "no_nonzero_pure_suffix"} + A = [[dot_sparse(c, d) for _, d in R] for _, c in F] + D = [[dot(a, b) - dot_sparse(c, d) for b, d in R] for a, c in F] + pair = bilinear(A, D) + if pair is None: + return outcome | {"status": "no_unit_pairing", "image_pairing": [[str(x) for x in row] for row in A], + "local_minus_image": [[str(x) for x in row] for row in D]} + x, y = pair + a = linear([dict(zip(bank, row, strict=True)) for row, _ in F], x) + b = linear([dict(zip(bank, row, strict=True)) for row, _ in R], y) + c = linear([r for _, r in F], x) + d = linear([r for _, r in R], y) + require(dot_sparse(a, b) == dot_sparse(c, d) == 1, "wrong final unit pair") + return outcome | {"status": "exact_paired_support", "witness": { + k: {r: str(v) for r, v in row.items()} for k, row in zip("abcd", [a, b, c, d], strict=True)}} + + +def controls(): + require(P > 2 and all(P % i for i in range(2, isqrt(P) + 1)), "nonprime modulus") + require(modulo_witness([{2: 1, 3: 2}, {2: 4, 3: 5}], set())[-1] == P - 3, "minor control") + require(modulo_witness([{2: 1}, {2: 4}], set())[-1] is None, "modular loss control") + yes = pairing([{1: Q(1)}], [{1: Q(1)}], {1}, [0]) + no = pairing([{1: Q(1)}], [{2: Q(1)}], {1, 2}, [0]) + require(yes["status"] == "exact_paired_support" and no["status"] == "no_unit_pairing", "unit controls") + return ["full exterior modular minor", "modular loss requires exact fallback", "true unit pair", "pure unpaired rows"] + + +def main(args): + tests = controls() + price = loads(pinned(args.price, PRICE)) + cohort = loads(pinned(args.cohort, COHORT)) + keys = [[t, CHART, PIVOT] for t in CUTS] + require(price["stock"] == keys and price["head"] == cohort["head"] == HEAD, "wrong frozen stock") + allowed = set(cohort["endpoint_cohort"]) + require(len(allowed) == 615 and PIVOT in allowed and 319 not in allowed, "wrong endpoint cohort") + start = monotonic() + word = loads(decompress(pinned(args.word, WORD))) + outcomes = {} + try: + bank = reverse_banks(word, start + 20) + prefix = sparse_states(word, bank, start + 20, reverse=False, mod=True) + for t in CUTS: + safe(start + 20) + rank, columns, det = modulo_witness(prefix[t], allowed) + status = "no_nonzero_pure_prefix_modular_minor" if det is not None else "exact_pairing_needed" + outcomes[t] = {"key": [t, CHART, PIVOT], "bank": bank[t], "prefix_modular_rank": rank, + "exterior_minor_columns": columns, "exterior_minor_det_mod_p": det, "status": status} + except Capped: + pass + exact = {t: r["bank"] for t, r in outcomes.items() if r["status"] == "exact_pairing_needed"} + if exact: + deadline = monotonic() + 35 + try: + a = sparse_states(word, exact, deadline, reverse=False, mod=False) + b = sparse_states(word, exact, deadline, reverse=True, mod=False) + for t in sorted(exact): + safe(deadline) + outcomes[t].update(pairing(a[t], b[t], allowed, exact[t]["public"])) + except Capped: + pass + rows = [outcomes[t] for t in sorted(outcomes)] + unvisited = [k for k in keys if k[0] not in outcomes or outcomes[k[0]]["status"] == "exact_pairing_needed"] + print(dumps({ + "head": HEAD, "word_sha256": WORD, "price_sha256": PRICE, "cohort_sha256": COHORT, + "stock": len(keys), "prime": P, "prefix_seconds": 20, "paired_seconds": 35, + "observed_scalar_denominators_invertible": True, "allowed_boundary_count": len(allowed), + "controls": tests, "rows": rows, "unvisited": unvisited, + "survivors": [r for r in rows if r["status"] == "exact_paired_support"], + "dispositions": dict(Counter(r["status"] for r in rows)), + }, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + parser = ArgumentParser() + for name in ("price", "cohort", "word"): + parser.add_argument("--" + name, type=Path, required=True) + main(parser.parse_args()) diff --git a/research/p104-chart1089-split-bound/inputs/7334-WORD.json.gz b/research/p104-chart1089-split-bound/inputs/7334-WORD.json.gz new file mode 100644 index 0000000000..73f4300719 Binary files /dev/null and b/research/p104-chart1089-split-bound/inputs/7334-WORD.json.gz differ diff --git a/research/p104-chart1089-split-bound/inputs/paired_rank.py b/research/p104-chart1089-split-bound/inputs/paired_rank.py new file mode 100644 index 0000000000..b712cdb1f8 --- /dev/null +++ b/research/p104-chart1089-split-bound/inputs/paired_rank.py @@ -0,0 +1,187 @@ +"""Rational paired exclusion using wedge identities and a stacked rank check.""" +from collections import Counter +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +import sys +from time import monotonic + +GEOMETRY="4c349e06b22bfebb431fab1c9ae04f0e798f398acc6fdd99591b49b1c95ef6ca" +WORD="4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" + + +@cache +def coefficient(s): + return Q(s) + + +def checked(path,digest): + data=path.read_bytes() + if sha256(data).hexdigest()!=digest: + raise ValueError(f"changed pin: {path.name}") + return data + + +def plus(row,other,q): + for i,x in other.items(): + v=row.get(i,0)+q*x + if v: + row[i]=v + else: + row.pop(i,None) + + +def null_pure(bank,rows,allowed): + """Eliminate exterior inputs, carrying coefficient vectors on the bank.""" + pivots={} + pure=[] + for r in bank: + row={i:x for i,x in rows[r].items() if i not in allowed} + u={r:Q(1)} + while row: + lead=max(row) + if lead not in pivots: + pivots[lead]=row,u + break + p,a=pivots[lead] + ratio=-row[lead]/p[lead] + plus(row,p,ratio) + plus(u,a,ratio) + else: + full={} + for i,x in u.items(): + plus(full,rows[i],x) + assert set(full)<=allowed + pure.append((u,full)) + assert len(pivots)+len(pure)==len(bank) + return pure + + +def rank(matrix): + basis={} + for source in matrix: + row=source.copy() + while row: + lead=max(row) + if lead not in basis: + basis[lead]=row + break + plus(row,basis[lead],-row[lead]/basis[lead][lead]) + return len(basis) + + +def pairing(B,D): + # No (x,y) with xBy=1 and xDy=0 iff each xB is proportional to xD + # and ker(x -> xD) lies inside ker(x -> xB). + rows=len(B) + cols=len(B[0]) if B else 0 + def wedge(b,d): + return any(b[i]*d[j]!=b[j]*d[i] for i in range(cols) for j in range(i)) + has_wedge=any(wedge(b,d) for b,d in zip(B,D,strict=True)) + if not has_wedge: + for i in range(rows): + for j in range(i): + if wedge([x+y for x,y in zip(B[i],B[j],strict=True)], + [x+y for x,y in zip(D[i],D[j],strict=True)]): + has_wedge=True + break + if has_wedge: + break + dr=rank([{i:x for i,x in enumerate(r) if x} for r in D]) + sr=rank([{i:x for i,x in enumerate(d+b) if x} for d,b in zip(D,B,strict=True)]) + return has_wedge,dr,sr + + +def side(word,banks,allowed,deadline,reverse): + n=word["public"] + tape=word["program"] + vectors=[{i:Q(1)} for i in range(n)]+[{} for _ in range(word["owned_fields"])] + rows={} + cuts=range(len(tape),min(banks)-1,-1) if reverse else range(0,max(banks)+1) + for t in cuts: + if t%128==0 and monotonic()>=deadline: + break + if t in banks: + rows[t]=null_pure(banks[t],vectors,allowed) + if t==0 and reverse: + break + op,d,*args=tape[t-1 if reverse else t] + if op=="MOVE": + continue + if op in ("INIT","CLEAR"): + vectors[d]={} + else: + q=coefficient(args[-2]) + source=d if op=="SCALE" else args[0] + assert op=="SCALE" or source!=d + if op=="SCALE": + vectors[d]={i:q*x for i,x in vectors[d].items()} + elif reverse: + plus(vectors[source],vectors[d],q) + if op=="COPY": + vectors[d]={} + elif op=="COPY": + vectors[d]={i:q*x for i,x in vectors[source].items()} + else: + assert op=="ADD" + plus(vectors[d],vectors[source],q) + return rows + + +def run(word,geom,keys): + deadline=monotonic()+32 + groups=Counter(k[0] for k in keys) + banks={row["cut"]:row["public_bank"] for row in geom["new"]["rows"] if row["cut"] in groups} + allowed=set(geom["endpoint_cohort"]) + forward=side(word,banks,allowed,deadline,False) + reverse=side(word,banks,allowed,deadline,True) + ans=[] + def dot(a,b): + return sum(x*b.get(i,0) for i,x in a.items()) + for t,n in sorted(groups.items()): + if t not in forward or t not in reverse or monotonic()>=deadline: + continue + F,R=forward[t],reverse[t] + w=dr=sr=None + if not any(c for a,c in F): + status="no nonzero pure prefix" + elif not any(d for b,d in R): + status="no nonzero pure suffix" + else: + B=[[dot(a,b) for b,d in R] for a,c in F] + C=[[dot(c,d) for b,d in R] for a,c in F] + D=[[x-y for x,y in zip(b,c,strict=True)] for b,c in zip(B,C,strict=True)] + w,dr,sr=pairing(B,D) + status="paired support unresolved" if w or dr!=sr else "no unit pairing" + ans.append(dict(cut=t,cases=n,status=status,prefix_dimension=len(F),suffix_dimension=len(R), + nonzero_wedge=w,exterior_rank=dr,stacked_rank=sr)) + missing=set(groups)-{r["cut"] for r in ans} + counts=Counter() + for row in ans: + counts[row["status"]]+=row["cases"] + return dict(cases=len(keys),rows=ans,counts=dict(counts), + unvisited=[key for key in keys if key[0] in missing]) + + +def main(): + root=Path(sys.argv[1]) + which=sys.argv[2] + assert which in ("first","remaining") + geom=json.loads(checked(root/"lead/OCCUPANCY.json",GEOMETRY)) + word=json.loads(decompress(checked(root/"inputs/7334-WORD.json.gz",WORD))) + assert pairing([[Q(1),Q(0)]],[[Q(0),Q(1)]])[0] + assert pairing([[Q(1)]],[[Q(2)]])==(False,1,1) + assert pairing([[Q(1)]],[[Q(0)]])==(False,0,1) + keys=geom["representative_keys" if which=="first" else "unvisited_keys"] + assert len(keys)==(128 if which=="first" else 18) + data=run(word,geom,keys) + print(json.dumps(data|dict(selection=which,word_sha256=WORD,geometry_sha256=GEOMETRY, + controls=["nonzero wedge","proportional equal rank","nonzero pairing on difference kernel"]), + indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-chart1089-split-bound/inputs/paired_support.py b/research/p104-chart1089-split-bound/inputs/paired_support.py new file mode 100644 index 0000000000..46180f7b49 --- /dev/null +++ b/research/p104-chart1089-split-bound/inputs/paired_support.py @@ -0,0 +1,356 @@ +"""Exact pure prefix/suffix and unit pairing for the #7334 chart-207 split.""" +from argparse import ArgumentParser +from collections import defaultdict +from fractions import Fraction as Q +from functools import cache +from gzip import decompress +from hashlib import sha256 +from json import dumps, loads +from pathlib import Path +from signal import SIGALRM, alarm, signal +from time import monotonic + +HEAD = 'aaeec8c0acf01e99a5f331ef363a698d9c084ace' +WORD = '4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a' +ADMISSION = 'c95300e9bca27e44a25c82d794f88cbf70757c142806b0e4c590ea29feb81a13' +PROTECTED = {319,863,1355,1568} +CAP = 128 + + +class Capped(Exception): + pass + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def check_time(deadline): + if monotonic() >= deadline: + raise Capped + + +def pinned(path, digest): + raw = path.read_bytes() + need(sha256(raw).hexdigest() == digest, f'Changed input {path.name}') + return raw + + +def unique(pairs): + doc = dict(pairs) + need(len(doc) == len(pairs), 'Duplicate receipt key') + return doc + + +def read(raw): + return loads(raw,object_pairs_hook=unique) + + +@cache +def rational(value): + return Q(value) + + +def axpy(dst, src, factor): + for j,v in src.items(): + value = dst.get(j,0) + factor*v + if value: + dst[j] = value + else: + dst.pop(j,None) + + +def dot(a,b): + return sum(v*b.get(j,0) for j,v in a.items()) + + +def compose(weights, rows): + vector = {} + for role, coefficient in weights.items(): + axpy(vector,rows[role],coefficient) + return vector + + +def pure_kernel(rows, allowed, deadline): + pivots, pure = {}, [] + for role,row in rows.items(): + check_time(deadline) + exterior = {j:v for j,v in row.items() if j not in allowed} + coeff = {role:Q(1)} + while exterior: + j = min(exterior) + if j not in pivots: + lead = exterior[j] + pivots[j] = ({k:v/lead for k,v in exterior.items()}, + {k:v/lead for k,v in coeff.items()}) + break + other, op = pivots[j] + factor = -exterior[j] + axpy(exterior,other,factor) + axpy(coeff,op,factor) + else: + projection = compose(coeff,rows) + assert projection.keys() <= allowed + pure.append((coeff,projection)) + assert len(pivots)+len(pure) == len(rows) + return sorted(pivots), pure + + +def solve_bilinear(B,D,deadline): + """Find x,y with xBy=1 and xDy=0, or prove no such rational pair.""" + n = len(B) + def trial(x): + bx,dx = compose(x,B),compose(x,D) + if not bx: + return None + if not dx: + j = min(bx) + return x,{j:1/bx[j]} + pivot = min(dx) + for j in sorted(bx.keys() | dx.keys()): + value = bx.get(j,0)*dx[pivot]-bx.get(pivot,0)*dx.get(j,0) + if value: + y = {j:dx[pivot]/value} + if dx.get(j,0): + y[pivot] = -dx[j]/value + assert dot(bx,y) == 1 and dot(dx,y) == 0 + return x,y + return None + for i in range(n): + check_time(deadline) + hit = trial({i:Q(1)}) + if hit: + return hit + # Each wedge coordinate is a homogeneous quadratic in x. Basis vectors + # and pair sums determine all coefficients over Q. + for i in range(n): + check_time(deadline) + for j in range(i+1,n): + hit = trial({i:Q(1),j:Q(1)}) + if hit: + return hit + # All wedges vanish. Only xD=0 but xB!=0 can give a pair. + _, kernel = pure_kernel(dict(enumerate(D)),set(),deadline) + for x,_ in kernel: + hit = trial(x) + if hit: + return hit + return None + + +def paired(prefix,suffix,deadline): + B,D = [],[] + for a,c in prefix: + check_time(deadline) + dot_boundary = {j:v for j,(_,d) in enumerate(suffix) if (v:=dot(c,d))} + dot_difference = {j:v for j,(b,_) in enumerate(suffix) if (v:=dot(a,b)-dot_boundary.get(j,0))} + B.append(dot_boundary); D.append(dot_difference) + hit = solve_bilinear(B,D,deadline) + if hit is None: + return None + x,y = hit + a,c = (compose(x,[pair[i] for pair in prefix]) for i in (0,1)) + b,d = (compose(y,[pair[i] for pair in suffix]) for i in (0,1)) + assert dot(a,b)==dot(c,d)==1 + return dict(a=a,b=b,c=c,d=d) + + +def initial_groups(word): + n = word['public'] + main = set(word['live']) | {r+112 for r in word['live']} + main.update(word['hosted']['X2']); main.update(word['hosted']['Y2']) + cohort = {r for r in range(n) if r not in main and (word['initial'][r],word['final'][r])==(3,127)} + return cohort-PROTECTED,cohort-PROTECTED + + +def prefix_rows(word, cuts, deadline): + n = word['public']; rows = [{r:Q(1)} for r in range(n)]+[None]*word['owned_fields'] + charts = word['initial']+[None]*word['owned_fields'] + banks, seen = {}, 0 + try: + for clock,event in enumerate(word['program']): + if clock%64 == 0 or clock in cuts: + check_time(deadline) + if clock in cuts: + banks[clock] = {r:rows[r].copy() for r in range(n) if charts[r]==207} + if clock >= max(cuts): + break + op,dst,*args = event + if op == 'MOVE': + old,new,owned = args + assert charts[dst] == old and owned==(dst>=n) + charts[dst]=new + elif op == 'INIT': + assert dst>=n and rows[dst] is None + rows[dst],charts[dst]={},args[0] + elif op == 'CLEAR': + assert dst>=n and charts[dst]==args[0] + rows[dst]=charts[dst]=None + elif op == 'SCALE': + assert charts[dst]==args[1] + rows[dst]={j:rational(args[0])*v for j,v in rows[dst].items()} + else: + src,q,chart=args + assert charts[dst]==charts[src]==chart and src!=dst and op in {'ADD','COPY'} + if op=='COPY': + assert dst>=n and not rows[dst], 'Dirty COPY' + axpy(rows[dst],rows[src],rational(q)) + seen=clock+1 + except Capped: + pass + return banks,seen + + +def suffix_rows(word,banks,deadline): + n=word['public']; cols=[{r:Q(1)} for r in range(n)]+[{} for _ in range(word['owned_fields'])] + snapshots,seen={},0 + try: + for clock in range(len(word['program']),min(banks)-1,-1): + if clock%64==0 or clock in banks: + check_time(deadline) + if clock in banks: + snapshots[clock]={r:cols[r].copy() for r in banks[clock]} + if clock==min(banks): + break + op,dst,*args=word['program'][clock-1] + if op in {'ADD','COPY'}: + src,q,_=args + axpy(cols[src],cols[dst],rational(q)) + if op=='COPY': + cols[dst]={} + elif op=='SCALE': + cols[dst]={j:rational(args[0])*v for j,v in cols[dst].items()} + elif op in {'INIT','CLEAR'}: + cols[dst]={} + else: + assert op=='MOVE' + seen+=1 + except Capped: + pass + return snapshots,seen + + +def geometry_keys(geometry): + if 'representative_keys' in geometry: + raw=geometry['representative_keys'] + elif 'keys' in geometry: + raw=geometry['keys'] + else: + raw=[(row['cut'],row['chart'],pivot) for row in geometry['segments'] for pivot in row['pivots']] + result=[tuple(row) if not isinstance(row,dict) else (row['cut'],row['chart'],row['pivot']) for row in raw] + need(len(result)==len(set(result)) and all(len(row)==3 and row[1]==207 and 44588<=row[0]<=44628 for row in result),'Wrong geometry key inventory') + return result + + +def audit(word,geometry,deadline): + all_keys=geometry_keys(geometry) + if not all_keys: + return dict(status='empty_geometry',selected=0,decisions=[],unresolved=[]) + keys=all_keys[:CAP] + cohort,pivots=initial_groups(word) + if 'endpoint_cohort' in geometry: + assert sorted(cohort)==geometry['endpoint_cohort'] + overflow=[tuple(key) for key in geometry.get('unvisited_keys',())] + assert len(overflow)==len(set(overflow)) and not set(overflow).intersection(all_keys) + bank_plan=defaultdict(list) + for cut,chart,pivot in keys: + need(pivot in pivots,'Protected or non-helper pivot') + bank_plan[cut].append(pivot) + banks,forward=prefix_rows(word,bank_plan,deadline) + decisions,opens={}, {} + try: + for cut,bank in banks.items(): + need(set(bank_plan[cut])<=bank.keys(),'Pivot absent from literal chart bank') + exterior,pure=pure_kernel(bank,cohort,deadline) + if any(c for _,c in pure): + opens[cut]=(exterior,pure) + else: + decisions[cut]=dict(status='no_nonzero_pure_prefix',public_bank=list(bank), + prefix_exterior_pivots=exterior,prefix_nullity=len(pure)) + except Capped: + pass + backward=0 + if opens: + snapshots,backward=suffix_rows(word,{c:banks[c] for c in opens},deadline) + try: + for cut,bank in snapshots.items(): + exterior,pure=pure_kernel(bank,cohort,deadline) + pre_rank,pre=opens[cut] + row=dict(public_bank=list(bank),prefix_exterior_pivots=pre_rank, + suffix_exterior_pivots=exterior,prefix_nullity=len(pre),suffix_nullity=len(pure)) + if not any(d for _,d in pure): + decisions[cut]=row|dict(status='no_nonzero_pure_suffix') + continue + witness=paired(pre,pure,deadline) + if witness is None: + decisions[cut]=row|dict(status='no_unit_pairing') + continue + assert compose(witness['a'],banks[cut])==witness['c'] + assert compose(witness['b'],bank)==witness['d'] + decisions[cut]=row|dict(status='exact_support_only',witness={k:{j:str(v) for j,v in value.items()} for k,value in witness.items()}) + except Capped: + pass + rows=[dict(key=key,**decisions[key[0]]) for key in keys if key[0] in decisions] + unresolved=[key for key in all_keys if key[0] not in decisions or key not in keys] + overflow + return dict(status='CAPPED' if unresolved else 'EXHAUSTED',selected=len(keys), + eligible_cohort=sorted(cohort),prefix_events=forward,suffix_events=backward, + decisions=rows,unresolved=unresolved,support_only=[row['key'] for row in rows if row['status']=='exact_support_only']) + + +def controls(): + inf=float('inf') + _,a=pure_kernel({4:{0:Q(1),2:Q(1)},5:{2:Q(1)}},{0},inf) + _,b=pure_kernel({4:{0:Q(1)},5:{3:Q(1)}},{0},inf) + hit=paired(a,b,inf) + assert hit and hit['a'][4] == -hit['a'][5] != 0 + assert dot(hit['a'],hit['b']) == dot(hit['c'],hit['d']) == 1 + _,wrong=pure_kernel({4:{0:Q(1),3:Q(1)},5:{3:Q(1)}},{0},inf) + assert paired(a,wrong,inf) is None + assert solve_bilinear([{0:Q(1)},{1:Q(1)}],[{0:Q(1)},{1:Q(2)}],inf)[0]=={0:Q(1),1:Q(1)} + assert solve_bilinear([{0:Q(1)},{0:Q(2)}],[{0:Q(1)},{0:Q(1)}],inf) is not None + return ['signed_unit_pair','unequal_pairing_rejected','quadratic_cross_term','left_kernel_D'] + + +def main(): + p=ArgumentParser(description=__doc__) + p.add_argument('--controls-only',action='store_true') + for key in ('word','price','geometry','admission'): + p.add_argument('--'+key,type=Path) + p.add_argument('--price-sha'); p.add_argument('--geometry-sha') + a=p.parse_args() + assert __debug__ + checks=controls() + if a.controls_only: + print(dumps(dict(controls=checks),indent=2,sort_keys=True)); return + need(all((a.word,a.price,a.geometry,a.admission,a.price_sha,a.geometry_sha)),'Sealed geometry and price are required') + price=read(pinned(a.price,a.price_sha)); geom=read(pinned(a.geometry,a.geometry_sha)) + admission=read(pinned(a.admission,ADMISSION)) + assert price['head']==admission['head']==HEAD and admission['exit']==0 + assert price['productive_delta']=={'1':17,'8':17,'9':-17} and not price['paid_delta'] + assert admission['inputs']['WORD.json.gz']==WORD + if 'price_sha256' in geom: + assert geom['price_sha256']==a.price_sha + if 'word_sha256' in geom: + assert geom['word_sha256']==WORD + keys=geometry_keys(geom) + if keys: + def watchdog(*_): + raise TimeoutError('hard support watchdog') + signal(SIGALRM,watchdog) + alarm(35) + try: + deadline=monotonic()+32 + result=audit(read(decompress(pinned(a.word,WORD))),geom,deadline) + finally: + alarm(0) + else: + result=dict(status='empty_geometry',selected=0,decisions=[],unresolved=[]) + result.update(head=HEAD,word_sha256=WORD,admission_sha256=ADMISSION,price_sha256=a.price_sha, + geometry_sha256=a.geometry_sha,cap=CAP,seconds_cap=35,controls=checks, + unvisited_credit_upper=price['one_edit_optimistic_credit'][1]) + print(dumps(result,indent=2,sort_keys=True)) + + +if __name__=='__main__': + main() diff --git a/research/p104-chart1089-split-bound/lead/low_chart.py b/research/p104-chart1089-split-bound/lead/low_chart.py new file mode 100644 index 0000000000..e6a5368c70 --- /dev/null +++ b/research/p104-chart1089-split-bound/lead/low_chart.py @@ -0,0 +1,116 @@ +"""Fixed-paid exact 3+6 split support on chart 1089.""" +from collections import Counter +from gzip import decompress +from hashlib import sha256 +import json +from pathlib import Path +from runpy import run_path +import sys +from time import monotonic + +HEAD="aaeec8c0acf01e99a5f331ef363a698d9c084ace" +WORD="4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" +PRICE="3659931ae9d38e58629ad111c21a97e1e41175bf2e181c7084ed5645892cb146" +PINS={"paired_rank.py":"d1b7c34e6f8c8a7b810414762015e6e300a8292422af66ff671ae09741141f09", + "paired_support.py":"38c796cbe1a73f386177faf88cd53294d4b911f6cde7fd47cd9fcef3b558373f"} +KEYS=[[t,1089,1081] for t in range(44588,44600)] + + +def checked(path,digest): + b=path.read_bytes() + if sha256(b).hexdigest()!=digest: + raise ValueError(f"changed dependency: {path.name}") + return b + + +def banks_at(word,deadline): + n=word["public"] + active=word["initial"]+[None]*word["owned_fields"] + banks,owned={},{} + for t,e in enumerate(word["program"]): + if (t%128==0 or t>=44588) and monotonic()>=deadline: + break + if 44588<=t<=44599: + banks[t]=[i for i in range(n) if active[i]==1089] + owned[t]=[i for i in range(n,len(active)) if active[i]==1089] + assert 1081 in banks[t] + if t==44599: + break + op,d,*p=e + if op=="MOVE": + assert active[d]==p[0] and p[2]==(d>=n) + active[d]=p[1] + elif op=="INIT": + assert active[d] is None + active[d]=p[0] + elif op=="CLEAR": + assert active[d]==p[0] + active[d]=None + else: + assert active[d]==p[-1] + if op in ("ADD","COPY"): + assert active[p[0]]==p[-1] + else: + assert op=="SCALE" + return banks,owned + + +def main(): + root=Path(sys.argv[1]) + price=json.loads(checked(root/"price/PRICE.json",PRICE)) + assert price["head"]==HEAD and price["stock"]==KEYS + assert price["productive_delta"]=={"3":17,"6":17,"9":-17} and not price["paid_delta"] + engines=[] + for name,digest in PINS.items(): + path=root/"inputs"/name + checked(path,digest) + engines.append(run_path(str(path))) + rank,solve=engines + controls=solve["controls"]() + word=json.loads(decompress(checked(root/"inputs/7334-WORD.json.gz",WORD)),object_pairs_hook=solve["unique"]) + cohort,_=solve["initial_groups"](word) + assert len(cohort)==615 and 1081 in cohort and 319 not in cohort + assert word["program"][44599][:4]==["MOVE",1081,1089,207] + assert [len(word["frames"][i]) for i in (3,1089,127)]==[0,3,9] + deadline=monotonic()+18 + banks,owned=banks_at(word,deadline) + f=rank["side"](word,banks,cohort,deadline,False) if banks else {} + decisions,live={},{} + for t,rows in f.items(): + row=dict(public_bank=banks[t],owned_bank_excluded=owned[t], + prefix_kernel_dim=len(rows),prefix_exterior_rank=len(banks[t])-len(rows), + nonzero_pure_prefix=sum(bool(c) for _,c in rows)) + if any(c for _,c in rows): + live[t]=row + else: + decisions[t]=row|dict(decision="no nonzero pure prefix") + if live: + deadline=monotonic()+32 + suffix=rank["side"](word,{t:banks[t] for t in live},cohort,deadline,True) + for t,rows in sorted(suffix.items()): + if monotonic()>=deadline: + break + row=live[t]|dict(suffix_kernel_dim=len(rows),suffix_exterior_rank=len(banks[t])-len(rows)) + if not any(d for _,d in rows): + decisions[t]=row|dict(decision="no nonzero pure suffix") + continue + try: + w=solve["paired"](f[t],rows,deadline) + except solve["Capped"]: + break + if w is None: + decisions[t]=row|dict(decision="no unit pairing") + continue + decisions[t]=row|dict(decision="exact rational support only", + witness={k:{j:str(c) for j,c in v.items()} for k,v in w.items()}) + rows=[dict(key=k,**decisions[k[0]]) for k in KEYS if k[0] in decisions] + unvisited=[k for k in KEYS if k[0] not in decisions] + print(json.dumps(dict(head=HEAD,word_sha256=WORD,price_sha256=PRICE,engines_sha256=PINS, + controls=controls,case_cap=12,prefix_seconds_cap=18,exact_followup_seconds_cap=32, + prefix_survivors=[k for k in KEYS if k[0] in live], + counts=Counter(r["decision"] for r in rows),decisions=rows,unvisited=unvisited, + status="CAPPED" if unvisited else "EXHAUSTED"),indent=2,sort_keys=True)) + + +if __name__=="__main__": + main() diff --git a/research/p104-chart1089-split-bound/price/inputs/ADMITTED.json b/research/p104-chart1089-split-bound/price/inputs/ADMITTED.json new file mode 100644 index 0000000000..464c89e45c --- /dev/null +++ b/research/p104-chart1089-split-bound/price/inputs/ADMITTED.json @@ -0,0 +1,58 @@ +{ + "assumptions": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "base": "e54523517d0f03e58352e647c403a5af3e525a57", + "caller": "07a76c5e2738882c0cb322278e56f6cae3c9885d", + "caller_sha256": "255d89f38cd45e38e5770f559bc43dc217e989032359768cdc7e8cdfd64b47bc", + "crossing": [ + "0.00364665195644044790699554028334161", + "0.00364665195644044790699554028334162" + ], + "end": "2026-11-11T23:04:43Z", + "exit": 0, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "hosted_at_admission": "plan and historical success; candidate replay in progress", + "inputs": { + "EARLY-RESULT.json": "ad1ca9b2e2febbf80d9bf8b6ceef14ff90fcc29ef9358310e551628eb1706649", + "INPUTS.json": "abedac59097a1c35c27d91cbdb07207bc562a64743bc406d13c94a8bc970592d", + "NATIVE-RESULT.json": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812", + "PROPOSED-CLAIM.json": "6e31241944c123d2bd4aa8bc94d833b44b3d889bd6d9aafc579108f416b45f03", + "RESULT.json": "7f2d587c59f063b01f1e8b320084a7f0943f2f05d65e3e0f5e80448c6c8e8194", + "SOURCES.json": "ac7b4473035af648d6073e78b6c39675e706e8194b346bb55ed62a0adc81d593", + "VERIFY.json": "ede7dd2dd3733b9a73f72af9dd7edfe819b49b859c5c76e227ec82cb9c220513", + "WORD.json.gz": "4b9fd1187b34ed97c3ac0c760d73531735a5d0ebc5b4d4ab4377160b20d9bb2a" + }, + "kappa": "0.00364665195644", + "ours": "0", + "peer_gain": "0.000000430519994", + "prior_kappa": "0.003646221436446", + "receipt": { + "peer-prep/IDENTITIES.json": "f4d3f6ca2d87f8cd68c01ac9f77b69bd5a796f92bd567cea8afe3ac7c72e8e4b", + "peer-prep/STATIC.json": "500cc563b7dac8b1de1faf1dee9b820e73152dfddc15a650cd1191edd39e8c79", + "peer-price/RANK-STOCK.json": "4a7841699dd17688f6aada5c902a2a91e94558b2b1b4460c46b0e55aa95b3f9f", + "peer-price/READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "peer/COMMAND.txt": "714bfab024155d8216f3ef99f3ee7627ddc35ab341c486ac6bd53c476b757130", + "peer/COMMIT.stdout": "597470d8132a3812deb3624a859546c0c13d52b094fd6fc61e7416941130bd70", + "peer/END-UTC.txt": "9c46923c616c14da5b8ed503e1652021d7bd409a10ec91a78a03263013fba08a", + "peer/METADATA.stdout": "5873404cb4424dca918a00d503569f3c29a3190fd029a007e1afb2006399f647", + "peer/RUN.exit": "9a271f2a916b0b6ee6cecb2426f0b3206ef074578be55d9bc94f6f3fe3ab86aa", + "peer/RUN.stderr": "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855", + "peer/RUN.stdout": "d589626c7581fbb9928bc615364cfee49deb62dfc0a39a903417ca62be89cf8c", + "peer/START-UTC.txt": "5b78fd6d42a2b42206891318c08e6014de57d7ca46b0201cd11a166f452210f7" + }, + "source_history": "exact anchored base and recursive package provenance, sparse shallow stock wrapper not executed", + "stages": { + "caller": "PASS_HELPER_319_FUSED_CALLER 91166298911/25000000000000", + "early": "PASS_HELPER_319_EXACT_NATIVE_AND_SIGNED_PRICE 0.00364665195644", + "frontier": "PASS_HELPER_319_FUSED_FRONTIER_PROPOSAL 91166298911/25000000000000", + "native": "PASS_HELPER_319_FUSED_NATIVE 3646017316711/1000000000000000" + }, + "start": "2026-11-11T22:54:48Z", + "status": "independently_reproduced_comparable", + "tree": "fa98712a459b20c10240450097c87de433f8a750" +} diff --git a/research/p104-chart1089-split-bound/price/inputs/AFFECTED-CHARTS.json.gz b/research/p104-chart1089-split-bound/price/inputs/AFFECTED-CHARTS.json.gz new file mode 100644 index 0000000000..8acc45b5b8 Binary files /dev/null and b/research/p104-chart1089-split-bound/price/inputs/AFFECTED-CHARTS.json.gz differ diff --git a/research/p104-chart1089-split-bound/price/inputs/IDENTITIES.json b/research/p104-chart1089-split-bound/price/inputs/IDENTITIES.json new file mode 100644 index 0000000000..b1644106d9 --- /dev/null +++ b/research/p104-chart1089-split-bound/price/inputs/IDENTITIES.json @@ -0,0 +1,72 @@ +{ + "body_clocks": [ + 40222, + 40840, + 42609, + 43022, + 43023, + 43024, + 43025, + 43026, + 43028, + 43030, + 43403, + 43491, + 43535, + 43696, + 43698, + 43887, + 45365, + 45396 + ], + "copy_and_chart_local_ownership_checked": true, + "dirty_readout": { + "319": 1 + }, + "exact_basis_columns": 14, + "forward_direction": { + "1081": -1, + "1467": 1 + }, + "literal_candidate_clocks": [ + 44588, + 44627 + ], + "paid_delta_per_word": { + "1": -1, + "5": -1, + "6": 1 + }, + "ranks": [ + 3, + 8, + 9 + ], + "roles": [ + 198, + 205, + 319, + 532, + 652, + 654, + 962, + 969, + 1081, + 1250, + 1303, + 1305, + 1453, + 1467 + ], + "scope": "Local normalized rational block, literal chart availability and nesting. Absolute Gaussian phase and whole caller separate.", + "status": "PASS_INDEPENDENT_319_BLOCK", + "window": [ + 44616, + 45718 + ], + "word_sha256": [ + "0358b9f6e0340fb3e5aa46c747c558b32a5280cbf9cd92c3b9de627dd18a9a4f", + "9aa8d6b054ba7eb2289d052c1079b16be518d2f0fbfb244569fa18e3733acdac" + ], + "wrong_sign_and_omitted_readout_rejected": true +} diff --git a/research/p104-chart1089-split-bound/price/inputs/OCCUPANCY.json.gz b/research/p104-chart1089-split-bound/price/inputs/OCCUPANCY.json.gz new file mode 100644 index 0000000000..fa27d44081 Binary files /dev/null and b/research/p104-chart1089-split-bound/price/inputs/OCCUPANCY.json.gz differ diff --git a/research/p104-chart1089-split-bound/price/inputs/RANK-STOCK.json b/research/p104-chart1089-split-bound/price/inputs/RANK-STOCK.json new file mode 100644 index 0000000000..7043a8a985 --- /dev/null +++ b/research/p104-chart1089-split-bound/price/inputs/RANK-STOCK.json @@ -0,0 +1,538 @@ +{ + "admission": "scientific admission pending at preflight; price is conditional on exact #7334 passing", + "complete_targets": { + "1": 306, + "2": 357, + "3": 799, + "4": 3825, + "5": 1360, + "6": 731, + "7": 323, + "8": 544, + "9": 10888, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208, + "137": 208 + }, + "crossing_upper": "182332597822022395349777014167081/50000000000000000000000000000000000", + "disjoint_move_pair_count_upper": 3116, + "head": "aaeec8c0acf01e99a5f331ef363a698d9c084ace", + "input_sha256": { + "READBACK.json": "337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82", + "dependencies/7298/pricing.py": "f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182", + "dependencies/round41/RESULT.json": "1b993aa8c66ffce5d2d9f13cafae320c62230722d599d251fa61afc6534b1bc7", + "receipts/NATIVE-RESULT.json": "c6d1b00a83185ab0062397b363258b1f3f6685d755e9c1d4f7d3e7e511240812", + "receipts/construct.py": "ecb39578063d7f09153a85370a3b9bb7cbf8b36ff9891033a1cce7a2fe7f7fda" + }, + "old_complete_paid": { + "1": 68384, + "2": 14501, + "3": 14093, + "4": 3791, + "5": 5865, + "6": 238, + "7": 170, + "8": 741, + "9": 32, + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 208 + }, + "old_margin": [ + "-29866980917152322049/10000000000000000000000000000000000000000000000000", + "-29866980917152266101/10000000000000000000000000000000000000000000000000" + ], + "one_edit_optimistic_upper": "1903560515893109741953230020081417399578277511361/5000000000000000000000000000000000000000000000000", + "one_per_public_helper_optimistic_upper": "2095820127998313825890506252109640556935683540008461/5000000000000000000000000000000000000000000000000", + "owned_paid_histogram": { + "1": 20, + "2": 9, + "3": 2, + "4": 13, + "5": 2, + "6": 1 + }, + "public_helper_count": 1101, + "public_paid_histogram": { + "1": 3980, + "2": 844, + "3": 827, + "4": 210, + "5": 343, + "6": 13, + "7": 10, + "8": 5 + }, + "public_paid_moves": 6232, + "rank_prices": { + "1+1": { + "complete_margin": [ + "858321385403521186417773068772405712363430437203/10000000000000000000000000000000000000000000000000", + "53645086587720074151110816798275357022714405823/625000000000000000000000000000000000000000000000" + ], + "credit": [ + "214580346350880296604443267200568173320145689813/2500000000000000000000000000000000000000000000000", + "858321385403521186417773068802272693280582759269/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-9141678614596478813582226931227594287636569562797/10000000000000000000000000000000000000000000000000", + "-571354913412279925848889183201724642977285594177/625000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -34, + "2": 17 + }, + "ranks": [ + 1, + 1 + ] + }, + "1+2": { + "complete_margin": [ + "1180782193580878473879905453225185303784278217059/10000000000000000000000000000000000000000000000000", + "1180782193580878473879905453225185303784278273007/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1180782193580878473879905453255052284701430539091/10000000000000000000000000000000000000000000000000", + "9446257548647027791039243626040418277611444313/80000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8819217806419121526120094546774814696215721782941/10000000000000000000000000000000000000000000000000", + "-8819217806419121526120094546774814696215721726993/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "2": -17, + "3": 17 + }, + "ranks": [ + 1, + 2 + ] + }, + "1+3": { + "complete_margin": [ + "1389848341449443791535950684381027395734536124509/10000000000000000000000000000000000000000000000000", + "1389848341449443791535950684381027395734536180423/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "347462085362360947883987671102723594162922111631/2500000000000000000000000000000000000000000000000", + "694924170724721895767975342205447188325844223279/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8610151658550556208464049315618972604265463875491/10000000000000000000000000000000000000000000000000", + "-8610151658550556208464049315618972604265463819577/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "3": -17, + "4": 17 + }, + "ranks": [ + 1, + 3 + ] + }, + "1+4": { + "complete_margin": [ + "193142263828747485141280111129765972731137687109/1250000000000000000000000000000000000000000000000", + "772569055314989940565120444519063890924550776427/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1545138110629979881130240889067994762766253818921/10000000000000000000000000000000000000000000000000", + "309027622125995976226048177813598952553250763791/2000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-1056857736171252514858719888870234027268862312891/1250000000000000000000000000000000000000000000000", + "-4227430944685010059434879555480936109075449223573/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "4": -17, + "5": 17 + }, + "ranks": [ + 1, + 4 + ] + }, + "1+5": { + "complete_margin": [ + "834392976237489866662283238867233696199702541757/5000000000000000000000000000000000000000000000000", + "417196488118744933331141619433616848099851284857/2500000000000000000000000000000000000000000000000" + ], + "credit": [ + "1668785952474979733324566477764334373316557405529/10000000000000000000000000000000000000000000000000", + "1668785952474979733324566477764334373316557405563/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-4165607023762510133337716761132766303800297458243/5000000000000000000000000000000000000000000000000", + "-2082803511881255066668858380566383151900148715143/2500000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "5": -17, + "6": 17 + }, + "ranks": [ + 1, + 5 + ] + }, + "1+6": { + "complete_margin": [ + "1771542005129348740048881099908835681263784441249/10000000000000000000000000000000000000000000000000", + "1771542005129348740048881099908835681263784497197/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1771542005129348740048881099938702662180936763281/10000000000000000000000000000000000000000000000000", + "354308401025869748009776219987740532436187352663/2000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8228457994870651259951118900091164318736215558751/10000000000000000000000000000000000000000000000000", + "-8228457994870651259951118900091164318736215502803/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "6": -17, + "7": 17 + }, + "ranks": [ + 1, + 6 + ] + }, + "1+7": { + "complete_margin": [ + "1859458789326391366180127207106590253932358169757/10000000000000000000000000000000000000000000000000", + "1859458789326391366180127207106590253932358225739/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "929729394663195683090063603568228617424755245903/5000000000000000000000000000000000000000000000000", + "5810808716644973019312897522301428858904720287/31250000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8140541210673608633819872792893409746067641830243/10000000000000000000000000000000000000000000000000", + "-8140541210673608633819872792893409746067641774261/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "7": -17, + "8": 17 + }, + "ranks": [ + 1, + 7 + ] + }, + "1+8": { + "complete_margin": [ + "1936286205289343096186514461761692902526099784907/10000000000000000000000000000000000000000000000000", + "1936286205289343096186514461761692902526099840821/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "968143102644671548093257230895779941721626053461/5000000000000000000000000000000000000000000000000", + "484071551322335774046628615447889970860813026739/2500000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-8063713794710656903813485538238307097473900215093/10000000000000000000000000000000000000000000000000", + "-8063713794710656903813485538238307097473900159179/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "1": -17, + "8": -17, + "9": 17 + }, + "ranks": [ + 1, + 8 + ] + }, + "2+2": { + "complete_margin": [ + "342461829925360215799616613766761397431076780873/2000000000000000000000000000000000000000000000000", + "856154574813400539499041534416903493577691980131/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1712309149626801078998083068863673968072536226363/10000000000000000000000000000000000000000000000000", + "856154574813400539499041534431836984036268113207/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-1657538170074639784200383386233238602568923219127/2000000000000000000000000000000000000000000000000", + "-4143845425186599460500958465583096506422308019869/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -34, + "4": 17 + }, + "ranks": [ + 2, + 2 + ] + }, + "2+3": { + "complete_margin": [ + "1038332533337951243124209252323374732610103592089/5000000000000000000000000000000000000000000000000", + "2076665066675902486248418504646749465220207240109/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "2076665066675902486248418504676616446137359506193/10000000000000000000000000000000000000000000000000", + "519166266668975621562104626169154111534339876561/2500000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-3961667466662048756875790747676625267389896407911/5000000000000000000000000000000000000000000000000", + "-7923334933324097513751581495353250534779792759891/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "3": -17, + "5": 17 + }, + "ranks": [ + 2, + 3 + ] + }, + "2+4": { + "complete_margin": [ + "2355602677701438428037034298000189461885076143183/10000000000000000000000000000000000000000000000000", + "1177801338850719214018517149000094730942538099557/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1177801338850719214018517149015028221401114232599/5000000000000000000000000000000000000000000000000", + "2355602677701438428037034298030056442802228465249/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7644397322298561571962965701999810538114923856817/10000000000000000000000000000000000000000000000000", + "-3822198661149280785981482850999905269057461900443/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "4": -17, + "6": 17 + }, + "ranks": [ + 2, + 4 + ] + }, + "2+5": { + "complete_margin": [ + "64550164305020182173891862721772434032493977189/250000000000000000000000000000000000000000000000", + "2582006572200807286955674508870897361299759143457/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1291003286100403643477837254450382171108455704779/5000000000000000000000000000000000000000000000000", + "2582006572200807286955674508900764342216911409609/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-185449835694979817826108137278227565967506022811/250000000000000000000000000000000000000000000000", + "-7417993427799192713044325491129102638700240856543/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "5": -17, + "7": 17 + }, + "ranks": [ + 2, + 5 + ] + }, + "2+6": { + "complete_margin": [ + "2772679409052218919811235238243020222832712173803/10000000000000000000000000000000000000000000000000", + "346584926131527364976404404780377527854089028721/1250000000000000000000000000000000000000000000000" + ], + "credit": [ + "554535881810443783962247047654577440749972899167/2000000000000000000000000000000000000000000000000", + "1386339704526109459905617619136443601874932247943/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7227320590947781080188764761756979777167287826197/10000000000000000000000000000000000000000000000000", + "-903415073868472635023595595219622472145910971279/1250000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "6": -17, + "8": 17 + }, + "ranks": [ + 2, + 6 + ] + }, + "2+7": { + "complete_margin": [ + "2937423609212213275948868600095877444095027517461/10000000000000000000000000000000000000000000000000", + "183588975575763329746804287505992340255939223337/625000000000000000000000000000000000000000000000" + ], + "credit": [ + "734355902303053318987217150031436106253044959869/2500000000000000000000000000000000000000000000000", + "2937423609212213275948868600125744425012179839527/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7062576390787786724051131399904122555904972482539/10000000000000000000000000000000000000000000000000", + "-441411024424236670253195712494007659744060776663/625000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "2": -17, + "7": -17, + "9": 17 + }, + "ranks": [ + 2, + 7 + ] + }, + "3+3": { + "complete_margin": [ + "2564668825570003745693079529156031553835334050633/10000000000000000000000000000000000000000000000000", + "256466882557000374569307952915603155383533410653/1000000000000000000000000000000000000000000000000" + ], + "credit": [ + "2564668825570003745693079529185898534752486372631/10000000000000000000000000000000000000000000000000", + "1282334412785001872846539764592949267376243186341/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7435331174429996254306920470843968446164665949367/10000000000000000000000000000000000000000000000000", + "-743533117442999625430692047084396844616466589347/1000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -34, + "6": 17 + }, + "ranks": [ + 3, + 3 + ] + }, + "3+4": { + "complete_margin": [ + "2946362489249908694206009944683839839364582367373/10000000000000000000000000000000000000000000000000", + "368295311156238586775751243085479979920572802913/1250000000000000000000000000000000000000000000000" + ], + "credit": [ + "736590622312477173551502486178426705070433672347/2500000000000000000000000000000000000000000000000", + "2946362489249908694206009944713706820281734689439/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-7053637510750091305793990055316160160635417632627/10000000000000000000000000000000000000000000000000", + "-881704688843761413224248756914520020079427197087/1250000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -17, + "4": -17, + "7": 17 + }, + "ranks": [ + 3, + 4 + ] + }, + "3+5": { + "complete_margin": [ + "1630341583973160089627948131376151155723919520129/5000000000000000000000000000000000000000000000000", + "3260683167946320179255896262752302311447839096189/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "3260683167946320179255896262782169292364991362273/10000000000000000000000000000000000000000000000000", + "815170791986580044813974065695542323091247840581/2500000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-3369658416026839910372051868623848844276080479871/5000000000000000000000000000000000000000000000000", + "-6739316832053679820744103737247697688552160903811/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -17, + "5": -17, + "8": 17 + }, + "ranks": [ + 3, + 5 + ] + }, + "3+6": { + "complete_margin": [ + "3528183420760683542117844246779527821574533741651/10000000000000000000000000000000000000000000000000", + "1764091710380341771058922123389763910787266898791/5000000000000000000000000000000000000000000000000" + ], + "credit": [ + "1764091710380341771058922123404697401245843031833/5000000000000000000000000000000000000000000000000", + "3528183420760683542117844246809394802491686063717/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-6471816579239316457882155753220472178425466258349/10000000000000000000000000000000000000000000000000", + "-3235908289619658228941077876610236089212733101209/5000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "3": -17, + "6": -17, + "9": 17 + }, + "ranks": [ + 3, + 6 + ] + }, + "4+4": { + "complete_margin": [ + "3415972937126856268850186467409402697562404412621/10000000000000000000000000000000000000000000000000", + "170798646856342813442509323370470134878120223431/500000000000000000000000000000000000000000000000" + ], + "credit": [ + "341597293712685626885018646743926967847955673467/1000000000000000000000000000000000000000000000000", + "3415972937126856268850186467439269678479556734721/10000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-6584027062873143731149813532590597302437595587379/10000000000000000000000000000000000000000000000000", + "-329201353143657186557490676629529865121879776569/500000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "4": -34, + "8": 17 + }, + "ranks": [ + 4, + 4 + ] + }, + "4+5": { + "complete_margin": [ + "237945064486638717744153752508310488639962668791/625000000000000000000000000000000000000000000000", + "3807121031786219483906460040132967818239402756587/10000000000000000000000000000000000000000000000000" + ], + "credit": [ + "3807121031786219483906460040162834799156555022671/10000000000000000000000000000000000000000000000000", + "1903560515893109741953230020081417399578277511361/5000000000000000000000000000000000000000000000000" + ], + "margin_with_extra_rank_one": [ + "-387054935513361282255846247491689511360037331209/625000000000000000000000000000000000000000000000", + "-6192878968213780516093539959867032181760597243413/10000000000000000000000000000000000000000000000000" + ], + "paid_delta": { + "4": -17, + "5": -17, + "9": 17 + }, + "ranks": [ + 4, + 5 + ] + } + }, + "scope": "Predecode price only. Pair arithmetic grants all ordinary and physical costs free; each original paid MOVE contributes at most once.", + "whole_move_capacity_optimistic_upper": "477927259198812997685714233883646598515886014070727/625000000000000000000000000000000000000000000000", + "word_git_blob": "73f43007192eb5a38eb5abb591b871df3e52c7cd" +} diff --git a/research/p104-chart1089-split-bound/price/inputs/derivative_check.py b/research/p104-chart1089-split-bound/price/inputs/derivative_check.py new file mode 100644 index 0000000000..ce5cdf3779 --- /dev/null +++ b/research/p104-chart1089-split-bound/price/inputs/derivative_check.py @@ -0,0 +1,67 @@ +"""Check decrease of the complete priced moments through the retained BIT cap.""" +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from json import dumps,loads +from pathlib import Path +from runpy import run_path + +ROOT = Path(__file__).resolve().parent +PINS = { + 'PRICE.json':'52e05b80069ce01cad3b8e5f3cf9123e930de36987bd398dd43f103953a4674a', + 'inputs/pricing.py':'f4d0b6c9314b838d882d6d06020f24881c19a3fda97a7c00df87b1e920785182', + 'inputs/7334-READBACK.json':'337668788fb39ec9575887f9c5faf438a880471f78d936357dabf7deeac5de82', +} + + +def derivative(histogram,low,high,tariff): + log,power = tariff['log_bounds'],tariff['power_bounds'] + ln2_low,ln2_high = log(Q(2)) + lower = upper = Q(0) + for rank,count in histogram.items(): + shift = rank.bit_length()-1 + a,b = log(Q(rank,1<