diff --git a/research/connector-frame-73-exclusion/README.md b/research/connector-frame-73-exclusion/README.md new file mode 100644 index 0000000000..101898d887 --- /dev/null +++ b/research/connector-frame-73-exclusion/README.md @@ -0,0 +1,245 @@ +# Paid connector frames still require 74 map calls + +The generic five-source dirty connector cannot use **73 A/B map calls**, even +with arbitrarily many invertible changes of the connector's coordinates. +Together with the existing 74-call construction, this gives the exact minimum +of 74 map calls in the contract below, even if frame calls have zero price. +This closes the first open question in Adam Gall's +[PR #1915](https://github.com/CrocSwap/integer-mult-bounds/pull/1915), inspected +at `d30d64fea909219c364b11c2452f2207326e2b1f`. + +PR #1915 excludes 72 map calls and proves the 74/76 unit-token bounds. +Its normalization argument is credited and restated here. The new step handles +the one operator that must occur three times in a 73-call word. No selected +supplier, physical runtime improvement or new multiplication exponent is claimed. + +## Contract + +Work over F2 with five immutable L-bit source rows `x_j`, 31 output rows +`y_m`, one connector `z`, and `L >= 1`. Every row starts arbitrarily dirty. +For every nonzero five-bit mask `m`, the required output is + +```text +y_m += A_m sum_{j: m_j=1} B_j x_j; all x_j and z restored. +``` + +The maps `A_m,B_j` are arbitrary L-by-L binary matrices. They may be singular +or noncommuting. A single straight-line word, including its frame matrices, +must work for every choice of these maps and inputs. The word may depend on +L and the requested masks, but not on the entries of the maps. + +The only operations are complete calls + +```text +B_j: z += B_j x_j +A_m: y_m += A_m z +FRAME_R: z <- R z, with R invertible +``` + +Each call preserves other rows and restores its private scratch and tape heads. +No additional connector, source mutation, output mixing, reset, direct product +call or free copy is allowed. Frame implementations are charged. This is +PR #1915's extension of Ross Richardson's +[original connector contract](../universal-connector-boundary/README.md). + +## Normalize the connector and count the exceptional map + +Let `P_t` be the chronological product of frames through time t. In normalized +coordinates `u = P_t^-1 z`, a source event at phase H inserts `H^-1 B_j x_j`. +A readout at phase K applies `A_m K` to u. Arbitrary connector dirt forces +`P_final = I`. Each active B needs at least two calls to cancel its transported +source. Each active A needs at least two calls to cancel connector dirt. +There are 36 active maps, so at least 72 map calls are necessary. + +For a paired source, restoration gives `H^-1 + H'^-1 = 0`, hence `H=H'`. +For a paired output, dirt cancellation gives `K+K'=0`, hence `K=K'`. +Between two readouts, a paired source contributes zero if both its events or +neither event occur in the interval. If exactly one occurs, its coefficient is +`A_m K H^-1 B_j`. For arbitrary A and B, this equals `A_m B_j` precisely when +`K=H`, and cannot be identically zero because `K H^-1` is invertible. + +Thus a 72-call word projects to an ordinary twice-per-source word whose prefix +differences include every requested mask. Richardson's exact 945-pairing +exclusion rules this out for five sources. The local verifier reconstructs +that census without importing predecessor code. + +At 73 calls, exactly one map occurs three times and every other map twice. +The following two cases exhaust the possibilities. They use no assumption +that every map count is even. + +## Case 1: one output has three readouts + +All five sources are paired. Every pair of source labels occurs together in +some paired output, even after removing the exceptional output from the 31 +masks. The preceding coefficient condition therefore forces every source's +insertion phase to be one common H. + +Let `K_1,K_2,K_3` be the three exceptional readout phases. Dirt cancellation +requires `K_1+K_2+K_3=0`. All three are invertible, nonzero and distinct. +Their proper nonempty subset sums are exactly the three K matrices. +The exceptional mask is nonzero, so some source coefficient must equal H +before multiplying by `H^-1`. Hence exactly one K equals H. Write its index +as r, and the other two indices as s,t. Then `K_t=H+K_s`. + +Let `q_r,q_s,q_t` be the source-parity prefix vectors at these readouts. +For each source j, the exceptional coefficient before `H^-1` is + +```text +H (q_rj + q_tj) + K_s (q_sj + q_tj). +``` + +Distinct nonzero matrices H and `K_s` are linearly independent over F2. +For this expression to be either zero or H for every j, `q_s=q_t` is +necessary. The requested mask is therefore `q_r + q_t`, already an ordinary +two-prefix difference. The extra readout adds no mask. The other 30 outputs +also give ordinary differences, contradicting the 945-pairing exclusion. + +## Case 2: one source has three insertions + +Call the exceptional source e. The other four sources are paired and every +output is paired. Outputs containing pairs of ordinary sources force their +insertion phases to one common H. Any output mask containing an ordinary +source must have readout phase H. + +Write the three normalized insertion matrices of source e as +`U_1,U_2,U_3`, where each U is the inverse of its physical insertion phase. +Restoration gives `U_1+U_2+U_3=0`. They are invertible and distinct. Consider +an output containing e and one ordinary source. Its interval must select a +subset of the U matrices with sum `H^-1`. The proper subset sums are exactly +the three U matrices, so exactly one, `U_r`, equals `H^-1`. +For the other indices s,t, `U_t=H^-1+U_s`. + +For any readout interval with phase H, let `d_k` indicate whether exceptional +event k lies inside it. The normalized coefficient of e is + +```text +H^-1 (d_r + d_t) + U_s (d_s + d_t). +``` + +It must be zero or `H^-1`. Independence of `H^-1` and `U_s` forces `d_s=d_t`. +Replace the exceptional event at r and the event at s by two ordinary +toggles of source e, and delete event t. Each interval for an output containing +an ordinary source preserves its mask, since the new e coefficient is +`d_r+d_s`. All ordinary source coefficients also remain unchanged. + +Only the singleton mask `{e}` may have used a different readout phase. It is +always a prefix difference of the new word: take the boundaries immediately +before and after either remaining e event. Consequently the new word has two +events per source and covers all 31 nonzero masks. This again contradicts the +945-pairing exclusion. This replacement is a proof device, not a claim that +arbitrary frame words can be erased without changing their map. + +## Complete cost consequence + +Both 73-call cases are impossible. Richardson's `five_extra_output` word +attains 74 map calls without frames, so the map-call minimum is exactly 74. +The verifier checks that full word and its dirty-state inverse. + +For a word W, price the complete implementation as + +```text +C(W) = I(W) + P(W) + D(W) + + sum_F n_F c_F + sum_frame_events c_R. +``` + +I includes admission and row layout. P includes coefficient and frame +preparation. D includes instruction storage, scheduling and root dispatch. +Each complete call price includes its arithmetic, source access, target +updates, private scratch and head restoration. At fixed positive map prices, +let `c_min = min_F c_F`. The new necessary map/frame bill is + +```text +sum_F n_F c_F + sum_frame_events c_R + >= 2 sum_F c_F + 2 c_min + sum_frame_events c_R. +``` + +If the word uses a nonidentity frame, restoring arbitrary dirt requires at +least two nonidentity frame events. With a positive lower frame price f_min, +the last term is at least `2 f_min`. For equal map price c, frames cannot +reduce the `74 c` map bill even when their own price is zero. For unit call +tokens this recovers PR #1915's 74 minimum and 76 minimum when nonidentity +frame use is required. For `L>=2`, a shear/inverse pair followed by the +unframed 74-call word attains 76. These token bounds were already in #1915. + +This is not an exact weighted optimum. Additional calls to cheap maps could +change which expensive map must repeat, and I, P and D still need pricing. +No occurrence of this interface in the selected supplier is established. + +## Reproduce the finite evidence + +The standard-library verifier checks the proof's finite implications and +independently replays the inherited positive construction. The claim for +arbitrary L is the written proof above, not a finite-search extrapolation. + +```sh +uv run --python 3.12 --no-project python scripts/research_package.py \ + --package research/connector-frame-73-exclusion +uv run --python 3.12 --no-project python -I -O -B \ + research/connector-frame-73-exclusion/verify.py +``` + +Both commands passed on CPython 3.12.13, macOS 27.0.1 arm64. The registered +run emitted `PASS_REGISTERED_RESEARCH_PACKAGE` and passed all four behavioral +tests. The optimized direct run emitted `PASS_CONNECTOR_FRAME_73_EXCLUSION`. +The repository's 42 onboarding tests, package metadata/source-pin check, +Ruff checks and `git diff --check` also passed. In a temporary mutation, +reversing the output-acceptance predicate made three of the four tests fail. +Hosted CI is separate. No selected-supplier cold replay was run. + +The receipt includes these bounded checks: + +| Check | Domain and conclusion | +| --- | --- | +| Phase identities | All 12 and 8,064 ordered zero-sum invertible triples in GL(2,2) and GL(3,2); all subset sums obey the two-case reduction | +| Arbitrary-map coefficients | 294,912 direct vector comparisons over every pair of two-by-two binary A/B maps, including singular and noncommuting maps | +| Exceptional output | All 810,810 pairing/boundary-triple/distinguished-phase cases; 170,820 scalar-mask cases, no new mask | +| Exceptional source | All 51,975 annotated source words; at most 31 masks even after granting the singleton; a concrete wrong-deletion counterexample | +| Full-word controls | The pinned 74-call word, basis-column and dirty-state inverse replay; odd-count framed restoration; missing restoration, missing readout and wrong target rejection | + +The source enumeration uses `binomial(11,3) * 105 * 3` cases: three positions +for source e, every canonical pairing of the four ordinary sources, and the +distinguished event. Exchanging the other two phase labels does not change +scalar-mask validity. It grants arbitrary frame availability at readout +boundaries, which enlarges the possible schedules. The exclusion survives +this favorable relaxation. + +## Scope, provenance and credit + +Base: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. +[TASK.json](TASK.json) records selector seed, scope, overlap and predecessor +head. [SOURCES.json](SOURCES.json) pins the inherited certificate, contract +and attribution by Git blob and SHA256. The local proof includes all needed +normalization steps and imports no code from pending PR #1915. + +The final overlap refresh completely paginated 588 open PRs at 14:30:45 UTC +and 566 Discussion records at 14:32:56 UTC on 2026-10-14, without warnings. +The direct predecessor remained at its pinned head. These are search leads, +not proof of novelty; arbitrary code diffs and all closed work were not searched. +The [scoped claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1884#discussioncomment-18925922) +records the complementary scope and attribution before the computation. + +Adam Gall's PR #1915 supplies the paid-frame contract, normalization, +paired-endpoint proof and the precise 73-map question. Ross Richardson's +PR943/PR934 supplies the universal connector, paired-prefix criterion, +five-source exclusion and attaining word. His pinned NOTICE retains the +common-factor fanout and dirty-commutator lineage, including @shhxera and +Chafik Boukhalfa. PR #1887 uses two connectors, PR #1858 uses map-dependent +structured charts, and PR #1524 permits source mutations. Those contracts +fall outside this theorem and their constructions are not contradicted. + +The selected record and all frozen inputs remain unchanged. This result +does not settle operator-specific synthesis, more workspace, physical hosting, +precision or any inherited multiplication-theorem obligation. It is a scoped +written proof with exact computational checks, not a proof-assistant theorem. + +## Open next questions + +No additional investigation is assigned by this package. The named 73-map +question is closed under its exact generic one-connector hypotheses. A new +construction attempt needs an explicit change to those hypotheses or a +separate unequal-price objective. No selected-supplier occurrence or cost +data is supplied to justify choosing such a next experiment here. + +Prepared by Arham Garg with substantial OpenAI Codex assistance in the proof, +implementation, checking and writing. New work is Apache-2.0. No independent +human review is claimed. diff --git a/research/connector-frame-73-exclusion/SOURCES.json b/research/connector-frame-73-exclusion/SOURCES.json new file mode 100644 index 0000000000..788c1c43f9 --- /dev/null +++ b/research/connector-frame-73-exclusion/SOURCES.json @@ -0,0 +1,45 @@ +{ + "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/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" + } + ], + "external_proof_context": { + "repository": "CrocSwap/integer-mult-bounds", + "pr": 1915, + "commit": "d30d64fea909219c364b11c2452f2207326e2b1f", + "path": "research/connector-frame-rigidity/README.md", + "git_blob": "8f792e62700ec3809075b500f233cee00f3543fe", + "sha256": "d4c5aea3ecc0e988dfd01ee9e47381d813a736cf7eec96eb4f352ab4dc6f3872", + "usage": "Attribution and open-question provenance only; no executable or proof assumption imported." + } +} diff --git a/research/connector-frame-73-exclusion/TASK.json b/research/connector-frame-73-exclusion/TASK.json new file mode 100644 index 0000000000..a7703c225a --- /dev/null +++ b/research/connector-frame-73-exclusion/TASK.json @@ -0,0 +1,118 @@ +{ + "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": "Exclude exactly 73 generic A/B calls for five sources and all 31 nonzero masks with one dirty connector and arbitrary paid invertible connector-only frames.", + "scope_change_reason": "Resolve the first open next question of PR1915, beyond its paired 72-map endpoint. The added operation is unchanged; the extra map call is the unresolved case.", + "bottleneck_link": "A 73-map construction could save an expensive recursive call when frames are cheap. A 74-map floor closes that route under the generic operator-independent contract.", + "budget_minutes": 60, + "stop_rule": "Analyze the triply read output and triply called source cases. Stop and report the missing implication if either common-phase reduction fails. Bound computation to exact GL(2,2), GL(3,2), five-source pairings and explicit dirty-state controls within the 60-minute session.", + "outcome": "negative-result", + "evidence": "README.md proves both 73-map cases impossible. verify.py independently checks matrix identities, all 945 pairings, 810810 exceptional-readout cases, 51975 annotated exceptional-source words, arbitrary-map coefficients, complete positive words and failure controls.", + "author": "Arham Garg", + "ai_assistance": "Substantial OpenAI Codex assistance, GPT-6-Astra, in proof, implementation, checking and writing. No independent human or proof-assistant review is claimed.", + "open_questions": [], + "no_open_questions_reason": "The specific 73-map question is resolved under its exact hypotheses. No selected-supplier occurrence or cost data justifies choosing another experiment here.", + "selection": { + "seed": "29b545b2df07ed5757ed1985b860422d", + "track": "recursive-interfaces", + "scope_key": "0c9f43f3c7d61edb36fe" + }, + "predecessor": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1915", + "head": "d30d64fea909219c364b11c2452f2207326e2b1f", + "author": "Adam Gall", + "scope": "The 72-map exclusion with arbitrary invertible frames; leaves 73 map calls open." + }, + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1884#discussioncomment-18925922", + "overlap": { + "entry_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T14:14:56.429668+00:00", + "complete_pagination": true, + "records": 580 + }, + "discussions": { + "fetched_at": "2026-10-14T14:17:14.822957+00:00", + "complete_pagination": true, + "records": 553 + } + }, + "entry_warnings": [], + "nearest": [ + { + "pr": 1915, + "head": "d30d64fea909219c364b11c2452f2207326e2b1f", + "relationship": "Direct predecessor; leaves 73 map calls open." + }, + { + "pr": 1887, + "head": "025d4fcd87f1b6ea01aa1c52721f8f46389aacce", + "relationship": "Adds a second connector, excluded here." + }, + { + "pr": 1858, + "head": "4b650a8471c38f87519da497019dde24228c7f8a", + "relationship": "Chooses charts from structured map relations, excluded here." + }, + { + "pr": 1524, + "head": "5c1f39788a0fc669b7e37e27785c63e85788c350", + "relationship": "Permits source mutations, excluded here." + } + ], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "submission_coverage": { + "open_prs": { + "fetched_at": "2026-10-14T14:30:45.295646+00:00", + "complete_pagination": true, + "records": 588 + }, + "discussions": { + "fetched_at": "2026-10-14T14:32:56.673495+00:00", + "complete_pagination": true, + "records": 566 + } + }, + "submission_warnings": [], + "submission_searched_at": "2026-10-14T14:32:56.794132+00:00" + } +} diff --git a/research/connector-frame-73-exclusion/VERIFY.json b/research/connector-frame-73-exclusion/VERIFY.json new file mode 100644 index 0000000000..60e15f5bfa --- /dev/null +++ b/research/connector-frame-73-exclusion/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/universal-connector-boundary/CERTIFICATE.json", + "research/universal-connector-boundary/NOTICE.md", + "research/universal-connector-boundary/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact phase and prefix reductions, independent five-source census, complete 74-call positive word and inverse, odd-count restoration, wrong-deletion counterexample." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 30, + "checks": "Complete-word acceptance and rejection of omitted source restoration, omitted dirty readout and wrong output mask." + } + ] +} diff --git a/research/connector-frame-73-exclusion/test_verify.py b/research/connector-frame-73-exclusion/test_verify.py new file mode 100755 index 0000000000..d99dacf32f --- /dev/null +++ b/research/connector-frame-73-exclusion/test_verify.py @@ -0,0 +1,49 @@ +#!/usr/bin/env python3 +"""Behavior checks for the arbitrary-dirty complete-word acceptance boundary.""" +import importlib.util +import json +import unittest +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("frame73", HERE / "verify.py") +verifier = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verifier) + + +class CompleteWordTests(unittest.TestCase): + def setUp(self): + source = HERE.parent / "universal-connector-boundary" / "CERTIFICATE.json" + self.fixture = json.loads(source.read_text())["schedules"]["five_extra_output"] + + def check(self, word, rows=None): + return verifier.check_unframed_word( + word, self.fixture["sources"], self.fixture["rows"] if rows is None else rows + ) + + def test_complete_74_call_construction(self): + self.assertEqual(self.check(self.fixture["word"]), (32, tuple(range(1, 32)))) + + def test_missing_source_restore_rejects(self): + word = self.fixture["word"].copy() + index = max(i for i, event in enumerate(word) if event[0] == "B") + del word[index] + with self.assertRaisesRegex(ValueError, "connector restoration"): + self.check(word) + + def test_missing_readout_rejects_arbitrary_connector_dirt(self): + word = self.fixture["word"].copy() + index = next(i for i, event in enumerate(word) if event == ["A", 20]) + del word[index] + with self.assertRaisesRegex(ValueError, "output map"): + self.check(word) + + def test_wrong_nonzero_target_rejects(self): + rows = self.fixture["rows"].copy() + rows[20] ^= 1 + with self.assertRaisesRegex(ValueError, "output map"): + self.check(self.fixture["word"], rows) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/connector-frame-73-exclusion/verify.py b/research/connector-frame-73-exclusion/verify.py new file mode 100755 index 0000000000..176d703cee --- /dev/null +++ b/research/connector-frame-73-exclusion/verify.py @@ -0,0 +1,326 @@ +#!/usr/bin/env python3 +"""Exact finite checks of the 73-map reduction. No predecessor code imports. + +Arham Garg, with substantial OpenAI Codex assistance. Apache-2.0. +The arbitrary-dimension statement is the written proof in README.md. +""" +import json +from collections import Counter +from hashlib import sha256 +from itertools import combinations, combinations_with_replacement, product +from math import prod +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def check_unframed_word(word, sources, rows): + # Each bit represents a distinct formal B_j x_j, plus independent z dirt. + # An output's bits represent A_i applied to those formal expressions. + z = 1 << sources + outputs = [0] * len(rows) + for kind, index in word: + if kind == "B": + require(0 <= index < sources, "invalid source index") + z ^= 1 << index + elif kind == "A": + require(0 <= index < len(rows), "invalid output index") + outputs[index] ^= z + else: + raise ValueError("unknown unframed operation") + require(z == 1 << sources, "connector restoration failed") + require(outputs == rows, "output map or arbitrary-dirty cancellation failed") + return z, tuple(outputs) + + +def xor_matrices(a, b): + return tuple(x ^ y for x, y in zip(a, b)) + + +def apply(matrix, vector): + return sum(((row & vector).bit_count() % 2) << i for i, row in enumerate(matrix)) + + +def invertible(matrix): + # Enumerate its kernel independently of the row arithmetic used elsewhere. + return all(apply(matrix, v) != 0 for v in range(1, 1 << len(matrix))) + + +def inverse(matrix, group): + n = len(matrix) + return next(b for b in group if all(apply(b, apply(matrix, 1 << i)) == 1 << i for i in range(n))) + + +def sum_selected(triple, bits): + value = (0,) * len(triple[0]) + for index, matrix in enumerate(triple): + if bits >> index & 1: + value = xor_matrices(value, matrix) + return value + + +def phase_checks(n): + matrices = list(product(range(1 << n), repeat=n)) + group = [a for a in matrices if invertible(a)] + members = set(group) + zero = (0,) * n + triples = [(a, b, xor_matrices(a, b)) for a in group for b in group + if xor_matrices(a, b) in members] + count = 0 + for triple in triples: + require(sum_selected(triple, 7) == zero, "tripled dirty coefficient") + require(len(set(triple)) == 3, "nonzero phases must be distinct") + sums = [sum_selected(triple, bits) for bits in range(8)] + require(set(sums) == {zero, *triple}, "unexpected partial triple sum") + for pivot, h in enumerate(triple): + other = [k for k in range(3) if k != pivot] + for bits, coefficient in enumerate(sums): + equal = ((bits >> other[0]) & 1) == ((bits >> other[1]) & 1) + require((coefficient in (zero, h)) == equal, "companion equality reduction") + if equal: + bit = ((bits >> pivot) ^ (bits >> other[0])) & 1 + require(coefficient == (h if bit else zero), "collapsed binary coefficient") + count += 1 + require(len(group) == prod((1 << n) - (1 << k) for k in range(n)), "incomplete GL census") + return group, triples, {"dimension": n, "invertible_matrices": len(group), + "ordered_zero_sum_triples": len(triples), "subset_checks": count} + + +def dense_coefficients(group, triples): + matrices = list(product(range(4), repeat=2)) + count = 0 + for triple in triples: + for h in triple: + inv = inverse(h, group) + for bits in range(8): + coefficient = sum_selected(triple, bits) + if coefficient not in ((0, 0), h): + continue + active = coefficient == h + for a, b in product(matrices, repeat=2): + for x in range(4): + bx = apply(b, x) + expected = apply(a, bx) if active else 0 + readout = insertion = 0 + for k, phase in enumerate(triple): + if bits >> k & 1: + readout ^= apply(a, apply(phase, apply(inv, bx))) + insertion ^= apply(a, apply(inv, apply(phase, bx))) + require(readout == expected, "triple-readout dense coefficient") + require(insertion == expected, "triple-source dense coefficient") + count += 2 + return count + + +def paired_words(n): + """Restricted-growth recursion: open the next label, or close an open one.""" + def visit(word, opened, active): + if len(word) == 2 * n: + yield tuple(word) + return + if opened < n: + yield from visit(word + [opened], opened + 1, active + (opened,)) + for label in active: + yield from visit(word + [label], opened, tuple(x for x in active if x != label)) + yield from visit([], 0, ()) + + +def prefixes(word): + result = [0] + for label in word: + result.append(result[-1] ^ (1 << label)) + return result + + +def differences(values): + return {a ^ b for a in values for b in values} + + +def pairing_census(certificate): + words = list(paired_words(5)) + require(len(words) == len(set(words)) == prod(range(1, 10, 2)), "incomplete pairing domain") + entries = sorted((list(w), sum(1 << x for x in differences(prefixes(w)))) for w in words) + histogram = Counter(mask.bit_count() for _, mask in entries) + receipt = {"sources": 5, "pairings": len(words), + "histogram": {str(k): v for k, v in sorted(histogram.items())}, + "canonical_entries_sha256": sha256(json.dumps(entries, separators=(",", ":")).encode()).hexdigest(), + "max_coverage": max(histogram)} + pinned = next(x for x in certificate["censuses"] if x["sources"] == 5) + require(receipt == pinned, "independent census differs from pinned predecessor") + require(max(histogram) < 32, "five-source obstruction failed") + return words, receipt + + +def check_phase_locking(): + checks = 0 + # Deleting any one exceptional output still couples every pair of sources. + for omitted in range(1, 32): + for j, k in combinations(range(5), 2): + require(any(m != omitted and m >> j & 1 and m >> k & 1 for m in range(1, 32)), + "paired output does not lock source phases") + checks += 1 + # With one tripled source, all four ordinary sources are coupled. + for exceptional in range(5): + for j, k in combinations([i for i in range(5) if i != exceptional], 2): + require(any(m >> j & 1 and m >> k & 1 for m in range(1, 32)), "regular phase lock") + checks += 1 + return checks + + +def triple_readouts(words): + trials = accepted = 0 + for word in words: + q = prefixes(word) + ordinary = differences(q) + for slots in combinations_with_replacement(range(len(q)), 3): + for pivot in range(3): + # 1,2,3 encode I,U,I+U in their two-dimensional F2 span. + phases = [0, 0, 0] + phases[pivot] = 1 + other = [k for k in range(3) if k != pivot] + phases[other[0]], phases[other[1]] = 2, 3 + mask = 0 + legal = True + for source in range(5): + coefficient = 0 + for phase, slot in zip(phases, slots): + if q[slot] >> source & 1: + coefficient ^= phase + if coefficient not in (0, 1): + legal = False + break + mask |= coefficient << source + if legal: + require(mask in ordinary, "third readout adds a new mask") + accepted += 1 + trials += 1 + return {"trials": trials, "scalar_mask_triples": accepted, "new_masks": 0} + + +def triple_sources(): + trials = maximum = 0 + wrong_deletion_witness = None + for positions in combinations(range(11), 3): + for paired in paired_words(4): + remaining = iter(paired) + word = [-1 if i in positions else next(remaining) + 1 for i in range(11)] + for pivot in range(3): + other = [k for k in range(3) if k != pivot] + weights = {positions[pivot]: 1, positions[other[0]]: 2, positions[other[1]]: 3} + values = [0] + for i, label in enumerate(word): + values.append(values[-1] ^ (weights[i] if label == -1 else 1 << (label + 1))) + require(values[-1] == 0, "triple-source restoration") + masks = {((d >> 2) << 1) | (d & 3) for d in differences(values) if d & 3 in (0, 1)} + projected = [max(0, label) for i, label in enumerate(word) if i != positions[other[1]]] + cover = differences(prefixes(projected)) + # The exceptional singleton may use its own output phase. + require(masks | {1} <= cover, "collapsed source word lost a requested mask") + require(len(cover) < 32, "collapsed pairing covers all masks") + maximum = max(maximum, len(masks | {1})) + if wrong_deletion_witness is None: + wrong = [max(0, label) for i, label in enumerate(word) if i != positions[pivot]] + lost = (masks | {1}) - differences(prefixes(wrong)) + if lost: + mask = min(lost) + encoded = ((mask >> 1) << 2) | (mask & 1) + interval = next((i, j) for i in range(12) for j in range(i, 12) + if values[i] ^ values[j] == encoded) + wrong_deletion_witness = { + "source_word": [max(0, label) for label in word], + "distinguished_occurrence": pivot, + "wrong_deleted_position": positions[pivot], + "lost_mask": mask, "readout_boundaries": interval, + } + trials += 1 + require(trials == 3 * 165 * 105, "incomplete triple-source domain") + require(wrong_deletion_witness is not None, "wrong-event deletion control not detected") + return {"annotated_source_words": trials, "max_coverage_with_singleton": maximum, + "wrong_event_deletion_counterexample": wrong_deletion_witness} + + +def odd_restoration_control(): + t = (2, 3) + cases = erasure_failures = 0 + for b in product(range(4), repeat=2): + for x, dirty in product(range(4), repeat=2): + z = dirty + for _ in range(3): + z ^= apply(b, x) + z = apply(t, z) + require(z == dirty, "odd-count restoration positive control") + erased = dirty + for _ in range(3): + erased ^= apply(b, x) + erasure_failures += erased != dirty + cases += 1 + # Erasing these frames is invalid, unlike the proven 73-map reductions. + require(erasure_failures > 0, "false general frame-erasure rule was not detected") + return {"restored_cases": cases, "unframed_failures": erasure_failures} + + +def dense_positive(word): + def replay(operations, initial, a, b): + state = initial.copy() + for kind, index in operations: + if kind == "B": + state[-1] ^= apply(b[index], state[index]) + else: + state[5 + index] ^= apply(a[index], state[-1]) + return state + + cases = 0 + for n in (1, 2, 3): + matrices = list(product(range(1 << n), repeat=n)) + a = [matrices[(i * 7 + 3) % len(matrices)] for i in range(31)] + b = [matrices[(j * 11 + 5) % len(matrices)] for j in range(5)] + + # All basis columns certify the complete finite linear map, including + # every independent source, target and connector dirt column. + inputs = [[(1 << (column % n)) if row == column // n else 0 + for row in range(37)] for column in range(37 * n)] + inputs.append([(1 << n) - 1] * 37) + for initial in inputs: + expected = initial.copy() + for i, mask in enumerate(range(1, 32)): + for j in range(5): + if mask >> j & 1: + expected[5 + i] ^= apply(a[i], apply(b[j], initial[j])) + actual = replay(word, initial, a, b) + require(actual == expected, "dense 74-call endpoint") + require(replay(word[::-1], actual, a, b) == initial, "dense 74-call inverse") + cases += 1 + return {"forward_cases": cases, "inverse_cases": cases, "dimensions": [1, 2, 3]} + + +def main(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["usage"] == "input": + require(sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "pinned source changed: " + row["path"]) + certificate = json.loads((HERE.parent / "universal-connector-boundary/CERTIFICATE.json").read_text()) + positive = certificate["schedules"]["five_extra_output"] + check_unframed_word(positive["word"], 5, list(range(1, 32))) + require(len(positive["word"]) == 74, "attaining construction is not 74 calls") + words, pairing = pairing_census(certificate) + g2, t2, phase2 = phase_checks(2) + _, _, phase3 = phase_checks(3) + report = {"status": "PASS_CONNECTOR_FRAME_73_EXCLUSION", "pairings": pairing, + "phase_censuses": [phase2, phase3], "dense_coefficients": dense_coefficients(g2, t2), + "phase_lock_checks": check_phase_locking(), "triple_readouts": triple_readouts(words), + "triple_sources": triple_sources(), "odd_restoration": odd_restoration_control(), + "dense_positive": dense_positive(positive["word"]), + "attaining_map_calls": len(positive["word"]), + "scope": "Finite checks support the written generic one-connector proof. No supplier admission or new kappa."} + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()