Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 41 additions & 0 deletions research/connector-pair-source-path-seed2cdb/CERTIFICATE.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
{
"result": "pair-source connector calls B_jk: z += B_j x_j + B_k x_k on the universal-connector-boundary five-source model",
"scope": "one added complete-call family; everything else of research/universal-connector-boundary's Exact interface unchanged",
"minimum_source_path_length": 10,
"prefixes": [0, 2, 3, 5, 13, 15, 30, 26, 10, 8, 0],
"word_steps": [2, 1, 6, 8, 2, 17, 4, 16, 2, 8],
"step_weights": [1, 1, 2, 1, 1, 2, 1, 1, 1, 1],
"step_call_types": ["B_1", "B_0", "B_12", "B_3", "B_1", "B_04", "B_2", "B_4", "B_1", "B_3"],
"multiplicities": [2, 4, 2, 2, 2],
"weight_sum": 12,
"coverage_count": 32,
"queries_all31_matrix": 72,
"lower_bound": {
"readout_queries": 62,
"source_path_length": ">= 10",
"nine_point_census": {
"sets": 7888725,
"covering": 0,
"max_coverage": 29,
"method": "recursive enumeration (search_paths.py) and independent itertools enumeration (verify.py --full) agree"
},
"counting_step": "C(8,2) = 28 < 31 so |P| >= 9; the census gives |P| >= 10; closure gives |P| <= L"
},
"predecessor": {
"package": "research/universal-connector-boundary",
"fixed_alphabet_queries": 74,
"fixed_alphabet_support_bound": "72, proven unattainable in the fixed alphabet (README: the support bound of 72 is unattainable; parity rules out 73)",
"fixture_b_leaf_prices": [1, 4, 10, 16, 28],
"predecessor_best_b_leaf_cost_min_relabeling": 120
},
"pricing": {
"b_leaf_cost_fixed_labeling": 126,
"b_leaf_cost_min_relabeling": 120,
"b_leaf_cost_max_relabeling": 174,
"leaves_forward_min_relabeling": 182,
"queries": 72,
"dispatch_break_even": "at the optimal labeling this schedule ties the predecessor's leaf cost exactly and saves 2 dispatch records; at the fixed fixture labeling it is +12 leaf charges versus -2 dispatch records, so it is favorable iff one query's dispatch/dispatch-record cost exceeds 6 leaf-price units"
},
"credit": "Aaron Wang, with help from opencode",
"base_commit": "51122344de9382e784c7f89953456d8cd55513ef"
}
11 changes: 11 additions & 0 deletions research/connector-pair-source-path-seed2cdb/EXPECTED.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
{
"fast": {
"command": "python3 -I -O -B research/connector-pair-source-path-seed2cdb/verify.py",
"expected_stdout_last_line": "PASS_CONNECTOR_PAIR_SOURCE_PATH"
},
"full_census": {
"command": "python3 -I -O -B research/connector-pair-source-path-seed2cdb/verify.py --full",
"expected_stdout_last_line": "PASS_CONNECTOR_PAIR_SOURCE_PATH_CENSUS",
"expected_census": {"sets": 7888725, "covering": 0, "max_coverage": 29}
}
}
137 changes: 137 additions & 0 deletions research/connector-pair-source-path-seed2cdb/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,137 @@
# Pair-source connector calls: five-source universal path of exactly ten, and the 72-query support bound attained

**Recursive-interface construction plus exact finite exclusion; no new kappa.**
Aaron Wang, with help from opencode.

Add exactly one operation family to the connector alphabet of
[research/universal-connector-boundary](../universal-connector-boundary/README.md):
the **pair-source connector call** `B_jk: z += B_j x_j + B_k x_k`, one complete
query depositing two sources at once, charged two coefficient/source accesses
and one query record. Everything else of that Exact interface is unchanged:
dirty rows, paired readouts, restoration of `z`, no free copies.

Result on the five-source, all-31-nonzero-row matrix:

