From bb36fc65ee0b161229169505f4840c436c5ca2b9 Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Wed, 11 Nov 2026 14:22:27 +1100 Subject: [PATCH 1/3] Reuse #7147 selected replay navigation for onboarding This is the exact documentation prerequisite retained by #7156. It points the onboarding check to the selected #7000/#7001 review. Credit to Rohan Arun and the source authors. --- docs/ci-verification.md | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) 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). From d2e54af81f9dda6487636b79d4964a2385d89b2b Mon Sep 17 00:00:00 2001 From: Clear1nsight <22630354+Clear1nsight@users.noreply.github.com> Date: Wed, 11 Nov 2026 21:53:51 +1100 Subject: [PATCH 2/3] Replay the historical selected check at its inspected commit MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The PR #6292 rejection census and package plan are statements about 2485805. Load its exact sources and planner in a private sparse checkout, keeping all source hashes, 19 expected rejections, nine package selections and the empty-plan control. Subsequent edits to the live Makefile and CI guide no longer invalidate this historical check. The original audit is by unpaidmoon, building on Dennis’s historical replay gate. The pinned repository view follows the precedent of Matarener’s PR #5434. Repair prepared with substantial OpenAI Codex assistance. --- .../historical-selected-replay-gap/README.md | 6 +- .../SOURCES.json | 60 +++++++++--------- .../VERIFY.json | 31 +-------- .../historical-selected-replay-gap/verify.py | 63 ++++++++++++++----- 4 files changed, 82 insertions(+), 78 deletions(-) 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") From b58b30291adc8fb891229936acd6549168a6e10d Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 08:05:13 -0800 Subject: [PATCH 3/3] Bound coupled BIT chart relabeling --- research/bit-coupled-chart-bound/AUDIT.json | 13 + research/bit-coupled-chart-bound/CUTS.json.gz | Bin 0 -> 52963 bytes research/bit-coupled-chart-bound/README.md | 104 ++++++++ research/bit-coupled-chart-bound/SOURCES.json | 30 +++ research/bit-coupled-chart-bound/TASK.json | 77 ++++++ research/bit-coupled-chart-bound/VERIFY.json | 24 ++ research/bit-coupled-chart-bound/pricing.py | 82 ++++++ research/bit-coupled-chart-bound/verify.py | 241 ++++++++++++++++++ 8 files changed, 571 insertions(+) create mode 100644 research/bit-coupled-chart-bound/AUDIT.json create mode 100644 research/bit-coupled-chart-bound/CUTS.json.gz create mode 100644 research/bit-coupled-chart-bound/README.md create mode 100644 research/bit-coupled-chart-bound/SOURCES.json create mode 100644 research/bit-coupled-chart-bound/TASK.json create mode 100644 research/bit-coupled-chart-bound/VERIFY.json create mode 100644 research/bit-coupled-chart-bound/pricing.py create mode 100644 research/bit-coupled-chart-bound/verify.py diff --git a/research/bit-coupled-chart-bound/AUDIT.json b/research/bit-coupled-chart-bound/AUDIT.json new file mode 100644 index 0000000000..e44f42dc0d --- /dev/null +++ b/research/bit-coupled-chart-bound/AUDIT.json @@ -0,0 +1,13 @@ +{ + "best_directed_whole_upper": "-150259748047868384659982093203238820648182213478633/2500000000000000000000000000000000000000000000000", + "certificate_sha256": "1b99adc18dc7bb1839cc98d17b3be022bae939dd16d0f7d6bcea8fc24cd1f678", + "changed_optimal_assignments": 0, + "edges": 62474, + "forged_flow_rejected": true, + "scopes": 897, + "signed_original_net": [ + "-300519496095736769319964186406477641296364427008833/5000000000000000000000000000000000000000000000000", + "-150259748047868384659982093203238820648182213480307/2500000000000000000000000000000000000000000000000" + ], + "status": "PASS_INDEPENDENT_897_BIT_FLOW_CUT_CERTIFICATES" +} diff --git a/research/bit-coupled-chart-bound/CUTS.json.gz b/research/bit-coupled-chart-bound/CUTS.json.gz new file mode 100644 index 0000000000000000000000000000000000000000..352274d35ac7dd8a66c1a2f2308e7bdeb72b963d GIT binary patch literal 52963 zcmZU(byQnTv_4F6mqKxeLZP?^cP|w8;_mLnrN!O7xO;Jj;O_2j0fNJqzW1)XertXC zV`ols&Y3+k&un@2kVPOu{rf<_pLLv9*$mr$e%Mr0nz|(Z(up5=q(Q&|8>Q=p!m@^@ zvo0WPyy5%Tw8e>*$~vc2qXoY`P4$E5y02o^z(e#FCEoj_(97-Y<FjI@`)V41fh=xPK*j z-e19e8o;Gw&2=bE`yDBA>bW3lI>siakmVUkLq*e+91pT7UDSwC>LOB!cM+3KGvS(} zh98bh%ks+auRjnh)aak1uUDc`k$ZWT-&|l{EV}ZItQ#AaEd=5uBaP~6pB6aB*~Px? zBrD4_nr4GS%<1dj-Wu20_@ky>I6R#}Ch~3^rcT%O>-*0Oa;3$?1tV73zf8PFz5{_K zc2u7qg^XA$qm{iFJB9(%H|2-+;D%>2Q2nl{RGWRLeODn({JKIDXFQ2*q6izY?HC37 zpOLjBj7E+}sfs*aImVm$AP#;4cEv%UQ!-qp={F_5WEs-Zar&>NMRZ~QndnZiz`0~k zCU<()ll#rTiJdG()IusnYt8xq-2Lx~u34c_ayj4As3Uwij%kmhXHd)uMkt;!)Gk2v z)f=X=jvVH)t{n2k=iIbuMM;un`_=aZ0RJMJUZ%BslC zM&^}0i;IP4@YfWY$7|iwu|TTls5OvR8bgkxz=isZK08{nuf$LBH`SZ+D7v3q?I#vD zmE*IK6p9FL=h4}4NqQvlcP<}_x|)1}owPArX)JnX&RL+`gsA3k%USzeBXvSCyS87~ zHM$zDJ6TLySqndN(~9u5knW)|@&K9@To^#~p)&QSjs^>k55ao^ESg|~$A$gf%ks17 z%_&y>)E$dc+vui^1>(n?OFsMLUvvmp(h^%%=N;pMrW?2P_3CbKeW(hq(qSZ3PZWL! z8urYU&swu*7K3Z<>p$gFb~P|a)eZu?=a|Bj;x2#;<=mqmlrWlW+FxVpb8pHghulEV zBP_SFDl}$*Cc@)Hy5cz90~1QcW#c_@Vq+XYmUNS7+F4;M0qkLBjI(7h(4NM++`&Y?i>7{NlGebVmZKYha^LM zp6n3fFABD4Qx*&_F|MM`uH+-DP8ya+07i-TiX|}NG9{EsIjpGMx$Su+$lL8U@HCri z`-fiK%Xkv!o<)GW6prrwe$Y|h;s&?g9XhR4eX0PQsDtBP%E8G&;b@hcp&JfD&-%PV zUv^dBS@^GA&!3HZyJT7-E>|#>C>EpQPB(w(+`Ab@beP^*;RrN{LIfz3dc$JW9Gb|*1N3Hl>j@#Urih>q3cfz6y3zal|kZ@ZyY=yJk)tLfXJO?24dyl>a=Y~Q12 zQ&{HmuHj8-Rd%1bv&RjAm;SmSc)ty>x8331G}K43+xZMw_D}%V1RXoGnR^^%&+?V? z)rVz49=dPodeP;Nm;}dGUpTU6485MwPn?xboLQn5O}3*{Cao`KCorOC(tmzTA2#aCRlM2qZY{?@xG)4~j!~Ge?;3G6 zn-4t=PK6~1pzEf%n=K4w?AT!NK_0`tx*%g%4no+rnRJ;K7#Ps%arfrW{6y;v)Vlx6 z^EI@(;MD}3@01iTW6}jY0a)JM*79N->N_brUN$@GBXu*22`V2H$i4QNzcNs`7VgM8 zcf{iKIc(75PnZOon1gx3qdKItaGh!ivd<{=*LQc$TCvZIUHW|2o!Myrd++w^ydW@5 zU_DI$eTVYG?(*hjWl4b6y9_cDj_PZ_+z8QUniUS@5lA=Ma#-ra>UT_{BOoFsqTYzN z?N`>BA*2%zgr?gw3wOh4gq)>iQj9d1`(}L^bkWMmgPMBCg!*2Xcq>kv4NsgoZb|$d zy3WcHWE#81JaTRtk^p&mHxWG541MtSW}|Ie@&V5C9hxX8X27UkI!34Iq0SFypNx?r z$b&kvRgZ^L08EmnkiMOF5(h5GDXwgy5so9hWnI9SE-q|C5>wNV-rdb)CqqX=1O|d+ zCx(eJGPVV3Iop6{Jga^G`o}0xVe)pX0py(1p{wRxC1|c}ej=6(hgv{!smHN`Tgxe^2s$_H?j^&WmeE%)qeNynZN50A1C}%kMyE zxtY^lzxh5vpl?8_XY#V7&1`a*7*A@z!_5|K7!x)inA4W#-tI8buyQQnO-?g0N%Jxk` zq0u+ofIyuZDtr7ocEZbCYJ$N1+05Aw7r)JstDgBds9u27>;}?zz30OS67MRz?{b0w zap9~6)9Z5fcA0lkSj5sRm!_AanW8fUq&^GR92C<*04C+Y39tvx%4K}h;oh5XpPEnM zcINrD!#sYcYVyQCxLiBjw4iX9GGZs|YyD^NZe@jC*nluNg$=N=Yg}ZVM z_1R=Ae*J!an*AdGWkc%zFMbuM0{y6S+e;gBRO0^cR*IRgI>KC-0BO;`S)DCzp=Sc* z;P$T!ZESpEP7C1}V{2{%yFNhK?u%66U%zB?|6%u66}>PvL}_lHyM;Kk%aI>d4r%jTd` z;=!+zfo8Kr&J2;W&aNFf`2-F+2*j5&M3^pq7po%JgC8_+XoGzCF%=y@toMayoe^yC z0taYZVs@EZJlTPLIJ~R7Mp5hRB(jVfs8*zs418^051u17LOgndLs{6_$-J+f69_hugPMAe zmQh!h#nyE&TV1)ug?(ff z8|Lx6qTqgfw$0?r1{@Brt*0BGG@F`0C)_BSa^NzW)j{}Xt`e>gZ3&tZqYct6aaA4J z@H(=avSIQn@i@(cjNxk7cNJ63-nmsUL-hGVbS~R97RB2~9x{r(VJ(ELmu`q9?&}Ng z)YntB;uYl*3(z-Fvr1MIUzz?(Uj!j3G@UD3C zS0@7CeSQ<7;_r70BE_-C&glL&@KlSvciook?#H?Pr3V{?N*SR1b87nqiUaAKj77D8673KD!PXkQ(HYf#PY2vqc)LX}uIFy| zut?GY``JQ?cl6 z2J4AQBeXnQAA|K3vMR4k=OWxS8^-Y+^2bj$$hK#>;EEvrCFg8mK7`2jN>9*&*nOL| z;sz?n!LwsXA&UYpdvO)tuZJptdD2AISMx6?%rJ$B zYNOc0v+gEe!7KdVr)a%_V!2bVbs|j2sM)9|OtNPUi9UBz!?_pv@+xhMFBEvaAljhz zvAmtiu;0x9)f}|tCf{otMMDhmntj#!5Gn-HM%_nR2%a^?v`(xB>#L}(L-Mp_Z5%=w zGfb!;wy@AUboo|BJC& zxs(IQ;u_8__l*}!)dS9ZNSWD7ymfA0A)DC}GE;R?D&ZZjQ^#!Ux|z4dnbLSw&nhh< z;H@;lW#`GAB@YdLHKJQq1KOaXFiyX!pGQW&vLLGj84Ei7zdcE(mldT6LFav&%V&G| zmcMH`Cuk5zt03p2*zKy?*Ld+9U4m~#k?r0g?88PH(VjW z)%;>}fd)t9EdJSX34|unW!y(5 zva|Jc4YRp#5R)}={04z{Ls$nIzPFBXF{UYoT{|RN-lgIAp9#Nqz~=o#d^;`j`sZMK z$3Q@h_?ET!5Zo^*w$IO3oEi_-L65F?U0+e>%bMiM02+opFZ^Oqh@66pB* z7b%OLoHtFR7&)8?+WDfh?k3UAFg69i(SA4O!4<|;_4H`d@3RDPCXoA{VzKy$_IAAd z=mU;KrOs5LYyal@D1OGwlFxg#ZT0%Q?tI5pcnZ>G z-E5l3_>j!xq?g4mC7&tz(^2lWEpisqENS*sae9zK(X9_x2-tP11wNnIdji{H*FQ@R zJ)S)%^LDBf-Uw_Ki-OlzikP23%8R7`e3S=<%#WQ|afv0yWR&;8iKnc0%^`mP*UD@M zc-WiY{GO5XZ!*yvA35M#J5wewWEV_>Qe z@0lhxpo8(r-nm4OsLuC!2NHKG9;tMQIANtZvz4?VDhsL+Q)9#dZW2Ep_hw(%!e`md zGLcRd|Awdz*_)z#XoUZUmPrcPFOuFx%^xy47x1&J$lVYQPnJm)n0UYZ^Rn>c+r7Dv zt$&entST@DF<%O8HABOwRvWm!-dsU$gyNH-HoG{K<|Hn7p8)H8Ww}#0)*gvtx_^mJ z68dL!jD~FLQf4Z$FiI7UGe=%1Uu9a!E@+)Ya}(p@+eq zngbUzj}_s|MhTN?My1sV8QvKeM>tF>CzXqDwFI6jBLNTJ-MB-?()z68um6ue}&Vz{Zo7TGO34)(R zQ90wyk6s*&v_uYeX_{csV|>;>_v&T%nwr^1Y_--2bYD@F-V_hsW@Qa~OJ)K-X!1dR4)u+tQ zEpMRuEbc|wnHO$#gu48`!9qW`zSdQvrM}v9 zznH*WI58`H9yZOpAF9iW^+*^(g5lfdFr+{2 zItyC0=lW9K4Ifqlq}(N*Fu_;W#sxoq-7nW>42} ziu%u2x4Y4)Rb1QI@yyO^HvIyh^aWIW(`H{#aUNL~gg?aPyc8Ew@ed)7DOKe;x~PM>tv9>~3hJH3h?jtPX?>@7RthbPf> zea^dof_A*F>z|*7f1S=R&Nn}`JgMtPBM5mqt}Fh~ttN8c@O#JrbUi=5zwYL|fx?7d zC%ayrFW*Kt<)4M#Eyu{-k8^&$&FVu~SfQ7fnD>{P>wDK|?=N$gZ?~Io57qAse$U14 zZ`FQr`k+PqD}BGmRlk>;uGb;Im#+6!zxR}!_bZ|Iq4$T!%{|(m_kR1ko}4WtXuR5N z+Qk4Vnfj5j1TFgal~rItqVB%bU!RzV0cN+C*{+xS_g9EAFZOa5^QXT) zZ?BC)FRX_PPy9d1hpZb+C?A{Y*3~1{Op7X%?6i1k_vuOIR=D#`ALo}2=Chg7X%WLZ zkw#yboIl>N?r+XWQ&TB?jx#V-IJYQmA8>vow6i1=SuHLa`oNRxpQc!w?-#^?5ex7= zeedii-Y1Q@%}K?M@&u`5G$xGhI*f!3A@S)XcmhBod`VoUp-pQTNu+5db(V`XtBz@< zqkl07wjOoJ=M&HQYhyw6Rvap14nV{85#8HN-?e4^j%Gm-)hO7pB~vB*iZR;M6U_jF ziPPzZ9tMZ8G7KEfQh63@xa!1xQm3xiU2Ux@9i*N)b4|5-td>(Z`nuU+y{_@=#ZD6E zYe{H&@xYbUi7Hv|KgFlN9~U5xi@@z z}~l^ z>Lba{mpJlRuX^iG=vwDGGT_*CQe}M;GFz5_KhR;s2PAUKq{`K!Qbd@s7523-odeO9 zo#l#+Omcyn7aYMp79L}6uYw+rdcGq4)$y`c%q3afH&PUu^2li}~yMhGZUCtB~d5j;j_gZ?XowiHN*k_`O_DzJt3LvvEzdem-r!zf8VA-3Yyj zycPJp^mV;o`@KHuzdvHUpHIHO;XT5=L+TbM?pkjiPmEn(PbSq~TS|r8@5}|?UYdp8 z{8kdXw5|{RUPmFX?0S1(#`yNQo>lO6N|t=^QZ4khn)Ckf{xYin>%PnFStyf5Fu9XTipjJz+r)qf?%#bK1wi}DOny8R=PjhH{pjW zDmDsAY|8%;Jv3|-+&m=9Ag}=<3ef6YKguAS8#(kL5(ry|fqf+Rbvjl}fYn^?s=PHc z7UNTlRumOBuJ{YRrG!Y+kQ^hWys&;o#>g_X@Xt>*i2lTX9;rQsCI~6Wz*zY3b9G=p zBFv+R_f<*`k>`+aEXAISR-?`<KkiN zDq%C-#vhZzDPB|@f8p0*Dk{AtnnpnJGsVmHXooIR8hzPQp_HV92x+>&#Qzn;-(o+S z94=EV$1{tCLJdg=8@<8~Pi|0#%rY%gk5N8Og|olRdx|9zO>>gaabw1Bj?^7DXq8u> zmpQ@3g(ydB`xMk=G7e2nl{oE1ZbFyF97z$8$C6<=6$M$Ihu%TZyb zs;J}=bdp#gKE__BF7swGA0i$`ICPSI$-Kla40Q`$__Tp}U{?KU7&KNZ71zg;ze~0_~Aqo=tZoa#uedN!pMeEr1T^$=PC6%4S=oF?a$L zf99$8QM41HFPCqRRZwD^(KMKhQuSWv^-2Y#YJ%c~te>lX#dp~gRQ;%WIl;iF^}B#F^T{ADko z0=I5ykkif>gL`wLGcGpB{R8eTrIxWfDV_}86h$>cRn{ZoN$h5Z$y_>z){jV^TmJ@* zUjR^2CzTUI*CT@xhZijr2Z;AKJa)EtO08%(oamz1uh^{!r49uqcly8ekUv zI#FMJDFR?BMC^oAi(`%ch&04ovlu=DPekj7vbUREZR;UmGWyF7vR}zZja9deU|>Pl z2D4o4q#z(+hu$(2CJV(K+Z-1;tbDxhcVR`jWywL~iPb`^@GXRyIK(UWF=#^ybar>x zkM-my7{qpBQ6V)Ax7U{e@rl^{z=Fi36lVa++hUFA zxEhdx%>X(YVU#ARc-7-|hC`(wI(S<8qfo;L?C1!SJWKrim}}gHSh6iXG_Aeonrgni zp>iIU$~m7|Z{q`66!?WTw5vq=cUKCvgifaELIIk_TsR@xxF^xQW{ke5SIw&t=_T&O z`9(7-JUzVRu_ByM8fWlL7C=O4)qv(-L*dTKkF^fsm6pvIT_6|z=GK38gcid_JoEEj zt2dPQt@572QS7O3=wb0Q?Ttq|&NT;?;tiFCy39fz<3S@2u6hr2y}7si`L^GzF!p{} z(=Xf7wq5x;5j0BQW=MDc8;9|c{u`-qH*s*9k^TlV=QD`HU%u&l%-{0;ni_){frTi~X`3_7lO^2JMWEtUK0;l~@dyCy_t)rOw zrdQpPz>hJ*&@wFZGf_R>+J`q8SOW4&9UA3Vf@IpNWt#yd3akZFtw?tJgj)CbLA=VP zwj;*u*SU~tqV--6Acj!Ar8s?t0*-^|Id?d>BaI?S|mC#pKV zSavu6!8V5w&b(}C9glT9C*8LLHm?k|w=rE6e}9zD$x0}H4r+CVeq$*^_W&R66s+Pd9qAoc;WDf zWft2u>oEUE%6+tJ%{2QINnxXcOemj-ZiUmh-eX}EC@eDeftXbR|K5$J@ z#cxHTP7~9Ph-Nfz`bDVVw>OBNZyC#scP4>Xgc?-g1H$r8;}t!7?cHZ}uL@31Zj+|*az^N2h2&v{;u*I@6$vb8 zHT%&mdt#!i)&Ck;;r;#fAX!Spvit+Np!Qmn^-Jng(pDJK9=Y{rRM+f|+6VYz%+2tn zJdALXKz;h`e)OIKtK=mLpWwu3l3oNqhFY @R?x(a z`EW3Eg-H5)D-V(MiLOkCLJTLrbzV_vojyN_Qk(Ao#IUhz`TZBpPt&qkl{o(^>`5v) zD#XHYf{Z>^&T%K6_p~kL7zom9t%#%Fg%ke<=8-WveUaLmI+Q>k-e$kEFiSSU@VVO6uq9RW{ce8}0G|FW-7oQ~!GUp;wTzC%Pg7ybI8`tl_ z?6Qs%9P|~NF?n;ix{UYhzb2?7$ie*hW-hb2 z#dq38yd75mx}QY(tX#nP22aM3zD$+L%(k&?nYoyu=61k7gLPOk2hxv&xo9S)nd5yv za>gB;WD?wW)R{a^+;NV>schli(PSlV4Bll-?b)0C#H81krRiU$83|~*7m-mXz@eGM zAZH+B{JsU?XK1u|*PBk+Z#RMD7)Xdf6vtE*(mBu+?p(Xw#EEA95yq%`udW6KH#J?a zrY93z%XAPYH+sH6-EJ0iH0|Wn^;XnuB$&Pgt==XsZA$rf8Ar>|n6AO2+#8~YIl`si;AI)I& zLzyeNE>RCtFvhPitDw)L}7&jqkhFkkBo76wBpk|q??Mu6_z{bB8fI9Zc*b86-5cnMgmk3w3OySoUK9Tq@fQQiq}JZFG0bLh znh{aDZsM~pG!6rA@^}c&3XA=IuO*Riy7S66gfBpQ$%OcH13Qm8iN=wgtC>n|pr$zc z9A*nrB6df#jX+039~D0Zm_xThDBX@%6}Qx;cl8TwdYg4eRt+U>Wcd>@)QlA z8CvPZ419vyFMX~6YH#VLP*rYh*t8Dej~UGJuIXA>N2*}VBVW9L2`a=}W&&Gj-(O|( zlw0U~aH4{kqzPwQ=lqc^ya99l){Y2K-x`f8yvNd3aKRc8e3r3XDbV(n`tyxLK=PRL z7Fv8CcQDG7t3L|4t=G5|EsM!Ke=E~I@)An2RqZF{+9Hapwbww4?)B4tJBu(^D-5)L`7YGQEl!hja2)4} zH2W`=C2aO7DzhyrV|e+5i*x6#7J3QS<>;P7uG1*lRVaUxXU%{-j;DPXepVkBZ)6Tj z3@Iy*oldl8g8&KPX(*L0eC!_+QxdO1h~LAZLjDtnmBB7HEp{}JkT5)aOB{rY`&`fQ z$KkTn&2#@-8Q@T?KTR@41H_-L_N@viWF#&wQ|Idbv1YDRW~kO+1Vza#iT|xdwwfy- z<+Y1MNS%tBQj~Iok(!ciiwZ`NZL7;a64e9IWcu?mYIwzGjN+~86VsNByvKbw)`$JA z6u(T=hXFb3ZYd@v73`Hp+wMPTiCjMn1U}CAd94QDDtpC_vN(A*k*D}Y>2{8OOpP05 zw3n40q757Urmk<=ZPoW*(oX(&vBDmgAUnE>!X~)8Tz%2fW6W$a$O^9hk3LuRA@yR) zw-7NmZ|QFvLMsM+?F$%&Ke%ghJtUnz|6ot&kxL0@lkgl7bTvUCy8{wM(RaN#P)3VO zH9DCAo>V5Zw@l3g57i}PUb3stZ{yhyrV?l{s!H5)wv|K_emHsgw z;`f(>`l-18anpJ%N-EK(@ofzE#&SZ`cCiSpsm@y5GsdR>6rL1AeB7ykJ)v8Qe7aZzWRQ? zT!#zIe8f{&r2nI`cYmU*^@V&y(E9lL!{t)XLgiVE$^!MfYKj=sL-2r8+wG|qhsyI3 zDobP6Xs&f5Ef88+pM%j0m$~a2mMue!{s1-3SGx-P$F|OfmyOOCnX8QsM|}swpMwmZ zVfZq(^ROU>9uZPULF-&&30nU$VJTY}*t(4>8z|v;N>~gGOhV<_w$^1t85^}pF)%UD zcpioP7hr=3Hs7(FcCWRc^#=ANqSuxHBYD_ely{ysr`Ej}DLHW6cCSiF+qR~y=i)8( ztO{=SDXpCr8pMv+V?xsPM$H&sF-wUy2)P!i%uwFm&Ozz7LDKK$vXrHD=NDRJ7Vx9V zB<~Eg<-%ZI7C}3>(Gtn)OZV zJKH@Qiz5y?d=3}a5!^8Zu!7)E8HS5w4*(TWWMnH5SmDGAM&mrlf8vAGxrE7G@1lDx zfO%Fiqi*PAVZ-xa9Gh&mI~> zOVfuMl)tDu+B9=6PLYy()Tw=keBl@4^6#k1*z0<;9u1swT{0TCI$1sunS>RfJ&=h3V_r>yLC z=K<GUTS*qdy$BrPzSxV4^->k{(J8Zqp(W)1OHS^b! zs;f%Yop-Q;@HhKzrZA$&dO|w4BO+fqnOna(csU1Xnz2$lW>p5+q$FOH=n%U`6xdzc z8&?$AInFUgw+?88D>d_+;PO@JWD=|14wTKtbnTQ8es(!@7bRh#1giOJgjhnR=Et6l;y$dJU7#SZVnH{y5RN};(@ zy=KeeZy82?n97UO-d37B{ghd3LCX}qjr@a(6{pJEEIQeVH*NWDUvzQ#?g$xED+}e8 zGL@1Zq{Sjkq-bg6+CHo{Q4^jW%8-y~V}{mjf1eVMu`*U7(t1nzUgLDy<7BlgD}Qz% zET~q^bb8B+(1o_s3G&nZT@1ByFO_MVeCKdBB=<%Xi$F|_+m|jI)YElRc}~#S=CvFmd`C##hGbRyl!A6^PC%pxzARg3zbUWUIS>H zk|VX9X#t9VLX0L2b|{6<5t%00j%i75-&1AYEH^_QJT{4D{xY53VK&CnME}_Psjum! z5^2F7>f#}{i|7tu>8d7uZNT7Q{bDq+2%rl$1GyfoZ7q0?6};@?>?xO3B&M4L0GFHy zI!KK2UlB*+m(@C{{+cQk!pM{PM%g*AzE>l&lat?=x}X?*!DEDX&4EKTE!Wr0`|!GQ zMsfV{BWvQiVADRzWx5DY6x?1r^=FD&#^v^;1`BO-9uszZNV1tFY#wgn!Sii)vI9Qm z#P&&Him*Lt+=n42ysn$i4gFLdY{)pm7O7%_2TT%U?QSSJ%EKmZ++5F1ix66YQh5$V zYh4fqoFnaVgau12SH=1+U3iQlSwTP6Y3|tn{y^ky)NP@Gx`e2gy57p-QJ73COS46* zQ~moW$rL#nX9{sB3^mM$cv#`61VhB4xjZ{mSey3lzN#t*^kKY;0TUE(oqE7fof$Jr zs!~0U6vOEmn8r?egB9p3S)T)KSOxLX)~wL}%c@t)buz+6R>|TCNHL{p6nP&%(o^Jt z1hyGJF=oY9BP77(J0>m4eWS)$D2NM#mOKwhWs5)?DodhK(5l?M#IptbP;4Z_D%1PX zX&c>juo~kTYq2JqKwE!n8;_=)&ScBv=f{C2db}GkQ^7AoI8`JcPoI&~ed_}2L41yb z(kf4q&ekSP$SgGI=l2CIKW>9shrE>|Z~0?7W8N~zR*7+-vme;N#A>7@U1*Q@oz>sO zx0&e56j0Q01aCbZ1&_CGu~2Eli&@V3KqM_T7OGJ=h3PR|0*BSblHo+AAbS)}po7Cae~7bHS~8Wd zWAb2|gMq|R0eh=SXoz0ir&DW@%&_s}U&)coR{dolbh8Zy_D4;0zNIIF(;l0SIKlx0 zb^hf7ln;m>uLjL9{)@29k`&Av<5P7`$q~07-J=|JQ{#IKL5R>op_` zD0PaXF!A*yL}VMzgx1l1=6QDCK6`$_pXh`$C(C?YRXUoPm%$@|nXMx1$*oG0tT7Pg z%WyUe{HHhOUfs-10tQ@+)|re8+o2v@JtRvHHwYl3)g&+3$o1M}VdYERFz^aGMl0e@ z-N0k*z$Gq0D8j3@{XwO)B2GwFozWUJN%JgGCsHh^`FwA9Zq2S(>K%Wl;2~dUHbvx1 z*xc?BipDcF;Abg%r@Z06EEq5&X-@o;sSTCc@3u4;e9HfAv!BViW|VB0Nr+gW(b)d^ z50nd8X_7FH#y7?OdO7Ds-#9#NB#U^jPI zD-aeGjA%rI0)jOQEJ=O{PnJbD?we&^Lk^JgkrHi`JdXrr~b0~d}B|u z`B*gcWe(~dit#>{+d7tCn%Zm^*KzzE7R^B-oi4C`;#X3zelMv#WUcdhlHjQ|( z_qeu!C9s&=G+1^Zs*nsH6Y@~FKS9E%K@Ql@OEEEs{hEbq+Z4#QV&Q>5=aprz+8u7r z+-Dl%7n)$#3{zUOIcP|o2@#B@G-}1{Q=O{?`ryZ2cLTwAHHwJ9_*k|9p7FBD}ohyjkvcZ&}JI&lz|6CqEpo(UGT4jE%%$Wz=OFQV{z;~ep=#E zB412c2sGQE^!fq#vYG3XV$K$bGZndR;qmF%teR3lrTL()=%6kUEw&X{ff9v3heAqZ zg`?;_7H^j#NzT$Js~c!7R%l29`;po(Hdy4NWc0x&lRXQ`XtSw!5jneLSig?vFR9$Bj0h8<})M>&YO#8I}K_CK+~;O4AnRqF@dUv^Gwv;%RA1 zudvFVx8iLXI6V8~vE7b5?HN8kt*03agSuW&!jB>Tadku&VfVQ_@-i##fq?>~p`V?7 zHA=$ZlU?Pqpx>cb#d~^$fOG1>dU186)>8pN^ZyVuunCayLa})3Y_OBW03c)|d3;gZ zM14p~%tv{Whb00sE0Dx6y?DtmNR-6F@}g7}s{t*XCm{X~rC>{pWhAsF#;St~(X366 zFrZsC5CqE0FP^FxL@_1c4|?4~Dw05iznr||MzVLr8dMn*vzk+`MJlZg=Nex0<%1B{ zm?q65jQf=KmkfB1E;eulBhQAU_BY~{z=U??*Jop^gV^!rZ=T_wNjVV6+M@Ue&1fh7 zk=1c+0{@ZK;BdPfBf|mfxeb;alYS}zJgiO?9rIsgB`;`KHDds>G%_6kn zjI1HdlH@@wODbBUlg&@NZ0E+h_yWG2+19}7=$~hB@cZ=F= zp>pFTSZwBbq2!}0!!|sAfXH=(3K>&)I3e02Z(+K9gk73+6T?tb9~i49rQmN;M&K$S;Q}QaBQh zR2bBmVjqurqUeDpy5+vo#xLJP;O%jbQt%K?q#IFDzsmdMH+A#P&J;8n(_F~EgAU5p zVgk|~GSKW@LW>JU=JeA*io%fe_(zB?-%TDQwd5WyAt6@zf3xFWSX8$_?P_;uVXCh1 zk5GRe7v0vY5kGyZ3p-08iCBVb^`&~`jfelZ_%ADt1<&iIiiR0cI9;6LJ+GfW+MJ|R zNd*r+eJ9aD@ENf}eC+m+Z(7hKv*}=2YXutjai;3+8 zm94K36}PS#B1g_a$Y!jmCq)L+V`k(k1r+8hB9-&cOZ5(f4PMqgLO1 z5m(oR1@XKq?C6?jE}(Z+SR+18U8Rnv^IS59-;huEk?;6GO0MQh{xi!xS5CtVW5r;P zWz6>V?5)Pb+Pe@hn9@irAoJpP$;BCHBFg#@858ioSNT{@@2j z2P=(rA3TWR*@ZB}u+AG0ULSFg)|ud}M|G@Jecxybg0Fu>rufKJXb-W>-I>2VBJ}h> zdpzU*DTu3NG);^KL zK5?sEiOt=L<{Yf}fMP*U1d`Q4IbqZNo-z*SihX*f6>2`|WHJf=881=yyOYT9tBLBA zN06OEjeid`JjzilTz}hhpeO3V^^g&%&IIo;_M7k&CMa*4wUXTpuit=lQ@ngBm+4#- zTDgh#LxL}*^>Qq5{&71CvG-;(bb+0A(gKJ`_&zxkWdP*nvnyBt; zhAYE%{1kzz-S-xeefT7zPX-0hHmd$n$TfmI3jM8XB96E>(ewFr%Ug8=C^XqMX4cv^ zBBg+dn4zqFN~ks?)JmiCoy6>A`?7GUY$2ZCGgidfu-%$_$570c~C6^p5-n9&m+nyFf>Hh+APWOX6c?bon9{m+a zW+AJP()-UM{j)_-CMqd7k5G%6^O!SGE}mvpFGW@DLshLZDkuAc4z_l0W6gK?fv0OK z-%9@ktqscJ(6%h z9&N~*A&jB;&KSk?SLN-o^K1*r-n5HUzWa9DS^*PMOjY2*U*jdaPu40TPf<1%E0Fr zhyQg?249XN+-b%eKI5p%= zgkLF@{oN#xBg1h#l8t^R?`?;4hRrfUmre+g?Sayhu99wu@Kdj;rt^3*V>EhX$V{m37;b7Vwa>qC z7&Z}Qu&*XoP|SOpi4-+kp_jUOmCwCN_H4f6q`eiTy*)Stpq1X6md!o0ZI|8?8kz9( zrG~WtFJ~$S5XA{!b_BVkJ2X1i1`rYdLu9Z7!~G0$jMCJ{wO`Y$$n%2EUPlBRSL_!5 zBk4tK9)+*G)_6tuU3pBnQ}Cs2P(9aDlelzxHJ}vxylf@Ur22ohOPz&D{PmCUzz({u zAd>z26YI?o+tG;ZRpd(Y356%lSliCOC4qQ;MzYp|Ww_1J$vFPLa_mtCfmR58!o4Y+ z`vO9lzO+<7MDV3Otv`Em8;5xn$o1+{X%?T>dX-W~Y-_q7E z_)2H<=&uoXX>uN=|DYa39*|_e|LZ`fFHvF#ByJoLZi7i{HsRL=IS-)-g zK+0CmFOBvwYq39Cl4uke2$TT+h2{zTcB7D!n7Ya%HUN@c4wLRZN&WqCu6X%erqxVg zp#CBqwpGm-<;DKxVPY6ZL}60aex3+{o@qS5CgzW0U?h%|NbHeeuac1;8+`muaB@Z!tVST?q{;%`2^wl&gUq3 zLF6O7zP;QzMfQo6Ts#uyo3h`UxqR+y{y!eR0XnYkdpl{^#x^Et?8dh3#n94r|NktHJ}GAckM!_6Edtes zSEAP(`p--!zUv@!XOFs>UBL35+&gJQ0@-*tM#mhLDF5m_iH?CFue>AsL9Hj84Sm%>#YR*2!gvrwO%S&llhFb7 z%fDiN*|baKPhwO=UIQFEtbBCWSJEs0s!?f1Gt2f#o}9Pv?MaJ;iEnnC1h%L2zgNx2 z0Mp*#<pPzQySpYnvD6{QHv1%0wL;7zM6#4|}A@}d1=aJyj2 z(-nj0?5Hhm@`F2%Hkfojt1o}0M?Pc5-#> z)|sIk(r-w`HU&v4c-=-cebZpLQsTm{;5|o{7Lg22*%-~-F|Ei>zhzoW{znyk;cMtb z{H@?Ys`j)W=4JDhOGPweKQzg4#!%>;UZAOI8m;u)A;B3uW!ZjbEhFxg{;6A1?Cj^G zmCDl*xP=9((;kfvjD=|(+Ja{{8W`@AsOt9eXyU>1Fiy-i|2ScTUe(qo*8tlsiJm37 z(4U9%T^Z8bhQmp8dda#M&f(Umlf@Q|Y8tUB;(ThR2~KPXt8nSDc?sRV$$Y+WH;T=q zFtWF)_lqWQ@ffNu-=F-2Gg}i`N<{2cvq7Y&GfydNZzJ(eYu?N-56wgm2L;1>gdyVi zVwc&S@+O!ve-#MXEZppiTunTi(2lj~qv{sGY%_fY?F0&N5}rESZ|uM5po+g7hv`xY z*1jgM6Mysl1JdNl3ax{-i4zZy($OCT(JVJ1#KTuZq0W$09AVV&Vk85D`yx5Oe#4 z5v3+)#W0cdwZKxY7Q6gub@uy9bj~-`QA~G^-=6?s$gfiQ0C-gC#3yQtjsbnruIw!q zGsrTzyo@8&LS(jhiKw)pV7>8ad`EOIDYJOq66Pe{lKH9Ql(jR!p)Kk-m=e)CrgBR^ z4N`6VjjG$K9Z7=b7t~`kM`xM+m)!DWjJC{8#vWl>ZNyE#f$TK3K%6Q;u8W9mCO){} z5QcYV^M+q%87T#m+ZLqAv|-ogwDXU==@yWx<7h#mzDw^KhBr~Lu-;)@HRf|az9CG;t0;@ySv5)rY8g4=nxFz zQIhBHqlr&NV9vhQ=R1mR#Z%3(3O*`?4hlc8}yRb*_R`ym+YysOJmd23!3Qkre^OLm0Xl6W%_Py=S50<#a|Ni~*} z;V=B$KL%fjHvO;8WALlSFRT%tGcz!Q&wDy zE&R&N^8tKny?^cX6||A4IFcm8b9Vne@~NMIFtuI)o1+{_e(0>B5gc9ICp71d_(Df@lC&6X81XenKcO z^gqAC%;OBC;@ga>k*yqi2iD%du*E-%<0-|3w&VL1bN3TBHY3X$fA1$gbUD~Pg_AJW zH2ni9tTvst3|$Lf4EQU5S=B_ZyDHl!Jfrk0?$*IfCtWw9wo60U1;GU4xyA&YlSCO` zzuUyuC?95sj+6Q1YLILVKUNY` zE9NemL<&SXi0QpI%sW|$l5?TGOqNrVG`cS6lXjx}w(w}FuPV&OVce-BYY4Wrl3Z8l zo$fy3X)B>+(>fVSsv@5PcZZGIc0y$}1|Ei=AcWgw`Lj~63i`*hvV_z7m}mfq6D6B67EERdAx69TL64I-Wha5KHeS8 zrpS#76rkJ8a>G%wj&h>8KuGQP;9xT$&j!V%ye7vXy7oycn{&S%Ek!r zCV&QE4Q|IGPHTW0Q(5-@u1yWti|7{S=2g~P!^O6(Iy$m)e!FbDyX+MaWV#~8yrK_1 zi_9~Kl-UC%`LtRKYyhhGQ>R;ZZ4* z>DmJsdx^;G^s$JD?DXx*z^X4b)NPgj4NhQoD;+yOvc|_SLb0J zt;utUU=Fz`ptwWLMqz7DyGq}kZ{R7;h?xN3Sw0<#w*9dND@@&InoY_!oqnUK53<1< zw1Q(H9l$s}w#YTchoPiI6uoEx_Yd)AGkmd59kz{6%Ix?FkSwZOr4f9F^G%>m6KQ8G zzzVr}zD0`$-n}-RRb*{YKb`)4$TT#QqC)Ehc||tr2{DZ;@k{r9iufPhMSQxArfMyh z;&}@AGz=F<5xt6*rlRltMy5uY)`H%CK3&5)iZb6EOMP~JHOYUTW$7w{oi0Q+OH z2>;v<1aVqTMaw%)9BdwUK{5aVMQaLm4*ergcv#l>(d#RDni!D!$o_(09Uyk<_D?K) z1FADVw9>pou>9HAGX~;UTY;sCAUMP1Do><}K?A)}3)}Ktk$a`E2@0d6DU&?@mJkOO z@fN}EN`h!o8$*02#1W=FjG#}qbhYkn-nJ(Y9KR$;@rhs&Eq>UHXej!3l!3>q>L@fJ zz)B1&TY$*+ClJ~0@BBwpou1B|%_N{MKVCy{EG$Cpkak{kCc&y9Y^s$8^fl@I_2|&- zj+Dl}vOl!<379^c^bas10{&e6x0(ouoE&@G@j=4A>WHg>2`@6P@G~kYrKa*0Cr1-h zadTExCM>BqG_$O^Huuz{+VrxedWo{`3VFvX!M<>N>WYC3Vb;$*n-l-yk5t@_&%P8O zj0Aj^z1UPHmM$E?1G`<>^w1{+8E?e|>VA`(aEeDAQ15}7&m}--PU_%2|hY>hNp94g|Crf{AXjyACR-u~iATL$YvF^COcw9kKR1|C_05%5(WCKWsx3~#7 zsjSXw0RwyF&}xRNg-)J4``M~ zMB^B3es$&S1CyDVTpL1Dtq!l`M8$VnF{>#pV0JbOq^T|)JBH_@e{9>{KBE9WT z@LC##%KlCoPDp;NbA%`7)K$8*d_sKhGz?>~ECbG}T7aBpJ5 z!r3_}&-9c4VQbxWAuBI)9~0S*7A^Ygm9{-yxE6ar1hEwBauwbhS{{Wrqw4!ZgCnxb zb7>6%N56Ky7zZCCe&Tcmeok>3c5cF8LIRqz@J|FmcF5nz&V$l`Cxn|=*RS9<<=^i< zdx$$Cmp>Yg99GuNs2X_Je91bjynMWjRD~wAe2ZpB84FtW_Y1Yiiz^~*BbSlO%hE`( zCjQz^$|-hnW7?d}!4XTjk6x1Po#u#J-2lG_(X|t1TM}ZWxm=C|U2|-aXObVhwhxiH zo<6;1M^Y8t6lp)2W_Nr5eBiWtOOCG5t3)0kB7DER3=89bHF^cEDZf6m8?8k) ziBjA=dfja_UG+EmFyD!7?IRFR=9tX>O(TdvX+)}20=pKjW34fluh=F+(d`wl+~cxC z)z(2U5imGTBuIkgvGey1Cf`YJjQny5VvBeAA2YAB|97nE^pPhJQOpY|0n5=s5FEVNYIC$d}~rQjG*XgL;UzTmjg?ov_RiHMcwh?-h-1!}O2cYjCv5jcoMQBb#@xl!@&E2ult(Q=ia;w@LW z=Ay`T&&2=w&(Z89mYHn9-99Ty%GzkCn4+yKOcpr?yh^+E$+z<5gY`L%`P`B51E^kh zl`UT#1 z|8L;sXeipM_Nx7=Z`<0cde@!6VNea@lmBuw^=f*RCUQ{KCwtWi9Rm_Y)iBPlN!^cF z>*@n)NE_@wmLyX#^UAC!BGi%9tW+ncd#kphNzl?jj=_s4^R)^)-am8W>5aa|q1K8Jffx;ns&5Kp&^fwTD@yV&YM;1ay27qvrh$5NREgb}m@A@tI<9BxL zgJr0ecb3)$H1q2Y5bHzHN~PC|man%+@0EGrW7_B{3o+Ub(yh+|R^#FF(FOrP^o6hy z`(+1f=yJGM+!%xmGCE+FSzcht-#0TY;4K$hjfSpaPj524f3Cm!3-RmmI6UryA}8QFLOD;}>YnNM(~+|)&F=}Rvfs7BIXe(Sqk%8|;K7Xk()DjBeppvmF}k9zXx z)Q8f~9?I)y6$7?alm`gd_(W$GUqpNQg7F?nR%{&5lHgh?mMJOJ38N}*eKyOE)nK8 z#dE58;b@GlF1||?XmEe9E8rJneP;Exuq3D{n_L4hQfZ_OmfkuTMhqQas@)0doO?I0GdF5ujJO?Nl*LI{>3fZ~X;#oawB~A@ zdzwseof}Q`lC_ts<8+V^(D6=vJ2TdzY*0+TsMyfh<`}C!s#JY0^R7odvnSy{k<_aqQ{UiyBo513AS{vk>eCIv^ zT1?%ip$ijKy<*CMCZbwz z3b0;Dw1_8Z2ad|v9!ck8y`K~T_6CQHG0^qw^*655-?rU?eG2?&h ze(3UZ$Ql=pzMgs&@BH^# zE2?nJ+`;#&qj1cc9#R)3?U8wCjjAiCq3@DXLJ#Kb!48@pKIG3n^6Wo87T!NJfUI~D zWiiOQ>*0TzV~V4kwUKzb0nuzK*GMr89nnho#~gwGq7?eAI%2V>&A zl%|3WH}=_z6$Pe3`?ut41kOcb)xu}CfoW`NaYhNJ6wz*2FjY^=egDuu4**EWv~#UW8TOzsTOM$zNn|k3wbiG5Rac9F`gG zH?-lWBDe`OugGggYc}jju^kWci?NDm9dv5 zt-RBH?N_I$S~PRLV^@HXNdUw3jd`->5+6oHeqErOi0%v&8s;6-4C9p(G)NoX0J zz2d5bG;dLv(-%GQ^wmfyeNP4xHBB5@Vp zJJEoznyH@YtLYvB-q=jZ#HsR;^wpLscON}BK$112-O63e=EX%5QNF$##8RI{hyG%O zbkDh+=9yHbLmZtQNz#=)F!L?F&`vz3@~SuV6U%}cOcsHkV0N@Fn2U0o6leLpc|km< z!O}bkKhwq%zx0mWn=tfE-rSim`+JR@X^c@o(NtH7)7r_Q)l;9~om8!l#vZ<+#BSIk zaq{O!c5R;gcx~hDYE$%rM5*Iz8W{IiuUfa*P$YJAIo*T7W?08_phC>|jSF80hTM@*BxY^s zMqmm;X8W4NWY5rt?2ciWPma+WD)Uv@8cYSbv&*Dey!C}#3DTv_dAOnvfz_Q2QziP$ zH1fwIaG1ZX@|1Y_b1dxwEOaf4X$oU;7Q!XtNmP0ZI2hH(8;D1SEq27B!9!kSngH0? zD{2y3^IRE09CYd6g8yQlJpf+GZh7Hp+kI7^K4#}Ij#@dmj0)4^dEG%-f90#6&O^Dw zo7l=PY_lAh3nuyr3Tjw*N}K7SZHPHrPDRTP^F-5`_y~`24w~GC*}bkpwfRY=9?@QR zSlFJ1Nsk`Tit$pf^B$jLq@U!2G_yNiDSC|el-|+w)Lp1PB5JETl0Sy9I=@f&?GW`h zjN18o{{e}^ApiCN@E2GDDNFy`N%}Mu^)y$v2VNy<2241LK_KvHa1bAmMLh3bi8Y%| zzY?{54L010$2=^bAkYd@?GQp6vfRpgkwqOnA7ypHhuU#$mAUA*$XOZJ9ur8fV zuZs$C(dG-5`IF{%*HO7|Ohz3|SHaN{v`^A3a^(_UEyk*%QanKd+>;TxET%XReU)%mV#4^-5h&rOK`J|&5ff0ohl=tx+!G9=G zstI*>FLA?`AL+VB3d&LYPqq*=nwD#~eJDXw2@Ye%LL*>pDkwO7bwWu~6dr;C*I+~6Q_2;OQw4_u zxA~3jv5c7}Av2oKj^$r%>JI`RZPhpUr#^d$lBgnREEEH66;>IKFMWV!5g!0Yar4Rp zHube0Up{X++`o<|2qm%_Sd}IaQwFo;=9m;rYh@W6k-pH&$lAj82q*=FC@1`&9QW4u z7W#NTae+$|lJ)e5KeaB7_yyFXzzKtE9=r4F`sDDbS+nGZD-#mNaxFieW6;?+!lr^x zqo06|6t&kti`C~=zqYq}TfeTRlx`y5U(8I3&tvyeM8n^YcQbM&nU|RRDYEVqtD|fu zTyHsyni1l!q2E9V4P+vy<%j_BC}=@LaNM-)-e@w24ej2Me}X?4(>0a=C8`UG#?ju8F2+;))$b}%+aH`U z@_~R;y&TBs2b+d&q}D1r#lICDOX+`g!&VEfbh`^U^oq0hWR|LAo06XqB*!4(!T{Wvu0NSWf06xI=PhTHlkm0Dlp@% zYh^!h0!HqIt~#ovaNG+X3qp2abSZt);fCXoBmLwH+~1PfD*`zG=!`f;%l}kToF&0a zb7;hhJe+puC11NO@{MHkiIUhwx{Tt-P)Z*O=!LEy(Sdp%hjAA8^9iNDg28EA9>bD{ zf@k5o@QMVxHLSc&p%5;9Lx`rxW6Yo(zV9w&_fw0UHi(@k3Vy+X62tm+@$Nf^P^pOd z2}4z{h5B8t;$Qry={0Kg`JzqLyRq4O@H(B{L2b56u&1AIrOjJRb^Z!GM1`HQ@)Y7M z=WQ4N{VE*KFR0C7za$mOUa#_BFc4E^ghsTP-Oz5Ooi>zh9^u`NdkppzffS$TBV00O zIsJzLu!yO+VT`m2T6K`%$dCfaV1i(O2mb7z`uK`9qta$V)iD>5uMKvXe&me68FIvI zkr#Iud!;dTD6KFvu-d>@)Z7CWdAk;1#}EcqI$v9p2mSD*CSb!X8n$^*<$Oquo#S7nigYuj~6aRw@%LnGhY*7&ik9-F1i0mV<<;RB-a_v8G~snmLxI>T4A^HFwbFPN%|w}xSBK9N;-+DT4mkS z07t~!gLD!T%2Sk~(QIsa)*Pk93O;^D0K1Z{3KJz^%iLy_lab( zbFzo7H^pQQ)TxJ792B9_G>&o7$fJA2{JdgrSdNGf@AZy6zqCDs(I@i{g2&|eT+eqzARtJ9@?OFVz~R;++lpkQ3x71lpLE)UAW2 z((3_uW@|<*WDsNia-Y{I&5QD50@|x;=)F+i@vH?!%E8=$`ZBg#Q2ENh@qq>@k&-w2JmD7#YAVPOhi-oWl4Ff-byq7jX%YH#i>AtpBq{N$-rvg+GaxyV2+1tv2@}K$09?|jm z_Ia(?#P1N|k#t2py64ny*5BUUGeDg0cF-(urCk@<{``|En7nSBJd5cn1m%Hu3b_vDXgsRpW2f)2AjAcHPd6VJw=k7liEXH?7kPn0K+ z{I>K--_su@y?S_&yh~>Irw{kf6jjhJ9RQ5KzpK*_-x)NrK^Jn4K$rj3)u9N6>41!QtnYUeJs z8GRUyAP-J&Z>+bHf0QLpb*cOp?FOk+m!gHo z`#HP?o}eLSf80;3*i-um+jsf!G_%U4iA3T$TzV`3?cR0<-vkogIojau=&J$+M1Hl}X-W`^9Z6VY4*P z`>P=vQKzIBX@~}@y^TYH*ncPyoJe86n~xJ7KSrnY=p*I$rO^un)Z5f zE$Bq@?QW4*P7q$-G?A92z-8%z+3b)C5kNerMo5nmeA1BZhHWTo7;QJ~xas1{e z*3g4ChKcadTL$H{%@o!=t4Hdq%@z`n^u65(exrHPYChP={2mI!TzF>8`d~WyH=kdT zp8$r5Pu)sAF7Njkeb!4`hf4$cm#FLCu?fHq7SgQF9WzD2p2mEP9gKl1gFZl5dzj*j zEgI0LmF16cMq2zwaE}-zB-)20iI>FLv;_M5&Lvh@FURXJk)mOK|8E>1qwi^(bHjt; zV2*NB67IR=Zy=`KBB4^0A8XsA`f1)lq3+fq=DXJ2Nb}WJgHNAp<-yFt0{b#cxWXet zdy1X&wwT9S{Ggz_O4NP%x4}toOaer$?a^8NhS(dlF$a)018+|i8-1y4o*NCW5~f9F zqgOp^9sgWIpZf=D`b@g~fXvGtTlmCO%iW=w=<-f}=n~KF25((Ibe98v6vf;->=m-) zk*yTd+{PZk+N&gV7;gEpCaZK-8p7?@HEsVWsdEG3iw-isz=@H^e&(Z!8>LdQ1p{LZ zUo=xv{+M=(DoWIx1^Zap_|M8nvW8V+Ysj ziy5D9Zs?FYdN^fLp5wMvVol|;b8s~JK$`u=@3&AEbnq3J`@m#4-`E+>0S>=`G1$_d z?0+TdTTc;-=XbNe)Jf><2VoRo5{v&sJ9-1F=<#d3a1|((7SnXC!QA(}TGC>UxDu7{ z47L;4+Y0HB$$`BYKdQ88AhW)2SX>Y;&y4VpVzP7ihYus55=;0KgA18GCc1?S`7u!6 zmJJd~4PZTM!8r{=xlgm=OX+f95*BMZzdai=C{z*UVA4PJ2!<^a_e(ySnOSGAn5~xEhTkuVW8X9mcd2UdpNeok{8l$ZGDt@ z&=u}#HScIN7N;q%1&$vY(1Nad>gJ}2`c`Xm#BPIcz^;1B@S;MsK(5IRf#^^+cK7G# zWAK<|Mp@j;C6hxvUaA-)%81QiTXLCLo%y~(O5q;Fpw%MTrb3l1%6%C3m^ACdxK+-d zh*}HU7xM0~(FN+LdRG{$@*d<1lujT(7_mqeUnPNjYg6kpVQ zbNh?4NVQJpve~npjCP5>*7`bSK02IPjUKB%!)PAw57_PDezE{#57A>uk#AOfS`95(+jPAFpM2kC14r_Rw3%$Az?W2Ja{<(6GVX=(1L0NVA?o@rsV)rg3Dbc;VCZQXh~>a zXDrr`JnYCKgB2PDeOK4iiGu9>rk(Y9;&L21T5mm{_V<}r5DpDvB3H;)`l^*Usgsf= zh=K;0rOcgbo*=5#1JT$+e+bNa&EgI7V}8wI*h<~+^Gx4H=oYjD%Z;WB8UD@nHT8uQ zrjSkm>|i|v9JbG~lX3gb|Hfge33TGx$q0s=UxU`b5f>b)lHB4wW-not#;<-ttsj7m zINn;-FB%Lyok)k!!*Q}MkLGknze|Vs-K^|(794lLvRo#&21vopEw#L7QAI`o^{e3# zzJ$-Kv}qtC&n1E9UqK%=c;q6_Mb%#WyUYEJ!UeDNRJHv0O@&_;;I)CzF;=KSy#=%f zbx3l{vm|Iwm_C^}$avfX^JePu3bT zAo#%Sp|Bzsz%T*Fk|-(-RRi7Sk|oEqpu)C_cw4hkBiER5cNs4STup*#cbR=sO>zvO z=w8d!)CqG*vb&iyBnU){n$29z9-SJs;0Hg-4=r4T-&4O@CR<^)kiCU35&GHFFA)IN zgaZfsiFNINQYUD1FLkd9Md77}jWpASij~~Fb`GnTbS>W`>Mxb5#3LipI!s=^1}UDU z7z$nDk*+6N#L@5>Yw?l%00IdGx1*vAy{*Fdeoi^DofrWO7rWA&LONcy*U^3`(nEC; zx$2CUR()fxWiTy3alB{`0(kj4`#MZuApRu_h~xie`e2ERi<*4-N%dH;H8^KGr;at| z$D;wGD$EjiSDrH6^lA~4Y4QM^ZWE4Q?+^cEnx?%vH3YDw9+?wLz#)>^h?o6ppXNMw zVM&Z9Ko2c`5YB`HsH!s&yOHOThOp6=ag^2xu33ETRa>#W-ud zrSH9w)>8J?KUo`>cC=bNnBU`qKH%Oj!YJZ34~<`wk;g^{RY0ZEw4htmMUsq2RSP64 z{KiZ;sssY=_l#&<8d1Io>nyV#KX#CJuP$T%ia!kAL|afySz)=XS?#dBP?Ya!h1`}e@uy$ zxOYb0LAV}aJ9(g@k8pQf>Y1{`m@XsrLmcHA&sh}Pdgl(Box|`fdd;K#@W*A%V}CK3 zAuK(L@De@A6BAv~toyMK;XQa^F+o(w;qJpN_9?66BP-5g($<*Y%V#p^+d>d0s{b7!;Gu**9J3iOF%^S?V{bIX zww6IIXU@j_J1CS#+qi&!fq$6>4? z<*lIUT2><37n=%jWa4fjo|Gg1 z{-o(E2R@dEhg+xPdRzsr<%tfTSfvRC!T0I!hd*1S_dQ?0%C!@_RaZ6lzsX#`#NDp2 znW)+);Wch7a4M%{UCF4vi_vT91*N=JJ)|zD`6!tWqyNY(WHK@0X&E-s;_)He0bjHL z|9%wb@5vAXaguZJ!k$*Ex8;l&J{DSQ_h|KUw7B)YLQizHLb$PcRnN=y_Hov&6-Phq zP~ujrCwSQ*K6L|htVYoXA2BD6Ig{Rbxo_nxWh#YDz%_zD>gCQFo%-WjC6A$~s)6JT zI6pXuoq717-E24<8BUgTMxvva@u`W%$T+DP_4f$)0}?wQ_LoCxi{1VWer?2wL%c%= zxvO#bhcWmV>&?9Zg+W+)Ip-}lY^QOU3n_Dv!96hpD|4b~y7u9go`5EcEpxb6ZEYX! zZS4HFRcV;pETZFg@cG*W)8jZ6c_NF{cZtSx@n>!6xhcO@ zT}a);x{j2b3$A-!Nf~r6Y(azHlI$sEWs+$nGQ=*ORq zMf^e=N3}AHH}K{~J>LunJ92Sn5iE)LuTUseeYEve5PTxmU4N z*f^os$)Z5qCt?yIttA%2z(#qZ-v*~gt z4LKagX;E!xXD>0+4<;f0-s02^88)M|LwsCRn?sI`&xTJCm+3G_8g{RM&&H=0wKHiF zJhO`q&8%S#%OoZI9}TkXKkr zUBQBflRom6HtsEy9CK96HJ5h!YU-=h$*p03ZJQ>qxQd?e3yHJ?ZsAFCNqKl>i+NQH zn$I!{M^Hx}P7@Z+Y+Y4h1+-Im>2um!b9iMNyPNkw64Nf+{c1T~l$sM{mUSv3CusTu zFpw-#Zb}y#R?2=bxP8Q*8Acn5y#%mOc%ujjnol`gqcsu1-h^`w+#prDk8y>d>q5Me z1P-u{J4of|@(g_vY9{F9(tAfm9d6)Q1Ut|ZDqLdH8NLsqCQ>Fql8Rlc{0?`V*WwGB zDW?#6C8+!_0vP_(U^6E43Sw`MVqB&urNUR`q7EKC>6IM%6&~W2WtSc`6B#?4Fo&7*mtQkgHS8Ta@@ii*pPZ|xBO#Y& zcW|?=LukG?cD$3HF?Cu^enfXzQX7exh?sQsOr&oa=6_OJ84@_$68viHvGz>xb%C8( z{u}E~lFal5p6!s=;G${;7OK%pKw27Ww{MvrBFs>Yf^=^)`e*K*uh;HAF4Os>9_XyLEXmKpVBlJ1Tj>j{w@Sj)0%c&jR@>7^K#&bht_q9SF)zy4>85j94rKh`RMa0X72N#%K+ zTixD97x;y5edD9f6Ny_<;cko(YHvUOj2yWY;(6%2noL#qWLp?sOlFEKlJWZ~Ja|P* z_?}Ap(mjK{0$^5)y%2xCFE{ihDC6oEzG?8}H>A|RojrvMa_M`oJwh>B87^(WW+Xnt zu3AIh$zCJ&EevW?rDKVSe949-4BTq*LI^60Of zM-|kmZFo<%K_|QawS%AU(VR`{nZkHy)^mwl5UilpCvnZx{2(wq_#iNSJyzJWkRelL zzQBjih>?o&<6Do)DI!V*a}xYHu~L?zuC;s?Em<}MI%&1tL2?QR{9}=G$?yw$W8FPw zw)Tsi1K*t=i69Hb<~UQVI7^kA2b69J3iRBm`B+*+aiVTw^#+SfW#+c6ES7(5 zW2bF+_7A3CyGV7U`s5*KvC8q4wz#~AiiCiZDvSHQ2%;l-+{%1mpzH4{9Fng{h()bE zSMW>tRxVQ#4&B){CS&jvlgt2Pu+XiWL4^7dCH~qws1ON`@@8JJ@g^nv(KA3`OSNSD ze5bf(W?dE{b8|tA>iBJYjijbj?Ck#ismkk$8+J^oN9ICJughJ6KMZ~c&*HCie{V<#3W`{CfXHOQWQ-yPvwGXCIsAYMGy!_+gIy4Q@z(bL*4N3-?KuNcXd6 z{w{a3{_wrx3tQ_M*g(C%|FE=;@Z1G1KHhJ!MBcg9Rfr0>PHdo0SBTwI{wj4#^6s)u z-aXE>gSLC}M{D}5eap1%eZ}v$yd@W8q$jo{6Er-(c_@GPrcv7|x};T7R!5L@r`Bo; z8df1H`@5P%)BdWRr$hth_8s>taBQh)Bj-wR{Wc4^iD~>=_V`jeL5T%GA!J!M<8IF`nG`m7SZMJz?*l#djEYxq9QV$$Y<5O5HY@&U`HeA+KpRjh%4n zZBVq#yC>pQoSMCpf<1Q6^kQ#B5{--2b-8tAT;1lty#uicr?X_2>Z_7dUooD-qTzB} zF|yRgD-@mEgT#iEMguh&pYKur(2uV`MLA_Kj~%@c(}G0f&a^TZVW79s@)Nq>hy5^R zUad9oa|GT$TW3XUCD|BzCee-UxQZlm=(OEYLycJXp|Oox`&`l*Ly*#@YLK;uE)ejz zT<0JF{!r*>s65(@sq78KT`(vou_N}+?tw$4(7(T=|9U&$`w{ikHZelWw0ziy+Io&G zD~Q^G3n*AWBpC3wDuIQAy4^zjqaWHU|iSIhs5D?-zG;_74$Lj<*1 z2d!Cmo?KC@yO5lBJTP*tCPEWsvzQa=XWd*%41|*6%QYBk>jD@mD(innR;91eS!fCo zu@-{HIx@6HsmLr%FOJp;Htf;lMR>3PH>V`@lf&0(a5+gEu7QZEx>u@Me-d6u+ zbFfNKm)X$tZ8F|5&AD7=g^H(mUmA{qI47E+(c=BF<;e&&VBzP-XS@AbD`>Wtl_T9k ztl2^L-;>8F0b`899I+l&Bzr;r#!(1(8^71Mr+2emMT1W{a*0dsJ}QF+ov=0Y#E_>9}Cd*v5>2qw)WflShR*d z^zRc?FSYLI$=KMx8txWd9B_c0SWG+O=qcy zLo;8Ib)-sP8M{5Bp0+HFd$N0}F$?D`8{=9*qax23a}GSC7x|daW*3P!teuBXkuhr6 zr_#2xw*)BNtI=(Z4bPSW6h4xrNcC^}6NOqoN6KXHsm$ywUwGCFq&!RS0ne|mpPQ0e z7J9o$mAvIe$`JT&GIWUp`T)DH_2kDdz%4MBfcSokuv-_d5-bW52B8K0A#hj3s~wvb z?zQf4$`6xL2l|KP@NpRL3?^9bBnCsN+A0q^W4g7`?24uVCbPr}6vuOvG(S^4fo-gw zsn*5Xb1|`6N?#Yh8EV57B0lqly1aHS8(O9TJdp#i)i2AXhhS&3l3e{9b#Z4 z4pA6{%q2d4twI=f{0&(PH;^a)Mt^|FEG{!Nv91mMgLpNbVpXj2w^tKQsC~>3+<*2A z8^UEygTo-=0M))CQ+B(vo2nOV&VPB$)ZL){XX~2x&xc7%7TfV9Yh+loc+^g_r-`DI z92YD4NrrS4>{V$c&4R98c%GS@mBa#hIgyi47z6%|aHYFL`Oaz8&e}R}#G9AqStuZlyCI+co&*sC?@1%Rq)}L|M*UF}|f}*4TS!Z-~)-qW3wbq20p6afuy=%+0E8QhI0W#PJ z%vI#d(0GwcHsxRTQ9~!zk6B1CzyGbpsjP|}t^fE2#Zz27mTH8MdPGwjoZBZYWYpwn zX=Xq<(rPGTt*E!8`h%b|0Kc0Ye zWUoqHWQT8u4QaxhH9P!x@Fzv0+L4zoZ|=RFlgu*R6L!)kk|g7Fw_w6v+TodjOnEK( zz60lXdwU2{y2s?6>G*5Bi)~OkUJmPR9@<`=H*E=uUI$KW9W%1k3H2F&A_2(K=`Aa2 zM?1FZ$;Cg&$G;t$b4V(}+0R;2)qN|>Jpa-=%))Xq>_nzQxtY?4#K3ld7DX+@P!@Zz z9DNNJbDCx=#Oi*KhI-hlDp;UIva8S`37|N+_g68gGH*y`V0i4QJV>3xLZNjmqfoy= zk#?QCQ*!8e%a~`kqlDNQh$9aCECHA0rOBi{wZAzg=7iKumFVZ6^k!#LXmsHM4LHR} zV(n)?#IauVu^EwC+1tiD=7u5z^Lc*VW%?-Zp-WZ;oY!z<+fgV3X0PGlX&fO}?3U^& z(U0sP`7Ls8pdyt~(BYNLEi5es-9P*9dyr$|-%ZUIsievkK9sBArldOJ@{%j0_{oaU zQY7^vGF6X{cSJEht1@<$y*X|GOd^5O%l|e#l@u_DqzN_alo| z6l9tt3WO0+V=1p;1atBqE^1F4a`D_I7JOU0yCmll7&?k1%&|{w>u|-lH&yIo%Hyda z&8dIBh4T=9tlf_6JZZ|Y4?}$e#7)xEAG@aUj487{iq7~_s8N+S3a|-*)}LgO@~U0T zt8Safh(CJLJt=JT*SNZODmB@yy9Yam+~A4zUvg%(mHmRbq^xw1S%-u%iVy4zq>fxP zQl?-vQi?R9Ymv{K5M21TV5N3zVP7q{gXyISx5{JIs@fOVt1>x{m^a--;8hZr?AG~q z|0=dh^P4kUo%iD*m37NaEustcKZiadC)KL+l#hQIiB*pub^J~y7Z3`WkBEli$FKfX zcGC<~1GJw|@;UOj${^EG!rG;D}$a(#zrTkhSZi*iu)1LU-YAjmx}uzKZrOlD*}yA`!7yN@-jBT&t?U=Ir>(GQ-?KTNgLsu^M{DTiAZh_kfL4Wn@I!igg?^5pk{KtawiHpy` z?{Xp1>zs=ZZ%?-i5EDYg94mO35J|h4gl}>rL@or-VnD(>Mg0X9N8uo@a-DS!B!r}2(jN{`hZ^#q<+F8Q(nFC=;^+^kY9dn@_bAFSnY zuA0MgN3cY`L>^qLbZt$EpP=m~SX|kFZ{x5e(pbGGZ5}m{w49AaKqh}!GK%AUQ7MBH8@GpKYp$mx*%M3>xo-@uEd9$jjkjvvSzyBLRo3~cfy)1HBHC^5%SIHN4Fqn^Um-)tAdYJ>UiYL+(AWv zuqF}sl3$hYt7Oa^^XP&@ZU)2(*@1AU(0Fe}j_4++lRue|U8$!$h)6kHEexTAStscuxq3n5Uu+gCWKZdsM9J*SjSo?IB{ zoPWS6at21e(@XQTy>EZqi_nTzx6e_faz}LYBz_iN0W^cQbdE}Nct_Mg^#P@%;U1`{ zDESsi5F=JI@CeLaLyd_B9+nkv+zUc~@e|?^_#t2_YxS{Chs|04Zy_A&KR@aqLDPuB>P=#e6M}1B}{}mnQEv99QDs+Qh#W zt4n?~&q}(D6S{iPqT@ZdB`a-G4$q@DXBY!%xA}(cNJYB@p)7>roi5nYL2vLnvg@zJ zZZYewBrSboTq?K*)UerCTOJ)iSCSW85cfr zgcYK^!}3Aue$Tb#4kh*I+vxoC(k9f2=-A|&Kf-OukF1SRlf5zkY;j=(iavN8&{7U7 zs_T8Y2K;RStCCTflFF1=WvzN6)M-!DGaZwKt z7g=JDQv<${CP|Y=geie4CosI>8{lgoHbn5tl)R%g*mO!OoOx>!aF78+Q*YJ(ycBHO zwAy8~K`Lj{%)Abg`ha%RQ2@@Own#|Z5KwJE%=#*~k2FtSd5%qXeQfQ){A=9W9GC|K zk{;+pz}8i+>95)QS3v7pMkN{-<(o&$(>Ga-q2J9C1UuO4fW3nZxNZ9$Ac_H`ntIx6^B2-QUk*$;e4>sqnVEiX|bt0fsdwbtHvw zA-L@YSf#ibdAEVRfrWz;n7w`A9Y|Eix#@XtpP58JxB!x;*Sctm`BTd#5C#40GGXc-vUQ*cK2_kRgNVg{c=nNq3c+;g& z%-nfh@hNurPzD0#xrT-qc~29qds>-JI+@&pwnw@6U|pA+)>=D{wO`cT^IeQACl|zk zNeQH4W(e$A2d2#=H|6#zcx?ceNCb@{ycW0GMjL67&`ko;Ba9^AR$86#W33}>r>+eb zpPFf>oDi{%Lil8CRz|+z3=?oVG}IxAV(o#5=K8LZ*N(>QcT~WoLi0Q~A=WovUo=Z5!mLX${>dT%!kS z@|gnveBmFi1_Iug^<(+hfH&!_xBbimLT+DW&0wY4UB#%pYWj$xas|iN+r*0Jq>6^a z@#U12A2afDzs|E@Y`Rj;A+|R?`?PR*T4jjrccKy-SMW0xAf zoMyPj7VyB*5>GjDuDkp+?g(-XThsav396OD9lkaeEpQ`uJ?t1ZfUoNctzTY7M~hZ>>J=qFCuR5KcBo z36fi_y{Hjdv25FPE+&zk%?mbSyf=t;-d0OlNSh;KiQSWT!kE9r{*tARQjDecON+~t zk=xd;8lTN(UUi@jqC%h2Ie=il;D*HpJIO%BsOAaA@oFCb;9vKcjkK zOTF}eh9rzbOXzMm6ig6?@EPA-k2cm=G&xSC#@abnr5kg%{~8}S?Vsf{UIhfdlW3C~ zwqWuCXbxyEwpO}w{rTQ)t8$@QCzgW%ZsZv$)^;qbQ89-7XR=X&c~JxOyb?_7H8X)= zl*zoX(#I~Nfp;NfE0aodfHI|&b+0$M1DyD4pyC|vFxX=JLR;k6zCm9`>U88H(uiiV zp>4fUP&3vNaz`1GzXeSJgaGgZniuv1_Cgt0fYjKK%~Z&ZvC!c@z6mCxhP&Z`<7}t9 z$Q`TJtyR{7sO~r1Sc{(!-91i0c6KoZ{0CCm%S(G#5Cf#S-CU{u8;TkDBQI1EA=u{> zM=tiA4Z1S@b}2$ffz#Rv+c%qTuZr75=-AQmYL@LjecE=|MSfMfwd~sg#j?s1#a1)6 zU?R{b6!9(r@urw~QSSKz<+z7m>UKOBj95y(X2*Q z)YvFbGVAZ6EroyRC01;Qx9SMHy@@u=aIju|a9H)Iib1Kf!*ENGf=nFax0HqW3F@k& z)GGg;2H(vkobdR% zP?8>=Zbw3xupC)UefMx$C@%1gR*kSnB8E{#S=X78D0GuCt0aRz^pZ`T^T;Z;s!(kY zuzXevbl52i>0w_J%OkkROLxp$xn%$3*YOgu7 zH4)=AABf3JZ7g{p1Z*Z?cl?&vvfM8U7uZq~v?m7O>cy~5^LxDz{f*qhZ3(ny%Aiol zR=v*w%OMSu9cCPR5W|78u){YU6FpzMS0#+kvl6F2%?GpkK(^*FDaUVQN!ssd-#O6Y zG}u!8QU0v{!oW(d#~}`XI^jFgEnvW6^{w%c$}j#nU|%f%WWwfv@F(J^7T67d-L$pW zz$pJQnd3B~=f^pbP+jP? z$ooykVt@VU{#!rHL25>X6-rq0dKr}SSZyzsEo?sWf3Z8c2Nj4(_W;W<+Gy}0xwthxlq;v6GCw)xAFV)G2JZi!%D?+dr4clBece5n!9L^k$adNl9 zBEh=Cx(^TC(8SX7XUb@ssJx^H1-(v9nRMoch!<&B#)YIf7N#mWykx?(06$>;{G>1Y-Qtf3g3p(XtJ@|PE> z-ha&(KT=_X8HmuxT_-cu>-Zs+jwEMzLkPppm~;MuMY_{}*bzv!H}^02RiB?@^u1tA zLpgf3d(2iG)1y!yc~?RUy-0#j=7HzRn9BJu`Y~S!J7FfYeDVzQ;Fa zL84vN21gZ&)gx!(<}2+s7E`%JfH^6Zsf9J2lXilk}$Lo$UmoDwAF zOo`a?`oHPp>1z`Cbo%k`WzgF)_dR=gNdjjd8s2=ZU^h=g;RJc%2#}T9xPl?*lXN|hIQ3XvOKqB zM0YjR4&*D;N%;HK!>`u7?W{?tCvrq@4PeW1xe;IlpLcN7mk$4sE_v!Y45rOn-fX@c zR!4By2ZG9nfyFVqgs?|jfT;MU8SLSL$9pYFxoKlQJ;3u_=zD-J-_wNpLqsh4Qb2^N zMtYpjQRZKfT2}LgK~DydVAZLs^DokC{w^y)=XDXpUWl0|S@R$WxJj_*MRC30YuI9( zY-Vs?F;MXXS8_6<}`{s{Ka^8c+IHR@2A6mqA@ib%ke& zSABOq=)=?x8;rZ&i*;_h*>Gv_bAXWvi?GzQI4M|Hxo8!YD`H_$ZdDPv4yxO{JtHXIa3b3BLbShk}P^e&us3*GUcl?gpr&U64x&^4zV4LTv4GGMbk6 z$Lt!xzS2~D$Xhj1{7=;>T-)^t#;b{Q)J*CbE+&>vS5b2$eMal7P+Mp%q@@?w; zGTCLfe-3rAM;gDq8UTCxq6*pjx=WP(v?CTk4_89VseNK;Mo(A<@|Wib*YPz;^81z7 zAl3^*qU_Q$-B2fkQUGb+0jbbczDCfMhg}XU2RqjgQr0AzKKz%DoJgH6jYD+($63ic zKQzW?N2Jz{e<0#Z@d!E#h@*aQq)FFY#%7CUrunj=yK=)WRBNqbZ2?+?7 zNa5xfafiYL14zk4f!KGf6d&2_t=%-*d+9cSH3Tj=_ByZsBkcF8-u5dWU=`D{FNt9h zQbsORYe$v|f*IGkIK(HhhMwL2EYcwtrW)1xXpAZoh@>xVlQ@k!Bx!l2mn<2v+m3Sk zXnD0Cy5-?dYySkeV=Su3+JGe8l@OcMblumrCoBKUAIXeE9!Ju6#UA-lN)N;~j-ua* z01y|eAHHr5?b!iAC_I5JGwu+_`@(+68JuKTI-$P$+YbYD~aRT3~;Mo9*`GrPezA<>Xk-VUz%T*xUvkbRUu7K1cB5F#vBE4ik*@NA} zD^o8Nj~}c&d?c#!4p-s8pNBx-b&RQ%gNcyh!!x=|QRG_pSXOxDn=i!i-$iw?h}t{q z63l)-=1_XJYTZaQU4E?Vp26pu;T9rm;PsA8g>$+kVqysh?xY)W>NWANjUF}7@)=$q zM@=JSeWPPk*Ja|}pL+mLa``Lx#ZLL$+PIFt<+%OOB)hgpcxk#*FOOm%C06kwsBWaw zq@tO=x!1D$CG5pU{Gjqa_Uq-zy5U&8z=qL3)3oX9=njvwB|2(oUk!84K0KG0A0RSy zNAZ3zdToUYcSm6*o-NkJylzJZOs z6nsSp#@gsw!wS9RR)q+k4AFsyFHE|be80`e#AmTdl1;-G73(JK7v=!pWt^g9AY1JV z^tnULYz|ENiB3xLN%0N42cGYutlKi4?}EeFu0bo%H6fOL{0}uDS-?d>&LfcHc)O&R zh|}f$Z5YmEz%9K`wK75k*N0NU zPy&cFw`!-bS{F1a{qcbDyei!M&-{5rZSV^xSg0#PkVaSK57fbdPSUR`zUMV2YAdq$ zib+#?TX{t&!CJBmQ33!uxI*dKkV(`I0yPL_!I8M;hUUN0)QZdm+ zT&f#dekZ=4(Jb)M&Fp;U2I@)`@Hmyvr9!p_991b)C~CxiTdlWRD)F)I^|9O-9i$)@1B{fAiRzIfv%GqG)bx;v zAQ$KM;WmRa)tZj~({$56b~(f)fAd~ty1X!(y;NXrnYa^r_gTg@LG;^8NOj=ORn+%~ zvqtaHiGhbVsIH^wQj9S@tbY!sLtgTBPj?b3=928ShgVGwEUDauV&fVT&&ZW63B>pr z=23t0jJI#QmmgLu2~ZwG@rz+3!XEzSQQ@}ZrbPS(?Gl)6)U)3Caez#moftUgEBY-g zRcyL4I9n9yuu3?ePzU))h!Jr-2QaZ z<6$%%hqFf*V*Hw$ALlcOxv>qHYkg&G>v+X9V)EgTgF-18+2|RE7n2j=#>L-JQXNxK z*-}!GcN5~kAd4gGDj>`K4ZM_3!IDLyJv3Ztd?V2LJ{}5amLJMm8d}^#I8^lb4rpdg zP1VgnTM+6j{Meow@b&x@qcgWVlZu~J-$1$M*t^CW12MKr+>|Da0lD%Z{*g;lO&V$J&m~0t9M5JgyLazLN+0lb4-7e$^pe+i8n*uq z1YjMBz`73lDeaX|9$XR(>nukOi1`cMXh7{w4l1h>DTIy2CiF)eUF{gt@Us-toCaq4 zAG0p?dI+*3Sjl0Vgl{Br^(zpSRPK|Q!c9~$D5Ix~82p|;{$l*wkEn8&I^c!c<7-%Q zQWPvGcu^S4g$!6C-Rhb9J<}QEWCMb^?j(d5FKw`V({GVu>SD&cA zhq0RpoKS1wd9qVG4IS)64obzg77s7pk3D@ouhm((5}kc;k^sxz%H5`yaSc`{gtJm$ zz(xcO8l(=QE&Li#0};<7&yR(9k2r&AgkW=_X9BGaQmyYCYi;&GHViflj|W_^D12w) z79@Q1N_!b6&#PAzutS1fc@u?K)^Ew)=D1o2z$Ot?3^)@v#F_I=?T#wBWqibKk78(x z%IwNpM~I~u=|wrXI{szcbrqwB(2T}6HR|MFc=W|S$Y7*=-QA*rKdj)EA0ir^LXsXk7X* zQ$q1jz#kGtofXo@m&ZlYMG{3Jhy$>mlG7$96=8(Ij`rE=F|{5L4lTlwND(kx(IReMxF`tQqWHph@voy}ZlkfM-ufrxlK|td z4t8vj;f`PH>=c^dEAz{m4e^7nu5>VXhC8@(mKt9;MQov^uJbH zTp+@)zI$8!ov<#!*%VUKp(t^GL;t$P{>AI~V#A7iv&-R3#D_-uJ>;9*F@hceFr9`3 zQ@@!K>4L5DL6FG}vI1^S2(o#Q4|=3)xV=Zi(e!YS4#XD^6m6`@u0*EW1jyzrRJYq3!7^+uMr#}b20FD${+$S=r;aQvc?+4xTQKDhCL5_hGu%I;v03=}Xs5GD1);zwO4SSR>* zKDHKx)6qc00M(01WoQ7dvz9|arDc-%%>Lq9e19-l%xQBIap$HceyUj(M7sWb-jqca6k|HOm{gbq?Ax2#5Z83 z$|a1NFhI{^lr8fY14c=%KgAk)$r^h1mIY_3Wg_-~+eYI$?0l_H6V3iIHf3;RWwrfz zQ_^vtlehlLYBJN4mY;?Hd`dO{T147Y20(AcCHduXFBC+}?fto2+r}X39d^zo-0S3eFYkb6=3Q2Ok~e*;}{CP(;N`_iC2Pxo9F%AN*{ z3;jAq^vBqu3-r%?oxymy&1N&efSw>!F)RO71Cb7MZp6)&SGzciPETgJ5O9-ENHo%Kv-baSXjo=4|Qrz^pmV&}?V zC|@iztcWQefPtp^$vgf*EplLu!%i)WHAcV6+C?Ev<9Xa}z+ZU>$6x-AZLal>^ROyh zH`c-;9|T&H0ymibK5N#mu#yg!4)@qXbLh$pLW_fF%y)W^g|zIjo1)bG)I`HXLq9xz zwtI5Oq9DRpP!|98H*H(zOw^h9Omy*6&o^5H+PIUq&cu9EoY|#c$al?3cOn8Pe)~JF zT!9P4hN%)LLVmyu-&I80o^%qDMKi6zuMKl{nYBd)RlMnfF@mmbW3D|Z!vk3*2fa=R zLYB9|xrL&I;_qsO9X6hR102+Z`d^&-e z0sPP0m)S2E^Iv{PC2^{jM7-*ra|R|gLyv6}D=;;ktXb$kW5FQEYmF1M=8VhoG6zvG zD&G1BT-uP)7>Q3@FLSNu3FN9!R+G;ek2m7H^c6fX}^LFE5V z|FGZ-BTRBum6dx%p^VFlgD7paS;jjartgaJOZu{T}|XM-}}HA9oNu}wIA z>oWG%eRa@S5eQ&o+F4_eUseM{`*HbTrvn?gcdJ-6b)^4F{q1(yU&Iu-dz8(luBL5D z%8p+;4AW7Zx8Ocy)B=lH5A`X{BXoUkVoPqi2iTekzw+X_1lNdw?7j7cgbfn44sERBcMWL&blex# z7w&ia`LS&Qy!TGMdS6FHnWUiR#IlX#7&Lq59xq#@j) zFmv$NOL!>S2UP0`{6F`XW~KsPhSzK*)!zhPH%onSasR;e0`1M|UR*j_v0OR61i#`C zD@r5?Q+yWX)F9XG!#bbjldiXH2^}o*Crw_eoaP7>U(|VID zM8T;~fdls=1V6Vj)`VZ`b%qp&rqpA;s1krfvf4ltJ-f89RE_~;oSm3l-=o`*PbD`c zH)&P>feI~s{yg2mXtf@Jsp`;c#>}r}tvCgwxPJCCmTpXGcoMfQFP_aW^Ys~7^N5+T ztRkW{!mW(kg8FJqbE(&V5_}ev7JELQ*g0m*_oR~+^732j_o(<1II7ksRk;q1GZD-E zswdjpi59suuUcEWIUT(g{*{f-Sc4Yrqrta=<&z_~xCKNJ6mS7`B@6i-x4_y`}HeOx7_;Do5i{KuVT`6@5n zVqh(b6cj%2k}^RBcf<5bNx{FKOS^xv4Pyol3~C-Ouck4E=g$QBO4ZwEA#QpIpT34v&F{T5bWLU(j7SKO+W-3V(XZtk2`d8@%K;le z30>qOW(7+4J3=5s56(3C-pSd>QI0|eMJBe@KAg`i8MxB7Rx4qH4UOSKC1yj_o(O@QAC{4=CLv99T3i6O{XU za{7!Xrpc6fUf@7-78Y<1bdJWW@5;!@xbzGPN*UQ4{5b=MioBQ4`o`j{PUUTPR&{np9-#k*3D0DPaePgk829OYg4 zOkJv8ZX2dPqYp0z(wXY}0Cjf`m8H-_6Q~wmh;}btGa{yeP)M#8HEsl5Q;!@tG_f?X2nF9GIwt%lA|ph4R-1273Oa2yD+Leem`l6v zfdD6?8loDaEN*iku!~kO+!fWdcw`@=-fiU?{C)QARrMGOQEDG8gH5`Wi#P4!o z5G}`9GsY@FT2ri%ncCU{{R$nLr&_{ELOXC^3DJPz`Rezlx%0v$zV9E)7`Gnna21N( zl#imuHi=Ui=v|GQZ&UD2SWA4NQl?o1YPAq&Ef}|GzCu(>3Uo$;mF0_}$0QMyX+jUk zwFehmTjLg-iAZ;*BUvB0jSP-~nL#sQ?7~HZmmnOTt)TQY`!w)3^ac4D_n|CdE$_FP z(c~i$OBkcGp(>Q9Xu#hh5;`g2ry)apj$sCXQi}lwndXy>?%%9o}18r;0PrkVdGhMM{?Mq zO{4kGc)zpZgopz@#Vp7ZZFAut_Y81gErV ztR96#GLs48ceTk96Go!n*l6xAv08&(1fiOtOX<{9@`ySD&Vh9TRTni#m60%I1n?Pi z? zooqThd;WgbkUl8vhyNoXb8k<06EqgQk4Qu@nlxlxr2We!D^mCO3$y$bRF%fhuiqO* zudRPz8kA)1B$y%pz?8%md&TO&q{VW-f`*1(jZJ&u(R*Alu0ut6IbW``P(QepbAi3G zD7XL+7)p4BnT^ZikV>>FUJ;|TYOH`iCv&^IB+T!>(AM7@y8Kvy1jE$t0mXv25$Zo- zU{n6q)tZ|X3AB-ahPr@l!W5F8?3vr~UPpwuV+fR(QHtG>*bCWyP1Y^vaaOrYIV-Uj zt`@E~&=E`!rPTxC6E3)KVh;TO%+oNJKHwoNVxi38wE8DqM02CSyB*Vkv@w}JQg_8i z;MF55MOHwem&$Ojq;dN(62DX1wU{5CMcm=?aK~-j;6Wq z&RAPziPu2WY>NNjm0&~GU0zT@44)Q7gAWBc?(PnyD6%gLFILO-6;y&-^7Evsdp$SA zik>^U zm{ceH8kRf!t+2-y7i@i*TJSBHb^d`ywaVk@y5f%cE2w~KLC-Ehb7e}_5<>Zuh`jz_ z_c}@2kl+2Q8Y@V_Zf3K8`Mb+ zl%6xP-x!?=22K~94D)!QwFr`M_qj-)P1sN%-wS_bzI6b@3)*7mL$&9c)VZNYw@>=D z{1W4G=cM>O`&ArF=$Y8}ynyFcPH;ilWo4PbnW1r&=Tu%kH=Efvrjj4;*_(5wL}0(V zqH|R$_m5gg2pS05OdFSbA&+LEJe8!alMC$hG}~`95;Zc-B)p%#sJAgTvhRQ2$;cjY z_~%PORblxDOdQSb)^o}x_yTboV)ItnYIXZq_oVFz-#}NV`sPcF-B=S}!+x#CH!Z9y z1p0Rxi&F6V6!^P1{RI6UL8a_0S*0s%Cb($ar?Y~nFpr7$3j)~-ef*rrCOCbxl!)o3 zf%3jG(^1*c**-N0Fs(+gK|jDBG5NXi;HyM*t5L_6}oP-0cXXqgAVXWJ_03kN-f&QLaWQoN&CGtzFDidJm>kl6vG)r$gAS5&Jbo90&U z>ZIyQ>;h|`I}phGEHwk=;qm>|a5 z@02@8?@e4Lh9VR$Aw9c-L9jEw8_J>J2biibQ?|)=1%uar?Q{%R3R=j4DIkbo!`RSl zTK|9-$@Q1*kABl;4+XbvyKs9*<+{7dg36v=&p=6ZR)BEnDSo9=rB)llWS2}BDhLV` zD1{(u{<;6jGO!?Sf(BO1W-X_D?q=w6=sX%KfNZij&dz&6D=BQUyv(XJ?uW!%4eUk5 zE0gsKacB!w2V#_;N-ITT^i%qW9 zNX}S%NTe3F81pn0S?|5sad23G@?AH@(d~Q2bPZK@vM`seetTV(rT69C<=up}DdB&8 z!Ue~>A;mM@+On%k&U%$NDj7-{F-S=c`35RQFcT=y1%+m(goYOAMd!F|orAb)%h-ul zX*YbZcv1SFW#kh?WlcxSyFV=Pmw!%N{W4NHn1%vr5)nGIn2eS3FA|qh5_N#`pb%9) zX)cx!l@H^J@4KWy+~EAs{3bTWuv9p@T4u(l5V#U9r1u1N=)pL_^WJbJiyK$nB^B_% z=~R~Vswz@_KGm{lG*eO~CgOfh+FC$y# zB6nRFqhyKn{ny&975(^WSV$qz(Kcn`JCq>?#dm1NvKT>KzAQ~CXR6kH!J0DR{EDz3 zEODSBDK3`~iq`xbEfKZ;!rts#nsO!a?sxp6&XrB|o{x+0jE}G#pUL%)_L{PU7G7OU<5=9cyah|C!}LqzXd9# zA2oBaeY6wgS`R^sZ_6z=^~;c7su~VeRQC9sNqyu9PwCKK{$zT>}>-6_h1>`6hUi@nuyRsh-2sk(w9yo9Ov>k87Q} zP>dJB4bCo|7toh2^MYNvz=b~B>3-YaC^`UNG`lsobrk_qFk`=p9$gt>534<+X((Ku z*Ne5w1*uq|^DAC<)}L_5nD@y$Pbw-%Yz@s5jwv2O298M9vwuc4!vLVyCN~eE)w#zq zmtySao9yF3+n#A#m);15?=F8EGzemB(AsOM z5fZ@BKVYueU*~W2nT!VieFo>`uW-g$Up5xO zyz=nE)1p&j&4t?Te>j1=BO3Ox#P8uZ=LrxBzg8jwwGC3W-EvirulU_D++erFTIuGh z^D5ziVj!e&iP3Q%UyJ1!Mn4?o$- z0+jP{PeQ{6-tEBVbhj^RBB*}WfVJ*hv)rr7lRYDq<93D5U~%qzFYc>xWla#g)c3)J z+pZyNTk4Wcj`%fePY-L{9ybJss3o3%KL6^bcIt=d_OSi@MWLlXE_%dGI_@ilshzL` z2dym!dQy{RQj;mq8-ETC%#2aF3>i$1>3JmBg+SXrF7^p7`>X8-Xnvvu4DuY3IwDU& zriJQpvv5x{EPn=!|M>s&$D57T9BOU-3NVk%Prs4<>NiW_Y6=RR8`+BYrQNcIE)Nnx zp`v}ae9O~iXLA-lR5>@39ncMC*WN#edT&{*D|Njx~NiSIOy1IT!mA$Rjk=#4b@lN6PHKN3`PFYy3?gFpR(;Q z%j91jF%rEcTad1atjFwJ3|@sq!=JtmvAq{H&P zyH;BJ?#ghj?~0n?S;;OX*KgL{o#D&CE$Gg{LZWs3p?3wx(Ep~208J%mx?5`uA#LXw zr1OaU&1%i8L?>CKUkPs@^Kpd*yL#4Hyaj%c^d%Vpz!`}?GSjWMa`2nF6#Bk|daGM8<0NZQNcYlIz)-2uhxDa0v!8Z9rkW5X=6+&fmhMS@Z!WUe` znU1})$&3y-`+DLgFnj9ESHSi{k4*KBgoBzA<(o-4^VQw?jS`0&B3iX@xU?iR1n|KV zzhFlwx{#;+_v&66B4PdogbDwF7?V==k{9fX^|{_>bpINDf!;>M}j_fhiaX3q;*R+x=l6S{Y7< zR*rtR{$W2zCN@xBl6u8fpTf@L^0F_M9tSQYVaDDC7R2ZE6BgH^=&W$Q^qam2t026C4--9 z-m2K-e;vdNZP{UTObiAV@00Rld}ixpmoRyrxu|N8As-Tk*UWY9p76%d?n6vJ@;X-;_*SVDlEy>lP{qP3J)FRbj>(Ea{O8nT(DU5 zZK;1&n1jpvlRR3p$w?0pv#;)^gq+zYG<3|X|5uaQ$24_?VO&7)qhg&3$YfzvSyANM zibn7%gz;e!A{q=%D|CWGwmL*50=*&=#JaJ>4LU^{U_f0^gh>k;y&!?|Rmy;fpyS$U z%K&R3h4z+v&po@i?Y#fJCpjlM=Q&Suevhud%XvN0O6)4xGQqpFZf)6TSIj>0xP;Jw z=>4)Qdxe4xWFw!4T@ow=;)4EMMmJ?xct^g?T6epPSW zsM*dT;FRZjn?*Y18OETn>5Wfp?HpPeNXU#~?>@J82X)TUqQ!vb6Q?~>9+{WN6Ls4R zwoGPsBT^EXz4B~7$h?0&Qev+i9%^30Kx(#&o5RbJq)JYu_lGh>_&p5D7>%r8^#$`% z0-|n5jYSAk{K2Yrrp0mM{2c0X_5RJ%cdLCf?GIG2n8R>dx~!ll;IKLDby<4FKzN0u zDe&6E<*OOeU!1j~Jk*5&lnkf*o9n-0G&|XIlg)=}vxZ+0ACOu+oBvbYgk7q>`=o1o zK*6b1^GU40Gswoajp>U2ji8gCxUQ8y)*{cy`-KtU_WUSjrn@e|-mKb?$MXwxWlVER z5I3kW^_%1rfnD@!#$>zI-RibQwKtYD*hp{r@siS>4QJZM$A{f0ANZUfvnKJoc&3J! zcU}6WYw_|WDgUOv=}9RTPG=5#v%LB|ia*aC?bRwW9^CN{+`D(AKhAt~?8jAGs3S*0 zy4*sUF#Vl(OjF%(GgPqw4)w7RXiyRb8l2Zha2uyz z8c~Y`B{Wcl(Cs(?IE`auDIT2vmdydurylG2>OcOXWX4eFE{xpWakvg>Yt20L+|FDJ zBKE?=h^^0wupK*T>C?hnW!BkP%q)XeXmW>>2+%UCLo*D4Cda(*VL3YQt#U^n=v6X` zjZ^hKmY;+_%qMVAC0%0PX;@@{o=b*|U6B2ybQkyNG?0R(X*`Ei;?N+16DDNA z8=Rhs#ero`P4_H=@pDLSV3U|^vx??bA|!_#r>~wi6)QsSn zt1vJkKuNk54Fsp)`F7BA`7B++AE~79H}7NN0r9vOUKTvRQ!7KP*)3xNVplxX-?;F9fzC5b0>h+ zM6eC<=Nj~J{4NhCLFn}+?Y{g5Gw+ePsM-193kRF$N=z3+cSH!JXqEyJujuy{grf0s zL?VNwkhw}`dr}1fMu|`;6I(H=9R)fZ)WcaBJ?#svMtaf+X#{FVNGk^P0t~(v&?F@2 hA;CD)cGrkriqNdLPb3|*8iQ)cp14<(d>eCL@((K7@ZJCb literal 0 HcmV?d00001 diff --git a/research/bit-coupled-chart-bound/README.md b/research/bit-coupled-chart-bound/README.md new file mode 100644 index 0000000000..fcaa076ace --- /dev/null +++ b/research/bit-coupled-chart-bound/README.md @@ -0,0 +1,104 @@ +# Whole-word bound on coupled BIT chart relabeling + +On the retained BIT word, a single adjacent nested chart pair cannot +support the fixed target κ = 10018846261809/2500000000000000. The +proof checks all 897 eligible pairs, with no unresolved pair. The exact +conditional κ change is 0% (**NO VERIFIED GAIN**). + +## Scope and bound + +Fix the scalar order, logical lifetimes, public starting and final +charts, every chart outside the active pair, and the complete caller +bill. For one active pair, relabel any shared ADD contact at either +chart, with the same label for both operands. The same relaxation +applies to owned INIT and CLEAR. A physical SWAP carries the contact +history of its logical role. Consecutive contacts on a role either +share a chart or use one direct transition between strictly nested +charts, charged at the dimension difference in either direction. The +upper bound grants zero incremental setup, scalar work, routing, +phase, ownership, restoration, precision and tape costs. + +The replay reconstructs 32,581 vertices, 62,474 role contact edges +and all 2,871 original paid MOVEs. The 897 distinct eligible pairs are +exactly the adjacent nested pairs occurring among those MOVEs. +For each pair, every variable contact has two possible labels. An +edge with two variable endpoints has zero cost for equal labels and +the rank-one tariff for unequal labels. An edge to a fixed endpoint +contributes a unary cost or forbids an incompatible label. Subtracting +the smaller of the two unary costs and adding it to a constant gives +a nonnegative source/sink capacity model. Each flow certificate has +the same value as its cut. This proves the minimum paid lower bound +over all simultaneous choices within that pair. Each cut witness +uses the original labels. The full invoice has 107,352 paid jobs, +19,950 productive fields and rank surplus 1,506. It is priced as +productive minus paid moments with rank tariff r^(1−κ). The verifier +encloses log(r) by a finite atanh series with geometric tail and the +exponential by alternating Taylor bounds. It rounds lower and upper +tariffs outward on the 10⁻⁴⁹ grid. Comparing upper old tariffs with +lower new tariffs leaves at most +`837/1250000000000000000000000000000000000000000000000` raw +savings across the complete 36-copy invoice from interval rounding. +The best whole-invoice net upper is exactly +`-150259748047868384659982093203238820648182213478633/2500000000000000000000000000000000000000000000000` +(approximately −60.10389921914735). + +The initial independent-edge bound retained all 897 pairs. The +first exact solver hit its 90-second cap. A 16-pair Dinic retry and +an 881-pair continuation then exhausted the scope. The retained +certificate verifies the exhaustive result without an optimizer. +No physical instance or changed BIT supplier was built. + +## Replay + +From a clean repository checkout, with CPython 3.12 and assertions: + +```sh +python3.12 -B scripts/research_package.py --package research/bit-coupled-chart-bound +``` + +The two live inputs are the word and invoice under +`research/paired-query-only-bit` at canonical commit +`e54523517d0f03e58352e647c403a5af3e525a57`. The +[source manifest](SOURCES.json) pins both paths, Git blobs and SHA-256 +digests. For a verified Git-free export, run from the extracted root: + +```sh +python3.12 -I -B research/bit-coupled-chart-bound/verify.py --root . +``` + +The independent checker rebuilds the literal logical lifetimes, +uses rational Gaussian elimination for nesting, reconstructs the +full 36-copy signed invoice, and checks every directed cut/flow +certificate. It tests altered source bytes and a forged flow. +Expected output and the SHA-256 digest of the decompressed certificate +are in [AUDIT.json](AUDIT.json). The certificates use exact integer +capacities at the directed tariff grid declared in the verifier. + +## Open next questions + +Can simultaneous choices among three or more chart labels change the +paid profile? First bound a specified multichart component with each +shared ADD contact and endpoint charged once. A target-clearing bound +would need an exact arbitrary-input action and fully charged replay. +Additional intermediate moves, new chart stock, changes to contact +order or lifetimes, and caller changes are outside this proof. Pairwise +bounds cannot be added for overlapping changes. + +## Credit + +[#6726](https://github.com/CrocSwap/integer-mult-bounds/pull/6726) +supplies the native BIT word and +[#7001](https://github.com/CrocSwap/integer-mult-bounds/pull/7001) +supplies the paired caller and retained signed invoice. The original +attribution and license remain with those files. +[#7289](https://github.com/CrocSwap/integer-mult-bounds/pull/7289) +bounds balanced changes to ingress destinations at fixed clocks. +[#7293](https://github.com/CrocSwap/integer-mult-bounds/pull/7293) +fixes the original charts and tests the available destination span. +This proof couples chart changes across both ADD operands and charges +each contact edge once. [#7277](https://github.com/CrocSwap/integer-mult-bounds/pull/7277) +is the separately reproduced complete conditional comparator used in +this campaign. The campaign's Round 30 complex flow audit supplied the +certificate algorithm. +OpenAI Codex and subagents materially assisted the proof, implementation, +independent audit and packaging. Apache-2.0. diff --git a/research/bit-coupled-chart-bound/SOURCES.json b/research/bit-coupled-chart-bound/SOURCES.json new file mode 100644 index 0000000000..2f232fb673 --- /dev/null +++ b/research/bit-coupled-chart-bound/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "usage": "input", + "git_blob": "b718d6b2848215ad785022106dfa9f871a3d1c0c", + "sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + }, + { + "path": "research/paired-query-only-bit/EFREE-RESULT.json", + "usage": "input", + "git_blob": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8", + "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b" + } + ] +} diff --git a/research/bit-coupled-chart-bound/TASK.json b/research/bit-coupled-chart-bound/TASK.json new file mode 100644 index 0000000000..3e6c2dfbe9 --- /dev/null +++ b/research/bit-coupled-chart-bound/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "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/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "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." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "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." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "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." + ], + "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." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "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.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "One adjacent nested chart pair at a time on the retained #7001/#6726 BIT word, with both ADD operands sharing their new chart and the complete 36-copy invoice.", + "scope_change_reason": "This holds scalar order, logical lifetimes, chart stock, public endpoints and caller fixed while changing both sides of shared ADD contacts.", + "bottleneck_link": "The complete retained BIT invoice is short by approximately 60.10389921914735 raw directed units at the fixed campaign target.", + "budget_minutes": 9, + "stop_rule": "Screen all eligible pair scopes within 180 seconds. A 90-second leading-cut attempt and 90-second 16-cut retry precede a 180-second continuation over at most 881 cases. Stop on a target-clearing cut, cap, or exhaustion. Independently verify every retained certificate within 180 seconds. A capped scope remains unresolved.", + "outcome": "negative-result", + "evidence": "README.md, CUTS.json.gz, AUDIT.json and verify.py. All 897 exact cuts and the full signed invoice are checked, with mutation and forged-flow controls.", + "author": "Round 30 research campaign", + "ai_assistance": "OpenAI Codex and subagents materially assisted proof, implementation, independent audit and packaging.", + "open_questions": [ + { + "question": "Can simultaneous choices among three or more chart labels produce a compatible whole-word saving?", + "why_it_matters": "One adjacent chart pair alone cannot pay the target shortfall. A shared ADD contact couples any interaction between different pairs.", + "first_step": "Fix a bounded multichart component and compute a rigorous global upper with each contact and endpoint paid once before choosing a site.", + "blocked_by": "The binary flow certificates do not bound multichart choices. A target-clearing upper still needs a fully charged exact arbitrary-input action and replay." + } + ] +} diff --git a/research/bit-coupled-chart-bound/VERIFY.json b/research/bit-coupled-chart-bound/VERIFY.json new file mode 100644 index 0000000000..4f2e4485cb --- /dev/null +++ b/research/bit-coupled-chart-bound/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "research/paired-query-only-bit/EFREE-RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py", + "--root", + "." + ], + "timeout_seconds": 180, + "checks": "Authenticate exact canonical BIT inputs and verify all 897 whole-word flow/cut certificates, full directed signed prices and corrupted-input and forged-flow controls." + } + ] +} diff --git a/research/bit-coupled-chart-bound/pricing.py b/research/bit-coupled-chart-bound/pricing.py new file mode 100644 index 0000000000..40ec194017 --- /dev/null +++ b/research/bit-coupled-chart-bound/pricing.py @@ -0,0 +1,82 @@ +"""Directed interval arithmetic and the retained signed BIT invoice.""" +from collections import Counter +from fractions import Fraction +from functools import cache + +TARGET = "10018846261809/2500000000000000" +SCALE = 10**49 + + +def rounded(x, upper): + scaled = SCALE*x + if upper: + return Fraction(-((-scaled.numerator) // scaled.denominator), SCALE) + return Fraction(scaled.numerator // scaled.denominator, SCALE) + + +@cache +def log_bounds(x): + z = (x-1)/(x+1) + terms = 60 + exact_partial = 2*sum(z**(2*i+1)/(2*i+1) for i in range(terms)) + tail = 2*z**(2*terms+1)/((2*terms+1)*(1-z*z)) + return rounded(exact_partial, False), rounded(exact_partial+tail, True) + + +@cache +def power_bounds(rank, k): + binary = 2**(rank.bit_length()-1) + shift = binary.bit_length()-1 + l2, u2 = log_bounds(Fraction(2)) + lo, hi = log_bounds(Fraction(rank, binary)) + lo, hi = k*(lo+shift*l2), k*(hi+shift*u2) + assert 0 <= lo <= hi < 1 + + def exponential(z, terms): + total = term = Fraction(1) + for i in range(1, terms+1): + term *= -z/i + total += term + return total + + return rounded(rank*exponential(hi, 35), False), rounded(rank*exponential(lo, 34), True) + + +def cost(hist, k): + lower = upper = Fraction(0) + for r, n in hist.items(): + a, b = (n*x for x in power_bounds(r, k)) + lower += min(a, b) + upper += max(a, b) + return lower, upper + + +def profile(invoice, native, word, ranks): + copies = invoice["native_calls"] + assert copies == len(invoice["native_instances"]) == 36 + assert {tuple((r["stage"], r["copy"])) for r in invoice["native_instances"]} == { + (stage, which) for stage in range(1, 19) for which in (0, 1) + } + assert all(r["ports"] == 111 for r in invoice["native_instances"]) + assert native == Counter({int(r): n for r, n in invoice["native_paid"].items()}) + assert sum(native.values()) == 2871 + caller_paid = {1: 444, **{r: 444 for r in range(7, 57, 7)}} + assert invoice["event_counts"]["QUERY"]*111 == caller_paid[1] + assert invoice["event_counts"]["IDLE_ONE"]*111 == 8*444 + full_paid = Counter({r: copies*n for r, n in native.items()}) + full_paid.update(caller_paid) + + helpers = Counter(ranks[word["final"][j]]-ranks[word["start"][j]] + for j in range(222, word["public"])) + assert helpers == Counter({int(r): n for r, n in invoice["native_helpers"].items()}) + caller_targets = {**{r: 444 for r in range(8, 65, 7)}, 127: 222} + full_targets = Counter({r: copies*n for r, n in helpers.items()}) + full_targets.update(caller_targets) + assert full_paid == Counter({int(r): n for r, n in invoice["paid"].items()}) + assert full_targets == Counter({int(r): n for r, n in invoice["targets"].items()}) + assert sum(full_paid.values()) == invoice["paid_jobs"] + assert sum(full_targets.values()) == invoice["productive_fields"] + signed = full_targets.copy() + signed.subtract(full_paid) + assert sum(r*n for r, n in signed.items()) == invoice["rank_surplus"] + return signed, copies diff --git a/research/bit-coupled-chart-bound/verify.py b/research/bit-coupled-chart-bound/verify.py new file mode 100644 index 0000000000..048d6fc6b4 --- /dev/null +++ b/research/bit-coupled-chart-bound/verify.py @@ -0,0 +1,241 @@ +"""Independently check every BIT label flow/cut and its complete invoice.""" +from argparse import ArgumentParser +from collections import Counter, defaultdict +from fractions import Fraction as F +from functools import cache +import gzip +from hashlib import sha256 +from itertools import pairwise +import json +from pathlib import Path +import runpy +from time import monotonic + +PACKAGE = Path(__file__).resolve().parent +WORD = "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz" +INVOICE = "research/paired-query-only-bit/EFREE-RESULT.json" + + +def authenticate(path, raw, digest): + if sha256(raw).hexdigest() != digest: + raise ValueError(f"changed input {path}") + return raw + + +def load_inputs(root): + manifest = json.loads((PACKAGE / "SOURCES.json").read_bytes()) + pins = {} + for entry in manifest["files"]: + if entry["usage"] != "input": + continue + path = entry["path"] + assert path in (WORD, INVOICE) and path not in pins + pins[path] = entry["sha256"] + assert set(pins) == {WORD, INVOICE} + contents = {} + for path, digest in pins.items(): + raw = (root / path).read_bytes() + contents[path] = authenticate(path, raw, digest) + try: + authenticate(path, raw + b"\n", digest) + except ValueError: + continue + raise AssertionError("mutated source accepted") + return json.loads(gzip.decompress(contents[WORD])), json.loads(contents[INVOICE]) + + + +def incidence(word): + n=word['public'] + slots=list(range(n))+[None]*word['owned_fields'] + attr=[(f,False,-1) for f in word['start']] + visits={i:[i] for i in range(n)} + paid=[] + for t,(op,i,*a) in enumerate(word['program']): + if op=='SWAP': + j=a[0] + slots[i],slots[j]=slots[j],slots[i] + elif op=='MOVE': + paid.append(tuple(a)) + else: + v=len(attr) + attr.append((a[-1],True,t)) + if op=='INIT': + assert slots[i] is None + slots[i]=n+t + visits[n+t]=[v] + else: + visits[slots[i]].append(v) + if op=='ADD' and a[0]!=i: + visits[slots[a[0]]].append(v) + if op=='CLEAR': + slots[i]=None + assert all(v is None for v in slots[n:]) + for i,f in enumerate(word['final']): + visits[slots[i]].append(len(attr)) + attr.append((f,False,len(word['program']))) + assert len(visits)==n+237 + edges=[edge for seq in visits.values() for edge in pairwise(seq)] + assert Counter((attr[u][0],attr[v][0]) for u,v in edges if attr[u][0]!=attr[v][0])==Counter(paid) + return attr,edges,paid + + +def linrank(rows): + pivot={} + for row in rows: + r=list(row) + for j in range(len(r)): + x=r[j] + if not x: + continue + if j in pivot: + r=[a-x*b for a,b in zip(r,pivot[j],strict=True)] + else: + pivot[j]=[a/x for a in r] + break + return len(pivot) + + +def add(cap,u,v,w): + if u!=v and w: + cap[u,v]+=w + + +def certify(caps, flow, side, source, sink, n): + balance=[0]*n + used=set() + for u,v,f in flow: + if (u,v) in used or not 0