From 1f2a413f9e27ce9609924f7ab196548c4cbe43d8 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Thu, 15 Oct 2026 21:20:58 +0000 Subject: [PATCH] Research: partitioned independent-walks 7q readout obstruction (no new kappa) Prove every covering dual of two restored walks at total Q=7 (partitions (2,5) and (3,4), independent dirt, dual even-parity) has exact R=112, so the abstract tariff is already >=490>436 at X=0. Answers the partitioned half of the independent-walks OQ after same-walk multi-connector; leave-alones and pending mc7q/dp8q fixtures untouched. Prepared by Wentao Li with substantial AI assistance. --- .../CERTIFICATE.json | 145 +++++++++ .../NOTICE.md | 28 ++ .../independent-walks-7q-obstruction/PROOF.md | 123 +++++++ .../README.md | 77 +++++ .../SOURCES.json | 24 ++ .../TASK.json | 100 ++++++ .../VERIFY.json | 52 +++ .../independent.py | 165 ++++++++++ .../independent-walks-7q-obstruction/model.py | 303 ++++++++++++++++++ .../test_package.py | 100 ++++++ .../verify.py | 228 +++++++++++++ 11 files changed, 1345 insertions(+) create mode 100644 research/independent-walks-7q-obstruction/CERTIFICATE.json create mode 100644 research/independent-walks-7q-obstruction/NOTICE.md create mode 100644 research/independent-walks-7q-obstruction/PROOF.md create mode 100644 research/independent-walks-7q-obstruction/README.md create mode 100644 research/independent-walks-7q-obstruction/SOURCES.json create mode 100644 research/independent-walks-7q-obstruction/TASK.json create mode 100644 research/independent-walks-7q-obstruction/VERIFY.json create mode 100644 research/independent-walks-7q-obstruction/independent.py create mode 100644 research/independent-walks-7q-obstruction/model.py create mode 100644 research/independent-walks-7q-obstruction/test_package.py create mode 100644 research/independent-walks-7q-obstruction/verify.py diff --git a/research/independent-walks-7q-obstruction/CERTIFICATE.json b/research/independent-walks-7q-obstruction/CERTIFICATE.json new file mode 100644 index 0000000000..3bb324671a --- /dev/null +++ b/research/independent-walks-7q-obstruction/CERTIFICATE.json @@ -0,0 +1,145 @@ +{ + "schema_version": 1, + "status": "PASS_INDEPENDENT_WALKS_7Q_OBSTRUCTION", + "scope": "Five-source common-B mutable-source Q/R/X alphabet (PR1898). Partitioned independent dual walks at total Q=7 (valid restored lengths (2,5) and (3,4)): covering dual even-parity readout has exact R=112; tariff floor at X=0 is 490>436. Answers independent-walks OQ (partitioned case) after same-walk multi-connector.", + "claim": { + "Q": 7, + "partition_covering_min_R": 112, + "partition_25_covering": 416640, + "partition_34_covering": 833280, + "partition_25_R_exact": 112, + "partition_34_R_exact": 112, + "tariff_floor_at_X0": 490, + "endpoint_Q6_tariff": 436, + "undercuts_436_after_complete_bill": false, + "length1_walks_invalid": true, + "answers_independent_walks_partitioned": true, + "oq_answer": "Every covering partitioned dual-walk schedule with total query count Q=n0+n1=7 (valid restored walks of lengths (2,5) or (3,4), distinct nonzero labels within each walk, independent dirt, dual even-parity readout) has exact R=112. At X=0 the abstract tariff is already 490>436; positive path X only increases the bill. Length-1 components are not restored (closed zero edge). Same-walk multi-connector remains the pending mc7q package; transfer-coupled schedules are out of scope here.", + "no_new_kappa": true + }, + "partition_2_plus_5": { + "kind": "partition_2_plus_5", + "Q": 7, + "covering_pairs": 416640, + "structural_ok": 416640, + "attainable_R": [ + 112 + ], + "histogram": { + "112": 416640 + }, + "min_R": 112, + "first_witnesses": { + "112": [ + [ + 0, + 1 + ], + [ + 0, + 2, + 4, + 8, + 16 + ] + ] + } + }, + "partition_3_plus_4": { + "kind": "partition_3_plus_4", + "Q": 7, + "covering_pairs": 833280, + "attainable_R": [ + 112 + ], + "histogram": { + "112": 833280 + }, + "min_R": 112, + "first_witnesses": { + "112": [ + [ + 0, + 1, + 2 + ], + [ + 0, + 4, + 8, + 16 + ] + ] + } + }, + "champion": { + "champion_25": { + "walks": [ + [ + 0, + 1 + ], + [ + 0, + 2, + 4, + 8, + 16 + ] + ], + "R": 112, + "path_X": 6, + "tariff": 502, + "structural": { + "covering": true, + "rank": 4, + "sigma_in_span": false, + "R": 112, + "sum_even": 40 + } + }, + "champion_34": { + "walks": [ + [ + 0, + 1, + 2 + ], + [ + 0, + 4, + 8, + 16 + ] + ], + "R": 112, + "path_X": 6, + "tariff": 502 + }, + "tariff_floor_at_X0": 490, + "endpoint_Q6": 436, + "single_walk_even_min_R": 82 + }, + "length1_invalid_examples": [ + { + "slots": [ + 0 + ], + "valid_restored_walk": false, + "path_X": null, + "note": "closed_(0,0)_zero_edge" + } + ], + "unit_tariff": { + "b": 38, + "a": 2, + "x": 2 + }, + "tariff_check": { + "formula": "38*Q + 2*R + 2*X", + "at_R112_X0": 490, + "champion_25": 502, + "champion_34": 502, + "endpoint_Q6": 436 + } +} diff --git a/research/independent-walks-7q-obstruction/NOTICE.md b/research/independent-walks-7q-obstruction/NOTICE.md new file mode 100644 index 0000000000..e330e2254f --- /dev/null +++ b/research/independent-walks-7q-obstruction/NOTICE.md @@ -0,0 +1,28 @@ +# Notice + +New material in this directory is Apache-2.0. + +Predecessor credit (do not alter historical notices elsewhere): + +- Arham Tahir / PR1898 `research/mutable-source-minimum-queries` — five-source + alphabet, minimum-query endpoint, abstract complete-call tariff. +- ywz65 / open PR2455 `research/mutable-source-six-query-xor` — component lemma + and restored interaction-graph census at six queries. +- Arham Tahir / PR1370 — path-local shear lowering. +- TennisBowling / PR1524 — equal-price theorem and unequal-price handoff. +- Ross Richardson / PR943/934 — prefix framework. +- Fork path-lowered `research/mutable-source-789q-invoice` / open #2677 — + distinct-slot spectrum and champion path; not edited. +- Open #2643 `research/seven-query-xor-floor` — restored `X ≥ 6` at `Q = 7`; + not edited. +- Open #2686 `research/seven-query-r-floor` — even-subset `R ≥ 82`; not edited. +- Open #2715 `research/cheaper-readout-7q-obstruction` — all-subset / + dirty-parity repair; not edited. +- Pending `research/multi-connector-7q-obstruction` (same-walk multi-connector / + priced shadow); not edited; this package answers its independent-walks + partitioned follow-up without competing on the same-walk fixture. +- Pending `research/dirty-parity-8q-obstruction`; not edited. +- Live pin: `research/mutable-source-shear-cost/CERTIFICATE.json`. + +Prepared by Wentao Li (VictorLiwentao, @Is__Victor) with substantial AI +assistance. diff --git a/research/independent-walks-7q-obstruction/PROOF.md b/research/independent-walks-7q-obstruction/PROOF.md new file mode 100644 index 0000000000..840622074f --- /dev/null +++ b/research/independent-walks-7q-obstruction/PROOF.md @@ -0,0 +1,123 @@ +# Partitioned independent walks cannot undercut tariff 436 at Q=7 + +This is a scoped obstruction in the five-source common-B mutable-source alphabet +of [PR1898](https://github.com/CrocSwap/integer-mult-bounds/pull/1898). It answers +the **partitioned independent-walks** open question left after same-walk +multi-connector / priced-shadow work on the #2715 lineage: can two restored +walks with **distinct slot lists**, independent dirt, and dual even-parity +readout undercut the six-query endpoint tariff `436` at total `Q = 7`? + +No new kappa is claimed. Leave-alone packages through #2715 are not edited. +Pending same-walk `multi-connector-7q` and `dirty-parity-8q` packages are not +edited or competed with on their fixtures. + +## Setup + +Retain queries `Q_j`, readouts `R_m: y_m += A_m z`, and paid source shears +`X_(s,t)`. A **restored walk** of length `n` is an open slot list +`(s_0,…,s_{n-1})` with `s_0 = 0` whose closed completion `(s_0,…,s_{n-1},0)` +has only nonzero edges. Length-1 lists are illegal: the closed return is the +zero edge `(0,0)`. + +A **partitioned independent dual** of total query count `Q = 7` is a pair of +valid restored walks of lengths `(n_0,n_1)` with `n_0 + n_1 = 7` and +`n_0,n_1 ≥ 2`. Up to swap the only cases are `(2,5)` and `(3,4)`. Each walk +carries its own dirt coefficient. For mask `m` the dual even-parity cost is + +```text +min_a (e0[a] + e1[a ⊕ m]), +``` + +where `e_i` is the even-subset table of walk `i` (with `e_i[0] = 0`). + +The abstract complete-call tariff at `(b,a,x)=(38,2,2)` is `38·Q + 2·R + 2·X`. + +## Length-1 exclusion + +A length-1 list `(0,)` closes to `(0,0)`. That edge has XOR `0`, so it is not a +restored walk. Consequently `(1,6)` and `(6,1)` are not legal partitions of a +`Q = 7` dual schedule. + +## Fixture A: partition `(2,5)` + +Short walk `(0,σ)` has even table `e0[0]=0`, `e0[σ]=2`. Long walk +`(0,b_1,b_2,b_3,b_4)` with distinct nonzero labels. Dual cost collapses to + +```text +R = Σ_{m=1}^{31} min( e1[m], 2 + e1[m ⊕ σ] ). +``` + +**Lemma (cover ⇒ outside coset).** Covering requires the long span `V` to have +rank `4` and `σ ∉ V`. Then masks in `V` pay `e1`, and masks in the complementary +coset pay `2 + e1(· ⊕ σ)`, so + +```text +R = 2 · Σ_{v ∈ V \ {0}} e1[v] + 32. +``` + +**Lemma (F₂⁴ even-sum).** Any four linearly independent nonzero labels are a +basis of a 4-dimensional subspace. With a free `0`-slot, even-subset cost of a +vector equals the least even integer `≥` its Hamming weight in that basis. +Summing over the `15` nonzero vectors of `F₂⁴` yields exactly `40`. Hence every +covering `(2,5)` schedule has + +```text +R = 2·40 + 32 = 112. +``` + +**Census.** Distinct-label pairs: `31 · C(31,4) = 975415` candidates; covering +count `416640`; attainable `R = {112}` only; structural identity holds on every +covering pair. + +Champion: `((0,1), (0,2,4,8,16))` with path `X = 6`, tariff `502`. +(The `X = 0` figure `490` is only the abstract lower bound from `R = 112`; +a length-5 closed walk lies in a bipartite hypercube, so odd closed single-bit +tours are impossible and attainable path `X` is strictly positive.) + +## Fixture B: partition `(3,4)` + +**Census.** Distinct-label pairs: `C(31,2)·C(31,3) = 2090175` candidates; +covering count `833280`; attainable `R = {112}` only (machine-checked dual +`min_a` on every covering pair — not a copy of a constant). + +Champion: `((0,1,2), (0,4,8,16))` with path `X = 6`, tariff `502`. + +## Tariff consequence + +Every covering partitioned dual at `Q = 7` has exact `R = 112`. Even at +`X = 0`, + +```text +38·7 + 2·112 + 2·0 = 490 > 436. +``` + +Positive path-`X` only increases the bill. Partitioned independent walks +therefore cannot undercut the six-query endpoint under the PR1898 abstract +tariff. By comparison, a single same-walk even-subset schedule can reach +`R = 82` ([#2686](https://github.com/CrocSwap/integer-mult-bounds/pull/2686)); +splitting the query budget across two independent dirt ports forces a much +worse readout invoice. + +## Scope limits + +- Fixes the **partitioned** independent-walk interface at total `Q = 7` with + distinct nonzero labels within each walk. Transfer-coupled schedules + (shared prefix, priced transfer, divergent suffixes) are outside; same-walk + multi-connector / priced shadow remains the pending `multi-connector-7q` + package. +- Shared non-path XOR schedules remain deferred (soft-overlap with #2643). +- Host screens are deferred. +- Leave-alone through #2715 (including #2593, #2643, #2677, #2686, #2687, #2715) + is not edited. +- No new kappa, physical supplier, or multiplication theorem. + +## Relation to predecessors + +| Prior | Already proves | This package adds | +|---|---|---| +| PR1898 | Min `Q=6`, endpoint tariff 436 | — | +| #2643 | `X≥6` at single-walk `Q=7` | — | +| #2686 | Even-subset `R≥82` on one walk | — | +| #2715 | All-subset collapses under dirty-parity; OQs | — | +| Pending mc7q | Same-walk dual / dirty shadow stay at `R≥82` | — | +| **This** | — | **Partitioned dual walks at `Q=7` have exact `R=112`; tariff floor `490>436`** | diff --git a/research/independent-walks-7q-obstruction/README.md b/research/independent-walks-7q-obstruction/README.md new file mode 100644 index 0000000000..39f9e7c009 --- /dev/null +++ b/research/independent-walks-7q-obstruction/README.md @@ -0,0 +1,77 @@ +# Partitioned independent-walk obstruction at seven queries + +**Scoped obstruction / priced alphabet; no new kappa.** Answers the +**partitioned independent-walks** open question on the #2715 / +multi-connector lineage in the five-source common-B mutable-source alphabet of +[#1898](https://github.com/CrocSwap/integer-mult-bounds/pull/1898): can two +restored walks with distinct slot lists, independent dirt, and dual +even-parity readout undercut tariff `436` at total `Q=7`? + +| Dual schedule | Covering pairs | Exact R | Tariff floor (X≥0) | Undercuts 436? | +|---|---:|---:|---:|---| +| Same-walk even-subset (#2686) | — | ≥82 | ≥442 at X=6 | no | +| Partition `(2,5)` | **416640** | **112** | **≥490** | **no** | +| Partition `(3,4)` | **833280** | **112** | **≥490** | **no** | + +Every covering partitioned dual has exact `R=112` (structural `F₂⁴` identity +on `(2,5)`; full dual census on `(3,4)`). Length-1 components are not restored. +Same-walk multi-connector remains the pending `multi-connector-7q` package. + +## Reproduction + +```sh +python3.12 -I -B research/independent-walks-7q-obstruction/verify.py +python3.12 -I -O -B research/independent-walks-7q-obstruction/verify.py +python3.12 -I -B research/independent-walks-7q-obstruction/independent.py +python3.12 -I -B research/independent-walks-7q-obstruction/test_package.py +python3.12 -B scripts/research_package.py --package research/independent-walks-7q-obstruction +``` + +Expected: + +```text +PASS_INDEPENDENT_WALKS_7Q_OBSTRUCTION partition_min_R=112 ... tariff_floor=490 ... answers_independent_walks_partitioned no_new_kappa +PASS_INDEPENDENT_PARTITIONED_WALKS_7Q covering_25=416640 covering_34=833280 partition_min_R=112 tariff_floor=490 ... no_new_kappa +PASS_INDEPENDENT_WALKS_7Q_PACKAGE_TESTS groups=6 +PASS_REGISTERED_RESEARCH_PACKAGE research/independent-walks-7q-obstruction outcome=completed +``` + +Default verify is read-only. Admission uses `need()`; `-O` also passes. + +## Overlap + +Base commit `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. Direct predecessors: +PR1898, #2643, #2686, #2715, pending same-walk multi-connector OQ. Leave-alone +through #2715 including #2593, #2643, #2677, #2686, #2687, #2715 is respected; +those packages are not edited. Pending `cursor/multi-connector-7q-60b9` and +`cursor/dirty-parity-8q-60b9` are not edited or competed with on their fixtures. +Deferred shared-XOR soft-overlap with #2643 and host screens are not opened. + +## Open next questions + +1. Can a **transfer-coupled** dual (shared prefix, priced transfer `C≥1`, + divergent suffixes) undercut tariff 436 after charging walks+transfers+dirt + at total `Q=7`? + Why it matters: remaining independent-walk direction after partitioned + collapse. + First step: fix shapes `(p,a,b)` with `p+a+b=7` and census dirt-legal R with + fair shared-prefix XOR billing. + Blocked by: larger search; pending same-walk mc7q not a blocker for this + freestanding fixture. +2. Do non-distinct (repeat-label) layers inside a partitioned walk improve on + `R=112`? + Why it matters: closes the one-repeat companion of the Hamilton layer. + First step: allow one repeated nonzero label in the length-5 walk of `(2,5)`. + Blocked by: larger search; expected to worsen coverage/cost. + +## Credit + +Credit **Arham Tahir / PR1898**, **ywz65 / PR2455**, **PR1370**, fork **789q** / +**#2677**, **#2643**, **#2686**, open **#2715**, pending same-walk +multi-connector (OQ answered here for the partitioned case; not edited), +**TennisBowling / PR1524**, **Ross Richardson / PR943**, and the retained +mutable-source lineage. Live input pin: +`research/mutable-source-shear-cost/CERTIFICATE.json`. Prepared by Wentao Li +([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance. +Apache-2.0. No independent human review or multiplication theorem is claimed. diff --git a/research/independent-walks-7q-obstruction/SOURCES.json b/research/independent-walks-7q-obstruction/SOURCES.json new file mode 100644 index 0000000000..719b378cbd --- /dev/null +++ b/research/independent-walks-7q-obstruction/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/mutable-source-shear-cost/CERTIFICATE.json", + "usage": "input", + "git_blob": "48958451bc819f2caa13bf3d9609423706ffb8a0", + "sha256": "665435375c025bbcf69eadf43bd9aeae44eb12fefdf12a78d5bfd66abde4ae3c" + } + ] +} diff --git a/research/independent-walks-7q-obstruction/TASK.json b/research/independent-walks-7q-obstruction/TASK.json new file mode 100644 index 0000000000..5f8aa82721 --- /dev/null +++ b/research/independent-walks-7q-obstruction/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 4, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Price partitioned independent dual walks at total Q=7 in the PR1898 alphabet: prove every covering (2,5) and (3,4) dual even-parity schedule has exact R=112 (tariff floor 490>436), answering the independent-walks partitioned OQ after same-walk multi-connector.", + "scope_change_reason": "The drawn connector-alphabet card is redirected to the explicit independent-walks open question left by the #2715 / multi-connector lineage on the #1898 fixture, which is the nearest freestanding priced obstruction outside leave-alones and pending same-walk / dirty-parity packages.", + "bottleneck_link": "A priced partitioned dual-walk alphabet decides whether splitting the seven-query budget across two independently dirty connectors can undercut the six-query endpoint.", + "budget_minutes": 60, + "stop_rule": "Stop after (2,5) structural identity, (3,4) dual census, length-1 invalidation, tariff floor, package tests; no transfer-coupled full census, no same-walk reopen, no host screens.", + "outcome": "completed", + "evidence": "CERTIFICATE.json (2,5) covering 416640 all R=112 with F2^4 even-sum 40; (3,4) covering 833280 all R=112; champions tariff 490/502; independent checker; corruption controls.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for derivation, implementation, checking and writing.", + "open_questions": [ + { + "question": "Can a transfer-coupled dual (shared prefix, priced transfer C>=1, divergent suffixes) undercut tariff 436 after charging walks+transfers+dirt at total Q=7?", + "why_it_matters": "Remaining independent-walk direction after partitioned collapse.", + "first_step": "Fix shapes (p,a,b) with p+a+b=7 and census dirt-legal R with fair shared-prefix XOR billing.", + "blocked_by": "Larger search." + }, + { + "question": "Do non-distinct (repeat-label) layers inside a partitioned walk improve on R=112?", + "why_it_matters": "Closes the one-repeat companion of the Hamilton layer.", + "first_step": "Allow one repeated nonzero label in the length-5 walk of (2,5).", + "blocked_by": "Larger search; expected to worsen coverage/cost." + } + ], + "predecessors": [ + { + "pr": 1898, + "credit": "Arham Tahir; minimum-query endpoint and abstract tariff fixture" + }, + { + "pr": 2715, + "credit": "Wentao Li; cheaper-readout obstruction; independent-walks OQ lineage" + }, + { + "pr": 2686, + "credit": "Wentao Li; even-subset R floor on one walk" + }, + { + "pr": 2643, + "credit": "Wentao Li; seven-query XOR floor X>=6" + }, + { + "pr": 2677, + "credit": "Wentao Li; path-lowered 7-9Q invoices" + }, + { + "pr": 2455, + "credit": "ywz65; six-query XOR necessity" + }, + { + "pr": 1370, + "credit": "Arham Tahir; path-local shear lowering / four-X word" + }, + { + "pr": 1524, + "credit": "TennisBowling; equal-price theorem / unequal-price handoff" + } + ] +} diff --git a/research/independent-walks-7q-obstruction/VERIFY.json b/research/independent-walks-7q-obstruction/VERIFY.json new file mode 100644 index 0000000000..6d1c1669a9 --- /dev/null +++ b/research/independent-walks-7q-obstruction/VERIFY.json @@ -0,0 +1,52 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/mutable-source-shear-cost/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Partitioned (2,5)/(3,4) dual census; structural F2^4 identity; length-1 invalid; champions; tariff floor 490; certificate match; source pins" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Same admission under PYTHONOPTIMIZE via need()" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 180, + "checks": "Separate partitioned dual census, champions, tariff arithmetic" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 600, + "checks": "Corruption rejection, duplicate JSON keys, -O controls, independent replay" + } + ] +} diff --git a/research/independent-walks-7q-obstruction/independent.py b/research/independent-walks-7q-obstruction/independent.py new file mode 100644 index 0000000000..8e698248ef --- /dev/null +++ b/research/independent-walks-7q-obstruction/independent.py @@ -0,0 +1,165 @@ +#!/usr/bin/env python3 +"""Independent partitioned dual-walk census at Q=7. + +Does not import model.py or verify.py. Prepared by Wentao Li with substantial +AI assistance. Apache-2.0. +""" +from __future__ import annotations + +import json +from collections import Counter +from itertools import combinations +from pathlib import Path + +HERE = Path(__file__).resolve().parent +CERT_PATH = HERE / "CERTIFICATE.json" +INF = 99 + + +def fail(message): + raise SystemExit(f"FAIL_INDEPENDENT: {message}") + + +def even_table(slots): + n = len(slots) + even = [INF] * 32 + even[0] = 0 + for bits in range(1, 1 << n): + size = bits.bit_count() + if size % 2: + continue + value = 0 + for i in range(n): + if bits >> i & 1: + value ^= slots[i] + if size < even[value]: + even[value] = size + return even + + +def dual_full(e0, e1): + total = 0 + for m in range(1, 32): + best = INF + for a in range(32): + c0, c1 = e0[a], e1[a ^ m] + if c0 < INF and c1 < INF: + best = min(best, c0 + c1) + if best >= INF: + return None + total += best + return total + + +def dual_short(e_long, sigma): + total = 0 + for m in range(1, 32): + best = INF + if e_long[m] < INF: + best = e_long[m] + if e_long[m ^ sigma] < INF: + best = min(best, 2 + e_long[m ^ sigma]) + if best >= INF: + return None + total += best + return total + + +def path_X(slots): + closed = slots + (0,) + total = 0 + for a, b in zip(closed, closed[1:]): + delta = a ^ b + if delta == 0: + return None + total += 2 * (delta.bit_count() - 1) + return total + + +def tariff(q, r, x): + return 38 * q + 2 * r + 2 * x + + +def census_25(): + hist = Counter() + covering = 0 + tables = { + nz: even_table((0,) + nz) for nz in combinations(range(1, 32), 4) + } + for sigma in range(1, 32): + for e_long in tables.values(): + r = dual_short(e_long, sigma) + if r is None: + continue + covering += 1 + hist[r] += 1 + return covering, hist + + +def census_34(): + hist = Counter() + covering = 0 + t3 = {nz: even_table((0,) + nz) for nz in combinations(range(1, 32), 2)} + t4 = {nz: even_table((0,) + nz) for nz in combinations(range(1, 32), 3)} + for e0 in t3.values(): + for e1 in t4.values(): + r = dual_full(e0, e1) + if r is None: + continue + covering += 1 + hist[r] += 1 + return covering, hist + + +def main(): + cert = json.loads(CERT_PATH.read_text(encoding="utf-8")) + claim = cert["claim"] + + c25, h25 = census_25() + c34, h34 = census_34() + if c25 != claim["partition_25_covering"]: + fail(f"25 covering {c25} != {claim['partition_25_covering']}") + if c34 != claim["partition_34_covering"]: + fail(f"34 covering {c34} != {claim['partition_34_covering']}") + if min(h25) != 112 or set(h25) != {112}: + fail(f"25 hist {dict(h25)}") + if min(h34) != 112 or set(h34) != {112}: + fail(f"34 hist {dict(h34)}") + if h25[112] != c25 or h34[112] != c34: + fail("histogram counts") + + # Champions + w25_a, w25_b = (0, 1), (0, 2, 4, 8, 16) + w34_a, w34_b = (0, 1, 2), (0, 4, 8, 16) + r25 = dual_short(even_table(w25_b), 1) + r34 = dual_full(even_table(w34_a), even_table(w34_b)) + if r25 != 112 or r34 != 112: + fail(f"champion R {r25} {r34}") + x25 = path_X(w25_a) + path_X(w25_b) + x34 = path_X(w34_a) + path_X(w34_b) + if x25 != 6 or x34 != 6: + fail(f"champion X {x25} {x34}") + if path_X((0,)) is not None: + fail("length-1 should be invalid") + + floor = tariff(7, 112, 0) + if floor != 490 or floor <= 436: + fail(f"tariff floor {floor}") + if tariff(7, 112, x25) < floor or tariff(7, 112, x34) < floor: + fail("champion tariff below floor") + + print( + "PASS_INDEPENDENT_PARTITIONED_WALKS_7Q", + f"covering_25={c25}", + f"covering_34={c34}", + "partition_min_R=112", + f"tariff_floor={floor}", + "endpoint=436", + "answers_independent_walks_partitioned", + "no_new_kappa", + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/independent-walks-7q-obstruction/model.py b/research/independent-walks-7q-obstruction/model.py new file mode 100644 index 0000000000..49809a4fa0 --- /dev/null +++ b/research/independent-walks-7q-obstruction/model.py @@ -0,0 +1,303 @@ +"""Partitioned independent-walk dual readout at seven queries. + +Answers the independent-walks open question left by multi-connector / #2715 +lineage (partitioned case): two restored walks with independent dirt and +distinct slot lists, total Q = n0 + n1 = 7, dual even-parity readout. + +Self-contained relative to PR1898 / #2643 / #2686 / #2715 / pending mc7q +same-walk. Prepared by Wentao Li with substantial AI assistance. Apache-2.0. +""" +from __future__ import annotations + +from collections import Counter +from itertools import combinations + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +INF = 99 + +EXPECTED = { + "partition_25_covering": 416640, + "partition_25_min_R": 112, + "partition_25_histogram": {"112": 416640}, + "partition_34_covering": 833280, + "partition_34_min_R": 112, + "partition_34_histogram": {"112": 833280}, + "partition_R": 112, + "champion_25_walks": ((0, 1), (0, 2, 4, 8, 16)), + "champion_34_walks": ((0, 1, 2), (0, 4, 8, 16)), + "champion_25_path_X": 6, + "champion_34_path_X": 6, + "tariff_floor_at_X0": 490, + "endpoint_tariff_Q6": 436, + "single_walk_even_min_R": 82, + "length1_invalid": True, +} + + +def tariff_qrx(q, r, x, extra=0): + """Abstract complete-call tariff at (b,a,x)=(38,2,2), plus optional extras.""" + leaves = 28 * q + r + nodes = 9 * q + dispatch = q + r + x + return leaves + nodes + x + dispatch + extra + + +def even_table(slots): + """Even-subset per-mask minima on a slot list (INF if unreachable).""" + need(type(slots) is tuple and slots and slots[0] == 0, "slots must start at 0") + n = len(slots) + even = [INF] * 32 + even[0] = 0 + for bits in range(1, 1 << n): + size = bits.bit_count() + if size % 2: + continue + value = 0 + for i in range(n): + if bits >> i & 1: + value ^= slots[i] + if size < even[value]: + even[value] = size + return even + + +def dual_independent_R(e0, e1): + """Σ_m min_a (e0[a] + e1[a⊕m]) with independent even-parity ports.""" + total = 0 + for m in range(1, 32): + best = INF + for a in range(32): + c0 = e0[a] + c1 = e1[a ^ m] + if c0 < INF and c1 < INF: + cost = c0 + c1 + if cost < best: + best = cost + if best >= INF: + return None + total += best + return total + + +def dual_R_short_long(e_long, sigma): + """Optimized dual when the short walk is (0, sigma): e_short[0]=0, e_short[sigma]=2.""" + total = 0 + for m in range(1, 32): + best = INF + if e_long[m] < INF: + best = e_long[m] + flipped = e_long[m ^ sigma] + if flipped < INF: + best = min(best, 2 + flipped) + if best >= INF: + return None + total += best + return total + + +def gf2_span(vals): + basis = [] + for v in vals: + x = v + for b in basis: + x = min(x, x ^ b) + if x: + basis.append(x) + basis.sort(reverse=True) + span = {0} + for b in basis: + span |= {s ^ b for s in span} + return frozenset(span), len(basis) + + +def path_X(slots): + """Path XOR cost on the restored closed walk slots + (0,).""" + closed = slots + (0,) + total = 0 + for a, b in zip(closed, closed[1:]): + delta = a ^ b + if delta == 0: + return None + total += 2 * (delta.bit_count() - 1) + return total + + +def valid_restored_walk(slots): + """A restored walk needs length ≥ 2 (closed return must be a nonzero edge).""" + if type(slots) is not tuple or not slots or slots[0] != 0: + return False + if len(slots) < 2: + return False + return path_X(slots) is not None + + +def sum_even_nonzero(even, span): + return sum(even[v] for v in span if v != 0) + + +def structural_25_identity(sigma, long_slots): + """Lemma check: covering (2,5) forces rank-4 long span, sigma outside, R=112.""" + e_long = even_table(long_slots) + span, rank = gf2_span(long_slots) + r = dual_R_short_long(e_long, sigma) + if r is None: + return { + "covering": False, + "rank": rank, + "sigma_in_span": sigma in span, + "R": None, + "sum_even": None, + } + need(rank == 4, "covering (2,5) long walk must have rank 4") + need(sigma not in span, "covering (2,5) sigma must lie outside long span") + even_sum = sum_even_nonzero(e_long, span) + need(even_sum == 40, f"even sum on F2^4 basis+0 must be 40, got {even_sum}") + need(r == 2 * even_sum + 32 == 112, f"structural R identity failed: {r}") + return { + "covering": True, + "rank": rank, + "sigma_in_span": False, + "R": r, + "sum_even": even_sum, + } + + +def enumerate_partition_25(): + """All distinct-label (2,5) pairs; covering ones have R=112 exactly.""" + hist = Counter() + covering = 0 + structural_ok = 0 + witnesses = {} + long_tables = {} + for nz in combinations(range(1, 32), 4): + slots = (0,) + nz + long_tables[nz] = (slots, even_table(slots)) + for sigma in range(1, 32): + for nz, (slots, e_long) in long_tables.items(): + r = dual_R_short_long(e_long, sigma) + if r is None: + continue + info = structural_25_identity(sigma, slots) + need(info["covering"], "dual cover without structural cover") + need(info["R"] == 112, "structural R") + covering += 1 + structural_ok += 1 + hist[r] += 1 + witnesses.setdefault(r, ((0, sigma), slots)) + return { + "kind": "partition_2_plus_5", + "Q": 7, + "covering_pairs": covering, + "structural_ok": structural_ok, + "attainable_R": sorted(hist), + "histogram": {str(r): hist[r] for r in sorted(hist)}, + "min_R": min(hist) if hist else None, + "first_witnesses": { + str(r): [list(w0), list(w1)] for r, (w0, w1) in witnesses.items() + }, + } + + +def enumerate_partition_34(): + """All distinct-label (3,4) pairs; covering ones have R=112 exactly.""" + hist = Counter() + covering = 0 + witnesses = {} + tables3 = { + nz: ((0,) + nz, even_table((0,) + nz)) for nz in combinations(range(1, 32), 2) + } + tables4 = { + nz: ((0,) + nz, even_table((0,) + nz)) for nz in combinations(range(1, 32), 3) + } + for _a, (s0, e0) in tables3.items(): + for _b, (s1, e1) in tables4.items(): + r = dual_independent_R(e0, e1) + if r is None: + continue + covering += 1 + hist[r] += 1 + witnesses.setdefault(r, (s0, s1)) + need(r == 112, f"(3,4) covering R must be 112, got {r}") + return { + "kind": "partition_3_plus_4", + "Q": 7, + "covering_pairs": covering, + "attainable_R": sorted(hist), + "histogram": {str(r): hist[r] for r in sorted(hist)}, + "min_R": min(hist) if hist else None, + "first_witnesses": { + str(r): [list(w0), list(w1)] for r, (w0, w1) in witnesses.items() + }, + } + + +def length1_invalid_examples(): + """Length-1 'walks' are not restored: closed return is a zero edge.""" + examples = [] + for slots in ((0,),): + examples.append( + { + "slots": list(slots), + "valid_restored_walk": valid_restored_walk(slots), + "path_X": path_X(slots), + "note": "closed_(0,0)_zero_edge", + } + ) + need(all(not ex["valid_restored_walk"] for ex in examples), "length-1 must be invalid") + need(all(ex["path_X"] is None for ex in examples), "zero return edge") + return examples + + +def champion_analysis(): + w25_a, w25_b = EXPECTED["champion_25_walks"] + w34_a, w34_b = EXPECTED["champion_34_walks"] + need(valid_restored_walk(w25_a) and valid_restored_walk(w25_b), "champ 25 valid") + need(valid_restored_walk(w34_a) and valid_restored_walk(w34_b), "champ 34 valid") + e25b = even_table(w25_b) + r25 = dual_R_short_long(e25b, w25_a[1]) + r34 = dual_independent_R(even_table(w34_a), even_table(w34_b)) + x25 = path_X(w25_a) + path_X(w25_b) + x34 = path_X(w34_a) + path_X(w34_b) + need(r25 == 112 and r34 == 112, "champion R") + need(x25 == EXPECTED["champion_25_path_X"], "champ 25 X") + need(x34 == EXPECTED["champion_34_path_X"], "champ 34 X") + struct = structural_25_identity(w25_a[1], w25_b) + need(struct["covering"] and struct["R"] == 112, "champ structural") + tariff25 = tariff_qrx(7, r25, x25) + tariff34 = tariff_qrx(7, r34, x34) + tariff_floor = tariff_qrx(7, 112, 0) + need(tariff_floor == EXPECTED["tariff_floor_at_X0"], "floor") + need(tariff_floor > EXPECTED["endpoint_tariff_Q6"], "no undercut at X0") + need(tariff25 >= tariff_floor and tariff34 >= tariff_floor, "champ tariffs") + return { + "champion_25": { + "walks": [list(w25_a), list(w25_b)], + "R": r25, + "path_X": x25, + "tariff": tariff25, + "structural": struct, + }, + "champion_34": { + "walks": [list(w34_a), list(w34_b)], + "R": r34, + "path_X": x34, + "tariff": tariff34, + }, + "tariff_floor_at_X0": tariff_floor, + "endpoint_Q6": EXPECTED["endpoint_tariff_Q6"], + "single_walk_even_min_R": EXPECTED["single_walk_even_min_R"], + } + + +def even_sum_standard_F2_4(): + """Σ_{v≠0} least_even_geq(wt(v)) over F2^4 = 40.""" + total = 0 + for v in range(1, 16): + wt = v.bit_count() + total += wt + (wt % 2) # least even integer ≥ wt, using free 0-slot + return total diff --git a/research/independent-walks-7q-obstruction/test_package.py b/research/independent-walks-7q-obstruction/test_package.py new file mode 100644 index 0000000000..f847c44985 --- /dev/null +++ b/research/independent-walks-7q-obstruction/test_package.py @@ -0,0 +1,100 @@ +#!/usr/bin/env python3 +"""Package fault controls for independent-walks 7q obstruction. Wentao Li + AI.""" +from __future__ import annotations + +import json +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PKG_NAME = "independent-walks-7q-obstruction" + + +def need(ok, message): + if not ok: + raise SystemExit(f"FAIL_TEST: {message}") + + +def run(args, cwd=None): + return subprocess.run(args, cwd=cwd or ROOT, text=True, capture_output=True) + + +def main(): + # 1) Default read-only verify. + proc = run([sys.executable, "-I", "-B", str(HERE / "verify.py")]) + need(proc.returncode == 0, proc.stderr + proc.stdout) + need("PASS_INDEPENDENT_WALKS_7Q_OBSTRUCTION" in proc.stdout, proc.stdout) + + # 2) -O admission via need(). + proc = run([sys.executable, "-I", "-O", "-B", str(HERE / "verify.py")]) + need(proc.returncode == 0, proc.stderr + proc.stdout) + need("PASS_INDEPENDENT_WALKS_7Q_OBSTRUCTION" in proc.stdout, proc.stdout) + + # 3) Certificate claim corruption fails. + with tempfile.TemporaryDirectory() as tmp: + tmp_path = Path(tmp) + research = tmp_path / "research" / PKG_NAME + shutil.copytree(HERE, research) + pinned = tmp_path / "research" / "mutable-source-shear-cost" + pinned.mkdir(parents=True) + shutil.copy2( + ROOT / "research" / "mutable-source-shear-cost" / "CERTIFICATE.json", + pinned / "CERTIFICATE.json", + ) + cert = research / "CERTIFICATE.json" + data = json.loads(cert.read_text(encoding="utf-8")) + data["claim"]["partition_covering_min_R"] = 0 + cert.write_text(json.dumps(data, indent=2) + "\n", encoding="utf-8") + proc = run([sys.executable, "-I", "-B", str(research / "verify.py")], cwd=tmp_path) + need(proc.returncode != 0, "corrupted certificate should fail") + + # 4) Source pin corruption rejection. + with tempfile.TemporaryDirectory() as tmp: + tmp_path = Path(tmp) + research = tmp_path / "research" / PKG_NAME + shutil.copytree(HERE, research) + pinned = tmp_path / "research" / "mutable-source-shear-cost" + pinned.mkdir(parents=True) + src = ROOT / "research" / "mutable-source-shear-cost" / "CERTIFICATE.json" + (pinned / "CERTIFICATE.json").write_bytes(src.read_bytes() + b"\n") + proc = run([sys.executable, "-I", "-B", str(research / "verify.py")], cwd=tmp_path) + need(proc.returncode != 0, "source drift should fail") + + # 5) Independent checker. + proc = run([sys.executable, "-I", "-B", str(HERE / "independent.py")]) + need(proc.returncode == 0, proc.stderr + proc.stdout) + need("PASS_INDEPENDENT_PARTITIONED_WALKS_7Q" in proc.stdout, proc.stdout) + + # 6) Duplicate JSON key rejection. + with tempfile.TemporaryDirectory() as tmp: + tmp_path = Path(tmp) + research = tmp_path / "research" / PKG_NAME + shutil.copytree(HERE, research) + pinned = tmp_path / "research" / "mutable-source-shear-cost" + pinned.mkdir(parents=True) + shutil.copy2( + ROOT / "research" / "mutable-source-shear-cost" / "CERTIFICATE.json", + pinned / "CERTIFICATE.json", + ) + cert = research / "CERTIFICATE.json" + raw = cert.read_text(encoding="utf-8") + corrupted = raw.replace( + '"schema_version": 1,', + '"schema_version": 1,\n "schema_version": 2,', + 1, + ) + need(corrupted != raw, "failed to inject duplicate key") + cert.write_text(corrupted, encoding="utf-8") + proc = run([sys.executable, "-I", "-B", str(research / "verify.py")], cwd=tmp_path) + need(proc.returncode != 0, "duplicate JSON key should fail") + + print("PASS_INDEPENDENT_WALKS_7Q_PACKAGE_TESTS groups=6") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/independent-walks-7q-obstruction/verify.py b/research/independent-walks-7q-obstruction/verify.py new file mode 100644 index 0000000000..4102e57d7d --- /dev/null +++ b/research/independent-walks-7q-obstruction/verify.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Partitioned independent-walks obstruction at Q=7; read-only default. + +Prepared by Wentao Li with substantial AI assistance. Apache-2.0. +""" +from __future__ import annotations + +import argparse +import hashlib +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from model import ( # noqa: E402 + EXPECTED, + champion_analysis, + dual_R_short_long, + dual_independent_R, + enumerate_partition_25, + enumerate_partition_34, + even_sum_standard_F2_4, + even_table, + length1_invalid_examples, + path_X, + structural_25_identity, + tariff_qrx, + valid_restored_walk, +) + +CERT_PATH = HERE / "CERTIFICATE.json" +SOURCES_PATH = HERE / "SOURCES.json" + + +def need(ok, message): + if not ok: + raise SystemExit(f"FAIL: {message}") + + +def sha256(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def load_json_reject_duplicates(path: Path): + text = path.read_text(encoding="utf-8") + + def _hook(pairs): + out = {} + for key, value in pairs: + if key in out: + raise ValueError(f"duplicate JSON key {key!r} in {path}") + out[key] = value + return out + + return json.loads(text, object_pairs_hook=_hook) + + +def check_source_pins(): + sources = load_json_reject_duplicates(SOURCES_PATH) + for rec in sources["files"]: + if rec["usage"] != "input": + continue + live = ROOT / rec["path"] + need(live.is_file(), f"missing input {rec['path']}") + need(sha256(live) == rec["sha256"], f"source bytes mismatch: {rec['path']}") + + +def build_certificate(): + need(even_sum_standard_F2_4() == 40, "F2^4 even-sum identity") + need(not valid_restored_walk((0,)), "length-1 invalid") + length1 = length1_invalid_examples() + + part25 = enumerate_partition_25() + need(part25["covering_pairs"] == EXPECTED["partition_25_covering"], "25 covering") + need(part25["min_R"] == EXPECTED["partition_25_min_R"], "25 min R") + need(part25["histogram"] == EXPECTED["partition_25_histogram"], "25 hist") + need(part25["structural_ok"] == part25["covering_pairs"], "25 structural") + need(part25["attainable_R"] == [112], "25 attainable") + + part34 = enumerate_partition_34() + need(part34["covering_pairs"] == EXPECTED["partition_34_covering"], "34 covering") + need(part34["min_R"] == EXPECTED["partition_34_min_R"], "34 min R") + need(part34["histogram"] == EXPECTED["partition_34_histogram"], "34 hist") + need(part34["attainable_R"] == [112], "34 attainable") + + champ = champion_analysis() + need(champ["tariff_floor_at_X0"] == EXPECTED["tariff_floor_at_X0"], "tariff floor") + need(champ["tariff_floor_at_X0"] > EXPECTED["endpoint_tariff_Q6"], "no undercut") + need(champ["champion_25"]["R"] == 112, "champ25 R") + need(champ["champion_34"]["R"] == 112, "champ34 R") + + # Explicit dual recomputation on champions (not copied from constant). + w25_a, w25_b = tuple(champ["champion_25"]["walks"][0]), tuple( + champ["champion_25"]["walks"][1] + ) + w34_a, w34_b = tuple(champ["champion_34"]["walks"][0]), tuple( + champ["champion_34"]["walks"][1] + ) + need(dual_R_short_long(even_table(w25_b), w25_a[1]) == 112, "recompute 25") + need( + dual_independent_R(even_table(w34_a), even_table(w34_b)) == 112, + "recompute 34", + ) + need(structural_25_identity(w25_a[1], w25_b)["R"] == 112, "recompute structural") + + # Same-walk baseline comparison: single even-subset floor is 82, not claimed here. + need(EXPECTED["single_walk_even_min_R"] == 82, "baseline even floor constant") + + cert = { + "schema_version": 1, + "status": "PASS_INDEPENDENT_WALKS_7Q_OBSTRUCTION", + "scope": ( + "Five-source common-B mutable-source Q/R/X alphabet (PR1898). " + "Partitioned independent dual walks at total Q=7 (valid restored " + "lengths (2,5) and (3,4)): covering dual even-parity readout has " + "exact R=112; tariff floor at X=0 is 490>436. Answers independent-" + "walks OQ (partitioned case) after same-walk multi-connector." + ), + "claim": { + "Q": 7, + "partition_covering_min_R": 112, + "partition_25_covering": part25["covering_pairs"], + "partition_34_covering": part34["covering_pairs"], + "partition_25_R_exact": 112, + "partition_34_R_exact": 112, + "tariff_floor_at_X0": EXPECTED["tariff_floor_at_X0"], + "endpoint_Q6_tariff": EXPECTED["endpoint_tariff_Q6"], + "undercuts_436_after_complete_bill": False, + "length1_walks_invalid": True, + "answers_independent_walks_partitioned": True, + "oq_answer": ( + "Every covering partitioned dual-walk schedule with total " + "query count Q=n0+n1=7 (valid restored walks of lengths (2,5) " + "or (3,4), distinct nonzero labels within each walk, " + "independent dirt, dual even-parity readout) has exact R=112. " + "At X=0 the abstract tariff is already 490>436; positive path " + "X only increases the bill. Length-1 components are not " + "restored (closed zero edge). Same-walk multi-connector remains " + "the pending mc7q package; transfer-coupled schedules are out " + "of scope here." + ), + "no_new_kappa": True, + }, + "partition_2_plus_5": part25, + "partition_3_plus_4": part34, + "champion": champ, + "length1_invalid_examples": length1, + "unit_tariff": {"b": 38, "a": 2, "x": 2}, + "tariff_check": { + "formula": "38*Q + 2*R + 2*X", + "at_R112_X0": tariff_qrx(7, 112, 0), + "champion_25": tariff_qrx( + 7, 112, champ["champion_25"]["path_X"] + ), + "champion_34": tariff_qrx( + 7, 112, champ["champion_34"]["path_X"] + ), + "endpoint_Q6": EXPECTED["endpoint_tariff_Q6"], + }, + } + return cert + + +def compare_certificate(live, pinned): + need(live["status"] == pinned["status"], "status") + need(live["claim"] == pinned["claim"], "claim drift") + need( + live["partition_2_plus_5"]["covering_pairs"] + == pinned["partition_2_plus_5"]["covering_pairs"], + "25 covering drift", + ) + need( + live["partition_3_plus_4"]["covering_pairs"] + == pinned["partition_3_plus_4"]["covering_pairs"], + "34 covering drift", + ) + need( + live["partition_2_plus_5"]["histogram"] + == pinned["partition_2_plus_5"]["histogram"], + "25 hist drift", + ) + need( + live["partition_3_plus_4"]["histogram"] + == pinned["partition_3_plus_4"]["histogram"], + "34 hist drift", + ) + need(live["tariff_check"] == pinned["tariff_check"], "tariff drift") + need(live["champion"]["tariff_floor_at_X0"] == pinned["champion"]["tariff_floor_at_X0"], "floor") + + +def main(argv=None): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument( + "--write-certificate", + action="store_true", + help="rewrite CERTIFICATE.json (maintenance only)", + ) + args = parser.parse_args(argv) + + check_source_pins() + live = build_certificate() + + if args.write_certificate: + CERT_PATH.write_text(json.dumps(live, indent=2) + "\n", encoding="utf-8") + print("WROTE_CERTIFICATE", CERT_PATH) + return 0 + + pinned = load_json_reject_duplicates(CERT_PATH) + compare_certificate(live, pinned) + claim = pinned["claim"] + print( + "PASS_INDEPENDENT_WALKS_7Q_OBSTRUCTION", + f"partition_min_R={claim['partition_covering_min_R']}", + f"covering_25={claim['partition_25_covering']}", + f"covering_34={claim['partition_34_covering']}", + f"tariff_floor={claim['tariff_floor_at_X0']}", + f"endpoint={claim['endpoint_Q6_tariff']}", + "no_undercut_partitioned_independent_walks", + "answers_independent_walks_partitioned", + "no_new_kappa", + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())