Research: prove sharp six source-XOR floor at seven queries (no new kappa)

research/seven-query-xor-floor/CERTIFICATE.json

@@ -0,0 +1,149 @@
+{
+  "schema_version": 1,
+  "status": "PASS_SEVEN_QUERY_XOR_FLOOR",
+  "scope": "Five-source common-B mutable-source Q/R/X alphabet (PR1898). Restored straight-line words. Exact minimum source-XOR count at Q=7.",
+  "claim": {
+    "Q": 7,
+    "min_X": 6,
+    "sharp": true,
+    "answers_789q_oq1": "No non-path (or path) schedule at Q=7 can reach X<=2; in fact X<=5 is impossible.",
+    "no_new_kappa": true
+  },
+  "component_lemma": {
+    "statement": "An interaction graph with c components forces at least n+c queries on n sources.",
+    "n": 5
+  },
+  "edge_bound": {
+    "argument": "Any interaction graph with e undirected edges on n=5 labels has c>=n-e components. For e<=2, c>=3 so Q>=n+c>=8. Census tightens X=2 to c>=4.",
+    "X_le_2_query_floor_from_edges": 8,
+    "X_le_2_query_floor_from_census": 9
+  },
+  "census": {
+    "n": 5,
+    "bound": 6,
+    "raw_half_word_counts": [
+      1,
+      20,
+      400,
+      8000
+    ],
+    "half_distinct_matrices": [
+      1,
+      20,
+      261,
+      2770
+    ],
+    "half_matrix_graph_states": [
+      1,
+      20,
+      270,
+      3130
+    ],
+    "last_layer_sha256": "03182f1a0a36c51ea1112ed41e3e4c3d99393dc479dc1c4c477673d0f7eeb190",
+    "by_length": [
+      {
+        "length": 0,
+        "identity_graphs": 1,
+        "connected_identity_graphs": 0,
+        "minimum_components": 5,
+        "query_floor_n_plus_c": 10,
+        "graphs_sha256": "d0bca111f8628137adc4c16f123496dcdd1d590d06cb5d9acd68b39fe656fb97"
+      },
+      {
+        "length": 1,
+        "identity_graphs": 0,
+        "connected_identity_graphs": 0,
+        "minimum_components": null,
+        "query_floor_n_plus_c": null,
+        "graphs_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945"
+      },
+      {
+        "length": 2,
+        "identity_graphs": 10,
+        "connected_identity_graphs": 0,
+        "minimum_components": 4,
+        "query_floor_n_plus_c": 9,
+        "graphs_sha256": "0899bb1953bc4b09e040dbb8308c5c134c718d3cfe052d06ff64baed6062eb7f"
+      },
+      {
+        "length": 3,
+        "identity_graphs": 0,
+        "connected_identity_graphs": 0,
+        "minimum_components": null,
+        "query_floor_n_plus_c": null,
+        "graphs_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945"
+      },
+      {
+        "length": 4,
+        "identity_graphs": 55,
+        "connected_identity_graphs": 0,
+        "minimum_components": 3,
+        "query_floor_n_plus_c": 8,
+        "graphs_sha256": "546640ef872e4f0d2ebda17f74c88eeea8ccff09cb9e16de7cff2ff6735cd024"
+      },
+      {
+        "length": 5,
+        "identity_graphs": 10,
+        "connected_identity_graphs": 0,
+        "minimum_components": 3,
+        "query_floor_n_plus_c": 8,
+        "graphs_sha256": "defa9e87f9e7cc3a75d63330d451e5d1c8cd011734d1a489ec0d84af6ba68504"
+      },
+      {
+        "length": 6,
+        "identity_graphs": 175,
+        "connected_identity_graphs": 0,
+        "minimum_components": 2,
+        "query_floor_n_plus_c": 7,
+        "graphs_sha256": "163a9c5ccd357bfc55f07c641213f247253db4894f6798c6e75c94104e2be060"
+      }
+    ]
+  },
+  "query_floors_by_X": {
+    "0": 10,
+    "1": null,
+    "2": 9,
+    "3": null,
+    "4": 8,
+    "5": 8,
+    "6": 7
+  },
+  "attaining_witness": {
+    "kind": "path_lowered_even_subset",
+    "closed_path": [
+      0,
+      1,
+      2,
+      6,
+      12,
+      24,
+      16,
+      0
+    ],
+    "Q": 7,
+    "R": 82,
+    "X": 6,
+    "tariff_at_38_2_2": 442,
+    "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
+      }
+    },
+    "credit": "Path-lowered champion from mutable-source-789q-invoice lineage; PR1898 alphabet."
+  },
+  "pr2455_crosscheck": {
+    "matched_graph_digests_0_through_6": true,
+    "note": "Open PR2455 proves X>=8 at Q=6; this package reuses the same meet-in-the-middle census through X=6 for the Q=7 floor. Per-length graph digests match that package's RESULT.json."
+  },
+  "new_kappa": false
+}

