Research: prove even-subset R floor 82 among X=6 at seven queries (no new kappa)

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

@@ -0,0 +1,160 @@
+{
+  "schema_version": 1,
+  "status": "PASS_SEVEN_QUERY_R_FLOOR",
+  "scope": "Five-source common-B mutable-source Q/R/X alphabet (PR1898). Even-subset readout on connector states of restored straight-line words with exactly seven queries. Exact minimum R among words with X=6.",
+  "claim": {
+    "Q": 7,
+    "min_R_among_X_eq_6": 82,
+    "min_R_even_subset_all_walks": 82,
+    "sharp": true,
+    "answers_7qxor_oq1": "Minimum even-subset R among restored seven-query words with X=6 is exactly 82; R<=78 is impossible in this readout class, so the abstract tariff cannot undercut 436 via lower R at X=6.",
+    "no_new_kappa": true
+  },
+  "classification": {
+    "distinct_six_nonzero": {
+      "covering_sets": 583296,
+      "attainable_R": [
+        82,
+        88
+      ],
+      "histogram": {
+        "82": 97216,
+        "88": 486080
+      },
+      "first_witnesses": {
+        "82": [
+          0,
+          1,
+          2,
+          4,
+          8,
+          15,
+          16
+        ],
+        "88": [
+          0,
+          1,
+          2,
+          3,
+          4,
+          8,
+          16
+        ]
+      },
+      "min_R": 82
+    },
+    "one_repeat_spanning_five": {
+      "kind": "one_repeat_on_standard_basis",
+      "covering_walks": 1680,
+      "attainable_R": [
+        96
+      ],
+      "histogram": {
+        "96": 1680
+      },
+      "min_R": 96,
+      "first_witness": [
+        0,
+        1,
+        0,
+        2,
+        4,
+        8,
+        16
+      ],
+      "argument": "GL(5) reduces every spanning 5-set one-repeat covering walk to this basis census; R totals are invariant. Only R=96 occurs."
+    },
+    "span_obstruction_samples": [
+      {
+        "labels": [
+          1,
+          2,
+          4,
+          8
+        ],
+        "rank": 4,
+        "best_even_subset_image_size": 16,
+        "covers_all_31": false,
+        "note": "rank4_omit_16"
+      },
+      {
+        "labels": [
+          1,
+          2,
+          3,
+          4,
+          5
+        ],
+        "rank": 3,
+        "best_even_subset_image_size": 8,
+        "covers_all_31": false,
+        "note": "rank3_dependent_five"
+      },
+      {
+        "labels": [
+          1,
+          2,
+          4,
+          8,
+          3
+        ],
+        "rank": 4,
+        "best_even_subset_image_size": 16,
+        "covers_all_31": false,
+        "note": "rank4_five_with_sum"
+      }
+    ],
+    "argument": "A covering even-subset slot list of length 7 must span F2^5, so it uses at least five linearly independent nonzero labels. With six intermediate slots after the leading 0, the covering cases are: (i) six distinct nonzero labels (Hamilton walks; R in {82,88}); (ii) five spanning nonzero labels with exactly one repeated vertex (R=96 on the GL(5) basis census). Fewer independent labels cannot cover. Therefore min R = 82."
+  },
+  "xor_floor_citation": {
+    "object": "research/seven-query-xor-floor (CrocSwap #2643)",
+    "statement": "Every restored seven-query word needs X>=6; sharp via the same champion.",
+    "use_here": "Together with min even-subset R=82, every X=6 word has R>=82.",
+    "not_reopened": true
+  },
+  "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 / seven-query-xor-floor lineage; PR1898 alphabet."
+  },
+  "tariff": {
+    "complete_prices": {
+      "b": 38,
+      "a": 2,
+      "x": 2
+    },
+    "six_query_endpoint": 436,
+    "beat_436_at_Q7_X6_requires_R_le": 78,
+    "min_tariff_at_Q7_X6": 442,
+    "undercuts_436": false
+  },
+  "new_kappa": false
+}

