diff --git a/research/seven-source-weight123-connector-seed7db30a/README.md b/research/seven-source-weight123-connector-seed7db30a/README.md new file mode 100644 index 0000000000..be28cb1cb2 --- /dev/null +++ b/research/seven-source-weight123-connector-seed7db30a/README.md @@ -0,0 +1,188 @@ +# Seven-source weight-1/2/3 dirty connector: exact 14-toggle boundary + +**Scoped construction and finite obstruction; no new κ.** For seven immutable +F2 sources and one dirty connector, consider the 63 output masks of weights one, +two, and three. Among all 135,135 canonical source words using each source toggle +exactly twice, the maximum number of these masks available as paired prefix +differences is **56**. No 14-source-call word supports all 63. The maximum is +attained by a literal word that supports every singleton and pair mask plus 28 +triple masks. Its 56 arbitrary outputs attain the dirty-query call floor: 126 +complete map calls. + +The result is limited to the stated seven-source batch and exactly two calls per +source map. It does not exclude a 142-call schedule using additional source +calls, and it is not a supplier, recursive assembly, multiplication bound, or +new κ result. + +## Exact finite result + +Bit `j` denotes source `B_j`; decimal masks in [RESULT.json](RESULT.json) use that +convention. The maximum-coverage source word is + +```text +0 1 2 0 3 2 4 3 5 4 6 5 1 6 +``` + +Its boundary prefixes are + +```text +0 1 3 7 6 14 10 26 18 50 34 98 66 64 0 +``` + +The 56 supported target masks are exactly seven weight-one masks, all 21 +weight-two masks, and 28 weight-three masks. The missing triple masks are + +```text +22 38 41 42 73 81 84 +``` + +The JSON receipt contains a pair of prefix-boundary indices for every supported +mask. The full census has two maximum-coverage words (both cover 56), zero +full-cover words, and the complete coverage histogram. Source-label +permutations preserve the target family, so canonical first-appearance labels +lose no cases. + +## Why prefix differences implement the batch + +At boundary `t`, let `q_t` be the seven-bit parity vector of the source toggles +already called. For arbitrary dirty connector `z_0` and arbitrary F2-linear +maps and inputs, + +```text +z_t = z_0 + sum_j q_t[j] B_j x_j. +``` + +For output mask `M`, call its map `A_M` at boundaries `s` and `t`. The dirty +connector term cancels, leaving + +```text +A_M z_s + A_M z_t + = A_M sum_j (q_s[j] + q_t[j]) B_j x_j. +``` + +Therefore any pair with `q_s XOR q_t = M` realizes exactly that output and +restores its dirty target. Every source appears twice, so the final connector is +restored. Readouts at a boundary commute because they update distinct output +rows and do not change the connector. This argument works at every vector +dimension and requires no invertibility or commutation of the maps. + +The maximum word supplies all 56 listed masks, so it constructs that arbitrary +56-output batch. Each active source map and each arbitrary-dirty output map must +be called at least twice in this connector contract. Thus `2(7+56)=126` +complete calls is attained for that support. For all 63 masks, the elementary +floor would be 140. At exactly 140 calls, dirty restoration forces every one of +the seven source maps and 63 output maps to occur exactly twice. Specializing +the arbitrary maps to scalar identities with independent source bits shows +that an output can then be correct only if its mask is a difference of two +source-prefix states. The complete census excludes that floor. Each map's +generic call count is even, so the full family needs at least 142 calls. No +142-call upper bound is claimed. + +## Complete cost comparison for the attained 56-output support + +Each source occurs in 19 of the 56 masks. Independent per-output stars therefore +use 38 calls to each `B_j` and two calls to each of the 56 `A_M` maps: 378 +complete map calls. The shared word uses two calls per source and two per output: +126 complete map calls, saving 36 complete source-map calls per source (252 in +total). + +Use an explicit straight-line event encoding with a one-bit opcode, a three-bit +`B` identifier and a six-bit `A` identifier. It contains every operation and +its map ID; boundary placement is encoded by event order, so it needs no runtime +search or uncharged address table. This encoding uses 1,848 bits for the 378-call +star program and 840 bits for the 126-call shared program. With `lambda` the +price per stored event bit, `delta` the per-event root-dispatch price, `c(B_j)` +the complete `B_j`-call price, and `c(A_M)` the complete target-call price, the +two invoices are + +```text +C_shared = I + P + 2 sum_j c(B_j) + 2 sum_M c(A_M) + 840 lambda + 126 delta +C_stars = I + P + 38 sum_j c(B_j) + 2 sum_M c(A_M) + 1848 lambda + 378 delta +C_shared - C_stars = -36 sum_j c(B_j) - 1008 lambda - 252 delta. +``` + +`I` is the common input admission and `P` is the common one-time coefficient +preparation. Each complete call price includes its source access, arithmetic, +target update, private scratch restoration, and head return. This is a +componentwise reduction for every nonnegative event-storage and dispatch price. +It counts the full calls; it does not assert that a physical supplier for this +interface exists. + +For comparison only, the hypothetical 140-call floor for all 63 outputs would +save 294 source calls and 1,176 event bits relative to independent stars, but +the exact search proves that schedule does not exist with two uses of each +source. + +## Exact domain, reproduction, and controls + +The source word induces a perfect matching of the 14 call positions: the two +positions carrying each source label are paired. Relabeling pairs by their +first position gives one canonical word per perfect matching, hence +`13*11*9*7*5*3*1 = 135,135` cases. `search.py` enumerates this domain by the +least unmatched position and emits the exact receipt. `verify.py` independently +enumerates restricted-growth double-occurrence words, checks the full histogram +and maximum, and replays the dirty-state identity on deterministic arbitrary +F2-linear maps at dimensions 1, 2, and 3. + +From the repository root: + +```sh +python3 -I -B research/seven-source-weight123-connector-seed7db30a/search.py +python3 -I -B research/seven-source-weight123-connector-seed7db30a/verify.py +python3 scripts/research_package.py --package research/seven-source-weight123-connector-seed7db30a --check-only +``` + +Expected markers: + +```text +SEVEN_SOURCE_WEIGHT123_SEARCH pairings=135135 targets=63 hits=0 best=56 +PASS_SEVEN_SOURCE_WEIGHT123_PAIRING_BOUND pairings=135135 max=56 full_hits=0 subset_calls=126 controls=3 +PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check) +``` + +Three failure controls detect a deleted source toggle, a deleted second dirty +readout, and a readout pair whose prefix difference omits a requested mask. All +arithmetic in the proof-relevant finite search and simulation is exact integer +arithmetic over F2. The abstract prefix identity, rather than the small random +fixtures, establishes arbitrary-dimension correctness for the attained support. +Local replay used CPython 3.14.7. CPython 3.12 is unavailable in this environment, +so the registered Python 3.12 package replay was not run; the package metadata +and pin check and the verifier in normal and optimized mode were run directly. + +## Assignment, overlap, and limits + +Cycle 27 used seed `7db30a45a4ca218f66c410637c8459f3`, track +`recursive-interfaces`, task `connector-alphabet-change`, priority revision 4, +and exact base `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. The selector task asks +for a changed connector alphabet. This changed-scope result retains the +singleton alphabet and changes the matrix-support family; it answers a distinct +structural question about seven sources and low-weight outputs. The selected +record SHA-256 is +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. + +The refreshed overlap scan covered 463 open PRs and 918 Discussions with +complete pagination and no warnings. Closest work: PR #2128 studies six-source +universal masks with charged DUO calls; PR #2146 excludes a six-source one-TRIO +universal path; PR #2182 studies fixed-port five-source and two-root universal +boundaries. These change the operation alphabet, mask family, or root count and +do not contain this one-root seven-source weight-1/2/3 census. Ross Richardson's +PRs #934/#943 supply the connector contract and paired-prefix criterion; they +are cited for that general reduction, not as a result of this seven-source +census. + +No selected record, frozen source, supplier, or frontier value changes. No +independent human review or proof-assistant formalization is claimed. Prepared +by Cinna Davis with substantial OpenAI Codex assistance in scoping, exact +enumeration, dirty-state replay, cost accounting, and writing. New work is +Apache-2.0. + +## Open next questions + +Can one additional even source toggle lift the seven-source weight-1/2/3 batch +from 56 to all 63 outputs at 142 total calls? This is the next even call count +above the excluded 140 floor and could retain most of the 294-call saving over +independent stars. First enumerate or construct normalized 16-event words with +one source used four times and the other six twice, then apply the same exact +prefix-difference test before evaluating any physical cost. This cycle did not +search that larger domain; the number of normalized words is much larger than +135,135, and a failed finite search would need to remain scoped. diff --git a/research/seven-source-weight123-connector-seed7db30a/RESULT.json b/research/seven-source-weight123-connector-seed7db30a/RESULT.json new file mode 100644 index 0000000000..6d80c852b3 --- /dev/null +++ b/research/seven-source-weight123-connector-seed7db30a/RESULT.json @@ -0,0 +1,413 @@ +{ + "attained_subset_cost": { + "shared_instruction_bits": 840, + "shared_source_calls": 14, + "shared_total_calls": 126, + "source_calls_saved": 252, + "source_incidence_per_map": [ + 19, + 19, + 19, + 19, + 19, + 19, + 19 + ], + "star_instruction_bits": 1848, + "star_source_calls": 266, + "star_total_calls": 378, + "target_calls": 112, + "weight_counts": { + "1": 7, + "2": 21, + "3": 28 + } + }, + "canonical_pairings_enumerated": 135135, + "coverage_histogram": { + "18": 7, + "19": 14, + "20": 63, + "21": 85, + "22": 175, + "23": 294, + "24": 420, + "25": 644, + "26": 1022, + "27": 1659, + "28": 2179, + "29": 3626, + "30": 6041, + "31": 7749, + "32": 8988, + "33": 12817, + "34": 14042, + "35": 16074, + "36": 11977, + "37": 13307, + "38": 9513, + "39": 8421, + "40": 5411, + "41": 4039, + "42": 2520, + "43": 1729, + "44": 882, + "45": 763, + "46": 266, + "47": 266, + "49": 84, + "50": 28, + "51": 14, + "53": 14, + "56": 2 + }, + "full_cover_paths": 0, + "full_family_cost_screen": { + "attained": false, + "hypothetical_shared_instruction_bits": 938, + "hypothetical_shared_source_calls": 14, + "hypothetical_shared_total_calls": 140, + "source_calls_savings_if_cover_existed": 294, + "source_incidence": 154, + "star_instruction_bits": 2114, + "star_source_calls": 308, + "star_total_calls": 434, + "target_calls": 126 + }, + "maximum_covered_masks": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 16, + 17, + 18, + 19, + 20, + 21, + 24, + 25, + 26, + 28, + 32, + 33, + 34, + 35, + 36, + 37, + 40, + 44, + 48, + 49, + 50, + 52, + 56, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 72, + 74, + 76, + 80, + 82, + 88, + 96, + 97, + 98, + 100, + 104, + 112 + ], + "maximum_missing_masks": [ + 22, + 38, + 41, + 42, + 73, + 81, + 84 + ], + "maximum_prefix_states": [ + 0, + 1, + 3, + 7, + 6, + 14, + 10, + 26, + 18, + 50, + 34, + 98, + 66, + 64, + 0 + ], + "maximum_readout_pairs": { + "1": [ + 0, + 1 + ], + "10": [ + 0, + 6 + ], + "100": [ + 4, + 11 + ], + "104": [ + 6, + 11 + ], + "11": [ + 1, + 6 + ], + "112": [ + 8, + 11 + ], + "12": [ + 4, + 6 + ], + "13": [ + 2, + 5 + ], + "14": [ + 0, + 5 + ], + "16": [ + 6, + 7 + ], + "17": [ + 2, + 8 + ], + "18": [ + 0, + 8 + ], + "19": [ + 1, + 8 + ], + "2": [ + 1, + 2 + ], + "20": [ + 4, + 8 + ], + "21": [ + 3, + 8 + ], + "24": [ + 6, + 8 + ], + "25": [ + 2, + 7 + ], + "26": [ + 0, + 7 + ], + "28": [ + 4, + 7 + ], + "3": [ + 0, + 2 + ], + "32": [ + 8, + 9 + ], + "33": [ + 2, + 10 + ], + "34": [ + 0, + 10 + ], + "35": [ + 1, + 10 + ], + "36": [ + 4, + 10 + ], + "37": [ + 3, + 10 + ], + "4": [ + 2, + 3 + ], + "40": [ + 6, + 10 + ], + "44": [ + 5, + 10 + ], + "48": [ + 8, + 10 + ], + "49": [ + 2, + 9 + ], + "5": [ + 2, + 4 + ], + "50": [ + 0, + 9 + ], + "52": [ + 4, + 9 + ], + "56": [ + 6, + 9 + ], + "6": [ + 0, + 4 + ], + "64": [ + 0, + 13 + ], + "65": [ + 1, + 13 + ], + "66": [ + 0, + 12 + ], + "67": [ + 1, + 12 + ], + "68": [ + 4, + 12 + ], + "69": [ + 3, + 12 + ], + "7": [ + 0, + 3 + ], + "70": [ + 4, + 13 + ], + "72": [ + 6, + 12 + ], + "74": [ + 6, + 13 + ], + "76": [ + 5, + 12 + ], + "8": [ + 4, + 5 + ], + "80": [ + 8, + 12 + ], + "82": [ + 8, + 13 + ], + "88": [ + 7, + 12 + ], + "9": [ + 2, + 6 + ], + "96": [ + 10, + 12 + ], + "97": [ + 2, + 11 + ], + "98": [ + 0, + 11 + ] + }, + "maximum_target_coverage": 56, + "maximum_word": [ + 0, + 1, + 2, + 0, + 3, + 2, + 4, + 3, + 5, + 4, + 6, + 5, + 1, + 6 + ], + "schema_version": 1, + "source_calls": 14, + "sources": 7, + "target_mask_weights": [ + 1, + 2, + 3 + ], + "target_masks": 63 +} diff --git a/research/seven-source-weight123-connector-seed7db30a/SOURCES.json b/research/seven-source-weight123-connector-seed7db30a/SOURCES.json new file mode 100644 index 0000000000..c6563186a7 --- /dev/null +++ b/research/seven-source-weight123-connector-seed7db30a/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/universal-connector-boundary/CERTIFICATE.json", + "usage": "input", + "git_blob": "079e3e1441dc07c2f0536e9527acf290e51ea9c0", + "sha256": "e733746ba3e5151c829b4e8728bfff5ae3ed24d8d203eb77c735d20758e8266a" + }, + { + "path": "research/universal-connector-boundary/NOTICE.md", + "usage": "input", + "git_blob": "d9afdf81f656278dab69239f0fd94924f97df87b", + "sha256": "1172648a1883827399d5103a9916deaa4314e4ee2c28653c183890f6bd5a7a17" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "input", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ] +} diff --git a/research/seven-source-weight123-connector-seed7db30a/TASK.json b/research/seven-source-weight123-connector-seed7db30a/TASK.json new file mode 100644 index 0000000000..9a1a8213be --- /dev/null +++ b/research/seven-source-weight123-connector-seed7db30a/TASK.json @@ -0,0 +1,136 @@ +{ + "actual_scope": "For the fixed one-root F2 connector and seven arbitrary immutable sources, exhaust all 135135 source words with exactly two toggles per source against the 63 output masks of weights 1, 2, and 3. The exact maximum prefix-difference coverage is 56, attained by two canonical words; the displayed witness supports all 28 masks of weights 1 and 2 plus 28 triples. Its 56-output schedule attains the 126-complete-call floor.", + "ai_assistance": "Substantial OpenAI Codex assistance in scope selection, proof derivation, exhaustive search implementation, independent verifier, exact cost accounting, overlap checks and writing. No independent human review or proof-assistant formalization is claimed.", + "author": "Cinna Davis", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "bottleneck_link": "A shared source path can avoid reconstructing source-side terms separately for each sparse output. On the attained 56-mask subset it reduces complete B-map calls from 266 to 14, saves 252 calls, and also shortens the explicit root event stream. No supplier instantiates this connector, so no kappa is claimed.", + "budget_minutes": 60, + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2221", + "evidence": "RESULT.json records zero full-cover paths, maximum coverage 56 (two paths), all 135135 cases and the complete histogram. The maximum witness yields an arbitrary-dirty 56-output construction with 126 complete map calls and a 378-to-126 comparison against independent stars. verify.py independently enumerates the canonical words and replays dimensions 1, 2 and 3; three negative controls pass.", + "open_questions": [ + { + "blocked_by": "The normalized 16-event domain is much larger than 135135. No schedule or completed costed implementation is established here; a finite miss would remain scoped.", + "first_step": "Normalize 16-event words to one label used four times and six labels used twice; use a collision-pruned exact search or a constructive prefix-set design, then replay every output boundary pair.", + "question": "Can one additional even source toggle produce a 16-event seven-source path whose prefix differences cover all 63 weight-1/2/3 masks?", + "why_it_matters": "It would move the sparse family from the exact 56-mask boundary to a complete 63-output construction at 142 total calls, still far below the 434-call independent-star schedule." + } + ], + "original_card": { + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "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." + }, + "id": "connector-alphabet-change", + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ], + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment." + ], + "starting_points": [ + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ] + }, + "outcome": "completed", + "overlap": { + "entry_coverage": { + "discussions": { + "complete_pagination": true, + "fetched_at": "2026-10-15T00:44:46.738091+00:00", + "records": 918 + }, + "open_prs": { + "complete_pagination": true, + "fetched_at": "2026-10-15T00:42:45.805613+00:00", + "records": 463 + } + }, + "entry_warnings": [], + "limits": "Open PRs include drafts; pagination was complete. Closed work is covered only through local notes and ledger. The scan does not search arbitrary code diffs or certify novelty.", + "nearest": [ + { + "head": "697369a971eed02c0fbcd75ebefec9f59945f08e", + "pr": 2128, + "relationship": "Six-source universal support with a changed DUO alphabet." + }, + { + "head": "302b0e87d9328fabc2a670248afb357bbb44041b", + "pr": 2146, + "relationship": "Six-source universal support with a changed TRIO alphabet." + }, + { + "head": "dc252de1cc594829c3031abdb4de104713bc474a", + "pr": 2182, + "relationship": "Five-source universal/fixed-port and two-root boundary; different support family and root count." + } + ] + }, + "predecessors": [ + { + "head": "f3100aec6ce6a7b061987875d5e9a8b93801ac0b", + "scope": "Three-source connector query optimum; predecessor framework.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/934" + }, + { + "head": "cf360b4b09b7d0419decdd6ac85421fefed55bdd", + "scope": "General dirty connector and paired-prefix-difference criterion.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/943" + }, + { + "head": "c713ff9eff95446508aeb865a9f58b1758b2a00a", + "scope": "Five-source universal path with charged pair-source calls.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2056" + }, + { + "head": "697369a971eed02c0fbcd75ebefec9f59945f08e", + "scope": "Six-source universal path with charged DUO calls.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2128" + }, + { + "head": "302b0e87d9328fabc2a670248afb357bbb44041b", + "scope": "Six-source universal path exclusion with one charged TRIO call.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2146" + }, + { + "head": "dc252de1cc594829c3031abdb4de104713bc474a", + "scope": "Fixed-port five-source optimum and two-root universal-mask boundary.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2182" + } + ], + "priority_revision": 4, + "schema_version": 1, + "scope_change_reason": "The selector card asks for a changed connector alphabet. This investigation retains the original alphabet and changes the object to a sparse seven-source output-support family, as required by the card change trigger. The initial weight-1/2 family has a trivial adjacent-toggle path, so before the bounded search it was refined once to all masks of weights at most 3. This is a structural side result about source sharing on sparse rows, not evidence for an extra operation.", + "scope_status": "changed", + "selection": { + "catalogue_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "priority_revision": 4, + "refined_scope_key": "6a70fd459cc03339ab38", + "seed": "7db30a45a4ca218f66c410637c8459f3", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selector_scope_key": "ff4f5113ed2256ab19ed", + "task_id": "connector-alphabet-change", + "track": "recursive-interfaces" + }, + "stop_rule": "Exhaust the 135135 canonical double-occurrence words on seven labels exactly once. Stop after the complete coverage histogram, maximum witness, independent restricted-growth replay, dirty-state positive fixtures, and three meaningful failure controls. Do not search 16-event words in this cycle.", + "task_id": "connector-alphabet-change" +} diff --git a/research/seven-source-weight123-connector-seed7db30a/VERIFY.json b/research/seven-source-weight123-connector-seed7db30a/VERIFY.json new file mode 100644 index 0000000000..c8862601b7 --- /dev/null +++ b/research/seven-source-weight123-connector-seed7db30a/VERIFY.json @@ -0,0 +1,45 @@ +{ + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/search.py" + ], + "checks": "Complete 135135-pairing exact census; deterministic RESULT.json receipt with coverage histogram and maximum witness.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Independent restricted-growth census, exact histogram and maximum check, arbitrary dirty-state maps at dimensions 1 to 3, and three negative controls.", + "timeout_seconds": 120 + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "checks": "Repeat the fail-closed census and controls with Python optimization enabled; verifier decisions do not depend on assert.", + "timeout_seconds": 120 + } + ], + "inputs": [ + "certificates/selected-result.json", + "research/universal-connector-boundary/CERTIFICATE.json", + "research/universal-connector-boundary/NOTICE.md", + "research/universal-connector-boundary/README.md" + ], + "python": "3.12", + "requirements": [], + "schema_version": 1, + "status": "ready" +} diff --git a/research/seven-source-weight123-connector-seed7db30a/search.py b/research/seven-source-weight123-connector-seed7db30a/search.py new file mode 100644 index 0000000000..1bd6fa9d5d --- /dev/null +++ b/research/seven-source-weight123-connector-seed7db30a/search.py @@ -0,0 +1,161 @@ +#!/usr/bin/env python3 +"""Exhaust the seven-source, two-occurrence prefix paths for masks of weight <= 3.""" + +from collections import Counter +import json +from pathlib import Path + + +N = 7 +PATH = Path(__file__).resolve().parent + + +def targets(): + return tuple( + mask + for mask in range(1, 1 << N) + if mask.bit_count() <= 3 + ) + + +def pairings(mask=0, pairs=()): + """Each perfect matching of positions 0..13 appears exactly once.""" + if len(pairs) == N: + yield pairs + return + first = next(i for i in range(2 * N) if not (mask >> i) & 1) + for other in range(first + 1, 2 * N): + if (mask >> other) & 1: + continue + yield from pairings( + mask | (1 << first) | (1 << other), + pairs + ((first, other),), + ) + + +def word_from_pairs(pairs): + word = [None] * (2 * N) + for label, (first, second) in enumerate(pairs): + word[first] = label + word[second] = label + return tuple(word) + + +def prefixes(word): + result = [0] + for label in word: + result.append(result[-1] ^ (1 << label)) + return tuple(result) + + +def differences(q): + return {q[i] ^ q[j] for i in range(len(q)) for j in range(i + 1, len(q))} + + +def first_readout_pairs(q, wanted): + result = {} + for mask in sorted(wanted, key=lambda x: (x.bit_count(), x)): + for i in range(len(q)): + for j in range(i + 1, len(q)): + if q[i] ^ q[j] == mask: + result[str(mask)] = [i, j] + break + if str(mask) in result: + break + return result + + +def main(): + wanted = set(targets()) + histogram = Counter() + total = hits = 0 + best = -1 + witness = None + best_witness = None + for pairs in pairings(): + total += 1 + word = word_from_pairs(pairs) + q = prefixes(word) + cover = differences(q) + score = len(wanted & cover) + histogram[score] += 1 + if score > best: + best = score + best_witness = (word, q, cover) + if score == len(wanted): + hits += 1 + if witness is None: + witness = (word, q) + + record = { + "schema_version": 1, + "sources": N, + "source_calls": 2 * N, + "target_mask_weights": [1, 2, 3], + "target_masks": len(wanted), + "canonical_pairings_enumerated": total, + "full_cover_paths": hits, + "maximum_target_coverage": best, + "coverage_histogram": {str(k): histogram[k] for k in sorted(histogram)}, + } + if best_witness is not None: + word, q, cover = best_witness + support = sorted(wanted & cover) + source_incidence = [sum((mask >> j) & 1 for mask in support) for j in range(N)] + weight_counts = { + str(k): sum(mask.bit_count() == k for mask in support) + for k in (1, 2, 3) + } + record["maximum_word"] = list(word) + record["maximum_prefix_states"] = list(q) + record["maximum_covered_masks"] = support + record["maximum_missing_masks"] = sorted(wanted - cover) + record["maximum_readout_pairs"] = first_readout_pairs(q, support) + record["attained_subset_cost"] = { + "weight_counts": weight_counts, + "source_incidence_per_map": source_incidence, + "star_source_calls": 2 * sum(source_incidence), + "shared_source_calls": 2 * N, + "target_calls": 2 * len(support), + "star_total_calls": 2 * sum(source_incidence) + 2 * len(support), + "shared_total_calls": 2 * N + 2 * len(support), + "source_calls_saved": 2 * sum(source_incidence) - 2 * N, + "star_instruction_bits": 4 * 2 * sum(source_incidence) + 7 * 2 * len(support), + "shared_instruction_bits": 4 * 2 * N + 7 * 2 * len(support), + } + full_incidences = sum(mask.bit_count() for mask in wanted) + record["full_family_cost_screen"] = { + "source_incidence": full_incidences, + "star_source_calls": 2 * full_incidences, + "hypothetical_shared_source_calls": 2 * N, + "target_calls": 2 * len(wanted), + "star_total_calls": 2 * full_incidences + 2 * len(wanted), + "hypothetical_shared_total_calls": 2 * N + 2 * len(wanted), + "source_calls_savings_if_cover_existed": 2 * full_incidences - 2 * N, + "star_instruction_bits": 4 * 2 * full_incidences + 7 * 2 * len(wanted), + "hypothetical_shared_instruction_bits": 4 * 2 * N + 7 * 2 * len(wanted), + "attained": False, + } + if witness is not None: + word, q = witness + record["witness_word"] = list(word) + record["prefix_states"] = list(q) + record["readout_pairs"] = first_readout_pairs(q, wanted) + (PATH / "RESULT.json").write_text( + json.dumps(record, indent=2, sort_keys=True) + "\n", + encoding="utf-8", + ) + print( + "SEVEN_SOURCE_WEIGHT123_SEARCH " + f"pairings={total} targets={len(wanted)} hits={hits} best={best}" + ) + if witness is not None: + print("word=" + " ".join(str(x) for x in witness[0])) + print("prefixes=" + " ".join(str(x) for x in witness[1])) + if best_witness is not None: + print("maximum_word=" + " ".join(str(x) for x in best_witness[0])) + print("maximum_missing=" + " ".join(str(x) for x in sorted(wanted - best_witness[2]))) + + +if __name__ == "__main__": + main() diff --git a/research/seven-source-weight123-connector-seed7db30a/verify.py b/research/seven-source-weight123-connector-seed7db30a/verify.py new file mode 100644 index 0000000000..5acf747157 --- /dev/null +++ b/research/seven-source-weight123-connector-seed7db30a/verify.py @@ -0,0 +1,243 @@ +#!/usr/bin/env python3 +"""Independent exact replay and dirty-state controls for the seven-source result.""" + +import json +from pathlib import Path +import random + + +N = 7 +ROOT = Path(__file__).resolve().parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def target_masks(): + return tuple(mask for mask in range(1, 1 << N) if mask.bit_count() <= 3) + + +def canonical_words(): + """Generate restricted-growth double-occurrence words, independently of pairings.""" + counts = [0] * N + word = [] + + def visit(next_label): + if len(word) == 2 * N: + if next_label == N: + yield tuple(word) + return + for label in range(next_label): + if counts[label] == 1: + counts[label] = 2 + word.append(label) + yield from visit(next_label) + word.pop() + counts[label] = 1 + if next_label < N: + counts[next_label] = 1 + word.append(next_label) + yield from visit(next_label + 1) + word.pop() + counts[next_label] = 0 + + yield from visit(0) + + +def prefix_states(word): + q = [0] + for label in word: + q.append(q[-1] ^ (1 << label)) + return tuple(q) + + +def difference_set(q): + return {q[i] ^ q[j] for i in range(len(q)) for j in range(i + 1, len(q))} + + +def first_pair_for(q, mask): + for left in range(len(q)): + for right in range(left + 1, len(q)): + if q[left] ^ q[right] == mask: + return [left, right] + return None + + +def matvec(rows, vector): + result = 0 + for i, row in enumerate(rows): + if (row & vector).bit_count() & 1: + result |= 1 << i + return result + + +def random_matrix(rng, width): + return tuple(rng.randrange(1 << width) for _ in range(width)) + + +def run_word(word, pairs, masks, source_maps, output_maps, sources, initial_outputs, z0, + drop_late_readout=None): + """Run the literal event schedule: reads at boundaries, then the next B toggle.""" + at_boundary = [[] for _ in range(len(word) + 1)] + for mask in masks: + left, right = pairs[str(mask)] + at_boundary[left].append(mask) + at_boundary[right].append(mask) + z = z0 + outputs = dict(initial_outputs) + for boundary in range(len(word) + 1): + for mask in at_boundary[boundary]: + if drop_late_readout == (mask, boundary): + continue + outputs[mask] ^= matvec(output_maps[mask], z) + if boundary < len(word): + source = word[boundary] + z ^= matvec(source_maps[source], sources[source]) + return z, outputs + + +def expected_outputs(masks, source_maps, output_maps, sources, initial_outputs): + expected = dict(initial_outputs) + for mask in masks: + source_sum = 0 + for source in range(N): + if (mask >> source) & 1: + source_sum ^= matvec(source_maps[source], sources[source]) + expected[mask] ^= matvec(output_maps[mask], source_sum) + return expected + + +def main(): + result = json.loads((ROOT / "RESULT.json").read_text(encoding="utf-8")) + wanted = target_masks() + need(len(wanted) == 63, "target family must contain 63 masks") + + histogram = {} + total = full = best = 0 + for word in canonical_words(): + total += 1 + score = len(set(wanted) & difference_set(prefix_states(word))) + histogram[score] = histogram.get(score, 0) + 1 + if score > best: + best = score + if score == len(wanted): + full += 1 + + need(total == 135135, "independent restricted-growth census is incomplete") + need(result.get("canonical_pairings_enumerated") == total, "pairing count mismatch") + need(result.get("full_cover_paths") == full == 0, "full-cover count mismatch") + need(result.get("maximum_target_coverage") == best == 56, "maximum coverage mismatch") + need(result.get("coverage_histogram") == {str(k): histogram[k] for k in sorted(histogram)}, + "coverage histogram mismatch") + + word = tuple(result["maximum_word"]) + q = prefix_states(word) + counts = [word.count(i) for i in range(N)] + need(len(word) == 14 and counts == [2] * N, "maximum witness is not a 14-toggle word") + need(list(q) == result["maximum_prefix_states"], "witness prefix states mismatch") + cover = set(wanted) & difference_set(q) + missing = set(wanted) - cover + need(len(cover) == 56, "witness does not attain the enumerated maximum") + need(sorted(cover) == result["maximum_covered_masks"], "witness covered-mask receipt mismatch") + need(sorted(missing) == result["maximum_missing_masks"], "witness missing-mask receipt mismatch") + need(len(missing) == 7, "expected seven missing weight-three masks") + need(all(mask.bit_count() == 3 for mask in missing), "a singleton or pair mask is missing") + pairs = result["maximum_readout_pairs"] + need(set(map(int, pairs)) == cover, "readout table is not exactly the witnessed support") + for mask in cover: + endpoints = pairs[str(mask)] + need(len(endpoints) == 2 and endpoints[0] < endpoints[1], "invalid readout endpoints") + need(q[endpoints[0]] ^ q[endpoints[1]] == mask, "wrong readout difference") + + incidences = [sum((mask >> j) & 1 for mask in cover) for j in range(N)] + weight_counts = { + str(k): sum(mask.bit_count() == k for mask in cover) + for k in (1, 2, 3) + } + subset_cost = { + "weight_counts": weight_counts, + "source_incidence_per_map": incidences, + "star_source_calls": 2 * sum(incidences), + "shared_source_calls": 2 * N, + "target_calls": 2 * len(cover), + "star_total_calls": 2 * sum(incidences) + 2 * len(cover), + "shared_total_calls": 2 * N + 2 * len(cover), + "source_calls_saved": 2 * sum(incidences) - 2 * N, + "star_instruction_bits": 4 * 2 * sum(incidences) + 7 * 2 * len(cover), + "shared_instruction_bits": 4 * 2 * N + 7 * 2 * len(cover), + } + need(result.get("attained_subset_cost") == subset_cost, "attained subset invoice mismatch") + full_incidence = sum(mask.bit_count() for mask in wanted) + full_screen = { + "source_incidence": full_incidence, + "star_source_calls": 2 * full_incidence, + "hypothetical_shared_source_calls": 2 * N, + "target_calls": 2 * len(wanted), + "star_total_calls": 2 * full_incidence + 2 * len(wanted), + "hypothetical_shared_total_calls": 2 * N + 2 * len(wanted), + "source_calls_savings_if_cover_existed": 2 * full_incidence - 2 * N, + "star_instruction_bits": 4 * 2 * full_incidence + 7 * 2 * len(wanted), + "hypothetical_shared_instruction_bits": 4 * 2 * N + 7 * 2 * len(wanted), + "attained": False, + } + need(result.get("full_family_cost_screen") == full_screen, + "full-family optimistic cost screen mismatch") + + # Dirty-state replay on arbitrary small F2-linear maps and inputs. + rng = random.Random(0x7DB30A45) + masks = tuple(sorted(cover)) + for width in (1, 2, 3): + for _ in range(4): + source_maps = [random_matrix(rng, width) for _ in range(N)] + output_maps = {mask: random_matrix(rng, width) for mask in masks} + sources = [rng.randrange(1 << width) for _ in range(N)] + initial_outputs = {mask: rng.randrange(1 << width) for mask in masks} + z0 = rng.randrange(1 << width) + expected = expected_outputs(masks, source_maps, output_maps, sources, + initial_outputs) + z, outputs = run_word(word, pairs, masks, source_maps, output_maps, sources, + initial_outputs, z0) + need(z == z0, "source word failed to restore arbitrary dirty connector") + need(outputs == expected, "dirty-state output identity failed") + + # Negative control 1: delete one source toggle; a dirty connector residue remains. + mutated_word = list(word) + mutated_word.remove(0) + identity = (1,) + residue = 0 + for source in mutated_word: + if source == 0: + residue ^= 1 # B_0 x_0, with B_0=I and x_0=1. + need(residue != 0, "deleted-source-toggle control did not detect lost restoration") + + # Negative control 2: delete the later readout for singleton mask 1. + source_maps = [identity] + [(0,)] * (N - 1) + output_maps = {mask: identity for mask in masks} + sources = [0] * N + initial_outputs = {mask: 0 for mask in masks} + z, outputs = run_word(word, pairs, masks, source_maps, output_maps, sources, + initial_outputs, 1, drop_late_readout=(1, pairs["1"][1])) + need(z == 1 and outputs[1] != 0, + "deleted-readout control did not expose dirty connector leakage") + + # Negative control 3: replace the singleton endpoint pair by two equal boundaries. + bad_pairs = dict(pairs) + bad_pairs["1"] = [pairs["1"][0], pairs["1"][0]] + sources = [1] + [0] * (N - 1) + initial_outputs = {mask: 0 for mask in masks} + expected = expected_outputs(masks, source_maps, output_maps, sources, initial_outputs) + _, bad_outputs = run_word(word, bad_pairs, masks, source_maps, output_maps, sources, + initial_outputs, 0) + need(bad_outputs != expected, "wrong-endpoint control did not detect an omitted mask") + + print( + "PASS_SEVEN_SOURCE_WEIGHT123_PAIRING_BOUND " + f"pairings={total} max={best} full_hits={full} " + f"subset_calls={subset_cost['shared_total_calls']} controls=3" + ) + + +if __name__ == "__main__": + main()