research/seven-query-xor-floor/NOTICE.md

@@ -0,0 +1,21 @@
+# 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 meet-in-the-middle restored interaction-graph census at six queries;
+  digests for lengths 0–6 are cross-checked here.
+- 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` — champion path and
+  non-path OQ1 answered here; that package is not edited.
+- Live pin: `research/mutable-source-shear-cost/CERTIFICATE.json` (ten-query
+  four-X context).
+
+Prepared by Wentao Li (VictorLiwentao, @Is__Victor) with substantial AI
+assistance.

research/seven-query-xor-floor/PROOF.md

@@ -0,0 +1,115 @@
+# Exact source-XOR floor at seven queries
+
+This is a scoped obstruction and sharpness statement in the five-source
+common-B mutable-source alphabet of
+[PR1898](https://github.com/CrocSwap/integer-mult-bounds/pull/1898).
+It does not claim a new kappa, physical supplier tariff, or global unequal-price
+optimum over all query counts.
+
+It answers open question 1 of the path-lowered
+`research/mutable-source-789q-invoice` lineage: whether a non-path XOR schedule
+at seven queries can reach `X≤2` with `R=82` (tariff `≤436`). The answer is
+negative for a stronger reason: **every restored seven-query word needs
+`X≥6`**, path or non-path. The credited path-lowered champion attains `X=6`,
+so the floor is sharp.
+
+## Alphabet and restoration
+
+Retain five distinct arbitrary-dirty F₂ source rows `x₀,…,x₄`, thirty-one
+distinct arbitrary-dirty outputs `y_m`, a connector `z`, and private scratch.
+Complete calls are `Q_j: z += B x_j`, `R_m: y_m += A_m z`, and paid
+`X_(s,t): x_t += x_s`. The exit map is
+
+```text
+y_m += A_m B(sum_j bit_j(m) · x_j_initial),
+```
+
+with every source, connector and private scratch restored. Straight-line words
+are data independent. Extra connectors, free copies, output mixing and
+source-specific B maps are excluded. This is PR1340/PR1898's source-shear
+alphabet.
+
+## Interaction graph and component lemma
+
+Build the undirected **interaction graph** on the five source labels: every
+`X_(s,t)` contributes the edge `{s,t}`, including edges whose matrix effects
+later cancel. Suppose the graph has `c` components `C_i` of sizes `n_i`.
+
+Each query increment lies in the coordinate subspace of its source's component.
+Connector restoration forces the sum of increments inside each component to be
+zero, so the increments that touch component `i` span a space of dimension at
+most `t_i − 1` whenever that component is queried `t_i` times. Covering the
+`n_i`-dimensional source space on that component therefore requires
+`t_i ≥ n_i + 1`. Every component must be queried (an unqueried component cannot
+contribute its sources to the AB image while restoring). Summing yields
+
+```text
+Q = Σ t_i ≥ Σ (n_i + 1) = n + c.
+```
+
+Thus an interaction graph with `c` components forces at least `n + c` queries.
+This lemma is the same component bound used by open
+[PR2455](https://github.com/CrocSwap/integer-mult-bounds/pull/2455) at six
+queries; the proof is reproduced here so the present package is freestanding.
+
+## Census of restored XOR words through length six
+
+A restored source-shear word of XOR-length `ℓ` is a product of `ℓ` elementary
+shears that returns every source to its initial basis. Meet-in-the-middle on
+`(source matrix, all-used-edge graph)` lists every restored interaction graph
+at each length `ℓ ≤ 6` (PR2455 technique; digests match that package's
+`RESULT.json` for lengths 0–6). Observed minimum component counts:
+
+| X length | Restored graphs | Min components | Query floor `n+c` |
+|---:|---:|---:|---:|
+| 0 | 1 | 5 | 10 |
+| 1 | 0 | — | — |
+| 2 | 10 | 4 | 9 |
+| 3 | 0 | — | — |
+| 4 | 55 | 3 | 8 |
+| 5 | 10 | 3 | 8 |
+| 6 | 175 | 2 | 7 |
+
+No length through six has a connected restored graph. In particular, every
+restored word with `X ≤ 5` has query floor at least 8, so it cannot run at
+exactly seven queries.
+
+A coarser edge bound already excludes the 789q OQ1 target without the census:
+any graph with `e ≤ 2` edges on five labels has `c ≥ 5 − e ≥ 3`, hence
+`Q ≥ 8`. The census strengthens `X = 2` to `c ≥ 4` / `Q ≥ 9` and extends the
+exclusion through `X = 5`.
+
+## Sharpness at seven queries
+
+The first XOR length whose census floor is `≤ 7` is `X = 6` (minimum
+components 2). Therefore every restored seven-query word satisfies `X ≥ 6`.
+
+The path-lowered closed prefix
+
+```text
+(0, 1, 2, 6, 12, 24, 16, 0)
+```
+
+attains `7 Q / 82 R / 6 X` under even-subset readout and path-local
+compute/uncompute lowering (credited champion of the 789q invoice lineage).
+Dirty root and inverse identities hold for the PR1898 abstract maps. Its
+abstract complete-call tariff at `(b,a,x)=(38,2,2)` is 442. Attainment shows
+the XOR floor is sharp.
+
+## Scope limits
+
+- No claim that seven-query words cannot undercut tariff 436 via a **lower R**
+  than 82 with `X ≥ 6`. Readout minima under unrestricted non-path schedules
+  remain open.
+- No claim about eight or nine queries beyond the inherited path-lowered floors.
+- No physical common-B hosting, precision, tape or selected-supplier invoice.
+- No new kappa.
+
+## Relation to predecessors
+
+| Prior | Already proves | This package adds |
+|---|---|---|
+| PR1898 | Min `Q = 6`, min `R = 96` at that `Q`, `8 X` construction | — |
+| PR2455 (open) | `X ≥ 8` at exactly six queries | — |
+| 789q invoice (fork, path-lowered) | Path-class `Q∈{7,8,9}` invoices; OQ1 asks non-path `X≤2` at `R=82` | — |
+| **This** | — | **`X ≥ 6` at exactly seven queries, sharp; rejects OQ1** |

research/seven-query-xor-floor/README.md

@@ -0,0 +1,98 @@
+# Seven-query source-XOR floor is exactly six
+
+**Scoped obstruction with sharp attainment; no new kappa.** In the five-source
+common-B mutable-source alphabet of
+[PR1898](https://github.com/CrocSwap/integer-mult-bounds/pull/1898), every
+restored straight-line word with **exactly seven queries** needs **at least six
+source XORs**. The bound is sharp: the credited path-lowered champion
+
+```text
+(0, 1, 2, 6, 12, 24, 16, 0)
+```
+
+attains `7 Q / 82 R / 6 X` (abstract tariff **442** at `(b,a,x)=(38,2,2)`).
+
+This answers open question 1 of the path-lowered
+`research/mutable-source-789q-invoice` lineage (beyond
+[#2455](https://github.com/CrocSwap/integer-mult-bounds/pull/2455) /
+[#1898](https://github.com/CrocSwap/integer-mult-bounds/pull/1898)): a non-path
+XOR schedule at seven queries **cannot** reach `X≤2` with `R=82` (nor any `R`),
+because already `X≤5` is impossible at `Q=7`.
+
+| X length | Min interaction components | Query floor `5+c` | Admits `Q=7`? |
+|---:|---:|---:|---|
+| ≤2 | ≥4 (census; edges alone give ≥3) | ≥9 | no |
+| 4 or 5 | 3 | 8 | no |
+| **6** | **2** | **7** | **yes (sharp)** |
+
+The component lemma (`Q ≥ n + c`) and the meet-in-the-middle restored-graph
+census through length six are recorded in [PROOF.md](PROOF.md) and
+[CERTIFICATE.json](CERTIFICATE.json). Graph digests for lengths 0–6 match open
+PR2455's published `RESULT.json` (that PR proves `X≥8` at **six** queries;
+this package uses the same census engine for the **seven**-query floor).
+
+No claim that seven-query words cannot undercut tariff 436 by lowering `R`
+below 82 while keeping `X≥6`. No physical supplier invoice or new κ.
+
+## Reproduce
+
+Python **3.12**, standard library only, from the repository root:
+
+```sh
+python3.12 -I -B research/seven-query-xor-floor/verify.py
+python3.12 -I -O -B research/seven-query-xor-floor/verify.py
+python3.12 -I -B research/seven-query-xor-floor/independent.py
+python3.12 -I -B research/seven-query-xor-floor/test_package.py
+python3.12 -B scripts/research_package.py --package research/seven-query-xor-floor
+```
+
+Expected:
+
+```text
+PASS_SEVEN_QUERY_XOR_FLOOR Q=7 min_X=6 sharp X<=5 blocked answers_789q_oq1 no_new_kappa
+PASS_INDEPENDENT_SEVEN_QUERY_XOR_FLOOR min_X=6 floors_block_X_le_5 ... tariff=442 controls=2
+PASS_SEVEN_QUERY_XOR_FLOOR_PACKAGE_TESTS groups=6
+PASS_REGISTERED_RESEARCH_PACKAGE research/seven-query-xor-floor outcome=completed
+```
+
+Default verify is read-only and compares a fresh census to
+[CERTIFICATE.json](CERTIFICATE.json). Use `--write` only to regenerate that
+receipt. Admission uses `need()` (not `assert`); `-O` also passes.
+
+## Scope and overlap
+
+Base commit `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. Direct predecessors:
+PR1898 (minimum-query endpoint), open PR2455 (six-query XOR necessity), and the
+fork path-lowered 789q invoice (OQ1). Leave-alone objects through
+[#2593](https://github.com/CrocSwap/integer-mult-bounds/pull/2593) and the
+pending `mutable-source-789q-invoice` R-spectrum repair are not edited.
+
+Closest prior: PR2455 proves `X≥8` at `Q=6` and does not settle seven queries.
+The 789q package prices path-lowered `Q∈{7,8,9}` bills and leaves non-path
+`X≤2` open. This freestanding package closes that XOR-floor obligation at
+`Q=7` for the full restored alphabet.
+
+## Open next questions
+
+1. What is the minimum readout count `R` among restored seven-query words with
+   `X=6`? Why it matters: tariff `38·7 + 2R + 2·6` undercuts 436 iff `R≤78`.
+   First step: search restored length-6 shear words whose query schedule admits
+   even-subset (or cheaper) coverings with `R≤78`. Blocked by: no such covering
+   census is claimed here.
+2. Does the same component+census method give a sharp XOR floor at eight
+   queries? First step: extend the restored-graph census to the first length
+   with `n+c ≤ 8` and match an attaining word. Blocked by: larger search.
+
+## Credit
+
+Credit **Arham Tahir / PR1898** (alphabet, minimum-query endpoint, abstract
+tariff), **ywz65 / PR2455** (component lemma and meet-in-the-middle restored
+census at six queries; digests reused as cross-check), **PR1370** (path-local
+shear lowering), the fork **789q invoice** lineage (path-class champion and
+OQ1), **TennisBowling / PR1524**, **Ross Richardson / PR943**, and the retained
+mutable-source lineage. Live input pin:
+`research/mutable-source-shear-cost/CERTIFICATE.json` (ten-query four-X
+context). 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.