research/seven-query-r-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 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` — distinct-slot
+  `R ∈ {82,88}` spectrum and champion path; that package is not edited.
+- Open #2643 `research/seven-query-xor-floor` — restored `X ≥ 6` at `Q = 7`
+  and OQ1 answered here; that package is not edited.
+- Live pin: `research/mutable-source-shear-cost/CERTIFICATE.json`.
+
+Prepared by Wentao Li (VictorLiwentao, @Is__Victor) with substantial AI
+assistance.

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

@@ -0,0 +1,96 @@
+# Exact even-subset readout floor at seven queries among X = 6
+
+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 readout optimum
+outside the even-subset connector-state class.
+
+It answers open question 1 of
+[CrocSwap/integer-mult-bounds#2643](https://github.com/CrocSwap/integer-mult-bounds/pull/2643)
+(`research/seven-query-xor-floor`): what is the minimum readout count `R`
+among restored seven-query words with `X = 6`? Under even-subset readout on
+connector states, the answer is **exactly 82**.
+
+## Setup
+
+Retain five distinct arbitrary-dirty F₂ source rows, thirty-one outputs, a
+connector, and private scratch. Complete calls are `Q_j`, `R_m`, and paid
+`X_(s,t)` as in PR1898. Straight-line words are data-independent; sources and
+connector restore.
+
+Each query contributes an effective F₂⁵ mask (the current linear form of the
+queried source). Connector restoration forces those seven masks to sum to
+zero, so the connector state follows a **closed walk of length 7** in F₂⁵.
+Even-subset readout prices a slot list `(s₀,…,s₆)` with `s₀ = 0` by
+
+```text
+R = Σ_{m=1}^{31} min{|T| : T ⊂ {0,…,6}, |T| even, ⊕_{i∈T} s_i = m}.
+```
+
+Zero query edges are forbidden, so consecutive slots differ and the return
+edge to 0 is present (`s₆ ≠ 0`).
+
+## Classification of covering walks
+
+A covering slot list must realize every nonzero mask, so the F₂-span of its
+slot values is all of F₂⁵. Hence it uses at least five linearly independent
+nonzero labels. With only six slots after the leading 0, the covering cases
+are:
+
+1. **Six distinct nonzero labels.** The intermediate slots are a permutation
+   of those labels (Hamilton walks on `{0} ∪ S`). Exhaustive even-subset
+   census over all `C(31,6)` choices yields covering sets only, with
+   attainable totals **`R ∈ {82, 88}`** (histogram `97216` / `486080`).
+2. **Five spanning nonzero labels with exactly one repeated vertex.** Any
+   such spanning 5-set is `GL(5)`-equivalent to the standard basis
+   `{1,2,4,8,16}`, and the even-subset total `R` is `GL(5)`-invariant.
+   The basis census of valid one-repeat walks (extra visit to `0`, or one
+   basis vector doubled) covers in every case with **`R = 96` only**
+   (`1680` walks).
+3. **Fewer than five independent nonzero labels.** The even-subset image lies
+   in a proper subspace, so some masks are missed. Explicit dependent samples
+   stay at image size `≤ 16`.
+
+Therefore every covering Q=7 even-subset schedule has `R ∈ {82, 88, 96}`, and
+the global minimum is **82**.
+
+## Minimum R among X = 6
+
+Open [#2643](https://github.com/CrocSwap/integer-mult-bounds/pull/2643) proves
+that every restored seven-query word needs `X ≥ 6` (sharp). Combined with
+`R ≥ 82` in the even-subset class, every restored seven-query word with
+`X = 6` has even-subset `R ≥ 82`.
+
+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)`).
+Dirty root and inverse identities hold. Thus the minimum is **exactly 82**.
+
+## Tariff consequence
+
+At `Q = 7` and `X = 6`, tariff `38·7 + 2R + 2·6 = 278 + 2R` undercuts the
+six-query endpoint **436** iff `R ≤ 78`. The floor `R = 82` gives tariff
+**442** and blocks that undercut inside the even-subset class.
+
+## Scope limits
+
+- No claim about readout alphabets cheaper than even-subset connector-state
+  combinations (odd-cardinality schedules, output mixing, extra connectors).
+- Leave-alone objects through #2643 (including #2593 triadic and the XOR
+  floor package) and pending `mutable-source-789q-invoice` are not edited.
+- No physical common-B hosting, precision, tape, or new kappa.
+
+## Relation to predecessors
+
+| Prior | Already proves | This package adds |
+|---|---|---|
+| PR1898 | Min `Q = 6`, endpoint tariff 436 | — |
+| PR2455 (open) | `X ≥ 8` at `Q = 6` | — |
+| 789q invoice (fork) | Path-class distinct-slot `R ∈ {82,88}` at `Q = 7` | — |
+| #2643 seven-query XOR floor | `X ≥ 6` at `Q = 7`, sharp; OQ1 asks min `R` at `X = 6` | — |
+| **This** | — | **Min even-subset `R` at `Q = 7` is 82 even with repeats; hence min `R` among `X = 6` is 82** |

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