| Quantity | Fixed alphabet (predecessor) | With pair-source calls |
|---|---:|---:|
| Minimum universal source path | 12 | 10 |
| Complete queries, all-31 matrix | 74 | 72 |
| Support bound `2*(5+31)` | 72, unattainable | 72, attained |
| Source-side leaf cost, best labeling | 120 | 120 |

The query optimum in the extended alphabet is **exactly 72**: 62 paired
readouts (each nonzero row needs two `A_i` calls) plus a source path of at
least 10, and the word below attains 10. In the fixed alphabet the same
support bound of 72 was proved unattainable by the 945-pairing census, and
parity ruled out 73.

## The word

Closed walk on `F_2^5`, one step per source query, step vectors of Hamming
weight 1 (single `B_j`) or 2 (pair `B_jk`):

```text
prefixes: 0 2 3 5 13 15 30 26 10 8 0
steps: 2 1 6 8 2 17 4 16 2 8
calls: B_1 B_0 B_12 B_3 B_1 B_04 B_2 B_4 B_1 B_3
```

The prefix set `P = {0,2,3,5,8,10,13,15,26,30}` has `P XOR P = F_2^5`
(verified two ways in `verify.py`). Place each output's two `A_i` readouts at
the two boundaries whose prefix XOR is its row mask; characteristic two makes
the dirty connector contributions cancel. Source multiplicities are
`(2,4,2,2,2)`, all even, so `z` is restored.

## Why ten is optimal

1. Each of the 31 nonzero masks needs its own unordered pair of prefixes, and
`C(8,2) = 28 < 31`, so `|P| >= 9`.
2. A complete census of all `C(31,8) = 7,888,725` nine-point sets of `F_2^5`
finds **zero** with `P XOR P = F_2^5`; maximum coverage is **29**. Two
independent implementations agree (recursive DFS in the discovery script;
`itertools.combinations` in `verify.py --full`). So `|P| >= 10`.
3. The walk is closed (`z` restoration), so `|P| <= L`; hence `L >= 10`, and
the word attains 10.

This is a finite computational exclusion for the stated interface, not an
impossibility theorem for other circuit models.

## Pricing (predecessor fixture)

Fixture: B factor leaf prices `1, 4, 10, 16, 28`; each `A` leaf price 1; every
call doubled for the inverse in the complete cost; dispatch `D` paid per root
query. Renaming sources preserves coverage, so free relabeling is granted on
both sides.

| Schedule | Queries | B leaves (min relabeling) | Total leaves |
|---|---:|---:|---:|
| This word, best labeling | 72 | 120 | 182 |
| This word, fixture labeling | 72 | 126 | 188 |
| Predecessor ten-call path | 74 | 118 | 182 |
| Predecessor twelve-call path | 74 | 120 | 182 |

