diff --git a/research/rank2-swap-batching/README.md b/research/rank2-swap-batching/README.md new file mode 100644 index 0000000000..431363d53d --- /dev/null +++ b/research/rank2-swap-batching/README.md @@ -0,0 +1,215 @@ +# Three GL2 swaps need five capped-rank invocations + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof; no new kappa.** Three independent coordinate-SWAP targets +have exact minimum **five invocations** when each paid coordinate-CNOT call +may have scalar rank one or two and costs one invocation. The complete +five-call word has rank profile `(2,2,1,2,2)` and total scalar rank nine. +It improves the six-invocation implementation that separately batches two +roles and processes the third role. Every additional dirty role returns +unchanged, with no off-diagonal residue. + +More generally, if a rank-one call costs `c1` and a rank-two call costs `c2`, +where `0 <= c1 <= c2 <= 2*c1`, the exact minimum is + +```text +c1 + 4*c2. +``` + +The disjoint batching bill is `3*c1 + 3*c2`. The new saving is therefore +`2*c1-c2`, positive for every strictly subadditive price `c2<2*c1`. +In particular, a power price `c_r=r^theta`, with `0<=theta<=1`, gives +`1+4*2^theta`. Scalar projector rank is not recursive child rank, so this +local result supplies no changed supplier histogram or multiplication bound. + +## Model + +Let `G=GL_2(F2)`, with + +```text +a = [[1,1],[0,1]], b = [[1,0],[1,1]], s=aba=bab=[[0,1],[1,0]]. +``` + +For any finite `R>=3`, work coefficientwise in `M_R(F2[G])`. All registers +start arbitrary. The required complete endpoint is +`T=diag([s],[s],[s],1,...,1)`. +A paid invocation is + +```text +D_N(g)=I_R+([g]+1)N, g in {a,b}, 1<=rank_F2(N)<=2. +``` + +The theorem allows arbitrary binary `N`, including nonidempotent matrices. +Restricting the alphabet to idempotents gives the same optimum, since the +attaining word uses only diagonal idempotents. Every factor is invertible: +its square is identity because `([g]+1)^2=0` in characteristic two. +Free scalar `GL_R(F2)` mixing may occur anywhere. There are no other free +address maps, resets, clean allocations or omitted restoration calls. + +The changed premise from the rank-one GL2 results is the cap-two invocation +price. David Arias's [PR2738](https://github.com/CrocSwap/integer-mult-bounds/pull/2738) +proves the scalar-rank tariff but explicitly leaves sublinear higher-rank +invocation prices outside its conclusion. Ross Richardson's +[PR2415 handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18944151) +names rank-two unit prices as a changed question. Their results are used as +cited mathematical premises; their scientific replays are not run here. + +## Attaining construction + +For a set `S` of role indices, write `E_S=sum_(j in S) E_jj`. +Execute these calls in the listed chronological order, with zero entries +on every role above two: + +| Call | Label | Role support | Scalar rank | +| --- | --- | --- | ---: | +| 1 | a | 0,1 | 2 | +| 2 | b | 0,2 | 2 | +| 3 | a | 2 | 1 | +| 4 | b | 1,2 | 2 | +| 5 | a | 0,1 | 2 | + +Role zero receives `a,b,a`, role one receives `a,b,a`, and role two receives +`b,a,b`. Both palindromic words equal `s`; the rightmost-first matrix-product +convention therefore gives the same stated endpoint. All factors are +diagonal in role space. Their formal product has no off-diagonal entries, +and every spectator diagonal remains exactly `[e]`. This is an identity in +the full group algebra, with no restriction on register values or addresses. + +The two target roles that share a call change between calls. Requiring a +fixed partition into a two-role block and a singleton would miss this word. +No scalar bridge, auxiliary role or uncharged cleanup is needed to attain it. + +## Optimality and the exact price + +We cite the rank-priced extension in +[PR2738, proof section 7](../coxeter-root-tariff/PROOF.md#7-rank-priced-extension-and-scope-boundaries), +using the product-preserving `GL_2(F2)=S3` bridge retained in +[PR2415](../gl2-swap-cut-corollary/README.md). +Its root-cut lower bound is valid for arbitrary binary scalar couplings, +free scalar mixing and arbitrary finite restored dirty workspace. Since +`s` is the length-three longest element of `S3`, **every legal circuit here +satisfies `sum_i rank(N_i)>=9`**. This nine-unit inequality is inherited, +not a new lower-bound theorem claimed by this package. + +Each invocation has rank at most two, so four invocations supply at most +eight rank units. At least five invocations are necessary. The table attains +five and nine rank units, proving the exact invocation minimum in both the +arbitrary-coupling and idempotent-only alphabets. + +For the price theorem, let `q1,q2` count rank-one and rank-two calls. Then +`q1+2*q2>=9`. If `q2<=4`, the nonnegative price assumptions imply + +```text +c1*q1+c2*q2 >= 9*c1-(2*c1-c2)*q2 >= c1+4*c2. +``` + +If `q2>=5`, the bill is at least `5*c2>=c1+4*c2`. These two cases cover +every finite circuit, including zero prices. The table attains the lower +bound exactly. No rounding of a numerical moment or finite word exclusion +is used in this proof. + +The interval `c1<=c2<=2*c1` is part of the statement. For example, with +`c1=1,c2=3`, nine rank-one calls cost nine, below the displayed formula +thirteen. The verifier rejects prices outside the stated interval. + +## Evidence and reproduction + +Use CPython 3.12 with the standard library, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rank2-swap-batching +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rank2-swap-batching/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/rank2-swap-batching/verify.py +``` + +Expected markers are `PASS_RANK2_SWAP_BATCHING minimum=5` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. A different installation can substitute +its own CPython 3.12 path. Default replay writes no files and needs neither +Git nor network. `--emit-receipt` prints a newly computed, source-hash-bound +receipt to standard output. The committed [RESULT.json](RESULT.json) is +generated by that command, never written by hand. + +The primary checker multiplies all formal coefficients using binary GL2 +matrices. A separate checker builds `S3` from permutations of three points +and applies the gates to every column of its faithful left regular module. +Both check the new complete endpoint. The finite fixtures cover all 168 +invertible scalar gauges at three roles, and elementary plus dense gauges +at four through six roles. Gauged calls include actual dirty-role coupling, +with separately applied entrance and exit maps. Each call omission and label +flip must change the formal endpoint; unmatched dirty coupling and an illegal +rank-three invocation must also fail. Exact rational price cases check the +new two-case integer-profile argument. Exact enumerated totals are in the +receipt, not extrapolated to larger spaces. + +The universal conclusion is the written construction and price proof using +the cited rank bound. The finite fixtures are corroboration. This is not an +exhaustive search over all legal words and does not replay predecessor +censuses or certify the inherited proof in a formal kernel. + +## Open next questions + +1. What native interface can implement this exact cap-two scalar-coupling + invocation at a strictly subadditive complete price? First specify its + data layout and arbitrary-input entry/exit contract, then charge its + compilation, scalar work, routing, ownership, precision and cleanup. + Those physical costs are unknown here; another construction round is + not justified by the formal five-call count alone. +2. What is the exact three-target tariff when scalar ranks above two are + allowed at a declared price? First specify one price schedule and compare + complete attaining words with the inherited nine-unit rank floor. + The cap-two price argument does not classify that changed alphabet. + +## Credit, overlap and limits + +David Arias's PR2738 supplies the rank-priced Coxeter theorem. Ross Richardson's +PR1989 supplies the symmetric-group cut theorem, and PR2415 supplies the GL2 +bridge and changed-price handoff. Adam Gall's PR1941 and Ross Richardson's +PR1966 retain the cut-method credit. Arham Tahir's +[PR1919](../ut3-rank-bounded-block-calls/README.md) supplies a related cyclic +rank-capped batching precedent for the distinct UT3 central target. +Ali Romman's [PR5031](../mixed-gl2-block-tariff/README.md) prices mixed GL2 +blocks at rank one and does not admit unit-priced rank-two invocations. +The underlying register-model lineage includes eumemic, Ali Romman, +Gareth Davidson and David Govea. All retained source notices remain unchanged. + +The new contribution is the displayed five-call GL2 support schedule and +its sharp cap-two invocation/concave-price consequence. The rank bound, +GL2 bridge, general cut method and the idea of higher-rank batching are +credited predecessors. No literature-priority claim is made. + +The [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19141448) +records the concrete scope. Base is canonical main +`4c0a359d88f22f05189d51f48387750b801a45d4`, priority revision seven. +A submission checkpoint fetched main at +`9269eea18a6a10dddeac6a4f696904c55ef1d365`; guidance, selected record and +the four relevant predecessor paths were unchanged. The scientific base +and immutable pins are retained. +The overlap snapshot covered 330 open PRs and 4193 Discussion records with +complete remote pagination. Sparse local coverage was 128 of 6760 note +paths, supplemented by distinctive main-tree and merged-PR searches and +direct predecessor reads. Arbitrary diffs and unpublished work are outside +that coverage. Open PR2444 concerns rank-one five-SWAP search tooling; +its changed-price boundary is a lead, not a claim to this cap-two result. + +Native/compiler admission, physical payload/tape/precision/stock costs, +a complete recursive invoice, selected cold replay, Lean, independent human +review and a complete multiplication theorem are unrun or outside scope. +The selected frontier is unchanged. See [SOURCES.json](SOURCES.json) for +immutable provenance pins and [TASK.json](TASK.json) for the scope change. + +### Verifier bounds and diagnostics + +The verifier has no recursive calls, solver, subprocess or background service. +Its matrix dimensions are at most six, group tables have six elements, +scalar-gauge enumeration has at most 512 candidates, and price-count checks +use a 13-by-13 grid. Each routine is shorter than sixty physical lines. +Explicit exceptions retain all invariants under optimized Python. + +Python dynamically allocates tuples, lists and arbitrary-size integers. This +is a managed-runtime deviation from fixed allocation, confined to the bounded +finite verifier, not a real-time or native-memory guarantee. The dimension +and enumeration caps bound live collections; no unbounded input is accepted. +The compensating checks are the normal and optimized warning-strict registered +commands. Revisit allocation and capacity if these corroboration bounds grow. +No shared repository diagnostic configuration is changed. diff --git a/research/rank2-swap-batching/RESULT.json b/research/rank2-swap-batching/RESULT.json new file mode 100644 index 0000000000..87d56746ef --- /dev/null +++ b/research/rank2-swap-batching/RESULT.json @@ -0,0 +1,34 @@ +{ + "claim_type": "scoped proof", + "minimum_invocations": 5, + "price_checks": { + "integer_profile_comparisons": 9360, + "invalid_price_controls": 3, + "price_cases": 65 + }, + "rank_mass": 9, + "rank_profile": [ + 2, + 2, + 1, + 2, + 2 + ], + "schedule_checks": { + "dirty_leak_controls": 68, + "gauged_endpoints": 236, + "omitted_call_controls": 1180, + "rank_cap_controls": 1, + "regular_basis_columns": 5172, + "wrong_label_controls": 1180 + }, + "schema_version": 1, + "source_sha256": { + "README.md": "2eded51bc7d80e360ff3937f3cc9feddb79e35b3f3d5ee3d69ac5b232b0d8054", + "SOURCES.json": "0026e1286fb9377ed5862fe91c109f34be038d2058fb50cba951f6cd362108d6", + "TASK.json": "fefb528b755540d19b5f65ac13bed14689461d0d2741441e84d88cc068c0c3e7", + "VERIFY.json": "fbbb18a55eefb282970c521dbacf5fd6d657513b2d8f4421b5a322549a75e5db", + "verify.py": "5d956a4b51cdbf26b933c428371936037d3a42a3d32a84abcd85977992e5da1c" + }, + "tariff": "c1+4*c2 for 0<=c1<=c2<=2*c1" +} diff --git a/research/rank2-swap-batching/SOURCES.json b/research/rank2-swap-batching/SOURCES.json new file mode 100644 index 0000000000..8a315b46f2 --- /dev/null +++ b/research/rank2-swap-batching/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "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/coxeter-root-tariff/PROOF.md", + "usage": "provenance", + "git_blob": "c67d51701a3dccf1028f8213502979372dbd73b3", + "sha256": "2e20ac459ed1524fca510b58d2792004e44024fd96b9f775501c47786c8325f8" + }, + { + "path": "research/gl2-swap-cut-corollary/README.md", + "usage": "provenance", + "git_blob": "c34c1460063ee4690c934d3c3fb3d81896f8931c", + "sha256": "3650918994be00323ccb61b75cdd81ecae47104a6e0765e319196618737949d9" + }, + { + "path": "research/mixed-gl2-block-tariff/README.md", + "usage": "provenance", + "git_blob": "0e70d9afe37947ca267a93892b791e5ea27c19e8", + "sha256": "c261a4d289c61e31dc495303f22d994b506c87b2f03de308ed94435bd7a1a4e0" + }, + { + "path": "research/ut3-rank-bounded-block-calls/README.md", + "usage": "provenance", + "git_blob": "dc0d1bac91fcebecc9fed4e8c3d26a11acca3ef5", + "sha256": "822574c7040b5571d729960951425a1ad9742ae8541a2af2882733f952975b5d" + } + ] +} diff --git a/research/rank2-swap-batching/TASK.json b/research/rank2-swap-batching/TASK.json new file mode 100644 index 0000000000..e3bf3f5f04 --- /dev/null +++ b/research/rank2-swap-batching/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "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 five-invocation minimum and c1+4*c2 tariff for three GL2 SWAP targets with scalar-rank cap two, arbitrary finite restored dirty workspace and free scalar mixing.", + "scope_change_reason": "Take PR2415 changed-price handoff and PR2738 higher-rank invocation boundary. The paid scalar-rank cap and subadditive price change the old rank-one premise; native implementation is not supplied.", + "bottleneck_link": "A complete formal schedule saves one invocation versus disjoint batching when scalar rank two is subadditive. Scalar projector rank is not recursive child rank, and physical supplier costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified five-call construction, exact inherited-bound consequence and bounded independent endpoint checks. Do not search larger caps or native suppliers.", + "outcome": "completed", + "evidence": "Written complete endpoint and price proof; independent formal GL2 and regular S3 endpoint checkers; omitted-call, label, dirty-leak, rank-cap and price controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a native interface implement this cap-two invocation with a strictly subadditive complete price?", + "why_it_matters": "The formal invocation saving changes no recursive supplier bill without a physical contract.", + "first_step": "Specify one layout and arbitrary-input entry/exit contract, then charge its compilation, scalar work, routing, ownership, precision and cleanup.", + "blocked_by": "No native implementation or complete cost is supplied." + }, + { + "question": "What is the exact three-target tariff if scalar ranks above two are allowed?", + "why_it_matters": "The cap-two proof does not classify other price alphabets.", + "first_step": "Fix one full price schedule and compare complete words with the cited nine-unit rank floor.", + "blocked_by": "A changed rank alphabet and matching lower bound are required." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19141448", + "selection": { + "mode": "handoff-first", + "source_prs": [ + 2415, + 2738 + ], + "changed_hypothesis": "scalar-rank-two invocation prices", + "predecessor_replay": "not run; cited premises only" + }, + "environment": { + "python": "CPython 3.12.15", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "dependencies": "standard library", + "platform": "macOS-27.0.1-arm64-arm-64bit" + }, + "overlap": { + "checked_at": "2026-10-23T08:14:00Z", + "open_prs": 330, + "discussion_records": 4193, + "local_note_paths": 128, + "head_note_paths": 6760, + "limits": "Sparse omitted notes, arbitrary diffs and unpublished work; supplemented with distinctive main-tree/merged-PR searches and direct predecessor reads." + }, + "upstream_refresh": { + "commit": "9269eea18a6a10dddeac6a4f696904c55ef1d365", + "guidance_and_selected_record": "unchanged from scientific base", + "compatibility": "Relevant pinned predecessor paths unchanged; scientific base retained without rebasing." + } +} diff --git a/research/rank2-swap-batching/VERIFY.json b/research/rank2-swap-batching/VERIFY.json new file mode 100644 index 0000000000..5212032305 --- /dev/null +++ b/research/rank2-swap-batching/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "New full formal and independent regular endpoints, rank-cap controls, exact price and integer profiles." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same new-result checks with assertions disabled." + } + ] +} diff --git a/research/rank2-swap-batching/verify.py b/research/rank2-swap-batching/verify.py new file mode 100644 index 0000000000..41f0cfeec8 --- /dev/null +++ b/research/rank2-swap-batching/verify.py @@ -0,0 +1,290 @@ +#!/usr/bin/env python3 +"""Check the new capped-rank schedule, its exact price, and rejection controls.""" +from __future__ import annotations + +import argparse +import hashlib +import itertools +import json +from fractions import Fraction +from pathlib import Path + +# Each tuple is one chronological invocation, not a recursive child profile. +SCHEDULE = (("a", (0, 1)), ("b", (0, 2)), ("a", (2,)), + ("b", (1, 2)), ("a", (0, 1))) +PACKAGE = Path(__file__).resolve().parent +MAX_ROLES = 6 # Finite corroboration only; the proof allows any finite count. + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def identity(n: int) -> tuple[int, ...]: + return tuple(1 << i for i in range(n)) + + +def multiply(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + n = len(a) + require(n == len(b) and 1 <= n <= MAX_ROLES, "matrix dimensions") + return tuple(xor_rows(b, row) for row in a) + + +def xor_rows(rows: tuple[int, ...], mask: int) -> int: + out = 0 + for i, row in enumerate(rows): + if mask >> i & 1: + out ^= row + return out + + +def rank(rows: tuple[int, ...]) -> int: + work = list(rows) + pivot = 0 + for col in range(len(rows)): + found = next((i for i in range(pivot, len(rows)) if work[i] >> col & 1), None) + if found is None: + continue + work[pivot], work[found] = work[found], work[pivot] + for i in range(pivot + 1, len(rows)): + if work[i] >> col & 1: + work[i] ^= work[pivot] + pivot += 1 + return pivot + + +def inverse(rows: tuple[int, ...]) -> tuple[int, ...]: + n = len(rows) + work = [row | (1 << (n + i)) for i, row in enumerate(rows)] + for col in range(n): + found = next((i for i in range(col, n) if work[i] >> col & 1), None) + require(found is not None, "singular gauge") + work[col], work[found] = work[found], work[col] + for i in range(n): + if i != col and work[i] >> col & 1: + work[i] ^= work[col] + require(tuple(row & ((1 << n) - 1) for row in work) == identity(n), "inverse left block") + return tuple(row >> n for row in work) + + +def coordinate_projector(n: int, support: tuple[int, ...]) -> tuple[int, ...]: + require(3 <= n <= MAX_ROLES, "corroboration role bound") + require(len(support) == len(set(support)) and all(0 <= i < n for i in support), "support") + return tuple((1 << i) if i in support else 0 for i in range(n)) + + +def group_table() -> tuple[list[tuple[int, ...]], list[list[int]], int, dict[str, int]]: + group = [(x, y) for x in range(4) for y in range(4) if rank((x, y)) == 2] + table = [[group.index(multiply(g, h)) for h in group] for g in group] + labels = {"a": group.index((3, 2)), "b": group.index((1, 3))} + labels["s"] = table[labels["a"]][table[labels["b"]][labels["a"]]] + require(len(group) == 6 and group[labels["s"]] == (2, 1), "GL2 labels") + return group, table, group.index((1, 2)), labels + + +def gates(n: int, gauge: tuple[int, ...]) -> list[tuple[str, tuple[int, ...]]]: + inv = inverse(gauge) + result = [] + for label, support in SCHEDULE: + p = coordinate_projector(n, support) + q = multiply(multiply(gauge, p), inv) + require(rank(q) == len(support) and multiply(q, q) == q, "projector rank/idempotence") + result.append((label, q)) + return result + + +def formal_endpoint(n: int, program: list[tuple[str, tuple[int, ...]]], + gauge: tuple[int, ...]) -> tuple[tuple[int, ...], ...]: + _, table, unit, labels = group_table() + zero = (0,) * n + state = [zero for _ in range(6)] + state[unit] = gauge # Free entrance map, followed by conjugated paid gates. + for label, q in program: + require(label in ("a", "b") and 1 <= rank(q) <= 2, "paid alphabet/rank cap") + products = [multiply(q, coeff) for coeff in state] + out = [list(coeff) for coeff in state] + for h in range(6): + for row in range(n): + out[h][row] ^= products[h][row] + out[table[labels[label]][h]][row] ^= products[h][row] + state = [tuple(coeff) for coeff in out] + return tuple(multiply(inverse(gauge), coeff) for coeff in state) + + +def expected_formal(n: int) -> tuple[tuple[int, ...], ...]: + _, _, unit, labels = group_table() + out = [[0] * n for _ in range(6)] + for i in range(n): + out[labels["s"] if i < 3 else unit][i] = 1 << i + return tuple(tuple(coeff) for coeff in out) + + +def permutation_compose(p: tuple[int, ...], q: tuple[int, ...]) -> tuple[int, ...]: + return tuple(p[q[i]] for i in range(3)) + + +def regular_scalar(vector: int, matrix: tuple[int, ...]) -> int: + out = 0 + for row, mask in enumerate(matrix): + for col in range(len(matrix)): + if mask >> col & 1: + out ^= ((vector >> (6 * col)) & 63) << (6 * row) + return out + + +def regular_endpoint(n: int, program: list[tuple[str, tuple[int, ...]]], + gauge: tuple[int, ...]) -> tuple[int, ...]: + # Independent group construction: permutations of three points, no GL2 table. + group = list(itertools.permutations(range(3))) + permutations = {"a": (1, 0, 2), "b": (0, 2, 1)} + action = {name: tuple(group.index(permutation_compose(p, h)) for h in group) + for name, p in permutations.items()} + outputs = [] + for column in range(6 * n): + value = regular_scalar(1 << column, gauge) + for label, q in program: + new_value = value + for source in range(n): + for h in range(6): + if value >> (6 * source + h) & 1: + for target in range(n): + if q[target] >> source & 1: + new_value ^= 1 << (6 * target + h) + new_value ^= 1 << (6 * target + action[label][h]) + value = new_value + outputs.append(regular_scalar(value, inverse(gauge))) + return tuple(outputs) + + +def expected_regular(n: int) -> tuple[int, ...]: + group = list(itertools.permutations(range(3))) + swap = (2, 1, 0) + return tuple(1 << (6 * role + (group.index(permutation_compose(swap, h)) if role < 3 else j)) + for role in range(n) for j, h in enumerate(group)) + + +def gauges(n: int) -> list[tuple[int, ...]]: + if n == 3: + return [tuple(rows) for rows in itertools.product(range(8), repeat=3) + if rank(tuple(rows)) == 3] + out = [identity(n)] + for i in range(n): + for j in range(n): + if i != j: + rows = list(identity(n)) + rows[i] ^= 1 << j + out.append(tuple(rows)) + # A dense, invertible gauge also couples successive dirty roles. + dense = identity(n) + for i in range(n): + rows = list(identity(n)) + rows[i] ^= 1 << ((i + 1) % n) + dense = multiply(tuple(rows), dense) + out.append(dense) + return out + + +def tariff(c1: Fraction, c2: Fraction) -> Fraction: + require(0 <= c1 <= c2 <= 2 * c1, "require 0 <= c1 <= c2 <= 2*c1") + return c1 + 4 * c2 + + +def check_prices() -> dict[str, int]: + prices = [(Fraction(0), Fraction(0))] + for denominator in range(1, 5): + for numerator in range(1, 5): + c1 = Fraction(numerator, denominator) + prices.extend((c1, c1 * ratio) for ratio in (Fraction(1), Fraction(5, 4), Fraction(3, 2), Fraction(2))) + comparisons = 0 + for c1, c2 in prices: + optimum = tariff(c1, c2) + attained = sum(c1 if len(support) == 1 else c2 for _, support in SCHEDULE) + require(optimum == attained, "price attained by the actual schedule") + require(optimum <= 3 * c1 + 3 * c2, "saving over disjoint batching") + for q1 in range(13): + for q2 in range(13): + if q1 + 2 * q2 >= 9: + require(q1 * c1 + q2 * c2 >= optimum, "integer rank-profile price bound") + comparisons += 1 + invalid = [(Fraction(-1), Fraction(0)), (Fraction(1), Fraction(1, 2)), + (Fraction(1), Fraction(3))] + for c1, c2 in invalid: + try: + tariff(c1, c2) + except ValueError: + continue + raise ValueError("invalid price accepted") + return {"price_cases": len(prices), "integer_profile_comparisons": comparisons, + "invalid_price_controls": len(invalid)} + + +def check_schedule() -> dict[str, int]: + cases = columns = omissions = flips = leaks = 0 + for n in range(3, MAX_ROLES + 1): + expected = expected_formal(n) + for gauge in gauges(n): + program = gates(n, gauge) + require(formal_endpoint(n, program, gauge) == expected, "full formal endpoint") + require(regular_endpoint(n, program, gauge) == expected_regular(n), "regular endpoint") + for i in range(5): + omitted = program[:i] + program[i + 1:] + require(formal_endpoint(n, omitted, gauge) != expected, "omitted call undetected") + require(regular_endpoint(n, omitted, gauge) != expected_regular(n), + "regular omitted call undetected") + flipped = list(program) + label, p = flipped[i] + flipped[i] = ("b" if label == "a" else "a", p) + require(formal_endpoint(n, flipped, gauge) != expected, "wrong label undetected") + omissions += 1 + flips += 1 + if n > 3: + broken = list(gauge) + broken[3] ^= gauge[0] # An unmatched free-map change leaks a target into dirt. + require(formal_endpoint(n, program, tuple(broken)) != expected, "dirty leak undetected") + leaks += 1 + cases += 1 + columns += 6 * n + require(tuple(len(s) for _, s in SCHEDULE) == (2, 2, 1, 2, 2), "rank profile") + require(sum(len(s) for _, s in SCHEDULE) == 9, "rank mass") + bad = [("a", identity(3))] + try: + formal_endpoint(3, bad, identity(3)) + except ValueError: + pass + else: + raise ValueError("rank-three paid call accepted") + return {"gauged_endpoints": cases, "regular_basis_columns": columns, + "omitted_call_controls": omissions, "wrong_label_controls": flips, + "dirty_leak_controls": leaks, "rank_cap_controls": 1} + + +def receipt() -> dict[str, object]: + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() for name in names} + return {"schema_version": 1, "claim_type": "scoped proof", "minimum_invocations": 5, + "rank_profile": [2, 2, 1, 2, 2], "rank_mass": 9, + "tariff": "c1+4*c2 for 0<=c1<=c2<=2*c1", "source_sha256": hashes, + "schedule_checks": check_schedule(), "price_checks": check_prices()} + + +def canonical(value: object) -> str: + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-receipt", action="store_true") + args = parser.parse_args() + actual = receipt() + if args.emit_receipt: + print(json.dumps(actual, indent=2, sort_keys=True)) + return + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + require(canonical(actual) == canonical(expected), "receipt mismatch") + print("PASS_RANK2_SWAP_BATCHING minimum=5 rank_profile=2,2,1,2,2 rank_mass=9 no_new_kappa") + print(canonical(actual)) + + +if __name__ == "__main__": + main()