From b4e312f952aea55a0b9f013a1d152423f6cf0f56 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Thu, 15 Oct 2026 16:33:37 +0000 Subject: [PATCH] Research: transfer-coupled all-shapes 7q obstruction (no new kappa) Full (p,a,b) census at Q=7 closes the remaining-shapes follow-up after #2817 (5,1,1)-only and #2779 OQ1. Global min R=84 only at (5,1,1) with X>=2; all other shapes R>=86; tariff floor 439>436. Prepared by Wentao Li with substantial AI assistance. --- .../transfer-coupled-all-shapes-7q/.gitignore | 1 + .../CERTIFICATE.json | 632 ++++++++++++++++++ .../transfer-coupled-all-shapes-7q/NOTICE.md | 32 + .../transfer-coupled-all-shapes-7q/PROOF.md | 86 +++ .../transfer-coupled-all-shapes-7q/README.md | 81 +++ .../SOURCES.json | 24 + .../transfer-coupled-all-shapes-7q/TASK.json | 108 +++ .../VERIFY.json | 52 ++ .../transfer-coupled-all-shapes-7q/dual.c | 29 + .../dual_lib.py | 85 +++ .../independent.py | 283 ++++++++ .../transfer-coupled-all-shapes-7q/model.py | 428 ++++++++++++ .../test_package.py | 134 ++++ .../transfer-coupled-all-shapes-7q/verify.py | 245 +++++++ 14 files changed, 2220 insertions(+) create mode 100644 research/transfer-coupled-all-shapes-7q/.gitignore create mode 100644 research/transfer-coupled-all-shapes-7q/CERTIFICATE.json create mode 100644 research/transfer-coupled-all-shapes-7q/NOTICE.md create mode 100644 research/transfer-coupled-all-shapes-7q/PROOF.md create mode 100644 research/transfer-coupled-all-shapes-7q/README.md create mode 100644 research/transfer-coupled-all-shapes-7q/SOURCES.json create mode 100644 research/transfer-coupled-all-shapes-7q/TASK.json create mode 100644 research/transfer-coupled-all-shapes-7q/VERIFY.json create mode 100644 research/transfer-coupled-all-shapes-7q/dual.c create mode 100644 research/transfer-coupled-all-shapes-7q/dual_lib.py create mode 100644 research/transfer-coupled-all-shapes-7q/independent.py create mode 100644 research/transfer-coupled-all-shapes-7q/model.py create mode 100644 research/transfer-coupled-all-shapes-7q/test_package.py create mode 100644 research/transfer-coupled-all-shapes-7q/verify.py diff --git a/research/transfer-coupled-all-shapes-7q/.gitignore b/research/transfer-coupled-all-shapes-7q/.gitignore new file mode 100644 index 0000000000..35598e80e2 --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/.gitignore @@ -0,0 +1 @@ +dual.so diff --git a/research/transfer-coupled-all-shapes-7q/CERTIFICATE.json b/research/transfer-coupled-all-shapes-7q/CERTIFICATE.json new file mode 100644 index 0000000000..121f27bfc9 --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/CERTIFICATE.json @@ -0,0 +1,632 @@ +{ + "schema_version": 1, + "status": "PASS_TRANSFER_COUPLED_7Q_OBSTRUCTION", + "scope": "Five-source common-B mutable-source Q/R/X alphabet (PR1898). Transfer-coupled dual walks at total Q=p+a+b=7 with shared prefix length p, divergent suffixes a,b, transfer surcharge C>=1, independent dirt, dual even-parity readout, and fair shared-prefix XOR billing. Answers #2779 OQ1 (transfer-coupled).", + "claim": { + "Q": 7, + "transfer_C_min": 1, + "global_covering_min_R": 84, + "global_min_shape": [ + 5, + 1, + 1 + ], + "second_min_R": 86, + "second_min_shape": [ + 4, + 1, + 2 + ], + "x0_covering_on_511": 0, + "path_X_even": true, + "covering_implies_X_ge_2_on_critical": true, + "tariff_floor_after_complete_bill": 439, + "endpoint_Q6_tariff": 436, + "undercuts_436_after_complete_bill": false, + "answers_independent_walks_transfer_coupled": true, + "oq_answer": "Every covering transfer-coupled dual at Q=p+a+b=7 (distinct labels, disjoint private suffixes, independent dirt, dual even-parity) has min R >= 84, attained only at shape (5,1,1). All other unordered shapes have min R >= 86, already giving tariff >= 439 at X=0 with C=1. On (5,1,1), Gray X=0 covering is empty, and fair path X is always even, so covering forces X >= 2 and tariff >= 38*7 + 2*84 + 2*2 + 1 = 439 > 436. Partitioned independent walks (#2779) remain at R=112; same-walk even-subset remains at R=82.", + "no_new_kappa": true + }, + "x0_lemma_511": { + "prefix_paths": 300, + "covering": 0 + }, + "critical_5_1_1": { + "shape": [ + 5, + 1, + 1 + ], + "Q": 7, + "covering_pairs": 8749440, + "attainable_R": [ + 84, + 88, + 90 + ], + "histogram": { + "84": 1458240, + "88": 2083200, + "90": 5208000 + }, + "min_R": 84, + "champion": { + "prefix": [ + 0, + 4, + 8, + 15, + 18 + ], + "suf_a": [ + 1 + ], + "suf_b": [ + 2 + ], + "R": 84, + "walks": [ + [ + 0, + 4, + 8, + 15, + 18, + 1 + ], + [ + 0, + 4, + 8, + 15, + 18, + 2 + ] + ] + } + }, + "second_4_1_2": { + "shape": [ + 4, + 1, + 2 + ], + "Q": 7, + "covering_pairs": 34997760, + "attainable_R": [ + 86, + 88, + 90, + 92 + ], + "histogram": { + "86": 5832960, + "88": 3333120, + "90": 9999360, + "92": 15832320 + }, + "min_R": 86, + "champion": { + "prefix": [ + 0, + 1, + 2, + 7 + ], + "suf_a": [ + 8 + ], + "suf_b": [ + 12, + 16 + ], + "R": 86, + "walks": [ + [ + 0, + 1, + 2, + 7, + 8 + ], + [ + 0, + 1, + 2, + 7, + 12, + 16 + ] + ] + } + }, + "companion_shapes": { + "1_1_5": { + "shape": [ + 1, + 1, + 5 + ], + "Q": 7, + "covering_pairs": 3499776, + "attainable_R": [ + 92, + 96, + 104 + ], + "histogram": { + "92": 1416576, + "96": 833280, + "104": 1249920 + }, + "min_R": 92, + "champion": { + "prefix": [ + 0 + ], + "suf_a": [ + 1 + ], + "suf_b": [ + 2, + 4, + 7, + 8, + 16 + ], + "R": 92, + "walks": [ + [ + 0, + 1 + ], + [ + 0, + 2, + 4, + 7, + 8, + 16 + ] + ] + } + }, + "1_2_4": { + "shape": [ + 1, + 2, + 4 + ], + "Q": 7, + "covering_pairs": 8749440, + "attainable_R": [ + 98, + 104 + ], + "histogram": { + "98": 3124800, + "104": 5624640 + }, + "min_R": 98, + "champion": { + "prefix": [ + 0 + ], + "suf_a": [ + 1, + 2 + ], + "suf_b": [ + 4, + 8, + 13, + 16 + ], + "R": 98, + "walks": [ + [ + 0, + 1, + 2 + ], + [ + 0, + 4, + 8, + 13, + 16 + ] + ] + } + }, + "1_3_3": { + "shape": [ + 1, + 3, + 3 + ], + "Q": 7, + "covering_pairs": 5832960, + "attainable_R": [ + 100, + 104, + 112 + ], + "histogram": { + "100": 1805440, + "104": 3749760, + "112": 277760 + }, + "min_R": 100, + "champion": { + "prefix": [ + 0 + ], + "suf_a": [ + 1, + 2, + 4 + ], + "suf_b": [ + 7, + 8, + 16 + ], + "R": 100, + "walks": [ + [ + 0, + 1, + 2, + 4 + ], + [ + 0, + 7, + 8, + 16 + ] + ] + } + }, + "2_1_4": { + "shape": [ + 2, + 1, + 4 + ], + "Q": 7, + "covering_pairs": 17498880, + "attainable_R": [ + 90, + 92, + 96, + 100 + ], + "histogram": { + "90": 4583040, + "92": 4999680, + "96": 5416320, + "100": 2499840 + }, + "min_R": 90, + "champion": { + "prefix": [ + 0, + 1 + ], + "suf_a": [ + 2 + ], + "suf_b": [ + 4, + 8, + 14, + 16 + ], + "R": 90, + "walks": [ + [ + 0, + 1, + 2 + ], + [ + 0, + 1, + 4, + 8, + 14, + 16 + ] + ] + } + }, + "2_2_3": { + "shape": [ + 2, + 2, + 3 + ], + "Q": 7, + "covering_pairs": 34997760, + "attainable_R": [ + 94, + 96, + 100, + 104 + ], + "histogram": { + "94": 7499520, + "96": 17498880, + "100": 9166080, + "104": 833280 + }, + "min_R": 94, + "champion": { + "prefix": [ + 0, + 1 + ], + "suf_a": [ + 2, + 4 + ], + "suf_b": [ + 8, + 15, + 16 + ], + "R": 94, + "walks": [ + [ + 0, + 1, + 2, + 4 + ], + [ + 0, + 1, + 8, + 15, + 16 + ] + ] + } + }, + "3_1_3": { + "shape": [ + 3, + 1, + 3 + ], + "Q": 7, + "covering_pairs": 34997760, + "attainable_R": [ + 88, + 90, + 92, + 94, + 96 + ], + "histogram": { + "88": 6666240, + "90": 7499520, + "92": 7499520, + "94": 9999360, + "96": 3333120 + }, + "min_R": 88, + "champion": { + "prefix": [ + 0, + 1, + 2 + ], + "suf_a": [ + 4 + ], + "suf_b": [ + 8, + 15, + 16 + ], + "R": 88, + "walks": [ + [ + 0, + 1, + 2, + 4 + ], + [ + 0, + 1, + 2, + 8, + 15, + 16 + ] + ] + } + }, + "3_2_2": { + "shape": [ + 3, + 2, + 2 + ], + "Q": 7, + "covering_pairs": 26248320, + "attainable_R": [ + 90, + 92, + 94, + 96 + ], + "histogram": { + "90": 4374720, + "92": 8124480, + "94": 7499520, + "96": 6249600 + }, + "min_R": 90, + "champion": { + "prefix": [ + 0, + 1, + 2 + ], + "suf_a": [ + 4, + 8 + ], + "suf_b": [ + 15, + 16 + ], + "R": 90, + "walks": [ + [ + 0, + 1, + 2, + 4, + 8 + ], + [ + 0, + 1, + 2, + 15, + 16 + ] + ] + } + } + }, + "champions": { + "champions": [ + { + "shape": [ + 1, + 1, + 5 + ], + "R": 92, + "fair_X_sample": 12, + "tariff_at_X0_C1": 451, + "obstruction_tariff_floor": 451 + }, + { + "shape": [ + 1, + 2, + 4 + ], + "R": 98, + "fair_X_sample": 12, + "tariff_at_X0_C1": 463, + "obstruction_tariff_floor": 463 + }, + { + "shape": [ + 1, + 3, + 3 + ], + "R": 100, + "fair_X_sample": 16, + "tariff_at_X0_C1": 467, + "obstruction_tariff_floor": 467 + }, + { + "shape": [ + 2, + 1, + 4 + ], + "R": 90, + "fair_X_sample": 14, + "tariff_at_X0_C1": 447, + "obstruction_tariff_floor": 447 + }, + { + "shape": [ + 2, + 2, + 3 + ], + "R": 94, + "fair_X_sample": 18, + "tariff_at_X0_C1": 455, + "obstruction_tariff_floor": 455 + }, + { + "shape": [ + 3, + 1, + 3 + ], + "R": 88, + "fair_X_sample": 18, + "tariff_at_X0_C1": 443, + "obstruction_tariff_floor": 443 + }, + { + "shape": [ + 3, + 2, + 2 + ], + "R": 90, + "fair_X_sample": 18, + "tariff_at_X0_C1": 447, + "obstruction_tariff_floor": 447 + }, + { + "shape": [ + 4, + 1, + 2 + ], + "R": 86, + "fair_X_sample": 18, + "tariff_at_X0_C1": 439, + "obstruction_tariff_floor": 439 + }, + { + "shape": [ + 5, + 1, + 1 + ], + "R": 84, + "fair_X_sample": 16, + "tariff_at_X0_C1": 435, + "obstruction_tariff_floor": 439 + } + ], + "global_min_R": 84, + "global_min_shape": [ + 5, + 1, + 1 + ], + "tariff_floor_critical": 439, + "hypothetical_R84_X0_C1": 435, + "endpoint_Q6": 436 + }, + "unit_tariff": { + "b": 38, + "a": 2, + "x": 2, + "transfer_C": 1 + }, + "comparisons": { + "partitioned_independent_min_R": 112, + "same_walk_even_min_R": 82, + "hypothetical_R84_X0_C1": 435 + } +} diff --git a/research/transfer-coupled-all-shapes-7q/NOTICE.md b/research/transfer-coupled-all-shapes-7q/NOTICE.md new file mode 100644 index 0000000000..a82ae9d313 --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/NOTICE.md @@ -0,0 +1,32 @@ +# 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. +- Open #2761 `research/multi-connector-7q-obstruction` — same-walk + multi-connector / priced shadow; not edited. +- Open #2764 `research/dirty-parity-8q-obstruction` — Q=8 dirty-parity; not + edited. +- Open #2779 `research/independent-walks-7q-obstruction` — partitioned + independent walks; not edited. +- Pending `research/transfer-coupled-7q-obstruction` — maximal-share + `(5,1,1)` only; remaining-shapes OQ answered here; 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/transfer-coupled-all-shapes-7q/PROOF.md b/research/transfer-coupled-all-shapes-7q/PROOF.md new file mode 100644 index 0000000000..2ad7ed42eb --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/PROOF.md @@ -0,0 +1,86 @@ +# Transfer-coupled duals 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 +open question 1 of [#2779](https://github.com/CrocSwap/integer-mult-bounds/pull/2779) +and the remaining-shapes follow-up left by the maximal-share `(5,1,1)` package: +after a **transfer-coupled** dual (shared prefix, priced transfer `C≥1`, +divergent suffixes) and a complete dirty bill at total `Q=7`, can any unordered +shape `(p,a,b)` undercut the six-query endpoint tariff `436`? + +No new kappa is claimed. Leave-alone packages through #2779 and the pending +`(5,1,1)`-only transfer-coupled package are not edited. + +## Setup + +Retain queries `Q_j`, readouts `R_m: y_m += A_m z`, and paid source shears +`X_(s,t)`. A **transfer-coupled dual** of shape `(p,a,b)` with +`p+a+b=7` and `p,a,b≥1` consists of: + +- a shared prefix of `p` slots starting at `0` (queries charged once); +- two nonempty divergent suffixes of lengths `a` and `b` with labels disjoint + from the prefix and from each other; +- a transfer surcharge `C≥1` (fork cost); +- two restored walks `W0 = prefix∥suf_a` and `W1 = prefix∥suf_b` carrying + **independent** dirt; +- dual even-parity readout + `R = Σ_{m=1}^{31} min_a (e0[a] + e1[a⊕m])`. + +Fair shared-prefix XOR billing charges prefix-internal edges once and both +fork/suffix/return branches fully. Path costs are always even: +`X = 2·Σ(wt(δ)-1)`. + +The abstract complete-call tariff at `(b,a,x)=(38,2,2)` is +`38·Q + 2·R + 2·X + C`. + +## Census + +Up to swapping suffixes (`a≤b`) there are nine shapes. Distinct-label covering +duals were enumerated with an exact `min_a` dual (C helper, pure-Python +cross-check): + +| Shape | Covering | Min R | +|---|---:|---:| +| `(1,1,5)` | 3499776 | 92 | +| `(1,2,4)` | 8749440 | 98 | +| `(1,3,3)` | 5832960 | 100 | +| `(2,1,4)` | 17498880 | 90 | +| `(2,2,3)` | 34997760 | 94 | +| `(3,1,3)` | 34997760 | 88 | +| `(3,2,2)` | 26248320 | 90 | +| `(4,1,2)` | 34997760 | **86** | +| `(5,1,1)` | 8749440 | **84** | + +Global minimum is `R=84` at `(5,1,1)` only. Every other shape has `R≥86`. + +## X=0 lemma on the critical shape + +On `(5,1,1)`, `X=0` forces every fair-path edge to have Hamming weight 1. +Returns to `0` then force suffix labels in `{1,2,4,8,16}`. Enumerating all +distinct weight-1 prefix paths of length 4 from `0` (300 paths) and all +admissible suffix pairs yields **zero** covering duals. Since fair `X` is +always even, every covering `(5,1,1)` schedule has `X≥2`. + +## Tariff consequence + +- Critical shape: `38·7 + 2·84 + 2·2 + 1 = 439 > 436`. +- All other shapes: `R≥86` already gives `38·7 + 2·86 + 2·0 + 1 = 439 > 436` + at `X=0`. + +Hypothetical `R=84,X=0,C=1` would tariff `435<436`, but that schedule class is +empty. Positive path-`X` only increases the bill. Transfer-coupled duals +therefore cannot undercut the six-query endpoint under the PR1898 abstract +tariff after a complete dirty bill. + +By comparison, partitioned independent walks (#2779) sit at `R=112`, and +same-walk even-subset (#2686) at `R=82` with a single dirt port (no transfer). + +## Machine checks + +`verify.py` recomputes the critical `(5,1,1)` and second `(4,1,2)` censuses, +the X=0 Gray lemma, champions of every shape, and the tariff floor. +`independent.py` recomputes all companion-shape censuses with a separate dual +path and rechecks the critical champion in pure Python. Package tests cover +corruption, source-pin drift, duplicate JSON keys, and `-O`/`need()` smoke. + +Prepared by Wentao Li with substantial AI assistance. Apache-2.0. diff --git a/research/transfer-coupled-all-shapes-7q/README.md b/research/transfer-coupled-all-shapes-7q/README.md new file mode 100644 index 0000000000..43b2cc0d41 --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/README.md @@ -0,0 +1,81 @@ +# Transfer-coupled all-shapes dual obstruction at seven queries + +**Scoped obstruction / priced alphabet; no new kappa.** Completes the +transfer-coupled census across every unordered shape `(p,a,b)` with +`p+a+b=7`, answering open question 1 of +[#2779](https://github.com/CrocSwap/integer-mult-bounds/pull/2779) and the +remaining-shapes follow-up left by the maximal-share `(5,1,1)` package on the +five-source common-B mutable-source alphabet of +[#1898](https://github.com/CrocSwap/integer-mult-bounds/pull/1898): after a +priced transfer `C≥1` and fair shared-prefix XOR, can any transfer-coupled dual +undercut tariff `436`? + +| Shape `(p,a,b)` | Covering pairs | Exact min R | Tariff floor (C=1) | Undercuts 436? | +|---|---:|---:|---:|---| +| Same-walk even-subset (#2686) | — | ≥82 | ≥442 at X=6 | no | +| Partitioned dual (#2779) | — | ≥112 | ≥490 at X=0 | no | +| `(5,1,1)` transfer-coupled | **8749440** | **84** | **≥439** (X≥2) | **no** | +| `(4,1,2)` | **34997760** | **86** | **≥439** at X=0 | **no** | +| All other unordered shapes | — | **≥88** | **≥443** at X=0 | **no** | + +Global covering minimum is `R=84` at shape `(5,1,1)` only. Gray `X=0` covering +on that shape is empty, and fair path `X` is always even, so covering forces +`X≥2` and tariff `≥439>436`. Every other unordered shape already has `R≥86`, +hence tariff `≥439` even at `X=0`. + +## Reproduction + +```sh +python3.12 -I -B research/transfer-coupled-all-shapes-7q/verify.py +python3.12 -I -O -B research/transfer-coupled-all-shapes-7q/verify.py +python3.12 -I -B research/transfer-coupled-all-shapes-7q/independent.py +python3.12 -I -B research/transfer-coupled-all-shapes-7q/test_package.py +python3.12 -B scripts/research_package.py --package research/transfer-coupled-all-shapes-7q +``` + +Expected: + +```text +PASS_TRANSFER_COUPLED_7Q_OBSTRUCTION global_min_R=84 ... tariff_floor=439 ... answers_independent_walks_transfer_coupled no_new_kappa +PASS_INDEPENDENT_TRANSFER_COUPLED_7Q companions=7 ... tariff_floor=439 ... no_new_kappa +PASS_TRANSFER_COUPLED_7Q_PACKAGE_TESTS groups=6 +PASS_REGISTERED_RESEARCH_PACKAGE research/transfer-coupled-all-shapes-7q outcome=completed +``` + +Default verify is read-only. Admission uses `need()`; `-O` also passes. +Requires a working `gcc` to build the local `dual.c` helper (pure-Python dual +fallback remains available). + +## Overlap + +Base commit `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. Direct predecessors: +PR1898, #2643, #2686, #2715, #2761, #2779, and the pending `(5,1,1)`-only +transfer-coupled package (not edited; this package supplies the missing +full-shape census). Leave-alone through #2779 including #2764, #2761, #2715, +#2687, #2686, #2677, #2643, #2593, #2487 is respected; those packages are not +edited. Deferred shared-XOR soft-overlap and host screens are not opened. + +## Open next questions + +1. Do non-distinct (repeat-label) layers inside a transfer-coupled schedule + improve on `R=84` at `(5,1,1)`? + Why it matters: closes the one-repeat companion of the distinct-label layer. + First step: allow one repeated nonzero label in the length-6 walks of `(5,1,1)`. + Blocked by: larger search; expected to worsen coverage/cost. +2. Does priced transfer `C>1` (or a dirt-correlated shared-prefix bill) change + the `(5,1,1)` floor enough to reopen an undercut at `X=2`? + Why it matters: tests sensitivity of the 439 floor to transfer pricing. + First step: reprice the same covering census with `C=2` and correlated prefix dirt. + Blocked by: model choice; leave-alone dirty-shadow fixtures not reopened. + +## Credit + +Credit **Arham Tahir / PR1898**, **ywz65 / PR2455**, **PR1370**, fork **789q** / +**#2677**, **#2643**, **#2686**, **#2715**, **#2761**, **#2779**, the pending +`(5,1,1)`-only transfer-coupled package (remaining-shapes OQ answered here; 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/transfer-coupled-all-shapes-7q/SOURCES.json b/research/transfer-coupled-all-shapes-7q/SOURCES.json new file mode 100644 index 0000000000..719b378cbd --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/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/transfer-coupled-all-shapes-7q/TASK.json b/research/transfer-coupled-all-shapes-7q/TASK.json new file mode 100644 index 0000000000..a01be111af --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/TASK.json @@ -0,0 +1,108 @@ +{ + "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": "Full transfer-coupled dual census over every unordered shape (p,a,b) with p+a+b=7 in the PR1898 alphabet: shared prefix, divergent suffixes, transfer C>=1, independent dirt, dual even-parity, fair shared-prefix XOR. Prove every covering schedule tariffs at least 439>436 (global min R=84 only at (5,1,1) with X>=2; all other shapes R>=86), answering #2779 OQ1 and the remaining-shapes follow-up after the (5,1,1)-only package.", + "scope_change_reason": "The drawn connector-alphabet card is redirected to the remaining-shapes transfer-coupled census left open after #2779 and the maximal-share (5,1,1) package on the #1898 fixture, outside leave-alones.", + "bottleneck_link": "A priced transfer-coupled dual alphabet decides whether sharing a query prefix across two independently dirty connectors can undercut the six-query endpoint after charging the transfer.", + "budget_minutes": 60, + "stop_rule": "Stop after all unordered shapes (p,a,b) census, X=0 Gray lemma on (5,1,1), tariff floor 439, package tests; no host screens, no leave-alone edits, no shared-XOR reopen.", + "outcome": "completed", + "evidence": "CERTIFICATE.json global min R=84 at (5,1,1) with X0 covering=0; all other shapes min R>=86; tariff floor 439; independent companion census; corruption controls.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for derivation, implementation, checking and writing.", + "open_questions": [ + { + "question": "Do non-distinct (repeat-label) layers inside a transfer-coupled schedule improve on R=84 at (5,1,1)?", + "why_it_matters": "Closes the one-repeat companion of the Hamilton-style distinct-label layer.", + "first_step": "Allow one repeated nonzero label in the length-6 walks of (5,1,1) and recompute dual R.", + "blocked_by": "Larger search; expected to worsen coverage/cost." + }, + { + "question": "Does priced transfer C>1 (or a dirt-correlated shared-prefix bill) change the (5,1,1) floor enough to reopen an undercut at X=2?", + "why_it_matters": "Tests sensitivity of the 439 floor to the transfer pricing model.", + "first_step": "Reprice the same covering census with C=2 and with correlated prefix dirt.", + "blocked_by": "Model choice; leave-alone dirty-shadow fixtures not reopened." + } + ], + "predecessors": [ + { + "pr": 1898, + "credit": "Arham Tahir; minimum-query endpoint and abstract tariff fixture" + }, + { + "pr": 2779, + "credit": "Wentao Li; partitioned independent-walks; transfer-coupled OQ1" + }, + { + "pr": 2761, + "credit": "Wentao Li; multi-connector / priced-shadow same-walk" + }, + { + "pr": 2715, + "credit": "Wentao Li; cheaper-readout obstruction; independent-walks 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/transfer-coupled-all-shapes-7q/VERIFY.json b/research/transfer-coupled-all-shapes-7q/VERIFY.json new file mode 100644 index 0000000000..a36c6d0152 --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/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": 220, + "checks": "Critical (5,1,1) and second (4,1,2) dual census; X=0 Gray lemma; champions; tariff floor 439; certificate match; source pins" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 220, + "checks": "Same admission under PYTHONOPTIMIZE via need()" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 560, + "checks": "Separate companion-shape census (private dual path), X=0, critical champion, tariff arithmetic" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 200, + "checks": "Corruption rejection, duplicate JSON keys, -O controls, X0/tariff smoke" + } + ] +} diff --git a/research/transfer-coupled-all-shapes-7q/dual.c b/research/transfer-coupled-all-shapes-7q/dual.c new file mode 100644 index 0000000000..00906bc3a5 --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/dual.c @@ -0,0 +1,29 @@ +/* Dual even-parity cost Sigma_m min_a (e0[a] + e1[a xor m]). + * Returns -1 if some mask is uncovered. Wentao Li + AI. Apache-2.0. + */ +#define INF 99 + +long dual_sum(const int *e0, const int *e1) { + long total = 0; + for (int m = 1; m < 32; m++) { + int best = INF; + for (int a = 0; a < 32; a++) { + int c0 = e0[a]; + if (c0 >= INF) { + continue; + } + int c1 = e1[a ^ m]; + if (c1 < INF) { + int s = c0 + c1; + if (s < best) { + best = s; + } + } + } + if (best >= INF) { + return -1; + } + total += best; + } + return total; +} diff --git a/research/transfer-coupled-all-shapes-7q/dual_lib.py b/research/transfer-coupled-all-shapes-7q/dual_lib.py new file mode 100644 index 0000000000..5e524c70ad --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/dual_lib.py @@ -0,0 +1,85 @@ +"""Compile and load the dual_sum C helper (falls back to pure Python). + +Prepared by Wentao Li with substantial AI assistance. Apache-2.0. +""" +from __future__ import annotations + +import ctypes +import subprocess +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +INF = 99 + +_dual_c = None +_IntArr = ctypes.c_int * 32 + + +def _compile_dual(): + src = HERE / "dual.c" + # Place the shared object beside the package when the tree is writable; + # otherwise use a private temp path (read-only verify copies). + candidates = [HERE / "dual.so", Path(tempfile.gettempdir()) / "tc7q_dual.so"] + last_err = None + for so in candidates: + try: + subprocess.run( + ["gcc", "-O3", "-shared", "-fPIC", "-o", str(so), str(src)], + check=True, + capture_output=True, + text=True, + ) + lib = ctypes.CDLL(str(so)) + lib.dual_sum.argtypes = [ + ctypes.POINTER(ctypes.c_int), + ctypes.POINTER(ctypes.c_int), + ] + lib.dual_sum.restype = ctypes.c_long + return lib + except (OSError, subprocess.CalledProcessError) as exc: + last_err = exc + continue + raise RuntimeError(f"failed to build dual.so: {last_err}") + + +def get_dual_c(): + global _dual_c + if _dual_c is None: + _dual_c = _compile_dual() + return _dual_c + + +def dual_sum_c(e0, e1): + """Return dual R or None if uncovered.""" + lib = get_dual_c() + result = lib.dual_sum(_IntArr(*e0), _IntArr(*e1)) + if result < 0: + return None + return int(result) + + +def dual_sum_py(e0, e1): + total = 0 + for m in range(1, 32): + best = INF + for a in range(32): + c0 = e0[a] + if c0 >= INF: + continue + c1 = e1[a ^ m] + if c1 < INF: + cost = c0 + c1 + if cost < best: + best = cost + if best >= INF: + return None + total += best + return total + + +def dual_sum(e0, e1): + try: + return dual_sum_c(e0, e1) + except RuntimeError: + return dual_sum_py(e0, e1) diff --git a/research/transfer-coupled-all-shapes-7q/independent.py b/research/transfer-coupled-all-shapes-7q/independent.py new file mode 100644 index 0000000000..9c2f39b7b4 --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/independent.py @@ -0,0 +1,283 @@ +#!/usr/bin/env python3 +"""Independent transfer-coupled companion census at Q=7. + +Does not import model.py or verify.py. Uses the same dual.c formula via a +private ctypes load (or pure Python fallback). Prepared by Wentao Li with +substantial AI assistance. Apache-2.0. +""" +from __future__ import annotations + +import ctypes +import json +import subprocess +import tempfile +from collections import Counter +from itertools import combinations +from multiprocessing import Pool +from pathlib import Path + +HERE = Path(__file__).resolve().parent +CERT_PATH = HERE / "CERTIFICATE.json" +INF = 99 + +COMPANIONS = ( + (1, 1, 5), + (1, 2, 4), + (1, 3, 3), + (2, 1, 4), + (2, 2, 3), + (3, 1, 3), + (3, 2, 2), +) + +_SO = None +_SO_PATH = None +_IntArr = ctypes.c_int * 32 + + +def fail(message): + raise SystemExit(f"FAIL_INDEPENDENT: {message}") + + +def _compile_dual_so(): + global _SO_PATH + src = HERE / "dual.c" + so = Path(tempfile.gettempdir()) / "tc7q_independent_dual.so" + subprocess.run( + ["gcc", "-O3", "-shared", "-fPIC", "-o", str(so), str(src)], + check=True, + capture_output=True, + text=True, + ) + _SO_PATH = so + return so + + +def _attach_dual(so_path=None): + global _SO + path = Path(so_path) if so_path is not None else _compile_dual_so() + lib = ctypes.CDLL(str(path)) + lib.dual_sum.argtypes = [ + ctypes.POINTER(ctypes.c_int), + ctypes.POINTER(ctypes.c_int), + ] + lib.dual_sum.restype = ctypes.c_long + _SO = lib + return lib + + +def dual(e0, e1): + try: + lib = _SO if _SO is not None else _attach_dual() + result = lib.dual_sum(_IntArr(*e0), _IntArr(*e1)) + if result < 0: + return None + return int(result) + except (OSError, subprocess.CalledProcessError): + total = 0 + for m in range(1, 32): + best = INF + for a in range(32): + c0 = e0[a] + if c0 >= INF: + continue + c1 = e1[a ^ m] + if c1 < INF: + cost = c0 + c1 + if cost < best: + best = cost + if best >= INF: + return None + total += best + return total + + +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 tariff(q, r, x, c=1): + return 38 * q + 2 * r + 2 * x + c + + +def _chunk(args): + p, a, b, prefs = args + # Fresh dual load inside worker. + hist = Counter() + covering = 0 + min_r = None + for pn in prefs: + rem = [x for x in range(1, 32) if x not in pn] + pref = (0,) + tuple(pn) + Asets = list(combinations(rem, a)) + Atables = {A: even_table(pref + A) for A in Asets} + if a == b: + for i, A in enumerate(Asets): + sa = set(A) + ea = Atables[A] + for B in Asets[i + 1 :]: + if sa & set(B): + continue + r = dual(ea, Atables[B]) + if r is None: + continue + covering += 1 + hist[r] += 1 + if min_r is None or r < min_r: + min_r = r + else: + Bsets = list(combinations(rem, b)) + Btables = {B: even_table(pref + B) for B in Bsets} + for A, ea in Atables.items(): + sa = set(A) + for B, eb in Btables.items(): + if sa & set(B): + continue + r = dual(ea, eb) + if r is None: + continue + covering += 1 + hist[r] += 1 + if min_r is None or r < min_r: + min_r = r + return covering, hist, min_r + + +def _pool_init(so_path): + """Preload the shared dual library once per worker.""" + _attach_dual(so_path) + + +def census(p, a, b, workers=4): + prefs = list(combinations(range(1, 32), p - 1)) + chunks = [(p, a, b, prefs[i::workers]) for i in range(workers)] + so_path = _compile_dual_so() + with Pool(workers, initializer=_pool_init, initargs=(str(so_path),)) as pool: + parts = pool.map(_chunk, chunks) + hist = Counter() + covering = 0 + min_r = None + for cov, h, mr in parts: + covering += cov + hist.update(h) + if mr is not None and (min_r is None or mr < min_r): + min_r = mr + return covering, hist, min_r + + +def x0_covering_511(): + def nbrs(v): + return [v ^ (1 << i) for i in range(5)] + + paths = [(0,)] + for _ in range(4): + paths = [p + (w,) for p in paths for w in nbrs(p[-1]) if w not in p] + covering = 0 + for pref in paths: + end = pref[-1] + used = set(pref) + cands = [ + sa + for sa in (1, 2, 4, 8, 16) + if sa not in used and (end ^ sa).bit_count() == 1 + ] + for i, sa in enumerate(cands): + for sb in cands[i + 1 :]: + r = dual(even_table(pref + (sa,)), even_table(pref + (sb,))) + if r is not None: + covering += 1 + return covering + + +def dual_py_champ(e0, e1): + """Separate pure-Python dual for the critical champion cross-check.""" + 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 main(): + cert = json.loads(CERT_PATH.read_text(encoding="utf-8")) + claim = cert["claim"] + if claim["global_covering_min_R"] != 84: + fail("cert global min") + if claim["tariff_floor_after_complete_bill"] != 439: + fail("cert floor") + if claim["undercuts_436_after_complete_bill"] is not False: + fail("cert undercut flag") + + # Warm the dual helper for the X=0 lemma and champion check. + try: + _attach_dual(_compile_dual_so()) + except (OSError, subprocess.CalledProcessError): + pass + + x0 = x0_covering_511() + if x0 != 0: + fail(f"X0 covering {x0}") + + ch = cert["critical_5_1_1"]["champion"] + pref = tuple(ch["prefix"]) + sa = tuple(ch["suf_a"]) + sb = tuple(ch["suf_b"]) + r = dual_py_champ(even_table(pref + sa), even_table(pref + sb)) + if r != 84: + fail(f"critical champ R {r}") + + companions = cert.get("companion_shapes") or {} + for p, a, b in COMPANIONS: + key = f"{p}_{a}_{b}" + covering, hist, min_r = census(p, a, b) + pinned = companions.get(key) + if pinned is None: + fail(f"missing companion {key}") + if covering != pinned["covering_pairs"]: + fail(f"{key} covering {covering} != {pinned['covering_pairs']}") + if min_r != pinned["min_R"]: + fail(f"{key} min_R {min_r} != {pinned['min_R']}") + if {str(k): hist[k] for k in sorted(hist)} != pinned["histogram"]: + fail(f"{key} histogram drift") + if min_r < 86: + fail(f"{key} broke R>=86 companion floor") + + floor = tariff(7, 84, 2, 1) + if floor != 439 or floor <= 436: + fail(f"tariff floor {floor}") + if tariff(7, 86, 0, 1) != 439: + fail("R86 floor") + + print( + "PASS_INDEPENDENT_TRANSFER_COUPLED_7Q", + f"companions={len(COMPANIONS)}", + "critical_champ_R=84", + "x0_covering=0", + "tariff_floor=439", + "answers_independent_walks_transfer_coupled", + "no_new_kappa", + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/transfer-coupled-all-shapes-7q/model.py b/research/transfer-coupled-all-shapes-7q/model.py new file mode 100644 index 0000000000..01760fea48 --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/model.py @@ -0,0 +1,428 @@ +"""Transfer-coupled dual readout at seven queries. + +Answers open question 1 of #2779 (partitioned independent-walks package): 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? + +Self-contained relative to PR1898 / #2643 / #2686 / #2715 / #2761 / #2779. +Leave-alones are not edited. Prepared by Wentao Li with substantial AI +assistance. Apache-2.0. +""" +from __future__ import annotations + +from collections import Counter +from itertools import combinations +from multiprocessing import Pool + +from dual_lib import INF, dual_sum + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +# Unordered shapes (p,a,b) with p+a+b=7, p,a,b>=1, a<=b. +SHAPES = ( + (1, 1, 5), + (1, 2, 4), + (1, 3, 3), + (2, 1, 4), + (2, 2, 3), + (3, 1, 3), + (3, 2, 2), + (4, 1, 2), + (5, 1, 1), +) + +EXPECTED = { + "shapes": { + "1_1_5": { + "covering": 3499776, + "min_R": 92, + "histogram": {"92": 1416576, "96": 833280, "104": 1249920}, + "champion": {"prefix": [0], "suf_a": [1], "suf_b": [2, 4, 7, 8, 16], "R": 92}, + }, + "1_2_4": { + "covering": 8749440, + "min_R": 98, + "histogram": {"98": 3124800, "104": 5624640}, + "champion": {"prefix": [0], "suf_a": [1, 2], "suf_b": [4, 8, 13, 16], "R": 98}, + }, + "1_3_3": { + "covering": 5832960, + "min_R": 100, + "histogram": {"100": 1805440, "104": 3749760, "112": 277760}, + "champion": {"prefix": [0], "suf_a": [1, 2, 4], "suf_b": [7, 8, 16], "R": 100}, + }, + "2_1_4": { + "covering": 17498880, + "min_R": 90, + "histogram": {"90": 4583040, "92": 4999680, "96": 5416320, "100": 2499840}, + "champion": {"prefix": [0, 1], "suf_a": [2], "suf_b": [4, 8, 14, 16], "R": 90}, + }, + "2_2_3": { + "covering": 34997760, + "min_R": 94, + "histogram": {"94": 7499520, "96": 17498880, "100": 9166080, "104": 833280}, + "champion": {"prefix": [0, 1], "suf_a": [2, 4], "suf_b": [8, 15, 16], "R": 94}, + }, + "3_1_3": { + "covering": 34997760, + "min_R": 88, + "histogram": {"88": 6666240, "90": 7499520, "92": 7499520, "94": 9999360, "96": 3333120}, + "champion": {"prefix": [0, 1, 2], "suf_a": [4], "suf_b": [8, 15, 16], "R": 88}, + }, + "3_2_2": { + "covering": 26248320, + "min_R": 90, + "histogram": {"90": 4374720, "92": 8124480, "94": 7499520, "96": 6249600}, + "champion": {"prefix": [0, 1, 2], "suf_a": [4, 8], "suf_b": [15, 16], "R": 90}, + }, + "4_1_2": { + "covering": 34997760, + "min_R": 86, + "histogram": {"86": 5832960, "88": 3333120, "90": 9999360, "92": 15832320}, + "champion": {"prefix": [0, 1, 2, 7], "suf_a": [8], "suf_b": [12, 16], "R": 86}, + }, + "5_1_1": { + "covering": 8749440, + "min_R": 84, + "histogram": {"84": 1458240, "88": 2083200, "90": 5208000}, + "champion": {"prefix": [0, 4, 8, 15, 18], "suf_a": [1], "suf_b": [2], "R": 84}, + }, + }, + "global_min_R": 84, + "global_min_shape": (5, 1, 1), + "second_min_R": 86, + "second_min_shape": (4, 1, 2), + "x0_covering_511": 0, + "min_even_path_X_for_covering": 2, + "transfer_C": 1, + "endpoint_tariff_Q6": 436, + "tariff_floor_critical": 439, + "partitioned_min_R": 112, + "same_walk_even_min_R": 82, +} + + +def shape_key(p, a, b): + return f"{p}_{a}_{b}" + + +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): + 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 path_edge_cost(a, b): + delta = a ^ b + if delta == 0: + return None + return 2 * (delta.bit_count() - 1) + + +def fair_path_X(prefix, suf_a, suf_b): + """Fair shared-prefix XOR: prefix internals once; both forks+suffixes+returns.""" + need(prefix and prefix[0] == 0, "prefix starts at 0") + need(suf_a and suf_b, "divergent suffixes nonempty") + total = 0 + for u, v in zip(prefix, prefix[1:]): + cost = path_edge_cost(u, v) + if cost is None: + return None + total += cost + for suf in (suf_a, suf_b): + seq = (prefix[-1],) + tuple(suf) + (0,) + for u, v in zip(seq, seq[1:]): + cost = path_edge_cost(u, v) + if cost is None: + return None + total += cost + return total + + +def walk_slots(prefix, suf): + return tuple(prefix) + tuple(suf) + + +def dual_R_from_walks(w0, w1): + return dual_sum(even_table(w0), even_table(w1)) + + +def _census_chunk(args): + """Worker: census one chunk of prefix nonzero tuples for shape (p,a,b).""" + p, a, b, pref_nz_chunk = args + # Local imports for spawn contexts. + from collections import Counter as _Counter + from dual_lib import dual_sum as _dual + from itertools import combinations as _comb + + def _even(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 + + hist = _Counter() + covering = 0 + min_r = None + champ = None + for pn in pref_nz_chunk: + used = set(pn) + rem = [x for x in range(1, 32) if x not in used] + pref = (0,) + tuple(pn) + Asets = list(_comb(rem, a)) + Atables = {A: _even(pref + A) for A in Asets} + if a == b: + for i, A in enumerate(Asets): + sa = set(A) + ea = Atables[A] + for B in Asets[i + 1 :]: + if sa & set(B): + continue + r = _dual(ea, Atables[B]) + if r is None: + continue + covering += 1 + hist[r] += 1 + if min_r is None or r < min_r: + min_r = r + champ = (pref, A, B, r) + else: + Bsets = list(_comb(rem, b)) + Btables = {B: _even(pref + B) for B in Bsets} + for A, ea in Atables.items(): + sa = set(A) + for B, eb in Btables.items(): + if sa & set(B): + continue + r = _dual(ea, eb) + if r is None: + continue + covering += 1 + hist[r] += 1 + if min_r is None or r < min_r: + min_r = r + champ = (pref, A, B, r) + return covering, hist, min_r, champ + + +def _census_511_chunk(chunk): + from collections import Counter as _Counter + from dual_lib import dual_sum as _dual + from itertools import combinations as _comb + + def _even(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 + + hist = _Counter() + covering = 0 + min_r = None + champ = None + for six in chunk: + for priv in _comb(six, 2): + shared = tuple(sorted(set(six) - set(priv))) + sa, sb = priv + pref = (0,) + shared + r = _dual(_even(pref + (sa,)), _even(pref + (sb,))) + if r is None: + continue + covering += 1 + hist[r] += 1 + if min_r is None or r < min_r: + min_r = r + champ = (pref, (sa,), (sb,), r) + return covering, hist, min_r, champ + + +def census_shape(p, a, b, workers=4): + """Distinct-label transfer-coupled census for shape (p,a,b).""" + need(p + a + b == 7 and min(p, a, b) >= 1, "shape must partition 7") + need(a <= b, "normalize a<=b") + if (p, a, b) == (5, 1, 1): + sixes = list(combinations(range(1, 32), 6)) + chunks = [sixes[i::workers] for i in range(workers)] + with Pool(workers) as pool: + parts = pool.map(_census_511_chunk, chunks) + else: + prefs = list(combinations(range(1, 32), p - 1)) + chunks = [prefs[i::workers] for i in range(workers)] + args = [(p, a, b, ch) for ch in chunks if ch] + with Pool(workers) as pool: + parts = pool.map(_census_chunk, args) + hist = Counter() + covering = 0 + min_r = None + champ = None + for cov, h, mr, ch in parts: + covering += cov + hist.update(h) + if mr is not None and (min_r is None or mr < min_r): + min_r = mr + champ = ch + need(covering > 0 and min_r is not None, f"no covering for {(p,a,b)}") + pref, sa, sb, r = champ + return { + "shape": (p, a, b), + "Q": 7, + "covering_pairs": covering, + "attainable_R": sorted(hist), + "histogram": {str(k): hist[k] for k in sorted(hist)}, + "min_R": min_r, + "champion": { + "prefix": list(pref), + "suf_a": list(sa), + "suf_b": list(sb), + "R": r, + "walks": [list(walk_slots(pref, sa)), list(walk_slots(pref, sb))], + }, + } + + +def nbrs5(v): + return [v ^ (1 << i) for i in range(5)] + + +def x0_covering_count_511(): + """Exhaustive Gray (wt-1 edges) covering count for shape (5,1,1). + + X=0 forces every fair-path edge to have Hamming weight 1. Returns to 0 then + force suffix labels in {1,2,4,8,16}. Enumerating all distinct wt-1 prefix + paths of length 4 from 0 and all admissible suffix pairs yields zero + covering duals. + """ + paths = [(0,)] + for _ in range(4): + paths = [p + (w,) for p in paths for w in nbrs5(p[-1]) if w not in p] + covering = 0 + for pref in paths: + end = pref[-1] + used = set(pref) + cands = [ + sa + for sa in (1, 2, 4, 8, 16) + if sa not in used and (end ^ sa).bit_count() == 1 + ] + for i, sa in enumerate(cands): + for sb in cands[i + 1 :]: + r = dual_R_from_walks(pref + (sa,), pref + (sb,)) + if r is None: + continue + covering += 1 + # Fair X is 0 by construction of the Gray edges. + need(fair_path_X(pref, (sa,), (sb,)) == 0, "Gray path must have X=0") + return {"prefix_paths": len(paths), "covering": covering} + + +def champion_checks(): + """Recompute dual R on every pinned champion; check tariff floors.""" + rows = [] + global_min = None + for p, a, b in SHAPES: + key = shape_key(p, a, b) + exp = EXPECTED["shapes"][key] + ch = exp["champion"] + pref = tuple(ch["prefix"]) + sa = tuple(ch["suf_a"]) + sb = tuple(ch["suf_b"]) + need(len(pref) == p and len(sa) == a and len(sb) == b, "champion shape") + need(pref[0] == 0, "champion prefix") + need(set(sa).isdisjoint(pref) and set(sb).isdisjoint(pref), "disjoint") + need(set(sa).isdisjoint(sb), "divergent private labels") + r = dual_R_from_walks(walk_slots(pref, sa), walk_slots(pref, sb)) + need(r == ch["R"] == exp["min_R"], f"champion R mismatch {key}") + x = fair_path_X(pref, sa, sb) + need(x is not None and x % 2 == 0, "fair X even") + t0 = tariff_qrx(7, r, 0, EXPECTED["transfer_C"]) + t_floor = tariff_qrx(7, r, 0 if r >= 86 else 2, EXPECTED["transfer_C"]) + rows.append( + { + "shape": [p, a, b], + "R": r, + "fair_X_sample": x, + "tariff_at_X0_C1": t0, + "obstruction_tariff_floor": t_floor, + } + ) + if global_min is None or r < global_min[0]: + global_min = (r, (p, a, b)) + need(global_min[0] == EXPECTED["global_min_R"], "global min R") + need(global_min[1] == EXPECTED["global_min_shape"], "global min shape") + # Critical: R=84 needs X>=2; R>=86 already safe at X=0. + crit = tariff_qrx(7, 84, 2, 1) + safe86 = tariff_qrx(7, 86, 0, 1) + need(crit == EXPECTED["tariff_floor_critical"], "critical floor") + need(safe86 == EXPECTED["tariff_floor_critical"], "86 floor") + need(crit > EXPECTED["endpoint_tariff_Q6"], "no undercut") + need(safe86 > EXPECTED["endpoint_tariff_Q6"], "no undercut at 86") + # Hypothetical illegal X=0 at R=84 would undercut — excluded by X lemma. + hypo = tariff_qrx(7, 84, 0, 1) + need(hypo == 435, "hypo arithmetic") + need(hypo < EXPECTED["endpoint_tariff_Q6"], "hypo would undercut if X=0 legal") + return { + "champions": rows, + "global_min_R": global_min[0], + "global_min_shape": list(global_min[1]), + "tariff_floor_critical": crit, + "hypothetical_R84_X0_C1": hypo, + "endpoint_Q6": EXPECTED["endpoint_tariff_Q6"], + } + + +def census_all_shapes(workers=4, shapes=None): + shapes = list(shapes) if shapes is not None else list(SHAPES) + out = {} + for p, a, b in shapes: + key = shape_key(p, a, b) + result = census_shape(p, a, b, workers=workers) + exp = EXPECTED["shapes"][key] + need(result["covering_pairs"] == exp["covering"], f"{key} covering") + need(result["min_R"] == exp["min_R"], f"{key} min R") + need(result["histogram"] == exp["histogram"], f"{key} hist") + out[key] = result + return out diff --git a/research/transfer-coupled-all-shapes-7q/test_package.py b/research/transfer-coupled-all-shapes-7q/test_package.py new file mode 100644 index 0000000000..f21222d151 --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/test_package.py @@ -0,0 +1,134 @@ +#!/usr/bin/env python3 +"""Package fault controls for transfer-coupled 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 = "transfer-coupled-all-shapes-7q" + + +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 seed_tree(tmp_path: Path): + 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", + ) + return research + + +def main(): + # 1) X=0 lemma + tariff arithmetic smoke (fast; full census is verify/independent). + proc = run( + [ + sys.executable, + "-I", + "-B", + "-c", + "import sys; sys.path.insert(0, %r); from model import x0_covering_count_511, tariff_qrx, need, champion_checks; " + "x=x0_covering_count_511(); need(x['covering']==0,'x0'); " + "need(tariff_qrx(7,84,2,1)==439,'floor'); " + "need(tariff_qrx(7,86,0,1)==439,'floor86'); " + "champion_checks(); print('PASS_SMOKE_X0_TARIFF_CHAMPIONS')" + % str(HERE), + ] + ) + need(proc.returncode == 0, proc.stderr + proc.stdout) + need("PASS_SMOKE_X0_TARIFF_CHAMPIONS" in proc.stdout, proc.stdout) + + # 2) Same smoke under -O (need() admission). + proc = run( + [ + sys.executable, + "-I", + "-O", + "-B", + "-c", + "import sys; sys.path.insert(0, %r); from model import x0_covering_count_511, tariff_qrx, need, champion_checks; " + "x=x0_covering_count_511(); need(x['covering']==0,'x0'); " + "need(tariff_qrx(7,84,2,1)==439,'floor'); " + "champion_checks(); print('PASS_SMOKE_O_NEED')" + % str(HERE), + ] + ) + need(proc.returncode == 0, proc.stderr + proc.stdout) + need("PASS_SMOKE_O_NEED" in proc.stdout, proc.stdout) + + # 3) Certificate claim corruption fails against live census. + with tempfile.TemporaryDirectory() as tmp: + research = seed_tree(Path(tmp)) + cert = research / "CERTIFICATE.json" + data = json.loads(cert.read_text(encoding="utf-8")) + data["claim"]["global_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) + 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) Duplicate JSON key rejection. + with tempfile.TemporaryDirectory() as tmp: + research = seed_tree(Path(tmp)) + 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) + need(proc.returncode != 0, "duplicate JSON key should fail") + + # 6) Independent tariff helper matches the abstract invoice. + proc = run( + [ + sys.executable, + "-I", + "-B", + "-c", + "def tariff(q,r,x,c=1): return 38*q+2*r+2*x+c\n" + "assert tariff(7,84,2,1)==439\n" + "assert tariff(7,86,0,1)==439\n" + "assert tariff(7,84,0,1)==435\n" + "print('PASS_INDEPENDENT_TARIFF_FN')", + ] + ) + need(proc.returncode == 0, proc.stderr + proc.stdout) + need("PASS_INDEPENDENT_TARIFF_FN" in proc.stdout, proc.stdout) + + print("PASS_TRANSFER_COUPLED_7Q_PACKAGE_TESTS groups=6") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/transfer-coupled-all-shapes-7q/verify.py b/research/transfer-coupled-all-shapes-7q/verify.py new file mode 100644 index 0000000000..b390e98b67 --- /dev/null +++ b/research/transfer-coupled-all-shapes-7q/verify.py @@ -0,0 +1,245 @@ +#!/usr/bin/env python3 +"""Transfer-coupled dual 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, + SHAPES, + census_all_shapes, + census_shape, + champion_checks, + dual_R_from_walks, + fair_path_X, + need, + shape_key, + tariff_qrx, + walk_slots, + x0_covering_count_511, +) + +CERT_PATH = HERE / "CERTIFICATE.json" +SOURCES_PATH = HERE / "SOURCES.json" + + +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(include_companions: bool): + x0 = x0_covering_count_511() + need(x0["covering"] == EXPECTED["x0_covering_511"], "X=0 covering must be 0") + + champs = champion_checks() + + crit = census_shape(5, 1, 1) + need(crit["min_R"] == 84, "critical min R") + need(crit["covering_pairs"] == EXPECTED["shapes"]["5_1_1"]["covering"], "511 cov") + need(crit["histogram"] == EXPECTED["shapes"]["5_1_1"]["histogram"], "511 hist") + + second = census_shape(4, 1, 2) + need(second["min_R"] == 86, "second min R") + need(second["covering_pairs"] == EXPECTED["shapes"]["4_1_2"]["covering"], "412 cov") + need(second["histogram"] == EXPECTED["shapes"]["4_1_2"]["histogram"], "412 hist") + + companions = None + if include_companions: + rest = [s for s in SHAPES if s not in ((5, 1, 1), (4, 1, 2))] + companions = census_all_shapes(shapes=rest) + for p, a, b in rest: + key = shape_key(p, a, b) + need(companions[key]["min_R"] == EXPECTED["shapes"][key]["min_R"], key) + + need(EXPECTED["min_even_path_X_for_covering"] == 2, "even X step") + floor = tariff_qrx(7, 84, 2, 1) + need(floor == 439, "floor 439") + need(floor > 436, "no undercut") + need(tariff_qrx(7, 86, 0, 1) == 439, "R86 floor") + + ch = EXPECTED["shapes"]["5_1_1"]["champion"] + pref = tuple(ch["prefix"]) + sa = tuple(ch["suf_a"]) + sb = tuple(ch["suf_b"]) + need(dual_R_from_walks(walk_slots(pref, sa), walk_slots(pref, sb)) == 84, "recompute") + need(fair_path_X(pref, sa, sb) is not None, "fair X defined") + + return { + "schema_version": 1, + "status": "PASS_TRANSFER_COUPLED_7Q_OBSTRUCTION", + "scope": ( + "Five-source common-B mutable-source Q/R/X alphabet (PR1898). " + "Transfer-coupled dual walks at total Q=p+a+b=7 with shared prefix " + "length p, divergent suffixes a,b, transfer surcharge C>=1, " + "independent dirt, dual even-parity readout, and fair shared-prefix " + "XOR billing. Answers #2779 OQ1 (transfer-coupled)." + ), + "claim": { + "Q": 7, + "transfer_C_min": 1, + "global_covering_min_R": 84, + "global_min_shape": [5, 1, 1], + "second_min_R": 86, + "second_min_shape": [4, 1, 2], + "x0_covering_on_511": 0, + "path_X_even": True, + "covering_implies_X_ge_2_on_critical": True, + "tariff_floor_after_complete_bill": 439, + "endpoint_Q6_tariff": 436, + "undercuts_436_after_complete_bill": False, + "answers_independent_walks_transfer_coupled": True, + "oq_answer": ( + "Every covering transfer-coupled dual at Q=p+a+b=7 (distinct " + "labels, disjoint private suffixes, independent dirt, dual " + "even-parity) has min R >= 84, attained only at shape (5,1,1). " + "All other unordered shapes have min R >= 86, already giving " + "tariff >= 439 at X=0 with C=1. On (5,1,1), Gray X=0 covering " + "is empty, and fair path X is always even, so covering forces " + "X >= 2 and tariff >= 38*7 + 2*84 + 2*2 + 1 = 439 > 436. " + "Partitioned independent walks (#2779) remain at R=112; " + "same-walk even-subset remains at R=82." + ), + "no_new_kappa": True, + }, + "x0_lemma_511": x0, + "critical_5_1_1": crit, + "second_4_1_2": second, + "companion_shapes": companions, + "champions": champs, + "unit_tariff": {"b": 38, "a": 2, "x": 2, "transfer_C": 1}, + "comparisons": { + "partitioned_independent_min_R": EXPECTED["partitioned_min_R"], + "same_walk_even_min_R": EXPECTED["same_walk_even_min_R"], + "hypothetical_R84_X0_C1": 435, + }, + } + + +def main(argv=None): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument( + "--write", + action="store_true", + help="rewrite CERTIFICATE.json (authoring; use with --full once)", + ) + ap.add_argument( + "--full", + action="store_true", + help="also census companion shapes (authoring / optional)", + ) + ap.add_argument( + "--quick", + action="store_true", + help="alias for default admission (critical+second only)", + ) + args = ap.parse_args(argv) + + check_source_pins() + include_companions = bool(args.full) or bool(args.write) + pinned = None + if not args.write: + # Fail-fast on pinned claim / structure before the multi-minute census. + pinned = load_json_reject_duplicates(CERT_PATH) + need(pinned.get("status") == "PASS_TRANSFER_COUPLED_7Q_OBSTRUCTION", "status") + need(pinned["claim"]["global_covering_min_R"] == 84, "pinned global min R") + need(pinned["claim"]["tariff_floor_after_complete_bill"] == 439, "pinned floor") + need(pinned["claim"]["undercuts_436_after_complete_bill"] is False, "no undercut") + need(pinned["claim"]["no_new_kappa"] is True, "no new kappa") + need(pinned["x0_lemma_511"]["covering"] == 0, "pinned X0") + need(pinned["critical_5_1_1"]["min_R"] == 84, "pinned 511") + need(pinned["second_4_1_2"]["min_R"] == 86, "pinned 412") + need(isinstance(pinned.get("companion_shapes"), dict), "pinned companions present") + for p, a, b in SHAPES: + if (p, a, b) in ((5, 1, 1), (4, 1, 2)): + continue + key = shape_key(p, a, b) + need(key in pinned["companion_shapes"], f"missing pinned {key}") + need( + pinned["companion_shapes"][key]["min_R"] + == EXPECTED["shapes"][key]["min_R"], + f"pinned {key} min", + ) + + cert = build_certificate(include_companions=include_companions) + + if args.write: + CERT_PATH.write_text(json.dumps(cert, indent=2) + "\n", encoding="utf-8") + pinned = load_json_reject_duplicates(CERT_PATH) + + need(pinned is not None, "certificate missing") + + need(pinned["status"] == cert["status"], "certificate status") + need( + pinned["critical_5_1_1"]["covering_pairs"] + == cert["critical_5_1_1"]["covering_pairs"], + "511 cov match", + ) + need( + pinned["second_4_1_2"]["covering_pairs"] + == cert["second_4_1_2"]["covering_pairs"], + "412 cov match", + ) + if include_companions: + for p, a, b in SHAPES: + if (p, a, b) in ((5, 1, 1), (4, 1, 2)): + continue + key = shape_key(p, a, b) + need( + pinned["companion_shapes"][key]["min_R"] + == cert["companion_shapes"][key]["min_R"], + f"live {key}", + ) + need( + pinned["companion_shapes"][key]["covering_pairs"] + == cert["companion_shapes"][key]["covering_pairs"], + f"live {key} cov", + ) + + print( + "PASS_TRANSFER_COUPLED_7Q_OBSTRUCTION", + f"global_min_R={cert['claim']['global_covering_min_R']}", + f"shape={tuple(cert['claim']['global_min_shape'])}", + f"tariff_floor={cert['claim']['tariff_floor_after_complete_bill']}", + "x0_covering=0", + "answers_independent_walks_transfer_coupled", + "no_new_kappa", + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())