diff --git a/research/two-swap-address-spectators/README.md b/research/two-swap-address-spectators/README.md new file mode 100644 index 0000000000..a10600771f --- /dev/null +++ b/research/two-swap-address-spectators/README.md @@ -0,0 +1,212 @@ +# Two swaps cost six calls with arbitrary address spectators + +**Scoped formal-model theorem.** For every finite address dimension `n>=2` +and scalar register count `R>=2`, two coordinate-SWAP targets cost exactly +six paid coordinate-CNOT calls, with free scalar mixing and arbitrarily many +restored dirty registers. This closes both higher-dimension questions in +[PR1495](https://github.com/CrocSwap/integer-mult-bounds/pull/1495)'s +[finite certificate](../coordinate-cnot-address-spectator/README.md). +It supplies no native implementation, multiplication supplier or new kappa. + +The new step is a row-write budget followed by a **parabolic subgroup +projection**. The all-register two-coordinate obstruction is retained from +commdata2338's [PR1414](https://github.com/CrocSwap/integer-mult-bounds/pull/1414). +We also restate its six-call consequence using Ross Richardson's +[cut corollary](../gl2-swap-cut-corollary/README.md) of +[PR1989](https://github.com/CrocSwap/integer-mult-bounds/pull/1989), making +the argument reviewable here without a finite word search. + +## Exact contract + +Work over `M_R(F2[GL_n(F2)])`. Address indices and scalar-register indices +are separate and both start at zero. A paid call is + +``` +D_N(g) = I_R + ([g] + [I_n]) N, +g = I_n + E_ij, i != j, +N = u v^T over F2, v^T u = 1. +``` + +Every coordinate CNOT is allowed; each call has a rank-one idempotent scalar +coupling and costs one. Scalar `GL_R(F2)` maps are free and may be interleaved. +The complete endpoint is `T=diag([s],[s],[I_n],...,[I_n])`, where `s` swaps +address coordinates zero and one and fixes the rest. + +Equality is coefficientwise in the full formal group algebra on arbitrary +inputs. Extra registers are dirty and individually restored; off-diagonal +couplings vanish. There are no free address maps, clean allocations, erasures +or resets. Preparation and undo calls are charged. This explicit formal +alphabet is distinct from a native pricing model or the older abelian model. + +## Proof + +**1. Normalize free scalar maps.** Commuting a scalar map past a paid call +conjugates `N`, preserving rank one and idempotence. Gather all scalar maps +into one residual factor. Augmentation sends every `[g]` to one and every +paid call and the target to `I_R`. The residual scalar factor is therefore +identity. Paid length and labels are unchanged. This normalization is credited +to Gareth Davidson/PR1333 in PR1414. + +**2. Count writes to each address row.** Apply the natural representation, +ordering the binary space by address blocks of size `R`. A call becomes +`I_(nR)+E_ij tensor N`. For a prefix matrix `P`, left multiplication +changes only block row `i`, by adding `N row_j(P)`. Each prefix is +invertible: every gate squares to identity because `E_ij^2=0`. Thus +`row_j(P)` has full row rank `R` and `rank(N row_j(P))=1`. + +If row `i` is written `c_i` times, telescoping its changes gives +`rank(row_i(P_final-I))<=c_i`. If `c_i=1`, its unique nonzero rank-one +change cannot disappear: calls targeting other rows leave it unchanged. +A row that finishes unchanged is therefore never written or written at +least twice. All dirty inputs are included. + +Let `E=diag(1,1,0,...,0)` on the scalar registers. The natural target is +`I_(nR)+(s-I_n) tensor E`. Its two active address rows each have delta +rank two; all other rows have delta zero. Hence + +``` +c_0 >= 2, c_1 >= 2; +for i >= 2, either c_i=0 or c_i>=2. +``` + +A successful word of at most five calls **cannot write a spectator address +row**, since that requires at least six calls. It may still read spectators: +remaining calls may have `i<2,j>=2`. + +**3. Remove read-only spectators in the formal algebra.** All remaining +labels belong to the subgroup + +``` +H = { [[A,B],[0,I_(n-2)]] : A in GL_2(F2), B arbitrary }. +``` + +Block multiplication shows that taking the upper-left block defines a group +homomorphism `pi:H -> GL_2(F2)`. For `n=2` it is the identity. +The inclusion `F2[H] -> F2[GL_n(F2)]` is injective: distinct group elements +remain distinct formal basis vectors. The normalized word and target lie +in this subalgebra, so their **formal** equality descends under the linear +extension of `pi`. + +An active-to-active CNOT maps to a coordinate CNOT in `GL_2`. A read from a +spectator maps to identity, making its paid factor `I_R`. Delete those +identity factors. The resulting word has at most five legal calls for two +swaps in the two-coordinate model, with the same projectors and dirty roles. + +This projection is invalid on all of `GL_n`: in dimension three, +`g=I+E_02` and `h=I+E_21` have identity upper-left blocks, while `gh` +has upper-left block `I_2+E_01`. Write exclusion must precede projection. +Natural-image equality alone cannot justify this formal step either, +because that representation has a nonzero algebra kernel. + +**4. Apply the two-coordinate obstruction.** PR1414's +[PROOF.md](../coordinate-cnot-register-bound/PROOF.md) proves the six-call +bound for every `R`. For completeness, the later PR1989 cut argument gives +a short derivation. Order nonzero address vectors as `(0,1),(1,1),(1,0)`. +The two CNOTs act as adjacent transpositions `(12),(23)`; their three-call +swap is `(13)`. Act simultaneously on the six ordered pairs of distinct +labels. On every scalar register, partition this basis into increasing +pairs `H+` and decreasing pairs `H-`. Put `q(M)=rank M[H-,H+]`. +Block multiplication and rank subadditivity give `q(UV)<=q(U)+q(V)`. + +Each adjacent transposition reverses exactly one increasing pair, so each +paid rank-one factor has crossing rank one. Free scalar mixing has crossing +rank zero. The swap reverses all three increasing pairs; on two registers +its target has crossing rank six. Restored dirty registers contribute zero. +Thus at least six paid calls are required, contradicting the projected word. +This cut method and its all-register extension are credited to PR1989 and +the retained corollary. + +**5. Attain six.** On scalar register zero use `a,b,a`, where +`a=I_n+E_01,b=I_n+E_10`, with projector `E_00`. Repeat with projector +`E_11` on scalar register one. Since `aba=s`, these six calls give the +complete formal endpoint, fixing all other roles and address coordinates. + +The minimum is six by this uniform written argument, not extrapolation from +finite checks. This does not classify shortest words: at length six the +row counts `(2,2,2)` satisfy the necessary budget. + +## Reproduction and finite evidence + +Python 3.12 and its standard library suffice. From the repository root: + +```sh +python -I -W error -B research/two-swap-address-spectators/verify.py +python -I -O -W error -B research/two-swap-address-spectators/verify.py +python -B scripts/research_package.py --package research/two-swap-address-spectators --check-only +python -B scripts/research_package.py --package research/two-swap-address-spectators +``` + +The direct command prints +`PASS_TWO_SWAP_ADDRESS_SPECTATORS finite_checks=passed uniform_minimum=6_by_written_proof no_new_kappa`. +Use `--json` for recomputed evidence. Explicit exception checks survive +optimized Python. No solver, network or predecessor code is imported. +Four proof/model inputs are authenticated by SHA256 and Git blob hash; +the registered runner checks historical provenance. + +The verifier checks deterministic eight-call prefixes for `n=2..6,R=2..5`, +including involutions, independent matrix multiplication, row-rank budgets +and nonzero single writes: 1,280 transitions, 5,120 row bounds and 2,656 +single-write checks. It exhausts 9,792 parabolic products at `n=3,4` and +2,996 write-count vectors of length at most five for `n=2..8`. It checks 20 full +formal six-call endpoints, their reversals and scalar conjugates, rejects +all 120 single-call omissions, and detects 12 dirty-only faults missed by +clean-input restrictions. Controls exhibit an invalid whole-group projection, +a nonzero formal element with zero natural image, and the forbidden rank-two +tariff under which three calls suffice. + +Author replay on Windows / CPython 3.12.0 / Git 2.47.1 passed both registered +commands. The current schema's orientation command, +`python -B scripts/research_selected_baseline.py`, also returned +`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`: selected source bindings and exact +metadata consistency only. The historical command printed in the original +task card does not handle this selected productive-helper schema. + +This is a scoped proof with finite supporting checks, not Lean verification +or independent human review. No selected-supplier cold replay, native +rational-address compiler, hosting, precision/tape bound, recursive paid +profile or outer analytic transfer is supplied. Selected kappa is unchanged. + +## Scope, overlap and credit + +Base: `cef4b52f2a59009865bf8eabde1be3f159063703`, current main at session +entry; priority revision 7. Picker task `bit-new-register-model`, nonce +`434b93a0ec53b6f1a0baea72e385b919`, scope key `7084092dd726e7ba1f2f`. +[TASK.json](TASK.json) preserves the original card and the changed scope: +a negative formal-model screen does not satisfy its native construction +gate. We compare with PR1495's finite GL3 screen and the two-coordinate +bounds, without rerunning the GL3 census or mixed-root tariff. + +The entry overlap snapshot covered 6,601 local README/TASK scope records, +308 open PRs including drafts, and 4,006 Discussion records with complete +pagination and no warnings (2026-10-23 02:29-02:31 UTC). Focused terms included +`coordinate-cnot-address-spectator`, `address spectator` and `two swaps`. +Coverage excludes arbitrary diffs, all closed-PR history and unpublished +work; no-match is not novelty proof. Canonical coordination: +[Discussion #1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19136566). + +Credit commdata2338 for PR1414's obstruction and PR1495's finite certificate +and open questions; Gareth Davidson (@bitplane)/PR1333 for the restricted +alphabet and normalization; Ross Richardson/PR1989 and the GL2 corollary +for the cut theorem. Their notes retain Adam Gall, Cinna Davis and earlier +cut-method credit. Credit eumemic/PR288, Ali Romman/PR468 and David Govea/PR720 +for the surrounding register-model and rational-address work. Source packages +remain unchanged. The contribution here is uniform address-spectator +elimination and its verifier, not the two-coordinate lower bound. + +Prepared for Mihir Srivastava (@mihir-s-05), with substantial OpenAI Codex +assistance in proof development, coding, checking and writing. No independent +human proof review or literature-priority claim is made. Apache-2.0. + +## Open next questions + +1. **Can three swaps benefit from spectator address coordinates?** The + two-coordinate minimum is nine, but the row budget permits an eight-call + candidate with counts `(3,3,2)`. First analyze the two spectator writes + and whether they can be eliminated. This note establishes neither such + a word's existence nor exclusion; a missing elimination lemma blocks + extending the argument. +2. **Which native operation escapes the rank-one coordinate-CNOT tariff?** + First specify a complete arbitrary-input endpoint and implementation, + then charge preparation and restoration. Native realization and full + recursive accounting block transfer to the selected construction. + Further finite searches in the two-swap model proved here are unnecessary. diff --git a/research/two-swap-address-spectators/SOURCES.json b/research/two-swap-address-spectators/SOURCES.json new file mode 100644 index 0000000000..a38f96197d --- /dev/null +++ b/research/two-swap-address-spectators/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/coordinate-cnot-address-spectator/README.md", + "usage": "input", + "git_blob": "15b3db71d9fc13b4e9806caf42dd56213936fc88", + "sha256": "f433d3891cdc88fb47e055c4246798980529268a9a17250574414f805935ddd5" + }, + { + "path": "research/coordinate-cnot-register-bound/README.md", + "usage": "input", + "git_blob": "cdcc5a9e7f11ab3dbf7745a175ddcca208c68211", + "sha256": "e1666512fb71cf34c427c69ffb61a18b61e897a7f8f91f87820edf744e85a9fe" + }, + { + "path": "research/gl2-swap-cut-corollary/README.md", + "usage": "input", + "git_blob": "c34c1460063ee4690c934d3c3fb3d81896f8931c", + "sha256": "3650918994be00323ccb61b75cdd81ecae47104a6e0765e319196618737949d9" + }, + { + "path": "research/coordinate-cnot-register-bound/PROOF.md", + "usage": "input", + "git_blob": "68fee5b5ccff5329e27300e40dcbd483640dd6b7", + "sha256": "bcee89f92dcce8253bd7eae6e924ddff598c900da81979c6171a412f03d765e1" + } + ] +} diff --git a/research/two-swap-address-spectators/TASK.json b/research/two-swap-address-spectators/TASK.json new file mode 100644 index 0000000000..c2933173da --- /dev/null +++ b/research/two-swap-address-spectators/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact six-call cost of two coordinate swaps for arbitrary finite address dimension n>=2 and arbitrary scalar register count R>=2, with restored dirty roles.", + "scope_change_reason": "The assigned card seeks a native escape. This bounded negative formal-model result instead resolves the two higher-dimensional questions in PR1495 using a row-write budget and subgroup projection; no native supplier is claimed.", + "bottleneck_link": "Side result on the bit-mechanisms track: excludes address-spectator or dirty-role enlargement as a two-swap saving in this exact tariff. It does not discharge the selected supplier obligations or change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the uniform proof, exact finite controls, registered replay and publication checks. Do not extend into a larger word census or native construction round.", + "outcome": "negative-result", + "evidence": "README.md gives the uniform proof; verify.py checks finite row-budget, parabolic-projection and full formal-endpoint fixtures with explicit failure controls. VERIFY.json registers normal and optimized replay.", + "author": "Mihir Srivastava, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for repository orientation, proof development, implementation, finite verification, writing and GitHub coordination. No independent human review claimed.", + "open_questions": [ + { + "question": "Can three swaps benefit from spectator address coordinates?", + "why_it_matters": "The two-coordinate minimum is nine; an eight-call count vector (3,3,2) is not excluded by this row budget.", + "first_step": "Analyze two writes to a spectator row and whether a formal endpoint forces an eliminable subword, before any bounded search.", + "blocked_by": "No elimination argument for a spectator row written twice; no eight-call candidate or exclusion supplied." + }, + { + "question": "Which native operation can escape the rank-one coordinate-CNOT tariff?", + "why_it_matters": "A changed formal price is irrelevant to the selected construction without a complete native implementation and paid profile.", + "first_step": "Specify a complete arbitrary-input endpoint and price all preparation and restoration for the proposed changed operation.", + "blocked_by": "Native realization and full recursive accounting remain absent." + } + ] +} diff --git a/research/two-swap-address-spectators/VERIFY.json b/research/two-swap-address-spectators/VERIFY.json new file mode 100644 index 0000000000..4c0b676750 --- /dev/null +++ b/research/two-swap-address-spectators/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coordinate-cnot-address-spectator/README.md", + "research/coordinate-cnot-register-bound/README.md", + "research/gl2-swap-cut-corollary/README.md", + "research/coordinate-cnot-register-bound/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Finite row-write ranks, subgroup projection, full formal witnesses, omitted calls, dirty-only faults, rank-two tariff and natural-image alias controls; source hashes." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Finite row-write ranks, subgroup projection, full formal witnesses, omitted calls, dirty-only faults, rank-two tariff and natural-image alias controls; source hashes." + } + ] +} diff --git a/research/two-swap-address-spectators/verify.py b/research/two-swap-address-spectators/verify.py new file mode 100644 index 0000000000..84deb92b6c --- /dev/null +++ b/research/two-swap-address-spectators/verify.py @@ -0,0 +1,299 @@ +#!/usr/bin/env python3 +"""Exact finite checks supporting README's uniform proof; no word census.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return tuple(1 << i for i in range(n)) + + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b, strict=True)) + + +def multiply(a, b): + out = [] + for row in a: + value = 0 + for i, other in enumerate(b): + if row >> i & 1: + value ^= other + out.append(value) + return tuple(out) + + +def rank(rows): + pivots = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = row + break + row ^= pivots[pivot] + return len(pivots) + + +def cnot(n, i, j): + need(0 <= i < n and 0 <= j < n and i != j, "invalid coordinate CNOT") + rows = list(identity(n)) + rows[i] ^= 1 << j + return tuple(rows) + + +def projectors(r): + return [tuple(y if x >> i & 1 else 0 for i in range(r)) + for x in range(1, 1 << r) for y in range(1, 1 << r) + if (x & y).bit_count() % 2] + + +def put(poly, label, coefficient): + value = add(poly.get(label, (0,) * len(coefficient)), coefficient) + if any(value): + poly[label] = value + else: + poly.pop(label, None) + + +def factor(label, coupling): + need(rank(coupling) == 1 and multiply(coupling, coupling) == coupling, + "paid coupling must be a rank-one idempotent") + out = {} + put(out, identity(len(label)), add(identity(len(coupling)), coupling)) + put(out, label, coupling) + return out + + +def formal_multiply(left, right): + out = {} + for g, a in left.items(): + for h, b in right.items(): + put(out, multiply(g, h), multiply(a, b)) + return out + + +def formal_word(n, r, calls): + out = {identity(n): identity(r)} + for label, coupling in calls: + out = formal_multiply(factor(label, coupling), out) + return out + + +def natural(poly, n, r): + """Address-major blocks; coefficient matrices act on scalar roles.""" + rows = [0] * (n * r) + for label, coefficient in poly.items(): + for i in range(n): + for j in range(n): + if label[i] >> j & 1: + for u in range(r): + rows[i * r + u] ^= coefficient[u] << (j * r) + return tuple(rows) + + +def row_update(before, r, i, j, coupling): + after = list(before) + update = multiply(coupling, before[j * r:(j + 1) * r]) + for u in range(r): + after[i * r + u] ^= update[u] + return tuple(after) + + +def check_row_budget(): + transitions = row_bounds = single_write_checks = 0 + for r in range(2, 6): + choices = projectors(r) + for n in range(2, 7): + initial = identity(n * r) + for sample in range(8): + state = initial + counts = [0] * n + for t in range(8): + i = (sample + t) % n + j = (i + 1 + (t // n) % (n - 1)) % n + coupling = choices[(13 * sample + 17 * t + n) % len(choices)] + after = row_update(state, r, i, j, coupling) + gate = natural(factor(cnot(n, i, j), coupling), n, r) + need(after == multiply(gate, state), "row-update convention") + need(multiply(gate, after) == state, "paid gate is involutive") + need(rank(after) == n * r, "prefix must be invertible") + counts[i] += 1 + for address in range(n): + block = slice(address * r, (address + 1) * r) + delta_rank = rank(add(after[block], initial[block])) + need(delta_rank <= counts[address], "row-write rank budget") + row_bounds += 1 + if counts[address] == 1: + need(delta_rank == 1, "a single write cannot restore a row") + single_write_checks += 1 + state = after + transitions += 1 + return dict(transitions=transitions, row_bounds=row_bounds, + single_write_checks=single_write_checks) + + +def projection(g): + return g[0] & 3, g[1] & 3 + + +def parabolic(n): + for a in itertools.product(range(4), repeat=2): + if rank(a) == 2: + for b in itertools.product(range(1 << (n - 2)), repeat=2): + yield (a[0] | b[0] << 2, a[1] | b[1] << 2, *identity(n)[2:]) + + +def check_projection(): + products = labels = 0 + sizes = {} + for n in (3, 4): + group = set(parabolic(n)) + sizes[str(n)] = len(group) + for g in group: + for h in group: + gh = multiply(g, h) + need(gh in group, "parabolic subgroup closure") + need(projection(gh) == multiply(projection(g), projection(h)), + "parabolic projection must preserve products") + products += 1 + for n in range(2, 9): + for i in (0, 1): + for j in range(n): + if i != j: + expected = cnot(2, i, j) if j < 2 else identity(2) + need(projection(cnot(n, i, j)) == expected, "projected label") + labels += 1 + g, h = cnot(3, 0, 2), cnot(3, 2, 1) + need(projection(multiply(g, h)) != multiply(projection(g), projection(h)), + "control: projection is NOT a homomorphism on all GL_n") + return dict(group_sizes=sizes, products=products, labels=labels, + outside_subgroup_counterexample=1) + + +def check_count_budget(): + candidates = admissible = 0 + for n in range(2, 9): + for k in range(6): + for writes in itertools.combinations_with_replacement(range(n), k): + counts = tuple(writes.count(i) for i in range(n)) + candidates += 1 + if counts[0] >= 2 and counts[1] >= 2 and all(c != 1 for c in counts[2:]): + need(not any(counts[2:]), "five-call budget permits no spectator writes") + admissible += 1 + need(admissible == 21, "bounded count-vector fixture changed") + boundary = (2, 2, 2) + need(sum(boundary) == 6 and all(c >= 2 for c in boundary), + "six-call boundary allows a spectator; no shortest-word classification") + return dict(count_vectors=candidates, admissible=admissible, + six_call_boundary=list(boundary)) + + +def direct_word(n, r): + return [(cnot(n, i, j), tuple(1 << role if u == role else 0 for u in range(r))) + for role in (0, 1) for i, j in ((0, 1), (1, 0), (0, 1))] + + +def target(n, r): + swap = list(identity(n)) + swap[0], swap[1] = swap[1], swap[0] + active = (1, 2, *((0,) * (r - 2))) + out = {} + put(out, identity(n), add(identity(r), active)) + put(out, tuple(swap), active) + return out + + +def check_endpoints(): + witnesses = omissions = dirty_faults = 0 + for n in range(2, 7): + for r in range(2, 6): + calls = direct_word(n, r) + expected = target(n, r) + need(formal_word(n, r, calls) == expected, "six-call formal endpoint") + need(formal_word(n, r, reversed(calls)) == expected, "reverse formal endpoint") + image = natural(expected, n, r) + for i in range(n): + block = slice(i * r, (i + 1) * r) + need(rank(add(image[block], identity(n * r)[block])) == (2 if i < 2 else 0), + "target row ranks") + mixing = cnot(r, 0, 1) + conjugated = [(g, multiply(mixing, multiply(p, mixing))) for g, p in calls] + need(formal_word(n, r, conjugated) == expected, "free scalar conjugation") + witnesses += 1 + for deleted in range(6): + need(formal_word(n, r, calls[:deleted] + calls[deleted + 1:]) != expected, + "omitted paid call accepted") + omissions += 1 + if n >= 3 and r >= 3: + dirty_projector = (0, 0, 4, *((0,) * (r - 3))) + damaged = formal_word(n, r, calls + [(cnot(n, 2, 0), dirty_projector)]) + need(damaged != expected, "unrestored dirty role accepted") + data_columns = sum(3 << (address * r) for address in range(n)) + need(all((x ^ y) & data_columns == 0 + for x, y in zip(natural(damaged, n, r), image, strict=True)), + "dirty-only fault must evade restricted clean-input testing") + dirty_faults += 1 + try: + factor(cnot(2, 0, 1), identity(2)) + except ValueError as error: + need(str(error) == "paid coupling must be a rank-one idempotent", "wrong rejection") + else: + raise ValueError("rank-two paid coupling accepted") + # If rank-two couplings were unit price, three pure-label factors would suffice. + forbidden = {identity(2): identity(2)} + for i, j in ((0, 1), (1, 0), (0, 1)): + forbidden = formal_multiply({cnot(2, i, j): identity(2)}, forbidden) + need(forbidden == target(2, 2), "changed-alphabet three-call control") + alias = {g: (1,) for g in itertools.product(range(4), repeat=2) if rank(g) == 2} + need(len(alias) == 6 and natural(alias, 2, 1) == (0, 0), + "nonzero formal element with zero natural image") + return dict(formal_witnesses=witnesses, reverse_witnesses=witnesses, + scalar_conjugations=witnesses, omission_rejections=omissions, + dirty_only_fault_rejections=dirty_faults, + rank_two_tariff_control=1, natural_alias_control=1) + + +def authenticate(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + checked = {} + for entry in sources["files"]: + if entry["usage"] == "input": + raw = (ROOT / entry["path"]).read_bytes() + digest = hashlib.sha256(raw).hexdigest() + need(digest == entry["sha256"], "source SHA256 mismatch: " + entry["path"]) + blob = hashlib.sha1(b"blob " + str(len(raw)).encode("ascii") + b"\0" + raw).hexdigest() + need(blob == entry["git_blob"], "source Git blob mismatch: " + entry["path"]) + checked[entry["path"]] = digest + need(len(checked) == 4, "expected four proof/model sources") + return checked + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--json", action="store_true", help="print recomputed finite evidence") + args = parser.parse_args() + result = dict(sources=authenticate(), row_budget=check_row_budget(), + projection=check_projection(), count_budget=check_count_budget(), + endpoints=check_endpoints()) + if args.json: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + print("PASS_TWO_SWAP_ADDRESS_SPECTATORS finite_checks=passed " + "uniform_minimum=6_by_written_proof no_new_kappa") + + +if __name__ == "__main__": + main()