At the best labeling this schedule ties the predecessor's leaf cost exactly
and saves 2 dispatch records, so the completed cost is strictly lower for any
positive per-query dispatch. At the fixed fixture labeling it pays
`+12` leaf charges (doubled) against `-2 D`, favorable iff one query's
dispatch/dispatch-record cost exceeds 6 leaf-price units. The tie at the best
labeling is optimal among 72-query schedules: a length-10 source path needs at
least one pair call (pure-single ten-call paths are excluded by the
predecessor's 945-pairing census), so its weight sum is at least 12, and
weight sum 12 with even multiplicities gives exactly this multiset.

## Verification

```sh
python3 -I -O -B research/connector-pair-source-path-seed2cdb/verify.py
```

Expected: `PASS_CONNECTOR_PAIR_SOURCE_PATH`. Checks the word (two coverage
recomputations), the dirty replay at `L = 1,2,3` with seeded dense
nonsymmetric noncommuting `F_2` maps and arbitrary dirty `x`, `z`, `y`
(exact boundary on all 31 outputs), three mutation controls (dropped call,
mutated step, misplaced readouts) that must all be rejected, and the pricing
numbers.

```sh
python3 -I -O -B research/connector-pair-source-path-seed2cdb/verify.py --full
```

Expected: `CENSUS {"sets": 7888725, "covering": 0, "max_coverage": 29}` then
`PASS_CONNECTOR_PAIR_SOURCE_PATH_CENSUS`. This is the exact nine-point census
behind `L >= 10`; it takes a few minutes.

## Scope and limits

- Exactly one added family (`B_jk`); a different extension is a different
question. Pair calls are charged, never free.
- No instance of this interface is claimed inside the selected supplier; this
is not a kappa claim and the selected record is unchanged. The `a < D/E`
diagnostic is not applicable: no supplier moment or recursive profile
changes here.
- The necessity side (62 readouts, two per nonzero row) inherits the
predecessor's specialization argument unchanged; only the source-path side
changes.
- The census covers nine-point sets exhaustively and finds the length-10 word
by seeded random search over covering sets (seed 4242, trial 911); minimality
rests on the census plus the counting bound, not on search exhaustion at 10.

## Open next questions

1. **Do triple-source calls `B_jkℓ` reach the readout-dominated floor?** The
source path could drop toward 8 or 9, but each call's leaf charge grows;
the same prefix-set method answers it. Blocker: none; a bounded census of
weight-3 steps is the first step.
2. **Six sources with pair calls.** The predecessor stops at the five-source
boundary. For six sources the counting bound gives `|P| >= 12`
(`C(11,2) = 55 < 63 <= C(12,2)`); does a pair-call universal path of length
12 exist? Blocker: the set census grows to `C(63,11)`; it needs a walkwise
search rather than a setwise one.
3. **Common-label realization of pair calls.** The predecessor leaves
realization open for single calls; a pair call needs two coefficient
accesses in one query record, which a real compiler must price.

Predecessor credit: `research/universal-connector-boundary` (fixed-alphabet
four/five-source boundary, 945-pairing census, 74-query optimum) and PR934's
three-by-three result. Claim thread:
https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18930631
30 changes: 30 additions & 0 deletions research/connector-pair-source-path-seed2cdb/SOURCES.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
{
"schema_version": 1,
"base_commit": "51122344de9382e784c7f89953456d8cd55513ef",
"files": [
{
"path": "docs/research/agent-task-catalog.json",
"usage": "provenance",
"git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1",
"sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"
},
{
"path": "research/universal-connector-boundary/README.md",
"usage": "provenance",
"git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f",
"sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476"
},
{
"path": "research/universal-connector-boundary/CERTIFICATE.json",
"usage": "provenance",
"git_blob": "079e3e1441dc07c2f0536e9527acf290e51ea9c0",
"sha256": "e733746ba3e5151c829b4e8728bfff5ae3ed24d8d203eb77c735d20758e8266a"
},
{
"path": "certificates/selected-result.json",
"usage": "provenance",
"git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
"sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
}
]
}
76 changes: 76 additions & 0 deletions research/connector-pair-source-path-seed2cdb/TASK.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,76 @@
{
"schema_version": 1,
"task_id": "connector-alphabet-change",
"original_card": {
"id": "connector-alphabet-change",
"question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?",
"starting_points": [
"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.",
"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."
],
"overlap_terms": [
"universal connector",
"source-toggle",
"connector alphabet"
]
},
"seed": "2cdb401748aa1ad1efaa95e93dcff850",
"track": "recursive-interfaces",
"priority_revision": 3,
"scope_key": "0c9f43f3c7d61edb36fe",
"base_commit": "51122344de9382e784c7f89953456d8cd55513ef",
"scope_status": "refined",
"scope_change_reason": "The card asks for one explicit alphabet extension with its implementation charged. Refined to the pair-source connector call family B_jk: z += B_j x_j + B_k x_k on the pinned five-source universal-connector-boundary model: one complete query per pair call, charged two coefficient/source accesses, no other interface change.",
"actual_scope": "Add exactly one operation family (pair-source connector calls B_jk) to the fixed single-source connector alphabet and determine the exact minimum universal source path and exact complete-query optimum for the five-source all-31-nonzero-row matrix in the extended alphabet, priced against the predecessor's fixture.",
"bottleneck_link": "The connector batch's complete queries are recursive-interface boundary work: the fixed alphabet's optimum 74 sat above the 72-query support bound which that alphabet proves unattainable. The pair family changes exactly this boundary cost: 74 -> 72, support bound attained.",
"stop_rule": "Stop when the exact minimum source path is pinned (construction plus exhaustive nine-point census), one fully priced comparison against the predecessor fixture is recorded, and the dirty replay and controls pass. No search beyond length 10 and no second alphabet family in this session.",
"evidence": "verify.py: word with D(w)=F2^5 by two recomputations, dirty replay at L=1,2,3 with seeded dense nonsymmetric noncommuting maps and exact boundary on all 31 outputs, three mutation controls rejected, exact pricing numbers; verify.py --full: independent itertools census of all 7,888,725 nine-point sets (0 covering, maximum coverage 29) excluding length 9.",
"outcome": "completed",
"author": "Aaron Wang",
"ai_assistance": "with help from opencode",
"open_questions": [
{
"question": "Do triple-source calls B_jkl lower the five-source universal path below ten, and at what leaf price?",
"why_it_matters": "Each added source per call raises leaf cost but could shorten the path; the prefix-set method answers it exactly and would locate the family-size optimum.",
"first_step": "Repeat the closed-walk census with steps of Hamming weight up to 3 (25 step types) at lengths 8 and 9, with the same counting lower bound.",
"blocked_by": "Nothing structural; it is a bounded enumeration, though larger than the weight-1/2 scan."
},
{
"question": "What is the pair-call universal path minimum for six sources?",
"why_it_matters": "The predecessor stops at the five-source boundary; six sources test whether the pair family scales or the covering sets become walkable only at large length.",
"first_step": "Establish the counting bound (|P| >= 12 since C(11,2) = 55 < 63 <= C(12,2)) and run a walkwise search at lengths 12 and 13 on F_2^6.",
"blocked_by": "The setwise census grows to C(63,11); a walkwise or meet-in-the-middle search is required instead."
},
{
"question": "How does a real compiler price a pair-source call's second coefficient access inside one query record?",
"why_it_matters": "The 72-query result assumes a pair call is one dispatch record with two coefficient/source accesses; the break-even against the fixed alphabet depends on that price.",
"first_step": "Instantiate one pair call in the universal-connector-boundary tape implementation sketch and count its instruction records and coefficient reads.",
"blocked_by": "The predecessor leaves common-label realization open even for single calls; this inherits that blocker."
}
],
"predecessor_credit": "research/universal-connector-boundary (fixed-alphabet four/five-source boundary, 945-pairing census, 74-query optimum) and PR934's three-by-three result.",
"time_cap": "one session; census capped at the nine-point scan; one bounded pivot maximum (none used)"
}
35 changes: 35 additions & 0 deletions research/connector-pair-source-path-seed2cdb/VERIFY.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
{
"schema_version": 1,
"status": "ready",
"python": "3.12",
"requirements": [],
"commands": [
{
"argv": [
"{python}",
"-I",
"-O",
"-B",
"{package}/verify.py"
],
"checks": "word (two coverage recomputations), dirty replay at L=1,2,3 with exact boundary, three mutation controls, pricing numbers",
"timeout_seconds": 300
},
{
"argv": [
"{python}",
"-I",
"-O",
"-B",
"{package}/verify.py",
"--full"
],
"checks": "exact nine-point census excluding length 9 (7,888,725 sets; zero covering; maximum coverage 29)",
"timeout_seconds": 600
}
],
"inputs": [
"research/connector-pair-source-path-seed2cdb/verify.py",
"research/connector-pair-source-path-seed2cdb/CERTIFICATE.json"
]
}
Loading
Loading