Prove the eight-query mutable-source tariff is exactly 460 (no κ)

research/eight-query-path-lowered-tariff/README.md

@@ -0,0 +1,198 @@
+# Eight-query path-lowered words: readouts 74 and source XORs 4 are attained together
+
+**Scoped exact finite computation, in the PR1898 abstract tariff. No new κ.** In the
+path-lowered even-subset class of
+[PR2677](https://github.com/CrocSwap/integer-mult-bounds/pull/2677)
+(`research/mutable-source-789q-invoice`), every eight-query word needs at least
+74 readouts `R` and at least 4 source XORs `X`, and one closed walk attains both.
+Both floors are known. The new fact is that they are attained together. The
+eight-query row of PR2677's table was a lower bound (`R >= 74`, `X >= 0`, tariff
+`>= 452`). It is now exact:
+
+```text
+min over eight-query words of  b*Q + a*R + x*X  =  8b + 74a + 4x   for all b, a, x > 0
+tariff at (b, a, x) = (38, 2, 2):  38*8 + 2*74 + 2*4 = 460   (24 above the six-query endpoint 436)
+```
+
+Witness, a closed prefix walk with 74 readouts and 4 source XORs (replayed on
+arbitrary dirty formal rows by the pinned model):
+
+```text
+(0, 1, 3, 2, 6, 14, 30, 20, 0)      also (0, 4, 20, 24, 9, 1, 3, 2, 0)
+```
+
+| Q | readout floor | XOR floor | attained together | tariff at (38,2,2) | vs 436 |
+|--:|--:|--:|---|--:|--:|
+| 6 | 96 | 8 | yes (PR1898 word) | **436** exact | 0 |
+| 7 | 82 | 6 | yes (PR2677 champion) | **442** exact | +6 |
+| 8 | 74 | 4 | **yes (this package)** | **460** exact | +24 |
+| 9 | 62 | 2 | open; best found `R=70` at `X=2` | between 470 and 486 | at least +34 |
+| >= 10 | 62 | 0 | not claimed | above 460 from `38Q` and `R >= 62` | |
+
+The Q = 6 and Q = 7 rows are the existing values; the census and replays here
+reproduce them. New here: the attaining Q = 8 word, which makes that row exact and
+price-independent; the exact walk spectra; the attained Q = 9 value 486; and the
+sharpness of the XOR floor at eight queries (below). The XOR floor itself is not
+claimed: it is the connector consequence recorded in PR5935 (below).
+
+## Model
+
+The model, cost formulas and word builder are those of PR2677's `model.py`, which
+the verifier imports as a pinned live input after a SHA256 check. A path-lowered
+word is a closed connector walk `0 = w_0, w_1, ..., w_Q = 0` in `F2^5` with every
+edge `w_i xor w_(i+1)` nonzero. Values and zero revisits may repeat. Then
+
+- `X = sum over edges of 2*(weight(edge) - 1)`, the path-local compute and uncompute
+  source XORs;
+- `R` is the total even-subset readout count over the slot values: mask `m` costs
+  the least even number of slots whose XOR is `m`;
+- the tariff is `38Q + 2R + 2X`, the PR1898 fixture.
+
+A walk covers when every nonzero mask is read, which forces its visited values to
+span `F2^5`. Only covering walks are words.
+
+## Source-XOR floor
+
+For arbitrary restored source-XOR words, PR5935
+(`research/connected-xor-word-floor`, this author's earlier package) proves
+`X >= 2(n - c)` for an interaction graph with `c` components. With the component
+inequality `Q >= n + c` of PR2455 this gives `X >= 2(2n - Q)`, so at five sources
+`X >= 2(10 - Q)` for `Q <= 10`. PR5935 records this: `X >= 4` at `Q = 8` and
+`X >= 2` at `Q = 9`. This package does not re-prove it.
+
+For self-containment, here is a direct proof in the path-local cost model. A
+covering closed walk with `Q` edges has `X >= 2*max(0, 10 - Q)`, `X = 2Q mod 4`, and
+equality at the floor holds exactly when every coordinate lies in exactly two edges.
+
+*Proof.* The visited values are partial sums of the edges, so the edges span
+`F2^5` and every coordinate occurs in some edge. The edges sum to zero, so each
+coordinate occurs in an even number of edges, at least two. The weight total is the
+sum of these five counts: even and at least 10. Then
+`X = 2*(total - Q) >= 2*(10 - Q)`, with equality iff the counts are `2,2,2,2,2`.
+For `Q <= 5` no covering walk exists, since six edges are needed to span `F2^5`. ∎
+
+**Sharpness.** Each X-floor layer below contains covering walks for `Q = 6..10`, so
+the floor `2(10 - Q)` is attained there by a path-lowered word, which is a restored
+word. At `Q = 8` this makes the XOR floor 4 sharp for arbitrary restored words, given
+PR5935's lower bound. That is the sharp eight-query XOR floor asked for in Open next
+question 2 of `research/seven-query-xor-floor`.
+
+## Eight queries
+
+1. **Readout floor, repeats allowed.** A walk with eight edges visits at most seven
+   distinct nonzero values. The census over every set of five, six or seven values
+   (3,535,767 sets, 3,097,024 covering) gives the spectra
+
+   | distinct nonzero values | `R` values (number of sets) |
+   |--:|---|
+   | 5 | 96 (83,328) |
+   | 6 | 82 (97,216), 88 (486,080) |
+   | 7 | 74 (416,640), 80 (1,180,480), 84 (833,280) |
+
+   So `R >= 74` for every eight-query word. Repeated prefix values or zero revisits
+   leave at most six distinct values and force `R >= 82`. This answers Open next
+   question 2 of PR2677 inside the class: the exact minimum is 74, attained only
+   with seven distinct nonzero values. This is also the readout half of Open next
+   question 2 of PR2686, repeats included. Its XOR half is the sharp floor 4 above.
+2. **XOR floor.** `X >= 4`, from PR5935 for every restored word and from the parity proof above in this class.
+3. **Attainment.** The exhaustive layer of closed eight-edge walks with every
+   coordinate in exactly two edges has 730,800 walks, the count given by
+   inclusion-exclusion. Of these, 30,240 cover with `R = 74` and `X = 4`. Its full
+   spectrum is `74: 30,240`, `80: 172,800`, `82: 8,640`, `84: 161,280`,
+   `88: 248,640`, `96: 84,000` and 25,200 non-covering walks.
+
+Both floors hold for every word and one walk attains both. The Pareto frontier at
+`Q = 8` is the single point `(R, X) = (74, 4)`, so the optimum does not depend on
+the prices. The same argument gives single-point frontiers `(96, 8)` at `Q = 6`
+and `(82, 6)` at `Q = 7`.
+
+## Price crossovers among Q = 6, 7, 8
+
+With the three exact rows `f6 = 6b + 96a + 8x`, `f7 = 7b + 82a + 6x` and
+`f8 = 8b + 74a + 4x`:
+
+```text
+f8 < f7  iff  b < 8a + 2x          f7 < f6  iff  b < 14a + 2x          f8 < f6  iff  b < 11a + 2x
+```
+
+At `(38, 2, 2)` all three fail, so the six-query endpoint stays optimal among
+`Q <= 8`. The verifier checks the equivalences on a grid of prices.
+
+## Nine and ten queries
+
+At `Q = 9` the XOR floor is 2 and the readout floor is at least 62. The X-floor
+layer has 453,600 walks and its least readout count is 70, so tariff 486 is
+attained. The exact minimum lies between 470 and 486. The next layer (weight total
+12, `X = 6`) is not enumerated.
+
+At `Q = 10` the `X = 0` layer has 113,400 walks and least `R = 64`, with no
+`R = 62` walk. That reproduces the read-only ten-query repair with 64 readouts and
+no source XOR recorded in `research/mutable-source-connector`, and it agrees with
+the four-XOR requirement of `research/mutable-source-shear-cost` for 62 readouts.
+No Q = 10 claim is made.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -B research/eight-query-path-lowered-tariff/verify.py
+python3.12 -B scripts/research_package.py --package research/eight-query-path-lowered-tariff
+```
+
+Expected marker:
+
+```text
+PASS_EIGHT_QUERY_PATH_LOWERED_TARIFF Q8=(R74,X4) tariff=460 floors_attained_Q6_Q7_Q8 Q9_in_470_486 no_new_kappa
+```
+
+The verifier takes about a minute. It checks:
+
+- the readout census above and its set counts;
+- the path-local XOR floor exhaustively on 638,832 covering walks in `F2^2`, `F2^3` and
+  `F2^4`, including attainment of the floor at every `Q` from `n + 1` to `2n`;
+- every X-floor layer at `Q = 6..10`, with walk counts equal to the closed-form
+  count `sum_i (-1)^i C(Q,i) C(Q-i,2)^5` and the spectra quoted here;
+- literal dirty-row replays with the pinned model of the two `Q = 8` witnesses,
+  the `Q = 7` champion `(0,1,2,6,12,24,16,0)`, the six-query word, the `Q = 9`
+  witness `(0,1,3,2,6,14,10,26,16,0)` and the ten-query paths;
+- the three crossover equivalences on prices `b` in 1..39 and `a`, `x` in 1..7;
+- 6,000 seeded random walks, repeats and zero revisits included, comparing the
+  set-based readout and edge-cost formulas with the pinned model.
+
+[SOURCES.json](SOURCES.json) pins the model. The exhaustive search that found the
+witnesses was a separate, unpackaged program. Every number above is recomputed by
+`verify.py` itself.
+
+## Scope and limits
+
+- The exact row is for path-lowered even-subset words: one closed connector walk,
+  path-local compute and uncompute source XORs, and PR2677's tariff. The readout and
+  walk-spectrum claims are not checked for arbitrary XOR-interleaved restored words.
+  Only the XOR floor, and its sharpness at eight queries, is stated for those, and
+  its lower bound is PR5935's, not re-proved here.
+- The tariff is the abstract complete-call fixture. No physical supplier, hosting,
+  precision or kappa claim is made. Independent human and formal proof-kernel review
+  are unclaimed.
+- Nine queries are not settled. Ten queries are cross-checked only.
+
+## Open next questions
+
+1. What is the exact tariff at nine queries (between 470 and 486)? Enumerate the
+   `X = 6` layer at `Q = 9` and compare its least readout count with 70. The layer is
+   larger than the ones here. No obstruction is known.
+2. Does the readout floor 74 hold for arbitrary XOR-interleaved restored words at
+   eight queries, with non-path source XORs? The census uses only the set of
+   connector values, so the first step is to check that a restored word's connector
+   values obey the same even-subset readout constraint.
+
+## Credit
+
+This contribution was produced by Nick Petalas. It builds on Wentao Li's PR2677
+(`research/mutable-source-789q-invoice`: model, invoice table and the open
+question), PR2686 (`research/seven-query-r-floor`) and PR2643
+(`research/seven-query-xor-floor`); on Arham Tahir's PR1898 (the alphabet and the
+six-query word); and on PR1370 and Ross Richardson's PR943 for the ten-query
+cross-check. The XOR floor `2(10 - Q)` is the connector consequence of PR5935
+(Nick Petalas) with ywz65's PR2455 component inequality; PR2455 also proves the
+six-query XOR bound. Predecessor files and notices are unchanged. Apache-2.0.

research/eight-query-path-lowered-tariff/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/mutable-source-789q-invoice/model.py",
+      "usage": "input",
+      "git_blob": "8ce90c48df0a2f9eba9847f3dfe71ce6677897d1",
+      "sha256": "6696b01837e526f365576c6e35367fa8a1494f5bd3f49af7fe38c52366668c13"
+    }
+  ]
+}

research/eight-query-path-lowered-tariff/TASK.json

@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "Exact eight-query row of the path-lowered even-subset mutable-source invoice (PR2677) at every positive price (b,a,x): the readout floor 74 and the source-XOR floor 4 are attained by one closed walk. Exhaustive X-floor layers at Q = 6..10; sharpness of the XOR floor at eight queries for arbitrary restored words, with its lower bound taken from PR5935. Answers Open next question 2 of PR2677, and of PR2686 and PR2643 at eight queries within these classes.",
+  "scope_change_reason": "The card asks for a new connector operation. This keeps the PR1898 alphabet and the PR2677 path-lowered schedule class unchanged and closes the unpriced eight-query row of an existing invoice table, a side result in the same abstract tariff.",
+  "bottleneck_link": "Side result. It settles the intermediate-query unequal-price handoff of the five-source common-B mutable-source connector for eight queries; it does not change a supplier or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the eight-query row is exact and the floor layers are enumerated; leave the Q = 9 exact minimum and non-path restored readout words open.",
+  "outcome": "completed",
+  "evidence": "verify.py: readout census over all 3,535,767 value sets of size 5, 6 and 7 (3,097,024 cover every mask; spectra {96}, {82,88}, {74,80,84}); parity-lemma controls on 638,832 covering walks in F2^2..F2^4; exhaustive X-floor layers at Q = 6..10 matching closed-form walk counts; literal dirty-row replays of the Q = 8 witnesses (R=74, X=4, tariff 460), the Q = 7 champion, the Q = 6 endpoint and the Q = 9 witness (tariff 486); 6,000 seeded random walks against the pinned model.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the exact minimum tariff at nine queries (floor 470, attained 486 at X = 2, R = 70)?",
+      "why_it_matters": "It completes the exact rows of the path-lowered invoice table between the six-query endpoint and the ten-query repairs.",
+      "first_step": "Enumerate the X = 6 layer (weight total 12, each coordinate in two or four edges) at Q = 9 and compare its least readout count with 70.",
+      "blocked_by": "A larger layer than the X-floor layers enumerated here; no obstruction known."
+    },
+    {
+      "question": "Does the readout floor 74 hold for arbitrary XOR-interleaved restored words at eight queries?",
+      "why_it_matters": "It would extend the exact eight-query row from path-lowered words to every restored five-source word with even-subset readouts.",
+      "first_step": "Check that the connector values of a restored word obey the same even-subset readout constraint, so that the census over value sets applies unchanged.",
+      "blocked_by": "The constraint is argued for path-lowered words only; no general proof is written here."
+    }
+  ]
+}

research/eight-query-path-lowered-tariff/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/mutable-source-789q-invoice/model.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Readout census over all 5-, 6- and 7-value sets, XOR parity lemma controls, exhaustive X-floor layers at Q = 6..10, literal dirty-row replays of the Q = 8, 7, 6 and 9 words, tariff crossovers, and 6,000 seeded random walks against the pinned model."
+    }
+  ]
+}