From ce50fccd8086bfeb8a61cc9eded572fb4741c387 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 08:36:44 +0530 Subject: [PATCH] Independent verification: stdlib re-certification of the eight-transfer threshold with all 2,502 solutions (no new kappa) PR1615 (bbMisk) first proved that the PR1438/PR1498 free-port two-connector family needs exactly eight transfers. This concurrent, code-disjoint package agrees with every overlapping PR1615 number and adds: a standard-library certificate of the exclusion and exact count that runs in the generic package hook (gap-reduction lemma), cross-checked by full-placement C and per-occurrence numpy engines; the complete eight-transfer solution set (2,502 canonical schedules, only port splits r=1 with 2,376 and r=5 with 126, all replayed as 80-call programs); and the exact four-transfer split maxima (PR1498's r=2 bound of 25 is not attained; the maximum is 21). Seed 58, connector-alphabet-change (refined). Prepared with substantial Anthropic Claude assistance. --- .../EXPECTED.json | 161 ++++++++++ .../README.md | 203 ++++++++++++ .../REMOTE-SOURCES.json | 15 + .../SOURCES.json | 30 ++ .../TASK.json | 66 ++++ .../VERIFY.json | 45 +++ .../engine.py | 106 ++++++ .../independent/census.c | 81 +++++ .../independent/census_numpy.py | 185 +++++++++++ .../references/PR1498-README.md | 303 ++++++++++++++++++ .../replay.py | 97 ++++++ .../verify.py | 184 +++++++++++ 12 files changed, 1476 insertions(+) create mode 100644 research/two-connector-eight-transfer-census-seed58/EXPECTED.json create mode 100644 research/two-connector-eight-transfer-census-seed58/README.md create mode 100644 research/two-connector-eight-transfer-census-seed58/REMOTE-SOURCES.json create mode 100644 research/two-connector-eight-transfer-census-seed58/SOURCES.json create mode 100644 research/two-connector-eight-transfer-census-seed58/TASK.json create mode 100644 research/two-connector-eight-transfer-census-seed58/VERIFY.json create mode 100644 research/two-connector-eight-transfer-census-seed58/engine.py create mode 100644 research/two-connector-eight-transfer-census-seed58/independent/census.c create mode 100644 research/two-connector-eight-transfer-census-seed58/independent/census_numpy.py create mode 100644 research/two-connector-eight-transfer-census-seed58/references/PR1498-README.md create mode 100644 research/two-connector-eight-transfer-census-seed58/replay.py create mode 100644 research/two-connector-eight-transfer-census-seed58/verify.py diff --git a/research/two-connector-eight-transfer-census-seed58/EXPECTED.json b/research/two-connector-eight-transfer-census-seed58/EXPECTED.json new file mode 100644 index 0000000000..517ceb3d9a --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/EXPECTED.json @@ -0,0 +1,161 @@ +{ + "zero": { + "restored": 30240, + "max_by_split": { + "0": 31, + "1": 17, + "2": 11, + "3": 11, + "4": 17, + "5": 31 + }, + "histogram_sha256": "ea0992346256fcf4d50a3307274013c796e46338ed47396c332c34dd6e09703f" + }, + "four": { + "max_by_split": { + "0": 31, + "1": 31, + "2": 21, + "3": 17, + "4": 19, + "5": 31 + }, + "pr1498_split_bounds": { + "0": 31, + "1": 31, + "2": 25, + "3": 17, + "4": 19, + "5": 31 + }, + "restored": 8994240, + "histogram_sha256": "81342993c98b860dac1e9120ae549dfdbb87f89893fba501574b1e62eeaefa5f" + }, + "six": { + "restored": 44936640, + "max_by_split": { + "0": 31, + "1": 31, + "2": 28, + "3": 22, + "4": 23, + "5": 31 + }, + "histogram_sha256": "4d33ab99d91ef7a8f70f203dc5bbba20592aafb57dbaa93e1de9579d21fcfcd5" + }, + "eight": { + "restored": 124284240, + "max_by_split": { + "0": 31, + "1": 32, + "2": 31, + "3": 27, + "4": 24, + "5": 32 + }, + "universal": 2502, + "universal_by_split": { + "1": 2376, + "5": 126 + }, + "universal_sha256": "ba04f2775171c9c32ae45406415c97a0440338a510266d9b758bf82da3ea7da0", + "discussion1412_pilot": { + "word": [ + 0, + 1, + 2, + 0, + 3, + 1, + 4, + 2, + 3, + 4 + ], + "ports": 31, + "gaps": [ + 0, + 1, + 1, + 2, + 1, + 0, + 1, + 0, + 1, + 1, + 0 + ] + } + }, + "independent_full_placement_receipts": { + "engine": "independent/census.c (every C placement, no gap reduction)", + "four": { + "candidates": 30270240, + "restored": 10402560, + "universal": 0, + "max_by_split": { + "0": 31, + "1": 31, + "2": 21, + "3": 17, + "4": 19, + "5": 31 + } + }, + "six": { + "candidates": 242161920, + "restored": 74692800, + "universal": 0, + "max_by_split": { + "0": 31, + "1": 31, + "2": 28, + "3": 22, + "4": 23, + "5": 31 + } + }, + "eight": { + "candidates": 1323241920, + "restored": 384199200, + "universal": 2502, + "max_by_split": { + "0": 31, + "1": 32, + "2": 31, + "3": 27, + "4": 24, + "5": 32 + } + } + }, + "independent_per_occurrence_receipts": { + "engine": "independent/census_numpy.py (each occurrence chooses its port; exact z1 restoration filter)", + "four": { + "legal": 10402560, + "universal": 0, + "max_by_split": { + "0": 31, + "1": 31, + "2": 21, + "3": 17, + "4": 19, + "5": 31 + } + }, + "six": { + "legal": 74692800, + "universal": 0, + "max_by_split": { + "0": 31, + "1": 31, + "2": 28, + "3": 22, + "4": 23, + "5": 31 + }, + "seconds_on_one_core": 842 + } + } +} diff --git a/research/two-connector-eight-transfer-census-seed58/README.md b/research/two-connector-eight-transfer-census-seed58/README.md new file mode 100644 index 0000000000..892a201e96 --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/README.md @@ -0,0 +1,203 @@ +# Independent verification of the eight-transfer threshold, with all 2,502 solutions + +**Independent verification; no new κ.** Seed 58 (recursive interfaces), card +`connector-alphabet-change`, refined scope recorded in [TASK.json](TASK.json). +Base `0b1cccf8`; the catalogue is at priority revision 3, which leaves this card +unchanged. + +The threshold theorem is **not new here**. Hanson Sun's (bbMisk) +[PR1615](https://github.com/CrocSwap/integer-mult-bounds/pull/1615), at head +`96916897`, answered first: + +- **PR1498's question.** It answers open question 1 of bitplane's + [PR1498](https://github.com/CrocSwap/integer-mult-bounds/pull/1498): six + transfers fail for every source-port split. +- **The threshold.** Cinna Davis's word from Discussion #1412 reaches eight, so + the threshold is eight. + +This package was built concurrently, without reading PR1615's code. It agrees +with every PR1615 number it overlaps, and adds three things: + +1. **Independent re-certification in the generic CI hook.** PR1615's + registered hook is witness-only, and its exclusion needs a native C++ + workflow. Here a gap-reduction lemma (below) brings the exhaustive `t ≤ 7` + exclusion and the `t = 8` count into a pure-Python census. It takes about + 20 s and 50 s on 10 cores and runs in the generic Python 3.12 package hook. + It is cross-checked by two further code-disjoint engines: + - a C engine that enumerates every placement; + - a numpy engine with per-occurrence ports. +2. **Every eight-transfer solution.** + - Exactly **2,502** canonical schedules realize all 31 masks with eight + transfers. + - **r = 1** (one source on `z1`) gives 2,376; **r = 5** (all on `z1`) gives + 126. + - No schedule with r = 0, 2, 3 or 4 is universal at eight transfers. The + best coverages are 31, 31, 27 and 24 of 32. + - The r = 5 class is Discussion #1412's restricted-port alphabet, up to + swapping `z0` and `z1`. The r = 1 schedules lie outside it. Free port choice + enlarges the solution set but saves no transfer. + - Every one of the 2,502 is replayed as a complete 80-call program. + - PR1615's census tool would yield these counts with a small change; they + are recorded here with replay evidence. +3. **PR1498's four-transfer split bounds.** PR1498 gives bounds + 31, 31, 25, 17, 19, 31 for r = 0…5 and notes they need not be sharp. The + r = 2 bound of 25 is **not attained**: the exact maximum is 21. The other + five bounds are exact. + +## Interface + +The interface is unchanged from +[woklerx's PR1438](https://github.com/CrocSwap/integer-mult-bounds/pull/1438) +and PR1498. PR1438 is merged in-repo as +[two-connector-transfer-boundary](../two-connector-transfer-boundary/README.md). +PR1498 is pinned in [REMOTE-SOURCES.json](REMOTE-SOURCES.json). + +**Rows.** +- Five read-only source rows `x_j`. +- 31 output rows `y_m`, one per nonzero mask `m` in F2⁵. +- Two independent arbitrary-dirty connector rows `z0` and `z1`. + +**Complete operations.** +- `B_j(p): z_p += B_j x_j`. +- `A_m(p): y_m += A_m z_p`. +- One paid one-way transfer `C: z0 += z1`. + +**Constraints.** +- Ports are chosen freely at every occurrence, and are charged. +- Every `B_j` and every `A_m` occurs exactly twice: 10 B and 62 A calls. +- Every source and both connectors are restored. +- The maps are generic, non-commuting F2-linear maps, and the dirt is + arbitrary. + +PR1498 step 1 shows that restoration forces both calls of a source onto one +port. A mask is realizable exactly when two cuts on the same connector have +equal dirt and source parts that differ by that mask. + +## Census + +| `t` | Universal schedules | Maximum masks covered (of 32) by port split r = 0…5 | +| --- | --- | --- | +| 1, 3, 5 | none: no schedule restores the connectors | — | +| 0 | 0 | 31, 17, 11, 11, 17, 31 | +| 4 | 0 | 31, 31, **21**, 17, 19, 31 | +| 6 | 0 | 31, 31, 28, 22, 23, 31 (as in PR1615) | +| 8 | **2,502** (r = 1: 2,376; r = 5: 126) | 31, 32, 31, 27, 24, 32 | + +Counts use canonical words, with labels by first occurrence, and one port per +source. + +## Gap reduction + +Between two consecutive B calls `z1` is fixed. Further transfers there only +alternate `z0` between two states of opposite dirt parity. So three transfers +in one gap give the same readout states and parities as one, and four give the +same as two. + +A schedule with three or more transfers in some gap therefore reduces to a +schedule with `t − 2` transfers, identical coverage and unchanged restoration +parities. This has three consequences: + +- censuses with at most two transfers per gap, run at `t = 0, 4, 6`, together + with PR1438's full-placement `t = 2` census (no 32-mask bin), exclude every + universal schedule with `t ≤ 7`; +- odd `t` cannot restore the dirt; +- at `t = 8`, a universal schedule with a long gap would reduce to a universal + `t = 6` schedule, so the reduced count of 2,502 is the exact count. + +## Verification + +```sh +python3 scripts/research_package.py --package research/two-connector-eight-transfer-census-seed58 --check-only +python3.12 scripts/research_package.py --package research/two-connector-eight-transfer-census-seed58 +``` + +`verify.py` uses only the standard library, parallelised over words. It has +three registered parts. + +1. **`controls`.** The engine reproduces: + - PR943's in-repo 105- and 945-word censuses for 4 and 5 sources, bin for + bin; + - PR1438's in-repo full-placement `t = 2` censuses for 1 to 5 sources: every + restored count and coverage histogram, with no gap reduction; + - at `t = 0` and `t = 4`, every port split: no universal schedule, with the + complete per-split coverage histogram pinned; + - no restored schedule for `t = 1, 3, 5`. +2. **`six`.** An exhaustive `t = 6` census over all 945 words and 32 port + splits: 44,936,640 restored reduced schedules, none universal, with the + per-split maxima and the complete coverage histogram pinned. +3. **`eight`.** An exhaustive `t = 8` census: + - exactly 2,502 universal schedules, with a pinned SHA-256 of the sorted list + (`ba04f277…`) and the split counts; + - each becomes an 80-call program (62 A, 10 B, 8 C), run on dense random + non-commuting F2 maps with arbitrary dirt; + - Discussion #1412's pilot is among them; + - on three witnesses (the first r = 1 schedule, the first r = 5 schedule and + the pilot), deleting any `C` or `A`, or reading any `A` on the wrong port, + fails. + +**Independent engine (offline).** +[independent/census.c](independent/census.c) enumerates every transfer +placement, with no gap reduction. It agrees on every per-split maximum, and +reproduces PR1615's `t = 6` totals: + +| `t` | Candidates | Restored | Universal | +| --- | --- | --- | --- | +| 4 | 30,270,240 | 10,402,560 | 0 | +| 6 | 242,161,920 | 74,692,800 | 0 | +| 8 | 1,323,241,920 | 384,199,200 | 2,502 | + +Run it with `cc -O2 -o census independent/census.c && ./census 8 0 1`, or +slice it with `./census 8 `. The receipts are in +[EXPECTED.json](EXPECTED.json). + +[independent/census_numpy.py](independent/census_numpy.py) lets every +occurrence choose its own port, filtered by exact `z1` restoration. + +| `t` | Legal schedules | Universal | Run time | +| --- | --- | --- | --- | +| 4 | 10,402,560 | 0 | — | +| 6 | 74,692,800 | 0 | 842 s on one core | + +Both match the per-split maxima above. So does PR1498's lemma that +restoration forces one port per source. + +## Scope + +- **Family:** only the incidence-minimal 72-operator-call family. Extra or odd + A/B incidences, reverse or bidirectional transfers, combined queries and + source mutations are not covered. +- **Proof:** a finite census with a short reduction lemma. +- **No supplier claim and no κ change.** The completed-price condition is + PR1498's `t·σ` tariff, instantiated at `t = 8` by PR1615: `8σ + ΔH < 2c` + against the 74-call repair, under equal port prices. + +## Open next questions + +The structured entries are in [TASK.json](TASK.json). + +1. **Is there a short structural proof that six transfers fail?** It should + also explain why only r = 1 and r = 5 reach eight. A projection argument + like PR1498's step 2 might do both, and it would remove the census + dependency. + - *First step:* classify the 2,502 witnesses by their transfer phases `u_i`. + - *Blocker:* none. +2. **Can extra incidences lower the threshold?** This is PR1615's question 1. + - *First step:* extend `engine.py` to 73 calls, with full dirt vectors per + readout. + - *Blocker:* the paired-readout reduction no longer applies. + +## Credit + +- **Hanson Sun (bbMisk), PR1615:** the six-transfer exclusion and the sharp + threshold, with priority. +- **Gareth Davidson (bitplane), PR1498:** the four-transfer obstruction, + source-port lemma, tariff and open question. +- **woklerx, PR1438:** the two-connector interface and full-placement censuses. +- **Cinna Davis (1337isnot1337), Discussion #1412:** the eight-transfer + construction. +- **Ross Richardson, PR943:** the universal-connector boundary and 945-word + census. + +Prepared by Sagar Thakrar with substantial Anthropic Claude assistance. That +included explorer and judge subagents, two of which wrote the independent +engines. New work is Apache-2.0. diff --git a/research/two-connector-eight-transfer-census-seed58/REMOTE-SOURCES.json b/research/two-connector-eight-transfer-census-seed58/REMOTE-SOURCES.json new file mode 100644 index 0000000000..b2140b8c6e --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/REMOTE-SOURCES.json @@ -0,0 +1,15 @@ +{ + "schema_version": 1, + "note": "Unmerged predecessor package PR1498, pinned at its PR head; the copy is byte-identical. PR1438 is merged and read in-repo.", + "copies": [ + { + "copy": "references/PR1498-README.md", + "pr": 1498, + "author": "bitplane (Gareth Davidson)", + "head": "b7baacc8048ab11d31751aee065206f2725a1a16", + "path": "research/two-connector-four-transfer-obstruction/README.md", + "git_blob": "abed92b09bde16fe47212b510086764944ef34bb", + "sha256": "5bbde91eb405150dce3073bf39419a7813d8f0529df3465ad97df66cb278a614" + } + ] +} diff --git a/research/two-connector-eight-transfer-census-seed58/SOURCES.json b/research/two-connector-eight-transfer-census-seed58/SOURCES.json new file mode 100644 index 0000000000..5ff83525cb --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/two-connector-transfer-boundary/EXPECTED.json", + "usage": "input", + "git_blob": "fb782704b64c9eb454cce465bddfb15912bbbd96", + "sha256": "bfa23c4ee9d0812c4e49a53ef4266b41a705424dde44104d3ccaf2d3c2e21188" + }, + { + "path": "research/universal-connector-boundary/CERTIFICATE.json", + "usage": "input", + "git_blob": "079e3e1441dc07c2f0536e9527acf290e51ea9c0", + "sha256": "e733746ba3e5151c829b4e8728bfff5ae3ed24d8d203eb77c735d20758e8266a" + } + ] +} diff --git a/research/two-connector-eight-transfer-census-seed58/TASK.json b/research/two-connector-eight-transfer-census-seed58/TASK.json new file mode 100644 index 0000000000..703c528e35 --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "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" + ] + }, + "scope_status": "refined", + "actual_scope": "In the PR1438/PR1498 free-port two-connector family, independently re-certify the PR1615 eight-transfer threshold with a standard-library census and classify every eight-transfer schedule: how many are there, and which port splits attain eight?", + "scope_change_reason": "The card asks whether one explicit alphabet extension has a favorable completed budget. PR1438/PR1498 introduced and priced this extension; PR1615 (bbMisk), published concurrently, settled its exact threshold of eight. This package keeps the extension and adds the complete solution set at eight (2,502 schedules, only port splits r = 1 and r = 5), a stdlib certificate of the exclusion that fits the generic package hook, and the exact four-transfer split maxima (PR1498 r = 2 bound 25 is not attained).", + "bottleneck_link": "Side result: pins down the full solution space of the cheapest two-connector repair (completed price 72c + 8 sigma + H_new) and shows free source ports enlarge it without saving a transfer. No kappa change.", + "budget_minutes": 180, + "stop_rule": "Stop once the t = 6 exclusion and t = 8 attainment are exhaustive with a stdlib registered engine that reproduces the PR943 and PR1438 censuses, every universal schedule replays literally, and an independent full-placement engine agrees; do not extend to extra-incidence families.", + "outcome": "completed", + "evidence": "verify.py (stdlib) reproduces PR943 n=4,5 and PR1438 n=1..5 censuses bin for bin; finds no universal schedule at t = 4 or 6 over all 945 words and 32 port splits (t = 6 maxima equal PR1615); and finds exactly 2,502 universal schedules at t = 8 (r = 1: 2,376; r = 5: 126; digest ba04f277...), each replaying as an 80-call program on dense random F2 maps. The independent full-placement census.c agrees at t = 4, 6, 8 and reproduces PR1615 t = 6 totals 242,161,920 / 74,692,800.", + "author": "Sagar Thakrar", + "ai_assistance": "Substantial Anthropic Claude (Claude Code, Opus) assistance, including explorer and judge subagents; two subagents wrote the independent C and numpy engines; the author wrote the registered engine, reviewed and ran everything, and is responsible for the result.", + "open_questions": [ + { + "question": "Is there a short structural proof that six transfers fail, explaining why only port splits r = 1 and r = 5 reach eight?", + "why_it_matters": "It would remove the exhaustive-census dependency of both PR1615 and this package.", + "first_step": "Classify the 2,502 witnesses by their transfer phases u_i and look for a projection invariant like PR1498 step 2.", + "blocked_by": "None." + }, + { + "question": "Can extra A/B incidences lower the threshold (PR1615 question 1)?", + "why_it_matters": "Each extra call costs c, so fewer transfers could change the completed comparison with the 74-call repair.", + "first_step": "Extend engine.py to 73 calls with full dirt vectors per readout.", + "blocked_by": "The paired-readout reduction no longer applies." + } + ] +} diff --git a/research/two-connector-eight-transfer-census-seed58/VERIFY.json b/research/two-connector-eight-transfer-census-seed58/VERIFY.json new file mode 100644 index 0000000000..5033f9569b --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/VERIFY.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/two-connector-transfer-boundary/EXPECTED.json", + "research/universal-connector-boundary/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "controls" + ], + "timeout_seconds": 300, + "checks": "Engine reproduces PR943 in-repo 105- and 945-word censuses (4, 5 sources) and PR1438 in-repo full-placement t=2 censuses (1-5 sources) bin for bin; pins complete per-split coverage histograms at t=0 and t=4 with no universal schedule; odd t restores nothing." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "six" + ], + "timeout_seconds": 300, + "checks": "Exhaustive t=6 census over all 945 words and 32 port splits: no universal schedule; pinned restored count, per-split maxima and complete coverage histogram." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--part", + "eight" + ], + "timeout_seconds": 600, + "checks": "Exhaustive t=8 census: exactly 2,502 universal schedules with pinned digest and split counts; each replays as an 80-call program on dense random F2 maps; Discussion 1412 pilot included; on three witnesses every deletion and wrong-port mutant fails." + } + ] +} diff --git a/research/two-connector-eight-transfer-census-seed58/engine.py b/research/two-connector-eight-transfer-census-seed58/engine.py new file mode 100644 index 0000000000..54151941f1 --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/engine.py @@ -0,0 +1,106 @@ +"""Exact census of the PR1438/PR1498 two-connector family (standard library). + +Model (PR1498): n read-only sources with increments b_j, two dirty connectors +z0 = e0 + ..., z1 = e1 + ..., operations B_j(p): z_p += b_j, C: z0 += z1, and +readouts A_m(p) of z_p. Every B_j occurs twice and both occurrences use the +source's port (forced by restoration, PR1498 step 1). A mask m is covered when +two cuts on the same connector have equal dirt and source parts differing by m. +""" +from collections import Counter + +# XOR-translation of a set of values {0..31} stored as a 32-bit mask is a bit +# permutation: flipping value bit k swaps the blocks selected by MASKS[k]. +MASKS = (0x55555555, 0x33333333, 0x0F0F0F0F, 0x00FF00FF, 0x0000FFFF) + + +def translate(s, v): + for k in range(5): + if v >> k & 1: + h = 1 << k + s = ((s & MASKS[k]) << h) | ((s >> h) & MASKS[k]) + return s + + +def words(n): + """All pairings of 2n positions, labels by first occurrence: (2n-1)!! words.""" + out = [] + def fill(w, label): + if label == n: + out.append(tuple(w)) + return + i = w.index(None) + w[i] = label + for k in range(i + 1, 2 * n): + if w[k] is None: + w[k] = label + fill(w, label + 1) + w[k] = None + w[i] = None + fill([None] * (2 * n), 0) + return out + + +def census_word(word, n, T, ports_list, reduced=True, want_full=False): + """Count restored schedules of one B word with exactly T transfers. + + reduced=True allows 0, 1 or 2 transfers per gap; reduced=False allows any. + Returns (leaves, Counter{(r, coverage size)}, list of full schedules). + """ + full_mask = (1 << (1 << n)) - 1 + gaps = 2 * n + 1 + hist, full, leaves = Counter(), [], [0] + for ports in ports_list: + r = bin(ports).count('1') + cvec = [0] * gaps + + def visit(S, D, v): + if S >> v & 1: + return S, D + S |= 1 << v + return S, D | translate(S, v) + + def go(g, budget, z0, q1, par, opened, S1, D1, Se, De, So, Do): + last = g == 2 * n + choices = (budget,) if last else range(0, min(budget, 2 if reduced else budget) + 1) + for c in choices: + if reduced and c > 2: + continue + cz0, cpar, cSe, cDe, cSo, cDo = z0, par, Se, De, So, Do + for _ in range(c): + cz0 ^= q1 + cpar ^= 1 + if cpar: + cSo, cDo = visit(cSo, cDo, cz0) + else: + cSe, cDe = visit(cSe, cDe, cz0) + cvec[g] = c + if last: + leaves[0] += 1 + if cpar == 0 and cz0 == 0 and q1 == 0: + cov = D1 | cDe | cDo + hist[(r, bin(cov).count('1'))] += 1 + if cov == full_mask and want_full: + full.append((word, ports, tuple(cvec))) + continue + j = word[g] + bit = 1 << j + nz0, nq1, nopened, nS1, nD1 = cz0, q1, opened, S1, D1 + nSe, nDe, nSo, nDo = cSe, cDe, cSo, cDo + if ports >> j & 1: + if q1 & bit: + if (opened >> j & 1) != cpar: # odd transfers while b_j sat in z1 + continue + else: + nopened = (opened & ~bit) | (cpar << j) + nq1 = q1 ^ bit + nS1, nD1 = visit(S1, D1, nq1) + else: + nz0 = cz0 ^ bit + if cpar: + nSo, nDo = visit(cSo, cDo, nz0) + else: + nSe, nDe = visit(cSe, cDe, nz0) + go(g + 1, budget - c, nz0, nq1, cpar, nopened, nS1, nD1, nSe, nDe, nSo, nDo) + + go(0, T, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0) + return leaves[0], hist, full diff --git a/research/two-connector-eight-transfer-census-seed58/independent/census.c b/research/two-connector-eight-transfer-census-seed58/independent/census.c new file mode 100644 index 0000000000..a2527aac96 --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/independent/census.c @@ -0,0 +1,81 @@ +/* Two-connector free-source-port census (PR1498 model), T paid transfers C: z0 += z1. + Five sources, each B_j twice (ten B calls), one port per source (forced by restoration, + PR1498 step 1), every placement of T C calls. + Dirt markers: z0 starts e0, z1 starts e1. Readout pair valid iff equal dirt coefficient. + Coverage = set of source-part differences over dirt-equal pairs of connector states (all cuts). + Usage: census T slice nslices -> prints histogram lines and witnesses. */ +#include +#include +#include +#include + +static int words[1000][10]; static int nwords = 0; +static void gen(int *pre, int len, int *cnt, int nl) { + if (len == 10) { memcpy(words[nwords++], pre, sizeof(int)*10); return; } + for (int j = 0; j < 5 && j <= nl; j++) { + if (j == nl) { cnt[j] = 1; pre[len] = j; gen(pre, len+1, cnt, nl+1); cnt[j] = 0; } + else if (cnt[j] == 1) { cnt[j] = 2; pre[len] = j; gen(pre, len+1, cnt, nl); cnt[j] = 1; } + } +} +static inline uint32_t xt(uint32_t s, int a) { /* {v^a : v in s} as 32-bit set */ + if (a & 1) s = ((s & 0x55555555u) << 1) | ((s >> 1) & 0x55555555u); + if (a & 2) s = ((s & 0x33333333u) << 2) | ((s >> 2) & 0x33333333u); + if (a & 4) s = ((s & 0x0F0F0F0Fu) << 4) | ((s >> 4) & 0x0F0F0F0Fu); + if (a & 8) s = ((s & 0x00FF00FFu) << 8) | ((s >> 8) & 0x00FF00FFu); + if (a & 16) s = (s << 16) | (s >> 16); + return s; +} +static inline uint32_t diffset(uint32_t s) { + uint32_t d = 0, t = s; + while (t) { int a = __builtin_ctz(t); t &= t - 1; d |= xt(s, a); } + return d; +} +int main(int argc, char **argv) { + int T = atoi(argv[1]); int slice = atoi(argv[2]); int ns = atoi(argv[3]); + int maxw = argc > 4 ? atoi(argv[4]) : 5; + int pre[10], cnt[5] = {0}; + gen(pre, 0, cnt, 0); + int L = 10 + T; + long long hist[6][33]; memset(hist, 0, sizeof hist); + long long cand = 0, rest = 0, full = 0; int printed = 0; + /* enumerate C position subsets as bitmasks of L bits with popcount T */ + for (int w = slice; w < nwords; w += ns) { + for (int ports = 0; ports < 32; ports++) { + int r = __builtin_popcount(ports); + for (uint32_t pos = (1u << T) - 1; pos < (1u << L); ) { + cand++; + int q0 = 0, q1 = 0, drift = 0, par = 0, b = 0; + uint32_t V1 = 1u, V0e = 1u, V0o = 0u; /* initial: q1=0; z0 source 0 at parity 0 */ + for (int i = 0; i < L; i++) { + if (pos & (1u << i)) { drift ^= q1; par ^= 1; } + else { int j = words[w][b++]; if (ports & (1 << j)) q1 ^= 1 << j; else q0 ^= 1 << j; } + V1 |= 1u << q1; + if (par) V0o |= 1u << (q0 ^ drift); else V0e |= 1u << (q0 ^ drift); + } + if (drift == 0 && q0 == 0 && q1 == 0 && par == 0) { + rest++; + uint32_t cov = diffset(V1) | diffset(V0e) | diffset(V0o); + int c = __builtin_popcount(cov); + hist[r][c]++; + if (cov == 0xFFFFFFFFu) { + full++; + if (printed < maxw) { + printed++; + printf("WITNESS word="); + for (int k = 0; k < 10; k++) printf("%d", words[w][k]); + printf(" ports=%d Cpos=", ports); + for (int i = 0; i < L; i++) if (pos & (1u << i)) printf("%d,", i); + printf("\n"); + } + } + } + /* next combination with same popcount (Gosper) */ + if (pos == 0) break; + uint32_t c0 = pos & -pos, rr = pos + c0; pos = (((rr ^ pos) >> 2) / c0) | rr; + } + } + } + printf("SUMMARY T=%d slice=%d/%d words=%d cand=%lld restored=%lld full=%lld\n", T, slice, ns, nwords, cand, rest, full); + for (int r = 0; r <= 5; r++) { printf("HIST r=%d", r); for (int c = 0; c <= 32; c++) if (hist[r][c]) printf(" %d:%lld", c, hist[r][c]); printf("\n"); } + return 0; +} diff --git a/research/two-connector-eight-transfer-census-seed58/independent/census_numpy.py b/research/two-connector-eight-transfer-census-seed58/independent/census_numpy.py new file mode 100644 index 0000000000..e6c2da0203 --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/independent/census_numpy.py @@ -0,0 +1,185 @@ +"""Code-disjoint exhaustive census of the PR1498 two-connector model. + +Model (PR1438/PR1498 README, re-derived here, no predecessor code read): + five read-only sources b_0..b_4, two dirty connectors z0,z1 with + independent formal dirt markers e0,e1; + B_j(p): z_p ^= b_j (each label exactly twice, each occurrence any port); + C: z0 ^= z1 (t calls); + A_m(p): reads z_p; each output read exactly twice. +A mask m is realizable iff two readout states (port,cut) have identical +dirt part and source parts XORing to m. A skeleton is legal iff both +connectors end exactly at their initial formal values. + +Formal value encoding: bits 0..4 = source coefficients, bit 5 = e0, bit 6 = e1. +""" +import itertools, sys, time, json, hashlib +from collections import Counter +import numpy as np + +N = 5 +E0, E1 = 1 << 5, 1 << 6 +SRC = (1 << N) - 1 + + +def canonical_words(): + # brute force over all distinct multiset permutations, quotient by + # first-occurrence relabeling (method differs from matching recursion) + seen = set() + for perm in set(itertools.permutations([0, 0, 1, 1, 2, 2, 3, 3, 4, 4])): + ren, out = {}, [] + for x in perm: + if x not in ren: + ren[x] = len(ren) + out.append(ren[x]) + seen.add(tuple(out)) + return sorted(seen) + + +def legal_port_patterns(w): + """All 2^10 per-occurrence port patterns, filtered by exact z1 restoration + (z1 is changed only by port-1 B calls, independent of C placement).""" + res = [] + for pat in range(1 << 10): + z1 = 0 + for k in range(10): + if (pat >> k) & 1: + z1 ^= 1 << w[k] + if z1 == 0: + res.append(pat) + return res + + +def placements(t): + """op sequences: entries -1 = C, k = k-th B call.""" + seqs = [] + for c in itertools.combinations_with_replacement(range(11), t): + seq = [] + for k in range(11): + seq.extend([-1] * c.count(k)) + if k < 10: + seq.append(k) + seqs.append(seq) + return np.array(seqs, dtype=np.int8).reshape(len(seqs), 10 + t) + + +# pair table: code a (7 bits), code b -> 32-bit mask bit of src xor if dirt equal +codes = np.arange(128) +dirt = codes >> 5 +src = codes & SRC +TABLE = np.where(dirt[:, None] == dirt[None, :], + np.left_shift(np.uint32(1), (src[:, None] ^ src[None, :]).astype(np.uint32)), + np.uint32(0)).astype(np.uint32).reshape(-1) +FULL = np.uint32(0xFFFFFFFF) + + +def census(t, words, full_pairs=True, witness_limit=50): + ops = placements(t) # (P, 10+t) + P, S = ops.shape + hist = Counter() + hist_by_r = {r: Counter() for r in range(6)} + legal_total = 0 + illegal_total = 0 + witnesses = [] + full_count = 0 + full_by_r = Counter() + for wi, w in enumerate(words): + pats = legal_port_patterns(w) + npat = len(pats) + # increments per pattern per B call + inc0 = np.zeros((npat, 11), dtype=np.int16) + inc1 = np.zeros((npat, 11), dtype=np.int16) + rvals = [] + for pi, pat in enumerate(pats): + for k in range(10): + if (pat >> k) & 1: + inc1[pi, k] = 1 << w[k] + else: + inc0[pi, k] = 1 << w[k] + rvals.append(len({w[k] for k in range(10) if (pat >> k) & 1})) + rvals = np.array(rvals) + # rows = pattern x placement + R = npat * P + prow = np.repeat(np.arange(npat), P) + orow = np.tile(np.arange(P), npat) + z0 = np.full(R, E0, dtype=np.int16) + z1 = np.full(R, E1, dtype=np.int16) + st0 = np.empty((R, S + 1), dtype=np.int16) + st1 = np.empty((R, S + 1), dtype=np.int16) + st0[:, 0] = z0 + st1[:, 0] = z1 + for s in range(S): + k = ops[orow, s].astype(np.int64) + isC = k < 0 + kk = np.where(isC, 10, k) + z0 = z0 ^ np.where(isC, z1, inc0[prow, kk]) + z1 = z1 ^ inc1[prow, kk] # inc1[:,10] == 0 for C + st0[:, s + 1] = z0 + st1[:, s + 1] = z1 + legal = (z0 == E0) & (z1 == E1) + legal_total += int(legal.sum()) + illegal_total += int((~legal).sum()) + if not legal.any(): + continue + st0 = st0[legal] + st1 = st1[legal] + rl = rvals[prow[legal]] + idx_p = prow[legal] + idx_o = orow[legal] + allst = np.concatenate([st0, st1], axis=1).astype(np.int64) if full_pairs else st0.astype(np.int64) + cov = np.zeros(allst.shape[0], dtype=np.uint32) + M = allst.shape[1] + for a in range(M): + ca = allst[:, a] * 128 + for b in range(a + 1, M): + cov |= TABLE[ca + allst[:, b]] + if not full_pairs: + # z1 coverage: values of z1 never interact with z0 (different dirt); + # add z1 pair differences separately + z1s = st1.astype(np.int64) + for a in range(S + 1): + ca = z1s[:, a] * 128 + for b in range(a + 1, S + 1): + cov |= TABLE[ca + z1s[:, b]] + cov |= np.uint32(1) # zero mask always (same readout twice) + pc = np.bitwise_count(cov).astype(np.int64) + for val, cnt in zip(*np.unique(pc, return_counts=True)): + hist[int(val)] += int(cnt) + for r in range(6): + m = rl == r + if m.any(): + for val, cnt in zip(*np.unique(pc[m], return_counts=True)): + hist_by_r[r][int(val)] += int(cnt) + fullm = cov == FULL + nf = int(fullm.sum()) + if nf: + full_count += nf + for r, cnt in Counter(rl[fullm].tolist()).items(): + full_by_r[r] += cnt + for i in np.nonzero(fullm)[0][: max(0, witness_limit - len(witnesses))]: + witnesses.append({"word": list(w), "pattern": pats[idx_p[i]], + "ops": ops[idx_o[i]].tolist()}) + return { + "t": t, "placements": P, "legal": legal_total, "illegal": illegal_total, + "hist": dict(sorted(hist.items())), + "max": max(hist) if hist else None, + "hist_by_r": {r: dict(sorted(h.items())) for r, h in hist_by_r.items()}, + "max_by_r": {r: (max(h) if h else None) for r, h in hist_by_r.items()}, + "full_count": full_count, "full_by_r": dict(full_by_r), + "witnesses": witnesses, + } + + +if __name__ == "__main__": + ts = [int(x) for x in sys.argv[1].split(",")] + full_pairs = (len(sys.argv) < 3 or sys.argv[2] != "fast") + words = canonical_words() + print("canonical words", len(words), flush=True) + if len(sys.argv) >= 5: + lo, hi = int(sys.argv[3]), int(sys.argv[4]) + words = words[lo:hi] + print("word range", lo, hi, flush=True) + for t in ts: + t0 = time.time() + res = census(t, words, full_pairs=full_pairs) + res["seconds"] = round(time.time() - t0, 1) + print(json.dumps(res), flush=True) diff --git a/research/two-connector-eight-transfer-census-seed58/references/PR1498-README.md b/research/two-connector-eight-transfer-census-seed58/references/PR1498-README.md new file mode 100644 index 0000000000..abed92b09b --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/references/PR1498-README.md @@ -0,0 +1,303 @@ +# Four paid transfers do not complete the universal five-source connector + +**Scoped obstruction for an enlarged alphabet; no new kappa.** Even when each +source operator may choose either dirty connector, **four paid one-way XOR +transfers cannot realize all 31 nonzero five-source masks** with exactly two +calls to every active B and A operator. At least **six** transfers are needed +in this incidence-minimal family. Six-transfer sufficiency remains open here. + +This answers the explicit open question in [woklerx's PR1438](https://github.com/CrocSwap/integer-mult-bounds/pull/1438), +pinned at `a61170c97c9ea2c396f6d76a953b0cf74a455cdd`. That work proves at +least four transfers and supplies a two-source mixed-mask example. The new +step is a source-port partition proof that excludes four for the full +five-source target. It reduces the exceptional cases to **Ross Richardson's +existing 945-pairing obstruction**, independently reproduced here; it does +not claim that old census as new. + +## Exact changed interface + +There are five immutable, arbitrary input rows x_j; 31 distinct arbitrary +output rows y_m, indexed by nonzero masks m in F2^5; and **two independent +arbitrary dirty connector rows** z0,z1. The target is + + y_m += sum_{j in m} A_m B_j x_j, + +with every source and both connectors restored. A_m and B_j are arbitrary +exact F2-linear maps of compatible dimensions; they need not commute, be +invertible or satisfy any additional identities. Correctness is generic in +the maps and holds for arbitrary incoming source, output and connector dirt. +Special zero maps or restricted input promises do not satisfy this generic +lower-bound hypothesis. + +The only complete operations are: + + B_j(p): z_p += B_j x_j, p in {0,1}; + A_m(p): y_m += A_m z_p, p in {0,1}; + C: z0 += z1. + +Every B_j and A_m occurs exactly twice: ten B and 62 A calls. Complete child +calls preserve all other rows, private scratch and required head/port/frame +state; their full port-specific prices are charged. The second row and C are +the actual extension of the old one-connector alphabet. There are no combined +queries, direct A_m B_j calls, free copies, source mutations, connector resets, +reverse-direction transfers or output feedback. Allowing B and A to choose a +physical port is a contract requirement with a price, not free rebinding of an +existing implementation. The theorem initially permits each occurrence to +choose a port; restoration forces the paired B ports to coincide. + +The claim is about the **72-operator-call family**, not every finite word in +this larger alphabet. In particular, odd operator multiplicities can become +legal with extra calls and changing ports. We do not import the predecessor's +general even-incidence argument into the enlarged alphabet. + +## Proof + +Write b_j=B_j x_j as independent formal source increments. Let e0,e1 be the +two independent incoming connector dirt markers. A readout contributes the +current connector expression with its output's A_m on the left. Since the +outputs have independent, generic A_m, two readouts cancel dirt precisely +when their two dirt coefficient vectors agree. Their source difference is +then the requested mask. Thus we may remove all A calls while studying the +B/C skeleton, retaining every connector value at every cut as a possible +readout. This is a necessary and sufficient paired-readout criterion, not a +clean-input relaxation. + +**1. Source ports are fixed by restoration.** A B call on z0 contributes e0 +times b_j to the final connector pair. A call on z1 contributes either e1 or +e0+e1, according to the parity of subsequent C calls. Two such contributions +cancel only when their columns agree. Hence both calls of a given B_j use +the same port, and a source assigned z1 has even C parity between its calls. +Partition the sources into J0,J1 and put r=|J1|. This exhausts even schedules +whose two B occurrences were allowed to choose different ports initially. + +**2. Four-transfer projection.** Let q0(t),q1(t) be the XOR sums of source +increments directly injected into z0,z1 up to time t. The sets of coordinates +supporting q0 and q1 are disjoint. For exactly four C calls, let u_i be q1 +immediately before the i-th transfer. Since each B occurs twice, connector +restoration requires + + u1 + u2 + u3 + u4 = 0. + +Here and below addition is XOR. At transfer phase p (after p transfers), + + z1 = e1 + q1(t), + z0 = e0 + (p mod 2)e1 + q0(t) + S_p, + S_p = u1 + ... + u_p. + +The even-phase S values are 0,u1+u2,0. The odd-phase values are u1,u4. +Consequently, the J1 projection of a dirt-cancelled z0 readout pair belongs +to + + K = {0, u1+u2, u1+u4}. + +A pair on z1 has no J0 component. A cross-port pair cannot cancel dirt: +z1 has marker e1 while z0 has e0 or e0+e1. In particular, a **mixed mask** +(meeting both source groups) can have at most **two distinct nonzero J1 +projections**. + +**3. Nonempty J0 and r>=2.** Universality requires a mixed mask for every +nonzero J1 projection, for example by adjoining one fixed J0 coordinate. +There are 2^r-1>=3 such projections, more than K can supply. This excludes +every split r=2,3,4 without a schedule census. A coarse coverage upper bound, +including the zero mask, is + + 2^r + (2^(5-r)-1) + 2(2^(5-r)-1) + = 2^r + 3*2^(5-r) - 3. + +The first term covers pure J1 masks, the second nonzero pure J0 masks, and +the last mixed masks. These split-specific bounds need not be sharp. + +**4. Exactly one source on z1.** Call its increment b. The row q1 is b +between its two B calls and zero otherwise. Therefore its nonzero u_i form +one consecutive block. Restoration makes the block length 0,2 or 4. + +For block length 0 or 4, both nonzero candidates in K vanish; no mixed mask +is available. For length 2, strip the dirt markers from the z0 history. +Its source part changes at the eight J0 B calls and at exactly the two C +calls with q1=b. It is therefore the prefix path of a **five-label word in +which every label appears twice**. All paired z0 readouts are among the +differences of that path, even after relaxing the equal-dirt restriction. +The only possible z1 readout differences are 0,b, and both already occur in +the projected path, since its b toggle occurs. The old five-source census +therefore bounds the entire coverage by 31 of 32 masks. + +**5. A single source group.** If J1 is empty, z0's source path is precisely +the old five-source path and z1 adds only zero. If J0 is empty, z1 follows +the old five-source prefix path. All possible paired z0 differences are in +K, whose two candidates u1+u2 and u1+u4 are already differences of vertices +of that z1 path. Again the old census gives at most 31 masks. + +The old census enumerates every pairing of ten positions: 9!!=945, with +labels assigned in order of first occurrence. The set of source-label +renamings preserves coverage. Its histogram of coverage sizes is + + 16:42, 19:120, 21:180, 22:56, 23:45, 24:220, + 26:110, 28:150, 31:22. + +Two independently implemented matching/interval enumerations reproduce the +histogram and the pinned canonical digest. This is the explicit finite +dependency of the proof; it is not an unrestricted circuit lower bound. + +For r=0,...,5, the resulting upper bounds are **31,31,25,17,19,31**. +The overall bound 31 is attained: use the old maximum-coverage word +`0,1,2,0,3,1,4,2,3,4` on z0 and append two cancelling pairs of C. It misses +mask 21 and realizes the other 30 nonzero masks. The verifier emits and +checks the complete paired-readout word. This deliberately simple sharpness +fixture reuses the predecessor's path; it is not a new five-source solution. + +Finally, a schedule with zero or two C calls can be padded at exit with +adjacent cancelling C pairs to get exactly four, preserving all existing +readouts and the ten B calls. Odd C counts cannot restore the independent +incoming dirt columns. Hence **every schedule with at most five C calls +fails**, establishing the necessary threshold six. This padding argument +is a correctness reduction; the added calls are not free in any cost bill. + +The projection idea also gives a general necessary condition: for 2k C calls +with k>=1 and two nonempty source groups, the even and odd phases each have at +most k distinct restored offset values. Their within-parity differences +provide at most k(k-1) nonzero J1 projections. Universality therefore requires +`2^r-1 <= k(k-1)`. This coarse condition alone does not settle six transfers. + +## Completed cost consequence + +Let c_Bj^p and c_Am^p be complete fixed-port child prices, and sigma the +complete price of one C call. Let H be **all remaining** parent preparation, +schedule dispatch, admission/reservation, frame access and exit work, counted +once outside those complete calls. An incidence-minimal candidate costs + + T_new = H_new + 2 sum_j c_Bj^p_j + 2 sum_m c_Am^r_m + t*sigma, + t >= 6. + +Both connectors are real dirty rows: 38 root rows for the five sources and +31 outputs, versus the old 37. Reserve the additional length-L row and all +child private storage; price frame/head movement and restoration on the +actual ports. No clean full row is introduced. This is a necessary lower +bill, not a construction attaining it. + +For an explicit implementation of C, `independent.py` provides a simple +one-head bit-tape backend. It **admits and prices one clean scalar scratch +bit**, initially and finally zero. For each coordinate, start at head 0, +load z1[k] into that bit by XOR, move to z0[k] and XOR it into the target, +return to z1[k] and XOR it out of the bit, then return the head to 0. +Source, private bit and head restore. For row bases b0,b1 it uses exactly + + 3L cell/register XOR instructions, + 2L*b1 + L*(L-1) + 2L*abs(b1-b0) single-cell head steps, + one instruction dispatch per XOR or head step. + +With the 38 root rows stored consecutively, b0=36L,b1=37L, the head bill is +`77L^2-L`; the primitive dispatch bill is `77L^2+2L`. Program preparation, +instruction access, clean-bit admission and call entry/exit still have their +explicit prices in sigma or H. The verifier checks every dirty tape basis +column and the inverse for L=1,...,5. This deliberately conservative backend +shows the transfer is implemented and charged; it is not a selected native +supplier, a runtime benchmark or a cheapest routing claim. A direct +two-address row-XOR realization has L target XORs, but access and restoration +cannot be replaced by a declaration that C costs zero. + +For comparison, the predecessor's actual 74-call repair repeats the output +operator for mask 21 (or uses its alternative repeated-source repair). The +output-repair cost at old port0 is + + T_old = H_old + 2 sum_j c_Bj^0 + 2 sum_m c_Am^0 + 2*c_A21^0. + +Any favorable new schedule must beat this complete expression, including +changed port prices and H. Under the **additional simplifying assumption** +of equal complete A/B prices c on both ports, a necessary condition is + + 6*sigma + (H_new-H_old) < 2*c. + +The former optimistic four-transfer comparison is unattainable for this +family. Even the six-transfer inequality is not sufficient: neither a +six-transfer construction nor its admission to a selected supplier is +provided. Extra A/B calls, bidirectional transfers, special common maps and +mutable sources are separate possible routes, outside this theorem. + +## Evidence and reproduction + +Python 3.12+, standard library only, no network during replay: + +```sh +python3.12 -I -B scripts/research_package.py \ + --package research/two-connector-four-transfer-obstruction +python3.14 -I -O -B research/two-connector-four-transfer-obstruction/verify.py +``` + +The registered replay runs the checker and package corruption controls. +`verify.py --write-expected` explicitly regenerates the deterministic receipt; +normal replay only reads it and compares every field. Guards remain enabled +under `-O`. Exact source and retained-file pins are in SOURCES.json and +REMOTE-SOURCES.json. Retained predecessor text is unmodified. + +The evidence consists of: + +- Independent old-path enumerations through five sources, including all 945 + five-source pairings and the exact source-bound histogram/digest. +- All **37,449** four-transfer prefix tuples over dimensions zero through + five, independently checking the projection identity. This is the stated + finite domain, not an enumeration of every five-source schedule. +- Two complete small-skeleton enumerations for one, two and three sources: + **30, 840 and 25,200** candidates, including every source-port assignment + and placement of four transfers. Every restored case checks the proof's + applicable reduction and the arbitrary-dirt paired-readout criterion. +- A complete two-source universal example using the credited PR1438 + skeleton, and the sharp five-source 31-mask example. Both replay in free + noncommutative operators, forward and inverse, retaining every independent + dirty row. Separate dense matrix banks at widths 1,...,4 check **880** + forward and **880** inverse basis columns, including noncommuting maps. +- Omission of each of the two-source example's **six A, four B and four C** + calls is rejected. Wrong-port and discarded-dirt controls are also checked. + The transfer backend separately checks **570** forward and **570** inverse + tape columns. + +The general claim follows from the written reductions and the explicit old +finite exclusion. Dense tests and small schedule censuses support the checker; +they are not an extrapolation to all widths or schedules. No full selected +cold replay, physical supplier admission, contraction, precision theorem, +analytic transfer, Lean proof or multiplication exponent is claimed. + +## Coordination and provenance + +Single random nonce `03de982dd845f2b40aeaaef2a1eecd7c`, revision-2 recursive +interfaces draw, card `connector-alphabet-change`; no reroll. The prescribed +universal-connector first example and selected baseline binding check passed. +Exact base: `4040a0f46d67b41c36a472a7cd4af791fd4c36cc`. The selected #1094 +frontier remains a historical context pin, not an input to this theorem. +Published contribution: [1498](https://github.com/CrocSwap/integer-mult-bounds/pull/1498); mathematical commit +`5431fba4a80e30925e0c2b2c161b9c68bbac1c17`. +The original claim and result are in [Discussion1486](https://github.com/CrocSwap/integer-mult-bounds/discussions/1486). + +The entry overlap check found PR1438 and [Cinna Davis's Discussion1412](https://github.com/CrocSwap/integer-mult-bounds/discussions/1412). +That separate claim fixes every B write to the transfer's source root and +announces an eight-transfer bound/construction. Here the B ports are freely +chosen and the proved lower bound is six. The present result does not +duplicate or establish its stronger restricted-port statement. PR1340/1370 +alter source rows under a common-B hypothesis; that alphabet is excluded. +The overlap tool searches open PR bodies, Discussion records and local +top-level notes, not every code diff or every closed submission; its output +does not prove novelty. Final overlap details are in TASK.json. + +## Open next questions + +1. **Does six suffice with freely chosen source ports?** This decides whether + the tightened necessary bill can be attained. First apply the source-port + projection bound to eliminate r>=3 when both groups are nonempty, then + search only the remaining six-transfer cases with full dirty restoration. + The all-B-on-one-root case also needs the separately claimed evidence + checked. No such search or proof is supplied here. +2. **Can a legal concrete supplier afford the surviving interface?** Before + implementation, pin its actual port prices, child contracts, extra row, + scalar scratch, instruction access, preparation and dispatch. Compare its + whole bill with an achieved old repair. The missing construction and + actual supplier admission are blockers; call counts alone do not answer it. +3. **Can extra operator incidences beat both tariffs?** Keep the same paid + operation alphabet and first analyze the 73-call boundary. The paired + source/readout reductions used here no longer suffice; a new all-word + argument would be required. The old general parity argument is unavailable. + +## Credit + +Prepared by **Gareth Davidson (@bitplane)** with substantial **OpenAI Codex +assistance**. Credit woklerx, Ross Richardson, Cinna Davis and all retained +dirty-commutator/common-factor predecessors; see NOTICE.md and the verbatim +source notices. New work is Apache-2.0. No independent human review is asserted. diff --git a/research/two-connector-eight-transfer-census-seed58/replay.py b/research/two-connector-eight-transfer-census-seed58/replay.py new file mode 100644 index 0000000000..3c006ff5f3 --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/replay.py @@ -0,0 +1,97 @@ +"""Literal replay of complete programs on dense random F2 maps. + +A schedule (word, ports, transfers per gap) becomes a full program of B, C and +A calls. Each nonzero mask m gets one A_m readout at each of two cuts on the +same connector whose dirt agrees and whose source parts differ by m. The +program then runs on random non-commuting maps with arbitrary dirt. +""" +import random + + +def program(word, ports, gaps, n=5): + """Return (ops, cut list). ops are ('B', j, p), ('C',), and later ('A', m, p).""" + ops, cuts = [], [] + z0 = q1 = par = 0 + def cut(): + cuts.append((len(ops), z0, par, q1)) + cut() + for g in range(2 * n + 1): + for _ in range(gaps[g]): + ops.append(('C',)) + z0 ^= q1 + par ^= 1 + cut() + if g < 2 * n: + j = word[g] + p = ports >> j & 1 + ops.append(('B', j, p)) + if p: + q1 ^= 1 << j + else: + z0 ^= 1 << j + cut() + if par or z0 or q1: + raise ValueError('schedule does not restore the connectors') + return ops, cuts + + +def place_readouts(ops, cuts, n=5): + """Insert two A_m calls per nonzero mask; raise if a mask is not covered.""" + inserts = [] + for m in range(1, 1 << n): + found = None + for a in range(len(cuts)): + for b in range(a + 1, len(cuts)): + pa, za, ra, qa = cuts[a] + pb, zb, rb, qb = cuts[b] + if qa ^ qb == m: + found = (pa, pb, 1) + elif ra == rb and za ^ zb == m: + found = (pa, pb, 0) + if found: + break + if found: + break + if not found: + raise ValueError('mask %d is not covered' % m) + inserts += [(found[0], m, found[2]), (found[1], m, found[2])] + out = list(ops) + for pos, m, p in sorted(inserts, key=lambda t: -t[0]): + out.insert(pos, ('A', m, p)) + return out + + +def matvec(rows, v): + return sum((bin(r & v).count('1') & 1) << i for i, r in enumerate(rows)) + + +def run(ops, n=5, width=4, trials=20, seed=0): + """True when every trial computes y_m += sum_{j in m} A_m B_j x_j and restores z0, z1, x.""" + rng = random.Random(seed) + lim = 1 << width + for _ in range(trials): + mat = lambda: [rng.randrange(lim) for _ in range(width)] + B = [mat() for _ in range(n)] + A = {m: mat() for m in range(1, 1 << n)} + x = [rng.randrange(lim) for _ in range(n)] + z = [rng.randrange(lim), rng.randrange(lim)] + y0 = {m: rng.randrange(lim) for m in A} + y, start, x0 = dict(y0), list(z), list(x) + for op in ops: + if op[0] == 'B': + z[op[2]] ^= matvec(B[op[1]], x[op[1]]) + elif op[0] == 'C': + z[0] ^= z[1] + else: + y[op[1]] ^= matvec(A[op[1]], z[op[2]]) + want = {m: y0[m] ^ _sum(matvec(A[m], matvec(B[j], x[j])) for j in range(n) if m >> j & 1) for m in A} + if y != want or z != start or x != x0: + return False + return True + + +def _sum(values): + out = 0 + for v in values: + out ^= v + return out diff --git a/research/two-connector-eight-transfer-census-seed58/verify.py b/research/two-connector-eight-transfer-census-seed58/verify.py new file mode 100644 index 0000000000..ed00af464c --- /dev/null +++ b/research/two-connector-eight-transfer-census-seed58/verify.py @@ -0,0 +1,184 @@ +#!/usr/bin/env python3 +"""All eight-transfer schedules of the free-port two-connector five-source family. + +PR1438/PR1498 model: five read-only sources, two arbitrary-dirty connectors, +every B_j and A_m called exactly twice, freely chosen ports, and t paid +one-way transfers C: z0 += z1. PR1615 (bbMisk) first proved the sharp +threshold of eight. This standard-library verifier re-certifies it (all 31 +nonzero masks are realizable iff t is even and t >= 8) and classifies every +eight-transfer solution. + +Parts, each registered as its own command in VERIFY.json: + controls The engine reproduces PR943's in-repo 105- and 945-word censuses + (n=4, 5) and PR1438's in-repo full-placement T=2 censuses (n=1..5) + bin for bin. It pins the complete per-split coverage histograms + at T=0 and T=4, finds no universal schedule there, and finds no + restored odd-T schedule. + six Exhaustive T=6 census over every word and port split: no + universal schedule, with the complete coverage histogram pinned. + eight Exhaustive T=8 census: exactly 2,502 universal schedules, with a + pinned digest. Every one replays as a complete 80-call program on + dense random F2 maps. Discussion 1412's pilot is among them, and + deletion and wrong-port mutants fail. + +Gap reduction (README): between consecutive B calls, z1 is fixed, so further +transfers only alternate z0 between two states. Three transfers in one gap +therefore have the coverage and parities of one, and four those of two. A +schedule with a gap of three or more reduces to one with T - 2 transfers and +equal coverage. Hence censuses with at most two transfers per gap, run for +T = 0, 2, 4, 6, exclude every universal schedule with t <= 7. They also make +the T = 8 count exact. + +Sagar Thakrar with substantial Anthropic Claude assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from hashlib import sha256 +import json +from multiprocessing import Pool +import os +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +sys.path.insert(0, str(PACKAGE)) +from engine import census_word, words # noqa: E402 +from replay import place_readouts, program, run # noqa: E402 + +EXPECTED = json.loads((PACKAGE/'EXPECTED.json').read_bytes()) +PR943 = ROOT/'research/universal-connector-boundary/CERTIFICATE.json' +PR1438 = ROOT/'research/two-connector-transfer-boundary/EXPECTED.json' + + +def require(condition, message): + if not condition: + raise SystemExit('FAIL: ' + message) + + +def check_pins(): + rows = json.loads((PACKAGE/'SOURCES.json').read_bytes())['files'] + for row in rows: + if row['usage'] == 'input': + require(sha256((ROOT/row['path']).read_bytes()).hexdigest() == row['sha256'], 'Pinned input: ' + row['path']) + for row in json.loads((PACKAGE/'REMOTE-SOURCES.json').read_bytes())['copies']: + require(sha256((PACKAGE/row['copy']).read_bytes()).hexdigest() == row['sha256'], 'Pinned remote copy: ' + row['copy']) + + +def _task(arg): + word, n, T, reduced, want = arg + return census_word(word, n, T, list(range(1 << n)), reduced=reduced, want_full=want) + + +def census(n, T, reduced=True, want_full=False): + """Aggregate over all words and port splits: (leaves, Counter{(r, size)}, full schedules).""" + jobs = [(w, n, T, reduced, want_full) for w in words(n)] + leaves, hist, full = 0, Counter(), [] + with Pool(os.cpu_count() or 1) as pool: + for lv, h, f in pool.imap_unordered(_task, jobs, chunksize=4): + leaves += lv + hist.update(h) + full += f + return leaves, hist, sorted(full) + + +def hist_sha256(hist): + return sha256(json.dumps(sorted([r, size, count] for (r, size), count in hist.items())).encode()).hexdigest() + + +def no_universal(T, key): + """Exhaustive reduced census with the complete (split, coverage) histogram pinned.""" + _, hist, full = census(5, T, want_full=True) + want = EXPECTED[key] + require(not full and max(size for _, size in hist) < 32, 'T=%d has a universal schedule' % T) + require(sum(hist.values()) == want['restored'] and maxima(hist) == want['max_by_split'], 'T=%d census' % T) + require(hist_sha256(hist) == want['histogram_sha256'], 'T=%d coverage histogram' % T) + return hist + + +def maxima(hist): + out = {} + for (r, size), _ in hist.items(): + out[r] = max(out.get(r, 0), size) + return {str(r): out[r] for r in sorted(out)} + + +def sizes(hist, r=None): + out = Counter() + for (split, size), count in hist.items(): + if r is None or split == r: + out[str(size)] += count + return dict(out) + + +def part_controls(): + certificate = json.loads(PR943.read_bytes()) + for row in certificate['censuses']: + _, hist, _ = census(row['sources'], 0) + require(sizes(hist, 0) == row['histogram'], 'PR943 %d-source census' % row['sources']) + print('PR943 single-connector censuses reproduced:', [row['sources'] for row in certificate['censuses']]) + for row in json.loads(PR1438.read_bytes())['censuses']: + n = row['sources'] + _, hist, _ = census(n, 2, reduced=False) + require(sum(hist.values()) == row['restored'] and sizes(hist) == row['coverage_histogram'], + 'PR1438 %d-source T=2 census' % n) + print('PR1438 full-placement T=2 censuses reproduced for 1-5 sources') + hist = no_universal(0, 'zero') + print('T=0: no universal schedule for any split; maxima by split', maxima(hist)) + hist = no_universal(4, 'four') + print('T=4: no universal schedule; maxima by split', maxima(hist)) + for T in (1, 3, 5): + _, hist, _ = census(5, T) + require(sum(hist.values()) == 0, 'odd T=%d restored a schedule' % T) + print('odd T = 1, 3, 5: no schedule restores both connectors') + + +def part_six(): + hist = no_universal(6, 'six') + print('T=6: %d restored schedules, none universal; maxima by split %s' % (sum(hist.values()), maxima(hist))) + + +def part_eight(): + leaves, hist, full = census(5, 8, want_full=True) + want = EXPECTED['eight'] + by_split = Counter(bin(ports).count('1') for _, ports, _ in full) + digest = sha256(json.dumps(full).encode()).hexdigest() + require(sum(hist.values()) == want['restored'] and maxima(hist) == want['max_by_split'], 'T=8 census') + require(len(full) == want['universal'] and dict(sorted(by_split.items())) == {int(k): v for k, v in want['universal_by_split'].items()}, + 'T=8 universal schedules') + require(digest == want['universal_sha256'], 'T=8 universal schedule digest') + pilot = want['discussion1412_pilot'] + require((tuple(pilot['word']), pilot['ports'], tuple(pilot['gaps'])) in set(full), 'Discussion 1412 pilot') + for i, (word, ports, gaps) in enumerate(full): + ops, cuts = program(word, ports, list(gaps)) + prog = place_readouts(ops, cuts) + require(len(prog) == 80 and sum(op[0] == 'A' for op in prog) == 62, 'program shape') + require(run(prog, trials=3, seed=i), 'replay of universal schedule %d' % i) + # Mutation controls on three witnesses: the first r = 1 schedule, the first r = 5 schedule and the pilot. + first = {r: next(s for s in full if bin(s[1]).count('1') == r) for r in (1, 5)} + for word, ports, gaps in (first[1], first[5], (tuple(pilot['word']), pilot['ports'], tuple(pilot['gaps']))): + ops, cuts = program(word, ports, list(gaps)) + prog = place_readouts(ops, cuts) + for kind in ('C', 'A'): + for i in [k for k, op in enumerate(prog) if op[0] == kind]: + require(not run(prog[:i] + prog[i+1:], trials=5), 'deleting one %s still passed' % kind) + for i in [k for k, op in enumerate(prog) if op[0] == 'A']: + mutant = prog[:i] + [('A', prog[i][1], 1 - prog[i][2])] + prog[i+1:] + require(not run(mutant, trials=5), 'a wrong-port readout still passed') + print('T=8: %d universal schedules %s, digest %s' % (len(full), dict(sorted(by_split.items())), digest[:16])) + print('all universal schedules replay as 80-call programs on dense random F2 maps; Discussion 1412 pilot included;', + 'on three witnesses every C or A deletion and every wrong-port readout fails') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--part', choices=['controls', 'six', 'eight'], required=True) + args = parser.parse_args() + require(sys.version_info >= (3, 11), 'Python 3.11 or later') + check_pins() + dict(controls=part_controls, six=part_six, eight=part_eight)[args.part]() + print('PASS_TWO_CONNECTOR_TRANSFER_THRESHOLD', args.part) + + +if __name__ == '__main__': + main()