Research: 7–9Q mutable-source invoices cannot beat six-query tariff 436

research/mutable-source-789q-invoice/CERTIFICATE.json

@@ -0,0 +1,132 @@
+{
+  "schema_version": 1,
+  "status": "PASS_MUTABLE_SOURCE_789Q_INVOICE",
+  "scope": "Path-lowered even-subset schedules on connector prefixes for the five-source common-B mutable-source connector; complete-call tariff (b,a,x)=(38,2,2) from PR1898.",
+  "comparators": {
+    "six_query_endpoint": {
+      "Q": 6,
+      "R": 96,
+      "X": 8,
+      "map_leaves": 264,
+      "echo_nodes": 54,
+      "root_dispatches": 110,
+      "borrowed_dirty_rows": 4,
+      "tariff": 436,
+      "complete_prices": {
+        "b": 38,
+        "a": 2,
+        "x": 2
+      }
+    },
+    "ten_query_four_X": {
+      "Q": 10,
+      "R": 62,
+      "X": 4,
+      "map_leaves": 342,
+      "echo_nodes": 90,
+      "root_dispatches": 76,
+      "borrowed_dirty_rows": 4,
+      "tariff": 512,
+      "complete_prices": {
+        "b": 38,
+        "a": 2,
+        "x": 2
+      }
+    }
+  },
+  "Q7": {
+    "R_spectrum_distinct_slots": {
+      "covering_sets": 583296,
+      "attainable_R": [
+        82,
+        88
+      ],
+      "histogram": {
+        "82": 97216,
+        "88": 486080
+      },
+      "intermediate_R_83_to_87_count": 0,
+      "argument": "Exhaustive even-subset R over all C(31,6) distinct nonzero 6-slot sets; covering sets attain only R in {82,88}. Under tariff 38Q+2R+2X, beating 436 requires R+X<85, so excluded intermediate R in {83..87} with low X cannot undercut; R=88 forces tariff>=442 even at X=0."
+    },
+    "min_R_distinct_slots": {
+      "min_R": 82,
+      "witness_count": 97216,
+      "first_witness": [
+        0,
+        1,
+        2,
+        4,
+        8,
+        15,
+        16
+      ]
+    },
+    "min_X_among_min_R": {
+      "target_R": 82,
+      "covering_sets": 97216,
+      "min_X": 6,
+      "sets_with_X_eq_6": 14595,
+      "sets_with_X_below_6": 0,
+      "champion_path": [
+        0,
+        1,
+        2,
+        6,
+        12,
+        24,
+        16,
+        0
+      ]
+    },
+    "tariff_floor_from_spectrum": {
+      "beat_436_requires_R_plus_X_lt": 85,
+      "exact_min_requires_R_plus_X_ge": 88,
+      "R82_min_X": 6,
+      "R82_tariff_floor": 442,
+      "R88_X_ge_0_tariff_floor": 442,
+      "min_tariff": 442
+    },
+    "champion_invoice": {
+      "Q": 7,
+      "R": 82,
+      "X": 6,
+      "map_leaves": 278,
+      "echo_nodes": 63,
+      "root_dispatches": 95,
+      "borrowed_dirty_rows": 4,
+      "tariff": 442,
+      "complete_prices": {
+        "b": 38,
+        "a": 2,
+        "x": 2
+      }
+    },
+    "beats_six_query": false
+  },
+  "Q8": {
+    "min_R_distinct_slots": {
+      "min_R": 74,
+      "witness_count": 416640,
+      "first_witness": [
+        0,
+        1,
+        2,
+        3,
+        4,
+        8,
+        16,
+        29
+      ]
+    },
+    "tariff_lower_bound_X_ge_0": 452,
+    "beats_six_query": false
+  },
+  "Q9": {
+    "R_lower_bound": 62,
+    "tariff_lower_bound": 466,
+    "beats_six_query": false,
+    "argument": "Each of 31 masks needs an even nonempty readout set, so R >= 62."
+  },
+  "conclusion": "Under this schedule class and abstract tariff, no path-lowered even-subset word with Q in {7,8,9} beats the sharp six-query endpoint tariff 436. Q=7 exact minimum 442 follows from the certified R spectrum {82,88} plus min X=6 on R=82.",
+  "new_kappa": false
+}

