diff --git a/research/connector-triple-query-floor/PROOF.md b/research/connector-triple-query-floor/PROOF.md new file mode 100644 index 0000000000..e52550af82 --- /dev/null +++ b/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. diff --git a/research/connector-triple-query-floor/README.md b/research/connector-triple-query-floor/README.md new file mode 100644 index 0000000000..c290f6381d --- /dev/null +++ b/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. diff --git a/research/connector-triple-query-floor/SOURCES.json b/research/connector-triple-query-floor/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/connector-triple-query-floor/TASK.json b/research/connector-triple-query-floor/TASK.json new file mode 100644 index 0000000000..512c446fc5 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/connector-triple-query-floor/VERIFY.json b/research/connector-triple-query-floor/VERIFY.json new file mode 100644 index 0000000000..8468e8a072 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/connector-triple-query-floor/verify.py b/research/connector-triple-query-floor/verify.py new file mode 100644 index 0000000000..0d063b4147 --- /dev/null +++ b/research/connector-triple-query-floor/verify.py @@ -0,0 +1,152 @@ +#!/usr/bin/env python3 +"""Triple-source connector steps do not lower the five-source query floor. + +The paired-readout contract needs 31 nonzero prefix differences and a closed +walk, so the prefix set P satisfies |P| <= L and C(|P|, 2) >= 31. Counting +gives |P| >= 9. An exhaustive census of the 7,888,725 nine-point sets that +contain 0 shows none have difference set F_2^5, so L >= 10 and the batch +costs at least 72 queries. Step weight never enters that argument: a +triple-source call is one more legal step, not a shorter prefix set. + +A second census walks itertools combinations and must match the odometer +totals. Failure controls reject an 8-point cover, a deleted prefix of the +published length-10 set, and a leaf bill below 120 for any length-10 walk +that uses a step of weight at least 2. +""" + +from itertools import combinations + +PRICES = (1, 4, 10, 16, 28) +PUBLISHED_PREFIXES = (0, 2, 3, 5, 8, 10, 13, 15, 26, 30) +NONZERO = (1 << 32) - 2 + + +def fail(message): + raise SystemExit("FAIL " + message) + + +def nonzero_mask(points): + seen = 0 + for i, left in enumerate(points): + for right in points[i + 1:]: + seen |= 1 << (left ^ right) + return seen + + +def census_odometer(): + """Nine-point sets containing 0, as 8-subsets of {1,...,31}.""" + index = list(range(8)) + count = covering = max_nonzero = 0 + checksum = 0 + while True: + points = (0,) + tuple(item + 1 for item in index) + seen = nonzero_mask(points) + count += 1 + width = seen.bit_count() + if width > max_nonzero: + max_nonzero = width + if seen == NONZERO: + covering += 1 + checksum = (checksum + seen) & 0xFFFFFFFFFFFFFFFF + cursor = 7 + while cursor >= 0 and index[cursor] == 23 + cursor: + cursor -= 1 + if cursor < 0: + break + index[cursor] += 1 + for follower in range(cursor + 1, 8): + index[follower] = index[follower - 1] + 1 + return count, covering, max_nonzero, checksum + + +def census_combinations(): + count = covering = max_nonzero = 0 + checksum = 0 + for choice in combinations(range(1, 32), 8): + seen = nonzero_mask((0,) + choice) + count += 1 + width = seen.bit_count() + if width > max_nonzero: + max_nonzero = width + if seen == NONZERO: + covering += 1 + checksum = (checksum + seen) & 0xFFFFFFFFFFFFFFFF + return count, covering, max_nonzero, checksum + + +def even_multiplicity_types(total): + """Nondecreasing 5-tuples of even integers >= 2 that sum to total.""" + found = [] + + def walk(remaining, slots, start, prefix): + if slots == 1: + if remaining >= start and remaining % 2 == 0: + found.append(prefix + (remaining,)) + return + value = start + while value <= remaining - 2 * (slots - 1): + if value % 2 == 0: + walk(remaining - value, slots - 1, value, prefix + (value,)) + value += 2 + + walk(total, 5, 2, ()) + return found + + +def leaf_bill(multiplicities): + """Pair the largest incidence with the cheapest source price.""" + ordered = tuple(sorted(multiplicities, reverse=True)) + return sum(incidence * price for incidence, price in zip(ordered, PRICES)) + + +def main(): + if (8 * 7) // 2 != 28 or 28 >= 31: + fail("eight prefixes can cover 31 nonzero masks") + if (9 * 8) // 2 < 31: + fail("counting already excludes nine prefixes") + + hyperplane = [value for value in range(32) if value & 1 == 0] + if nonzero_mask(hyperplane).bit_count() != 15: + fail("a coordinate hyperplane was not limited to 15 nonzero differences") + + published = nonzero_mask(PUBLISHED_PREFIXES) + if published.bit_count() != 31: + fail("published length-10 prefix set does not cover F_2^5") + for dropped in PUBLISHED_PREFIXES: + shortened = tuple(point for point in PUBLISHED_PREFIXES if point != dropped) + if len(shortened) != 9 or nonzero_mask(shortened) == NONZERO: + fail("deleting one published prefix still covered every mask") + + odometer = census_odometer() + combined = census_combinations() + if odometer != combined: + fail("odometer census %s disagrees with combinations %s" % (odometer, combined)) + count, covering, max_nonzero, _checksum = odometer + if count != 7888725 or covering != 0 or max_nonzero != 28: + fail("nine-point census returned %s" % (odometer,)) + + # Masks including the automatic zero difference: 28 + 1 = 29 of 32. + if max_nonzero + 1 != 29: + fail("mask count including zero is not the predecessor's 29") + + types_12 = even_multiplicity_types(12) + if types_12 != [(2, 2, 2, 2, 4)]: + fail("weight 12 has unexpected multiplicity types %s" % (types_12,)) + if leaf_bill(types_12[0]) != 120: + fail("minimum length-10 leaf bill is not 120") + # Length 10 admits step weight at most 5, so W <= 50. + for total in range(14, 51, 2): + bills = [leaf_bill(item) for item in even_multiplicity_types(total)] + if not bills or min(bills) <= 120: + fail("weight %d undercuts the leaf floor: %s" % (total, bills)) + + print( + "PASS_CONNECTOR_TRIPLE_QUERY_FLOOR" + " sets=%d covering=%d max_nonzero=%d max_masks=%d" + " queries=72 leaves=120 no_new_kappa" + % (count, covering, max_nonzero, max_nonzero + 1) + ) + + +if __name__ == "__main__": + main()