Prove triple-source connector steps keep the 72-query floor.

research/connector-triple-query-floor/PROOF.md

@@ -0,0 +1,46 @@
+# Proof notes: triple steps and the five-source query floor
+
+The verifier enumerates sets. This note records the inequalities those
+numbers are attached to. It is not a second census.
+
+## Prefix length
+
+A closed walk of `L` steps has `L + 1` prefix positions with the last equal
+to the first, so its image `P` satisfies `|P| <= L`. Each unordered pair of
+distinct prefixes contributes one difference. Covering 31 nonzero masks
+requires `C(|P|, 2) >= 31`. `C(8, 2) = 28` is short, so `|P| >= 9` and
+`L >= 9`.
+
+`P XOR P` is unchanged by adding a constant to every prefix. For any
+nonempty `P` and any `t in P`, the translate `P + t` contains `0` and has
+the same difference set. The sets that contain `0` are therefore enough.
+There are `C(31, 8) = 7,888,725` of them. The program finds that none is a
+difference basis of `F_2^5`, and that 28 is the maximum number of distinct
+nonzero differences. Including `0` gives at most 29 of the 32 masks, which
+matches the maximum stated by the pair-source package. Hence `|P| >= 10`
+and `L >= 10`.
+
+Each of the 31 outputs still needs two readout calls. The query count is at
+least `62 + L >= 72`. The bound never inspects the Hamming weight of a
+step. Weight 3, 4, and 5 are included.
+
+## Leaves at length 10
+
+An unused source keeps every difference inside a coordinate hyperplane,
+which has 15 nonzero vectors. Every source incidence `m_j` is therefore a
+positive even integer, so `m_j >= 2` and `W = sum m_j >= 10`.
+
+`W` is also the sum of the `L` step weights. For `L = 10`, that sum equals
+10 only if every step has weight 1. A step of weight at least 2 forces
+`W >= 11`. Even summands make `W` even, so `W >= 12`.
+
+The only nondecreasing 5-tuple of even integers `>= 2` summing to 12 is
+`(2, 2, 2, 2, 4)`. Against prices `(1, 4, 10, 16, 28)`, the cheap assignment
+costs `4*1 + 2*(4+10+16+28) = 120`. A length-10 step has weight at most 5,
+so `W <= 50`. The verifier enumerates every admissible multiplicity type
+for each even total from 14 through 50. Each of those bills is at least
+122.
+
+The published 10-point set covers. Whether a triple-using walk meets leaf
+bill 120 is left open. The query lower bound does not depend on that
+witness.

research/connector-triple-query-floor/README.md