research/mutable-source-789q-invoice/NOTICE.md

@@ -0,0 +1,6 @@
+This package was prepared by Wentao Li with substantial AI assistance.
+New material is Apache-2.0 under the repository LICENSE.
+
+Predecessor credit: Arham Tahir (PR1898/PR1370), ywz65 (PR2455),
+TennisBowling (PR1524), Ross Richardson (PR943), and the retained
+mutable-source connector lineage. Their notices and licenses remain.

research/mutable-source-789q-invoice/PROOF.md

@@ -0,0 +1,41 @@
+# Path-lowered 7–9 query invoices versus the six-query endpoint
+
+Retain the five-source common-B mutable-source alphabet of PR1340/PR1898:
+queries `Q_j: z += B x_j`, readouts `R_m: y_m += A_m z`, and paid source shears
+`X_(s,t)`. Correctness is required for every admissible exact `B`, `A_m` and
+every arbitrary dirty input, with sources, connector and scratch restored.
+
+Specialize to length-one identity maps. Connector prefixes are vectors in
+`F₂⁵`. A **path-lowered even-subset schedule** chooses a closed walk
+`p_0=0,p_1,…,p_Q=0` whose increments span `F₂⁵`, reads each nonzero mask on a
+minimum even subset of the identified slots `{p_0,…,p_{Q-1}}`, and implements
+each multi-bit edge by compute/uncompute into one target source (cost
+`2(wt(δ)-1)`).
+
+The PR1898 abstract fixture charges `(b,a,x)=(38,2,2)` complete-call units, so
+
+    tariff = 38 Q + 2 R + 2 X.
+
+**Q=6.** PR1898 attains and proves minimum `R=96` with attained `X=8`, tariff
+436. PR2455 proves `X≥8` at six queries, so 436 is exact in this class.
+
+**Q=7.** Every 6-subset `S⊂F₂⁵\{0}` is scored for even-subset `R` on slots
+`{0}∪S`. Covering sets attain only `R∈{82,88}` (histograms 97,216 and
+486,080); none land in `{83..87}`. Beating the six-query endpoint under this
+fixture requires `R+X<85`, so the excluded intermediate band cannot undercut
+436 even at `X=0`, and every `R=88` schedule already pays at least
+`38·7 + 2·88 = 442`. For each of the 97,216 sets with `R=82`, every full-rank
+ordering closed at 0 is scored for path-local `X`. None has `X<6`; 14,595
+attain `X=6`. Thus the `R=82` layer also pays at least
+`38·7 + 2·82 + 2·6 = 442`. The champion `[0,1,2,6,12,24,16,0]` attains that
+floor, so the exact minimum tariff is `442 > 436`.
+
+**Q=8.** Among distinct 7-nonzero slot sets the minimum even-subset `R` is 74,
+so with `X≥0` the tariff is at least `38·8 + 2·74 = 452 > 436`.
+
+**Q=9.** Already `R≥62` (one even nonempty readout set per mask), so the tariff
+is at least `38·9 + 2·62 = 466 > 436`.
+
+Hence no path-lowered even-subset word with `Q∈{7,8,9}` beats the six-query
+endpoint under this fixture. Words that share shear work across edges outside
+path-local compute/uncompute are outside this theorem.

research/mutable-source-789q-invoice/README.md

