Prove a pair-sum readout floor for partitioned walk duals at every Q (no new κ)

research/partitioned-walk-pair-sum-floor/README.md

@@ -0,0 +1,129 @@
+# Pair-sum floor for partitioned independent-walk duals
+
+**Scoped proof and finite certificate in the PR1898 abstract tariff; no new κ.**
+This answers open question 2 of Wentao Li's
+[PR #2779](https://github.com/CrocSwap/integer-mult-bounds/pull/2779)
+(`research/independent-walks-7q-obstruction`): repeated labels inside a
+partitioned walk cannot improve on `R=112` at `Q=7`. No such dual covers.
+The same argument gives a readout floor for every query count, every label
+pattern and any number of walks. It is attained at `Q=8` and `Q=9`.
+
+| Q | Readout floor `R` | Attained? | Tariff floor at `X=0` |
+|---:|---:|---|---:|
+| 7 | 102 (exact min is 112, below) | no | 470 |
+| 8 | **92** | yes, `(0,10)`, `(0,22,5,31,24,20)` | 488 |
+| 9 | **80** | yes, `(0,3)`, `(0,18,1,5,11,20,27)` | 502 |
+| 10 | 66 | unknown | 512 |
+| 11 | 62 | unknown | 542 |
+| ≥12 | 62 | — | > 436 from `38Q` alone |
+
+Every entry exceeds the six-query endpoint tariff `436`. Partitioned
+independent duals cannot undercut it at any query count or label pattern.
+
+## Model
+
+The model is that of PR #2779's `model.py`, which the verifier imports as a
+pinned live input. A restored walk is a slot list `(0,s_1,…,s_{n-1})` over
+`F₂⁵` whose closed completion has only nonzero edges. Labels may now repeat and
+`0` may be revisited at interior slots. Walk `i` has even-subset table `e_i`.
+A partitioned dual has `k ≥ 2` walks with lengths summing to `Q`. Mask `m` costs
+`min Σ e_i[a_i]` over `a_1⊕…⊕a_k = m`. For `k = 2` this is the PR #2779 formula,
+and the verifier checks agreement on every two-walk control. `R` sums the 31
+nonzero masks, and the tariff is `38Q + 2R + 2X`.
+
+## Proof
+
+**Table lemma.** For a walk `w`, `e[v]` is finite iff `v ∈ span(w)`, since an
+odd subset can toggle the slot-0 entry. Every finite nonzero value is even and
+at least 2, and `e[v] = 2` iff `v` is a nonzero pair sum `s_j ⊕ s_k`. A walk of
+length `n` has at most `C(n,2)` pair sums.
+
+**Covering.** A dual covers every mask iff the walk spans sum to `F₂⁵`. Walk
+`i` has rank at most `n_i − 1`, so covering needs `Σ(n_i − 1) ≥ 5`, that is
+`Q ≥ 5 + k`.
+
+**Q = 7 answer.** Only `k = 2` with `(2,5)` or `(3,4)` can cover, and the bound
+is tight. Each walk must therefore have `n_i − 1` linearly independent labels.
+A repeated label or interior zero revisit lowers the rank, so such a dual never
+covers. The remaining duals are exactly PR #2779's distinct-label duals, for
+which that package proves `R = 112`. So `112` is the exact minimum over all
+label patterns at `Q = 7`.
+
+**Pair-sum floor.** A nonzero mask costs at least 2. Cost 2 forces one port to
+pay 2 and the rest 0, so the mask is a pair sum of one walk. Every other mask
+costs at least 4. With `P` the union of nonzero pair sums,
+`R ≥ 4·31 − 2|P| ≥ 124 − 2 Σ C(n_i,2)`, and also `R ≥ 62`. Under
+`Σ n_i = Q`, `n_i ≥ 2`, `k ≥ 2`, convexity puts the maximum of
+`Σ C(n_i,2)` at `(2, Q−2)`, equal to `1 + C(Q−2,2)`. Hence
+
+```text
+R ≥ max(62, 122 − (Q−2)(Q−3)).
+```
+
+The two witnesses in the table attain this value at `Q = 8, 9`. So `92` and
+`80` are the exact minima there over all partitioned duals, with arbitrary
+labels and any number of walks.
+
+## Evidence
+
+`verify.py` checks, using PR #2779's `even_table`, `dual_independent_R`,
+`valid_restored_walk`, `path_X` and `tariff_qrx`:
+
+- the table lemma on every restored walk of length 2–5 with arbitrary labels
+  (924,482 walks);
+- the `Q = 7` rank census. 894,660 length-5 walks, of which 624,960 have
+  rank 4, all with distinct nonzero labels. 28,861 length-4 walks, 26,040 of
+  rank 3, likewise. Every length-2 and length-3 walk has full rank;
+- 4,000 seeded random duals with `Q` from 7 to 11, two or more walks and
+  arbitrary labels. Covering matches full span and every covering dual (2,456)
+  meets both floors. The k-port convolution equals PR #2779's two-port dual;
+- the partition maximum for `Q` from 7 to 11, the two witnesses (exact `R`,
+  path `X`, tariff), and the tariff floors.
+
+The random controls are sanity checks; the floor rests on the proof above.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/partitioned-walk-pair-sum-floor/verify.py
+python3.12 -B scripts/research_package.py --package research/partitioned-walk-pair-sum-floor
+```
+
+Expected final line:
+
+```text
+PASS_PARTITIONED_WALK_PAIR_SUM_FLOOR lemma_walks=924482 q7_full_rank_5walks=624960 q8_min_R=92 q9_min_R=80 min_tariff=470 no_new_kappa
+```
+
+The full run takes about 25 s. `--quick` checks the table lemma only up to
+length 4.
+
+## Limitations
+
+- This is an abstract-tariff result in the PR1898 five-source alphabet, not a
+  physical supplier, a complete multiplication theorem or a κ change.
+- The `k ≥ 3` cost rule is the natural min-plus extension of the two-port dual.
+  No earlier package defines it.
+- Same-walk, transfer-coupled and shared-dirt schedules are outside the scope.
+- Path cost `X` is only bounded below by 0. The witnesses have positive `X`.
+
+## Open next questions
+
+1. **Exact minima at `Q = 10, 11`.** The floor gives 66 and 62; a seeded search
+   of 200,000 `(2, Q−2)` duals found 72 and 66. Why it matters: it would settle
+   whether the pair-sum floor is sharp for every `Q`. First step: an exhaustive
+   search over pair-sum-distinct long walks up to `GL(5,2)` symmetry. Blocked
+   by: none; the tariff question is already settled there.
+2. **Transfer-coupled schedules.** Can the pair-sum count, with the shared
+   prefix charged once, bound transfer-coupled duals at every `Q`? Why it
+   matters: it would replace the per-shape censuses. First step: bound the
+   cost-2 masks of a shared prefix with divergent suffixes. Blocked by: the
+   transfer billing rule.
+
+## Credit
+
+Model, two-port dual, tariff and the distinct-label `R = 112` theorem: Wentao
+Li, PR #2779, building on Arham Tahir's PR1898 and the lineage credited there.
+This package was produced by Nick Petalas. Apache-2.0.

research/partitioned-walk-pair-sum-floor/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/independent-walks-7q-obstruction/model.py",
+      "usage": "input",
+      "git_blob": "49809a4fa0641bfea0b87b2f85e4c08cc23f0bfd",
+      "sha256": "8e68f12143bb4392ec4473eed65c0db5a156bf0c60d39dec998abcc840f57e0e"
+    }
+  ]
+}

research/partitioned-walk-pair-sum-floor/TASK.json

@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "connector-alphabet-change",
+    "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "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. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "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.",
+      "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions."
+    ],
+    "overlap_terms": [
+      "universal connector",
+      "source-toggle",
+      "connector alphabet"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "PR #2779 open question 2 (repeat labels in a Q=7 partitioned walk), extended to arbitrary labels, any number of walks and every query count in the same PR1898 abstract tariff.",
+  "scope_change_reason": "The card asks for a new connector operation. This keeps the alphabet and closes an open question on the partitioned independent-walk interface left by PR #2779, giving one floor in place of per-shape censuses.",
+  "bottleneck_link": "Side result. It closes the partitioned independent-walk route to undercutting the six-query endpoint tariff 436 at every Q; it does not change a supplier or κ.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the floor is proved and attained where checked; leave exact Q=10,11 minima open.",
+  "outcome": "completed",
+  "evidence": "verify.py: table lemma on all 924,482 restored walks of length 2-5, Q=7 rank census, 4,000 seeded random duals, witnesses attaining R=92 (Q=8) and R=80 (Q=9), tariff floors > 436.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What are the exact minimum readouts at Q=10 and Q=11 (floor 66 and 62; search best 72 and 66)?",
+      "why_it_matters": "Settles whether the pair-sum floor is sharp at every Q.",
+      "first_step": "Exhaustive search over pair-sum-distinct long walks up to GL(5,2) symmetry.",
+      "blocked_by": "None; the tariff question is already settled there."
+    },
+    {
+      "question": "Does a pair-sum count with the shared prefix charged once bound transfer-coupled duals at every Q?",
+      "why_it_matters": "It would replace per-shape transfer-coupled censuses.",
+      "first_step": "Bound the cost-2 masks of a shared prefix with divergent suffixes.",
+      "blocked_by": "The transfer billing rule."
+    }
+  ]
+}

research/partitioned-walk-pair-sum-floor/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/independent-walks-7q-obstruction/model.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Table lemma on all walks of length 2-5, Q=7 rank census, seeded random duals against the PR #2779 two-port dual, floor witnesses at Q=8 and Q=9, tariff floors."
+    }
+  ]
+}