@@ -0,0 +1,95 @@
+# Seven-query even-subset R floor among X = 6 is exactly 82
+
+**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** and even-subset
+connector-state readout needs **at least 82 readouts**. Among words with
+**`X = 6`**, that floor is sharp: the 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
+[#2643](https://github.com/CrocSwap/integer-mult-bounds/pull/2643)
+(`research/seven-query-xor-floor`): the minimum `R` among restored seven-query
+words with `X = 6` is **exactly 82** in the even-subset class. In particular
+`R ≤ 78` is impossible, so tariff `38·7 + 2R + 2·6` cannot undercut the
+six-query endpoint **436** by lowering `R` at `X = 6`.
+
+| Covering walk class | Distinct nonzero labels | Attainable even-subset R |
+|---|---:|---|
+| Hamilton (distinct slots) | 6 | **{82, 88}** |
+| One repeated vertex (GL basis census) | 5 spanning | **{96}** |
+| Rank `< 5` label sets | ≤4 independent | none (image ≤16) |
+
+The distinct-slot spectrum matches the path-lowered 789q invoice. Allowing
+repeated prefixes cannot beat 82: the only additional covering layer is
+`R = 96`. Combined with #2643's restored XOR floor `X ≥ 6`, every `X = 6`
+word has `R ≥ 82`.
+
+## Reproduce
+
+Python **3.12**, standard library only, from the repository root:
+
+```sh
+python3.12 -I -B research/seven-query-r-floor/verify.py
+python3.12 -I -O -B research/seven-query-r-floor/verify.py
+python3.12 -I -B research/seven-query-r-floor/independent.py
+python3.12 -I -B research/seven-query-r-floor/test_package.py
+python3.12 -B scripts/research_package.py --package research/seven-query-r-floor
+```
+
+Expected:
+
+```text
+PASS_SEVEN_QUERY_R_FLOOR Q=7 min_R_among_X=6 is 82 sharp repeat_layer_R=96 answers_7qxor_oq1 tariff_floor=442 no_new_kappa
+PASS_INDEPENDENT_SEVEN_QUERY_R_FLOOR min_R=82 ... tariff=442 answers_7qxor_oq1
+PASS_SEVEN_QUERY_R_FLOOR_PACKAGE_TESTS groups=6
+PASS_REGISTERED_RESEARCH_PACKAGE research/seven-query-r-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, open PR2455, fork path-lowered `mutable-source-789q-invoice` (distinct
+slot spectrum; not edited), and open #2643 seven-query XOR floor (OQ1; leave
+alone). Leave-alone through #2643 including #2593 triadic is respected.
+
+Closest prior: 789q prices path-class distinct-slot `R ∈ {82,88}` but does not
+classify repeated-prefix coverings; #2643 proves `X ≥ 6` and leaves min `R` at
+`X = 6` open. This freestanding package closes that readout obligation.
+
+## Open next questions
+
+1. Can a readout alphabet strictly cheaper than even-subset connector-state
+   combinations reach `R ≤ 78` at `Q = 7` with `X = 6`?
+   Why it matters: only then could seven queries undercut tariff 436 at the
+   #2643 XOR floor. First step: define one priced odd-cardinality or
+   multi-connector readout model and re-run the walk census. Blocked by: no
+   cheaper covering witness is known.
+2. Does the same walk classification give an exact min `R` at eight queries
+   with the #2643-style XOR floor?
+   Why it matters: completes the intermediate-query unequal-price handoff.
+   First step: extend covering censuses to length-8 walks (including repeats).
+   Blocked by: larger search.
+
+## Credit
+
+Credit **Arham Tahir / PR1898** (alphabet, minimum-query endpoint, abstract
+tariff), **ywz65 / PR2455** (six-query XOR necessity), **PR1370** (path-local
+shear lowering), the fork **789q invoice** lineage (distinct-slot spectrum and
+champion), open **#2643** (XOR floor; OQ1 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.