@@ -0,0 +1,110 @@
+# Seven–nine query invoices cannot beat the six-query mutable-source endpoint
+
+**Priced finite invoice under the PR1898 abstract complete-call tariff; no new κ.**
+Answers open question 1 of
+[CrocSwap/integer-mult-bounds#2455](https://github.com/CrocSwap/integer-mult-bounds/pull/2455)
+/ the unequal-price handoff of merged
+[PR1898](https://github.com/CrocSwap/integer-mult-bounds/pull/1898): bound attainable
+`R`/`X` bills at seven, eight and nine queries for the explicit fixture
+`(b,a,x)=(38,2,2)`.
+
+Under **path-lowered even-subset schedules** on connector prefixes (the same
+schedule class as PR1898's minimum-query word and PR1370's four-X path), no
+word with `Q ∈ {7,8,9}` beats the sharp six-query endpoint tariff **436**.
+
+| Q | Exact / bound | R | X | Abstract tariff | vs 436 |
+|---|---|---:|---:|---:|---|
+| 6 (PR1898 endpoint) | exact | 96 | 8 | **436** | — |
+| **7 (this)** | **exact minimum** (R∈{82,88}) | **82** | **6** | **442** | **+6** |
+| 8 | lower bound | ≥74 | ≥0 | **≥452** | +≥16 |
+| 9 | lower bound | ≥62 | ≥0 | **≥466** | +≥30 |
+| 10 (PR1370 four-X) | attained | 62 | 4 | 512 | +76 |
+
+The seven-query minimum is certificate-closed. Every 6-subset of nonzero F₂⁵
+points is scored for even-subset readout cost: covering sets attain only
+`R∈{82,88}` (97,216 / 486,080; none in `{83..87}`). Under tariff
+`38Q+2R+2X`, beating 436 needs `R+X<85`, so the excluded intermediate band
+cannot undercut even at `X=0`, and `R=88` already forces tariff `≥442`. On the
+`R=82` layer, every full-rank Hamiltonian closing is scored for path-local
+source-XOR cost (no set has `X<6`; 14,595 attain `X=6`), so that layer is also
+`≥442`. Champion path `[0,1,2,6,12,24,16,0]` attains `7 Q / 82 R / 6 X` and
+replays on arbitrary dirty formal rows. The eight-query bound is the
+exhaustive minimum `R=74` over all distinct 7-nonzero slot sets (`X≥0`). Nine
+queries cannot undercut 436 because already `R≥62` forces tariff `≥466`.
+
+This does **not** price arbitrary XOR-interleaved words outside path-local
+compute/uncompute lowering, nor claim a physical supplier tariff or new κ.
+
+## Reproduce
+
+Python **3.12**, standard library only, from the repository root:
+
+```sh
+python3.12 -I -B research/mutable-source-789q-invoice/verify.py
+python3.12 -I -O -B research/mutable-source-789q-invoice/verify.py
+python3.12 -I -B research/mutable-source-789q-invoice/independent.py
+python3.12 -I -B research/mutable-source-789q-invoice/test_package.py
+python3.12 scripts/research_package.py --package research/mutable-source-789q-invoice
+```
+
+Expected:
+
+```text
+PASS_MUTABLE_SOURCE_789Q_INVOICE Q6=436 Q7=442 Q8_floor=452 Q9_floor=466 no_new_kappa
+PASS_INDEPENDENT_789Q_INVOICE champion=442 floors=452,466 R_spectrum=[82, 88] controls=2
+PASS_REGISTERED_RESEARCH_PACKAGE research/mutable-source-789q-invoice outcome=completed
+```
+
+First-time certificate generation (authoring only):
+
+```sh
+python3.12 -I -B research/mutable-source-789q-invoice/verify.py --write
+```
+
+Default verify is read-only and compares the fresh census to
+[CERTIFICATE.json](CERTIFICATE.json). Admission uses `need()` (not `assert`);
+`-O` also passes. The principal census takes on the order of a few minutes.
+
+## Evidence map
+
+| Claim | Where |
+|---|---|
+| 6Q/10Q comparator invoices | `model.minimum_word_6q`, `model.four_x_ten_q` |
+| Exact min R at Q=7 | exhaustive `combinations(range(1,32),6)` in `verify.py` |
+| Attainable R spectrum `{82,88}` | same census; histogram in `CERTIFICATE.json`; rechecked by `independent.py` |
+| Exact min X among R=82 sets | exhaustive full-rank path orders; no `X<6` |
+| Exact min tariff 442 / no beat 436 | spectrum floors + min-X layer; machine-checked in `verify.py` |
+| Champion identity + tariff 442 | `path_word` + formal dirty replay; `independent.py` column image |
+| Q=8 R≥74 | exhaustive distinct 7-nonzero slot sets |
+| Q=9 tariff ≥466 | `R≥62` for 31 masks |
+
+## Scope limits
+
+No new kappa, frontier, native/hosted admission, or compiler/tape claim. The
+schedule class is path-lowered even-subset readout words with the PR1898
+abstract leaf/node/dispatch fixture. Global unequal-price optimality over all
+XOR interleavings remains open. Physical common-B source access remains open.
+
+## Open next questions
+
+1. **Can a non-path XOR schedule at seven queries reach X≤2 with R=82 (tariff ≤436)?**
+   Why it matters: shared shear preparation across edges might beat path-local
+   compute/uncompute. First step: search restored source programs of X-length
+   ≤2 that realize the champion prefix increments. Blocked by: no cheaper
+   shared-XOR witness is known.
+2. **What is the exact minimum R at eight queries allowing repeated prefix values?**
+   Why it matters: the distinct-slot bound R≥74 already excludes beating 436,
+   but repeats could matter for other tariffs. First step: meet-in-the-middle
+   over 8-tuples. Blocked by: larger search.
+
+## Credit
+
+Credit **Arham Tahir / PR1898** (minimum-query endpoint, abstract tariff fixture,
+unequal-price handoff), **PR1370** (four-X path and ten-query paired word),
+**ywz65 / PR2455** (sharp eight XORs at six queries; open question answered
+here), **TennisBowling / PR1524** (equal-price theorem / unequal handoff),
+**Ross Richardson / PR943** (prefix framework), and the retained mutable-source
+lineage. 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.

research/mutable-source-789q-invoice/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea",
+  "files": [
+    {
+      "path": "research/mutable-source-shear-cost/CERTIFICATE.json",
+      "usage": "input",
+      "git_blob": "48958451bc819f2caa13bf3d9609423706ffb8a0",
+      "sha256": "665435375c025bbcf69eadf43bd9aeae44eb12fefdf12a78d5bfd66abde4ae3c"
+    },
+    {
+      "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"
+    }
+  ]
+}

research/mutable-source-789q-invoice/TASK.json

@@ -0,0 +1,80 @@
+{
+  "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 path-lowered even-subset R/X bills at Q=7,8,9 under the PR1898 abstract tariff (38,2,2) and compare to the sharp six-query endpoint 436; answer #2455 OQ1 / #1898 unequal-price handoff.",
+  "scope_change_reason": "The drawn connector-alphabet card is refined to the explicitly open intermediate-query invoice left by PR1898/PR2455 on the already-admitted mutable-source alphabet, rather than proposing another alphabet extension.",
+  "bottleneck_link": "An intermediate query count that undercuts the six-query abstract tariff would change which unequal-price endpoint is preferred; a negative invoice closes that route inside the stated schedule class.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after exact Q=7 minimum, Q=8/Q=9 lower bounds, independent replay and certificate; no physical supplier search.",
+  "outcome": "completed",
+  "evidence": "CERTIFICATE.json exhaustive Q=7 R-spectrum {82,88} plus min-X on R=82; champion 7/82/6 tariff 442; Q=8 R>=74 floor 452; Q=9 floor 466; independent spectrum+column-image replay.",
+  "author": "Wentao Li",
+  "ai_assistance": "Substantial AI assistance for derivation, census implementation, checking and writing.",
+  "open_questions": [
+    {
+      "question": "Can a non-path XOR schedule at seven queries reach X<=2 with R=82 (tariff <=436)?",
+      "why_it_matters": "Shared shear preparation might beat path-local compute/uncompute and reopen an intermediate optimum.",
+      "first_step": "Search restored source programs of X-length at most 2 realizing the champion prefix increments.",
+      "blocked_by": "No cheaper shared-XOR witness is known."
+    },
+    {
+      "question": "What is the exact minimum R at eight queries allowing repeated prefix values?",
+      "why_it_matters": "Distinct-slot R>=74 already excludes beating 436 under this tariff, but repeats matter for other price ratios.",
+      "first_step": "Meet-in-the-middle over length-8 prefix tuples.",
+      "blocked_by": "Larger search than the distinct-slot census."
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 1898,
+      "credit": "Arham Tahir; minimum-query endpoint, abstract tariff, unequal-price handoff"
+    },
+    {
+      "pr": 2455,
+      "credit": "ywz65; sharp eight XORs at six queries; OQ1 answered here"
+    },
+    {
+      "pr": 1370,
+      "credit": "Arham Tahir; four-X path / ten-query paired word"
+    }
+  ]
+}