@@ -0,0 +1,128 @@
+# Triple-source connector steps do not lower the five-source query floor
+
+**Negative bound for one charged alphabet extension; no new κ.** Selected κ
+stays `0.001672660197076918`.
+
+The pair-source package attains 72 complete queries on the five-source
+all-31-nonzero-mask connector batch, and asks whether a triple-source call
+`B_{jkℓ}` can push the source path down to length 8 or 9. It cannot. The
+obstruction is the prefix set, not the step weights. Every closed walk whose
+pairwise prefix differences include all 31 nonzero masks has length at least
+10, for steps of weight 1, 2, 3, 4, or 5. The batch therefore costs at least
+`62 + 10 = 72` queries. Weight-at-most-2 calls already attain 72, so charging
+a triple call as one query plus three source-leaf accesses does not improve
+that query bill.
+
+On any covering closed walk of length 10 that uses a step of weight at least
+2, the source-leaf bill at prices `(1, 4, 10, 16, 28)` is at least 120 after
+assigning the repeated source to the cheapest price. The published pair-call
+word meets 120. A triple does not undercut it.
+
+## Contract
+
+The fixed interface is the one in
+`research/universal-connector-boundary`: five immutable sources, one
+arbitrarily dirty connector, and 31 nonzero output rows, each read twice.
+The connector is restored at completion. Prefix differences of the source
+walk are the available masks.
+
+The added operation is a triple-source call
+
+```text
+B_{jkℓ}: z += B_j x_j + B_k x_k + B_ℓ x_ℓ
+```
+
+one query record and three coefficient/source accesses. It is not free. The
+same prefix argument also covers weight-4 and weight-5 steps. No selected
+caller, native layout, or supplier admission is claimed.
+
+## Argument
+
+Let `P` be the set of source-prefix values on a closed walk of `L` steps.
+The last prefix repeats the first, so `|P| <= L`. Distinct nonzero
+differences need `C(|P|, 2) >= 31`. Thus `|P| >= 9`, because
+`C(8, 2) = 28 < 31`, and `L >= 9`.
+
+Differences are translation-invariant, and every nonempty set has a
+translate containing `0`. It is enough to inspect the `C(31, 8) = 7,888,725`
+nine-point sets that contain `0`. None of them satisfies `P XOR P = F_2^5`.
+The largest number of distinct nonzero differences is 28, which is 29 masks
+once the automatic zero difference is counted. That is the same maximum
+coverage 29 reported for nine-point sets by
+`research/connector-pair-source-path-seed2cdb`. Therefore `|P| >= 10` and
+`L >= 10`.
+
+Two scans produce the same count, cover count, maximum, and checksum: an
+index odometer, and `itertools.combinations`. Neither imports the
+predecessor verifier.
+
+A coordinate hyperplane has only 15 nonzero vectors. A covering walk
+therefore uses every source a positive even number of times, so the
+incidence total `W` is at least 10. On a walk of length 10, `W = 10` only
+when every step has weight 1. One step of weight at least 2 forces
+`W >= 11`, and even multiplicities force `W` even, hence `W >= 12`. The
+only five even parts of 12 that are all at least 2 are `(2, 2, 2, 2, 4)` up
+to order. Pairing multiplicity 4 with price 1 costs
+
+```text
+4*1 + 2*(4 + 10 + 16 + 28) = 120.
+```
+
+Step weight is at most 5, so `W <= 50` on a length-10 walk. Every admissible
+multiplicity type with even total from 14 through 50 costs at least 122.
+
+The published prefixes `{0, 2, 3, 5, 8, 10, 13, 15, 26, 30}` cover all 31
+nonzero masks. Deleting any one of them destroys that cover. This checks the
+length-10 side of the same difference test; it does not rerun the
+predecessor's dirty-map replay.
+
+## What this does not show
+
+The census is a finite exclusion in `F_2^5`, not a classification of every
+connector program. It does not decide whether some length-10 walk that uses
+a triple attains leaf bill 120. It does not rerun the 945 weight-1 pairing
+census, and it does not need that census: the query floor never uses it.
+Six sources, delivery cuts, frames, and a physical caller remain outside
+this contract. Unknown native costs are not zero. There is no new κ.
+
+## Reproduce
+
+From the repository root, CPython 3.12, standard library only. The census
+took about 70 seconds on the recording host; the manifest allows 240.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/connector-triple-query-floor
+```
+
+Expected:
+
+```text
+PASS_CONNECTOR_TRIPLE_QUERY_FLOOR sets=7888725 covering=0 max_nonzero=28 max_masks=29 queries=72 leaves=120 no_new_kappa
+PASS_REGISTERED_RESEARCH_PACKAGE research/connector-triple-query-floor outcome=negative-result
+```
+
+## Credit
+
+The five-source paired-readout model and the 74-query fixed alphabet are
+Ross Richardson's `research/universal-connector-boundary`. The 72-query
+pair-call word, the nine-point census target, and open question 1 are Aaron
+Wang's `research/connector-pair-source-path-seed2cdb`. The all-tariff
+formula for the old alphabet is Adam Gall's. New census, length bound, and
+leaf comparison by unpaidmoon, with substantial AI assistance (Cursor Grok
+4.7). Apache-2.0. No independent human or proof-kernel review is claimed.
+
+## Open next questions
+
+1. Does any closed length-10 walk that uses one triple-source step attain
+   source-leaf bill 120 on prices `(1, 4, 10, 16, 28)`? The query floor does
+   not depend on the answer; a witness would show the leaf bound is sharp
+   inside the larger alphabet. First step: search multiplicity type
+   `(4, 2, 2, 2, 2)` with exactly one weight-3 step and check prefix
+   coverage. Nothing structural blocks that search. It is larger than this
+   session's census, and a failure would not reopen length 9.
+2. For six sources, counting already gives `|P| >= 12` at every step weight,
+   because `C(11, 2) = 55 < 63`. Does a 12-point difference basis exist?
+   That decides whether the query floor sits at `2*63 + 12` before any walk
+   constraint. First step: a structure theorem or a symmetry-reduced census
+   of 12-point sets in `F_2^6`. The unrestricted binomial count blocks a
+   direct copy of this package's scan.

research/connector-triple-query-floor/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/connector-triple-query-floor/TASK.json

@@ -0,0 +1,68 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "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": "refined",
+  "actual_scope": "Charge a triple-source connector call as one query and three source accesses, and decide whether that family can shorten the five-source universal source path below 10.",
+  "scope_change_reason": "The card asks for one charged alphabet extension and a target-specific bound. This package takes the triple-source family left open by the pair-source path, on the same five-source paired-readout contract, and proves that the extension does not lower the 72-query or 120-leaf floors. It does not search for a saving.",
+  "bottleneck_link": "Connector query count is recursive-interface boundary work. The fixed alphabet costs 74 and pair calls attain the 72-query support bound. A triple call would matter only if it reduced that boundary; the prefix-set floor says it does not.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the nine-point census, the length-10 leaf comparison, and the failure controls agree. Do not search for a length-10 triple witness or open a six-source census.",
+  "outcome": "negative-result",
+  "evidence": "Two nine-point censuses of all 7,888,725 sets containing 0 agree: 0 covers, maximum 28 nonzero differences (29 masks including 0). Counting excludes 8. Published 10-point prefixes cover, and each one-point deletion fails. Length-10 walks with a step of weight >= 2 have source-leaf bill at least 120 at prices (1, 4, 10, 16, 28).",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial AI assistance from Cursor Grok 4.7 for the census, the leaf enumeration, and the writeup.",
+  "open_questions": [
+    {
+      "question": "Does a closed length-10 walk with one triple-source step attain source-leaf bill 120?",
+      "why_it_matters": "The query floor is already 72 without that witness. Attainment would show the leaf bound is sharp inside the triple alphabet.",
+      "first_step": "Search multiplicity type (4, 2, 2, 2, 2) with exactly one weight-3 step and test prefix coverage.",
+      "blocked_by": "Nothing structural. A negative search would not reopen length 9."
+    },
+    {
+      "question": "Does F_2^6 have a 12-point difference basis?",
+      "why_it_matters": "Counting gives |P| >= 12 at every step weight because C(11, 2) = 55 < 63. A 12-point basis would pin the six-source query floor before walk constraints.",
+      "first_step": "Prove a structure theorem or run a symmetry-reduced census of 12-point sets in F_2^6.",
+      "blocked_by": "The unrestricted binomial coefficient is too large for this package's direct scan."
+    }
+  ]
+}

research/connector-triple-query-floor/VERIFY.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 240,
+      "checks": "counting bound, two nine-point censuses, published 10-set and deletions, leaf bills for weights 12 through 50"
+    }
+  ]
+}