From 9fb1552f12ca4777ca660461a8b602e709285f99 Mon Sep 17 00:00:00 2001 From: ywz65 <154373401+ywz65@users.noreply.github.com> Date: Thu, 15 Oct 2026 07:02:28 -0700 Subject: [PATCH] Prove sharp asymmetric coordinate SWAP tariffs --- research/gl2-swap-weighted-tariff/README.md | 181 +++++++++++++ research/gl2-swap-weighted-tariff/RESULT.json | 25 ++ .../gl2-swap-weighted-tariff/SOURCES.json | 50 ++++ research/gl2-swap-weighted-tariff/TASK.json | 100 ++++++++ research/gl2-swap-weighted-tariff/VERIFY.json | 31 +++ .../gl2-swap-weighted-tariff/test_boundary.py | 57 +++++ research/gl2-swap-weighted-tariff/verify.py | 241 ++++++++++++++++++ 7 files changed, 685 insertions(+) create mode 100644 research/gl2-swap-weighted-tariff/README.md create mode 100644 research/gl2-swap-weighted-tariff/RESULT.json create mode 100644 research/gl2-swap-weighted-tariff/SOURCES.json create mode 100644 research/gl2-swap-weighted-tariff/TASK.json create mode 100644 research/gl2-swap-weighted-tariff/VERIFY.json create mode 100644 research/gl2-swap-weighted-tariff/test_boundary.py create mode 100644 research/gl2-swap-weighted-tariff/verify.py diff --git a/research/gl2-swap-weighted-tariff/README.md b/research/gl2-swap-weighted-tariff/README.md new file mode 100644 index 0000000000..e4647abcd7 --- /dev/null +++ b/research/gl2-swap-weighted-tariff/README.md @@ -0,0 +1,181 @@ +# Sharp asymmetric label tariffs for coordinate SWAP + +In the formal coordinate-SWAP model, assign fixed nonnegative real prices A and B +to the two paid labels a and b. For t target roles and any finite `R >= t` +arbitrary-input roles, the exact minimum is + +```text + t * (2 min(A,B) + max(A,B)). +``` + +This closes Open next questions item 2 of Aaron Wang's +[PR2444](https://github.com/CrocSwap/integer-mult-bounds/pull/2444), which proposed +weighted BFS for t=2,3. No further search is required for that tariff change: +even arbitrary noncommuting projectors and restored dirty spectators cannot +beat the cheaper of independent `aba` and `bab` words. + +The total-call bound `3t` and its general cut argument are **inherited**, credited +to Ross Richardson's [PR1989](https://github.com/CrocSwap/integer-mult-bounds/pull/1989) +and its explicit coordinate-SWAP corollary +[PR2415](https://github.com/CrocSwap/integer-mult-bounds/pull/2415). +The additional result here is the two individual label counts and their sharp +weighted combination, with exact zero-price and changed-premise boundaries. +This is a scoped formal-model theorem, not a new native supplier or exponent. + +## Model + +Work in `F2[G]` for `G=GL_2(F2)`, with + +```text +a = [1 1] b = [1 0] s = aba = bab = [0 1]. + [0 1] [1 1] [1 0] +``` + +Every paid factor is `D_N(g) = I_R + ([g]+1) N`, where g is exactly a or b +and `N=uv^T` is a binary rank-one idempotent (`v^T u=1`). Its price is A or B, +independently of N, position, R and the surrounding word. Arbitrary scalar +`GL_R(F2)` maps may be interleaved for free. There are no additional free address +maps, clean allocations, resets, erasures or copies. Every role begins arbitrarily. +The endpoint is coefficientwise equality with +`diag([s] I_t, I_(R-t))`; every spectator is individually restored, with no +off-diagonal residual. Spectators may be reused arbitrarily during the word. +These are exactly PR2415's model hypotheses; only the two label prices change. +For t=0 the empty word attains zero; all statements allow A=0 and/or B=0. + +## The two per-label bounds + +Apply the natural two-dimensional representation linearly to the group algebra. +It need not be injective: a necessary consequence of a formal identity suffices +for a lower bound. Order the resulting `2R` coordinates by address coordinate, +so each operator has four `R by R` blocks. For an operator M define + +```text +q_a(M) = rank_F2 M_12, q_b(M) = rank_F2 M_21. +``` + +For arbitrary compatible U,V, block multiplication gives + +```text +(UV)_12 = U_11 V_12 + U_12 V_22, +(UV)_21 = U_21 V_11 + U_22 V_21. +``` + +Rank subadditivity and `rank(XY) <= min(rank X, rank Y)` imply +`q_a(UV) <= q_a(U)+q_a(V)` and the same for q_b. This holds regardless of +commutation, invertibility or intermediate dirty couplings, so it applies to +arbitrarily long prefixes with any surrounding paid and free factors. + +The natural images of paid factors and free scalar maps are + +```text +D_N(a) -> [I N] D_N(b) -> [I 0] S -> [S 0]. + [0 I] [N I] [0 S] +``` + +Their `(q_a,q_b)` charges are `(1,0)`, `(0,1)` and `(0,0)`, respectively. +The target is `[[I-P,P],[P,I-P]]`, where `P=diag(I_t,0)`, hence its two crossing +ranks are both t. Applying subadditivity to the actual entire word proves + +```text + n_a >= t, n_b >= t. +``` + +No normalization of scalar mixing is needed, and no clean-state restriction is +introduced. All R roles are included in every block rank. + +## Combining with the credited total bound + +PR2415's source-bound specialization of PR1989 gives `n_a+n_b >= 3t` under the +same hypotheses. Briefly, the natural action of `GL_2(F2)` on its three nonzero +vectors identifies a,b with adjacent transpositions in S3. Its action on six +ordered distinct pairs splits into increasing and decreasing pairs. Each paid +label crosses exactly one independent direction in this cut; free scalar maps +cross none; SWAP crosses three per target. The same block-rank subadditivity +therefore gives `3t`. This paragraph restates the predecessor's proof; it is not +new work here. Exact source heads and the unchanged main proof hash are in +SOURCES.json. + +If `A <= B`, then + +```text +A*n_a + B*n_b = A*(n_a+n_b) + (B-A)*n_b + >= 3A*t + (B-A)*t = (2A+B)*t. +``` + +Every coefficient used to multiply an inequality is nonnegative. Interchanging +a and b proves the other case. On each target role j, the coordinate projector +`E_jj` and word `aba` give exactly `[s]` on j and identity everywhere else; +`bab` does the same. Choose `aba` when A<=B and `bab` otherwise, and concatenate +over all t target roles. These full formal words attain the stated price and +leave every arbitrary spectator untouched. Thus the lower bound is sharp. + +For example, `(t,A,B)=(5,1,2)` costs 20 exactly, and `(5,0,2)` costs 10 exactly. +Zero-price calls may be used freely often, but the number of positive-price +calls is still bounded as above. If both prices vanish, the minimum is zero. +The theorem is about minimum value, not uniqueness of optimal words. + +## Checks and limitations + +`verify.py` independently builds the six binary matrices, full group-algebra +convolution, full register matrices, their natural images and binary block ranks. +It imports no predecessor implementation. Its complete receipt records: + +- 54 exact formal attaining endpoints, both orientations, t=0..8 and + R=t,t+1,t+2; these include arbitrary dirty spectators by coefficient equality. +- All 1,302 paid factors for R=1..5 with their separate `(1,0)/(0,1)` charges; + every two-role free scalar map on both sides of all 12 two-role paid factors + (144 compositions). +- 2,160 mixed paid/free prefixes for R=1..6, checking the natural homomorphism, + both rank inequalities and accumulated label bounds. These are deterministic + sample words, not a complete search over words. +- All 25 pairs from prices `{0,1/3,1,2,7/2}`, t=0..8, against every count pair + `t<=n_a,n_b<=4t` satisfying the three inequalities; both attaining prices. +- Controls demonstrating why each count inequality is needed, detecting a + full-formal corruption invisible in the natural representation, rejecting an + omitted attaining call, and verifying the direct-SWAP changed-alphabet case. +- A negative-price boundary: `D_N(a)^2=I` coefficientwise, so if A<0, appending + arbitrarily many `aa` loops makes the cost unbounded below. Likewise for B<0. + Nonnegative prices are therefore a substantive hypothesis. + +These finite checks support the written all-parameter proof; they do not replace +it. The natural representation is used only as a lower-bound image; complete +formal coefficients verify every claimed endpoint. The inherited `3t` theorem +is not independently formalized in a proof assistant here. + +The result does not cover role-dependent or state-dependent prices, different +paid labels, higher-rank calls charged as one, partial spectator restoration, +restricted clean input states, nonlinear operations, or the abelian rational +frame model. Nor does it supply native address conversion, hosting, precision, +tape bounds, a recursive child invoice or an integer-multiplication theorem. + +## Reproduce + +Python 3.12+, standard library, from repository root: + +```sh +python3 -I -O -B research/gl2-swap-weighted-tariff/verify.py +python3 -I -O -B research/gl2-swap-weighted-tariff/test_boundary.py +python3 scripts/research_package.py --package research/gl2-swap-weighted-tariff +``` + +Default verification is read-only. `--out NEW_FILE` regenerates the complete +receipt and refuses overwrite. Checks use explicit failures, including under +`-O`. The boundary test verifies unchanged Git-free replay, corrupt/missing +receipt rejection and exclusive regeneration. + +## Open next questions + +1. Can a physically legal changed address label cross multiple directions for + less than the corresponding invoice? This matters because fixed a/b tariff + asymmetry is now closed. Start with one named native implementation and its + full recursive charge; arbitrary formal labels have no such implementation. +2. What is sharp when label prices depend on the projector support? The weighted + combination above uses a single price per label. First classify attainable + projector-specific crossing charges; support-changing free scalar maps make + the price convention itself part of the contract. + +Contributor: ywz65 with substantial OpenAI Codex assistance. Credit remains with +Ross Richardson's general cut theorem and coordinate-SWAP bridge, Aaron Wang's +explicit asymmetric-tariff handoff, and their cited model predecessors. TASK.json +records the original picker, scope change, exact freshness and separate AI review. +No independent human review, new selected frontier or frozen-source edit is claimed. diff --git a/research/gl2-swap-weighted-tariff/RESULT.json b/research/gl2-swap-weighted-tariff/RESULT.json new file mode 100644 index 0000000000..2ae3a1a791 --- /dev/null +++ b/research/gl2-swap-weighted-tariff/RESULT.json @@ -0,0 +1,25 @@ +{ + "controls": { + "direct_swap_changed_alphabet": true, + "identity_negative_price_loop": true, + "natural_alias_detected_formally": true, + "omitted_attaining_call": true, + "three_missing_inequality_controls": true + }, + "formal_witnesses": 54, + "formula": "minimum=t*(2*min(A,B)+max(A,B))", + "projection": { + "free_two_role_compositions": 144, + "mixed_prefixes": 2160, + "paid_factors": 1302 + }, + "schema_version": 1, + "scope": "fixed nonnegative label tariffs; formal GL2 coordinate SWAP", + "tariff": { + "example_t5_a0_b2": 10, + "example_t5_a1_b2": 20, + "feasible_count_inequalities": 48525, + "rational_tariff_pairs": 25, + "sharp_instances": 225 + } +} diff --git a/research/gl2-swap-weighted-tariff/SOURCES.json b/research/gl2-swap-weighted-tariff/SOURCES.json new file mode 100644 index 0000000000..7fbc63bf57 --- /dev/null +++ b/research/gl2-swap-weighted-tariff/SOURCES.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11" + }, + { + "path": "research/symmetric-adjacent-cut-bound/PROOF.md", + "usage": "provenance", + "sha256": "008be68867a8e85f4e18455d206e03f20aebfc28e9f08efba576180e7e1edc50", + "git_blob": "30dad3856246c9cef3b8014ee967dd545f3a092d" + } + ], + "predecessors": [ + { + "pr": 1989, + "head": "8b9f3ec8b1e5745c42fec68d75da5fbc82ea91ec", + "path": "research/symmetric-adjacent-cut-bound/PROOF.md", + "git_blob": "30dad3856246c9cef3b8014ee967dd545f3a092d", + "sha256": "008be68867a8e85f4e18455d206e03f20aebfc28e9f08efba576180e7e1edc50", + "usage": "Ross Richardson general inversion-sum cut theorem; credited total bound." + }, + { + "pr": 2415, + "head": "7b9997ba2ca13be75dfc423642e2ce6b8ed18d6e", + "path": "research/gl2-swap-cut-corollary/README.md", + "git_blob": "c34c1460063ee4690c934d3c3fb3d81896f8931c", + "sha256": "3650918994be00323ccb61b75cdd81ecae47104a6e0765e319196618737949d9", + "usage": "Ross Richardson exact GL2 model bridge and total3t with arbitrary restored spectators; inherited theorem." + }, + { + "pr": 2444, + "head": "ba13eec9546a5ac4fca1df37209e3c42249b61c2", + "path": "research/kb2-alt13-noncommuting-tooling/README.md", + "git_blob": "db49244bf185dc2312c4bb52e2f4f570be7acf39", + "sha256": "af2c549536dafb7f141ba2f16aa744964b33bba1c739f1dab00942df7eb134be", + "usage": "Aaron Wang exact-search tooling and explicit asymmetric-tariff Open question2; answered here." + } + ] +} diff --git a/research/gl2-swap-weighted-tariff/TASK.json b/research/gl2-swap-weighted-tariff/TASK.json new file mode 100644 index 0000000000..954b5e2320 --- /dev/null +++ b/research/gl2-swap-weighted-tariff/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "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.", + "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": "Sharp weighted coordinate-SWAP cost for all nonnegative fixed a/b tariffs, all t and arbitrary finite restored dirty spectators.", + "scope_change_reason": "PR2444 explicitly leaves asymmetric label tariffs open and proposes weighted BFS. Close that price-boundary handoff using separate label rank bounds and the credited PR2415/1989 total-call bound. No new native operation identity is claimed.", + "bottleneck_link": "Rules out fixed label-price asymmetry as a sharing escape in the coordinate-SWAP primitive; changed native operations or state-dependent charges remain separate.", + "budget_minutes": 60, + "stop_rule": "Stop after the per-label proof, weighted sharp bound, full-formal attaining words, price/premise controls and Git-free replay.", + "outcome": "completed", + "evidence": "README theorem and credited total-bound invocation; verify.py full formal endpoints, distinct label ranks and weighted certificates; RESULT and test_boundary.", + "author": "ywz65", + "ai_assistance": "Substantial OpenAI Codex assistance for derivation, code, checking and writing. No independent human review.", + "selection": { + "nonce": "723f27887286a083b111edff339a66c7", + "track": "bit-mechanisms", + "scope_key": "7f5f4426ef796683c485" + }, + "open_questions": [ + { + "question": "Can a legal changed native label cross multiple directions below its invoice?", + "why_it_matters": "Fixed a/b tariff asymmetry does not save.", + "first_step": "Price one named native realization.", + "blocked_by": "Formal labels alone lack a physical compiler." + }, + { + "question": "What is sharp for projector-dependent label charges?", + "why_it_matters": "The new theorem requires fixed label prices.", + "first_step": "Define a price contract stable under free scalar mixing.", + "blocked_by": "Projector support changes under free operations." + } + ], + "freshness": { + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "initial_overlap": { + "open_prs": 732, + "discussions": 1212, + "discussion_utc": "2026-10-15T13:50:12+00:00" + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/2444#issuecomment-6193816332", + "validation": "Registered optimized CPython3.12.14 replay and Git-free boundary passed. Separate AI proof review found no actionable issue. Current PR2444/2415 heads match pins; fresh weighted-tariff overlap only identifies predecessor handoff.", + "submission_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "submission_overlap": { + "open_prs": { + "fetched_at": "2026-10-15T14:01:14.092899+00:00", + "complete_pagination": true, + "records": 739 + }, + "discussions": { + "fetched_at": "2026-10-15T14:01:51.358114+00:00", + "complete_pagination": true, + "records": 1213 + } + }, + "warnings": [], + "overlap_refresh_tool_commit": "91156f0d41b133979c8004ad8d0f7e9f58d73cbc" + } +} diff --git a/research/gl2-swap-weighted-tariff/VERIFY.json b/research/gl2-swap-weighted-tariff/VERIFY.json new file mode 100644 index 0000000000..30f4ef7cad --- /dev/null +++ b/research/gl2-swap-weighted-tariff/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Full formal attaining words, separate label ranks, mixed prefixes, weighted certificates and changed-premise controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_boundary.py" + ], + "timeout_seconds": 180, + "checks": "Git-free read-only replay, receipt corruption/missing controls and exclusive regeneration." + } + ] +} diff --git a/research/gl2-swap-weighted-tariff/test_boundary.py b/research/gl2-swap-weighted-tariff/test_boundary.py new file mode 100644 index 0000000000..ea1619ecb6 --- /dev/null +++ b/research/gl2-swap-weighted-tariff/test_boundary.py @@ -0,0 +1,57 @@ +#!/usr/bin/env python3 +"""Git-free export and complete-receipt rejection controls.""" +from hashlib import sha256 +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def hashes(root): + return {p.name: sha256(p.read_bytes()).hexdigest() for p in root.iterdir() if p.is_file()} + + +def run(root, succeeds, message=None, extra=()): + p = subprocess.run([sys.executable, '-I', '-O', '-B', str(root/'verify.py'), *map(str, extra)], + cwd=root, text=True, capture_output=True, timeout=90) + need((p.returncode == 0) == succeeds, 'unexpected exit: '+p.stdout+p.stderr) + if message: + need(message in p.stdout+p.stderr, 'wrong rejection reason: '+p.stdout+p.stderr) + + +def main(): + with tempfile.TemporaryDirectory(prefix='swap-weighted-tariff-') as tmp: + root = Path(tmp)/'export' + shutil.copytree(HERE, root, ignore=shutil.ignore_patterns('__pycache__')) + before = hashes(root) + run(root, True) + need(before == hashes(root), 'default export changed a file') + receipt = root/'RESULT.json' + original = receipt.read_bytes() + data = json.loads(original) + data['tariff']['example_t5_a1_b2'] -= 1 + receipt.write_text(json.dumps(data)) + run(root, False, 'complete receipt mismatch') + receipt.unlink() + run(root, False, 'RESULT.json') + receipt.write_bytes(original) + out = root/'fresh.json' + run(root, True, extra=('--out', out)) + need(json.loads(out.read_text()) == json.loads(original), 'regeneration changed receipt') + run(root, False, 'FileExistsError', extra=('--out', out)) + out.unlink() + need(before == hashes(root), 'boundary tests failed to restore export') + print('PASS_SWAP_WEIGHTED_BOUNDARY git_free_unchanged=1 receipt_controls=2 exclusive_output=1') + + +if __name__ == '__main__': + main() diff --git a/research/gl2-swap-weighted-tariff/verify.py b/research/gl2-swap-weighted-tariff/verify.py new file mode 100644 index 0000000000..901b6aaab2 --- /dev/null +++ b/research/gl2-swap-weighted-tariff/verify.py @@ -0,0 +1,241 @@ +#!/usr/bin/env python3 +"""Independent full F2[GL2(F2)] witnesses and weighted lower-bound checks.""" +import argparse +from fractions import Fraction +from itertools import product +import json +from pathlib import Path +from random import Random + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def rank(rows): + basis = {} + for row in rows: + while row: + bit = row.bit_length()-1 + if bit in basis: + row ^= basis[bit] + else: + basis[bit] = row + break + return len(basis) + + +def binary_mul(a, b): + return tuple(xor(b[j] for j in range(len(b)) if row >> j & 1) for row in a) + + +def xor(values): + result = 0 + for v in values: + result ^= v + return result + + +GROUP = tuple(a for a in product(range(4), repeat=2) if rank(a) == 2) +ONE = GROUP.index((1, 2)) +A = GROUP.index((3, 2)) +B = GROUP.index((1, 3)) +SWAP = GROUP.index((2, 1)) +MUL = [[GROUP.index(binary_mul(a, b)) for b in GROUP] for a in GROUP] + + +def ring_mul(a, b): + return xor(1 << MUL[i][j] for i in range(6) for j in range(6) + if a >> i & 1 and b >> j & 1) + + +def identity(r): + return tuple(tuple((1 << ONE) if i == j else 0 for j in range(r)) for i in range(r)) + + +def matrix_mul(a, b): + r = len(a) + return tuple(tuple(xor(ring_mul(a[i][k], b[k][j]) for k in range(r)) + for j in range(r)) for i in range(r)) + + +def projector(r, u, v): + need((u & v).bit_count() % 2 == 1, 'not a rank-one idempotent') + return tuple(v if u >> i & 1 else 0 for i in range(r)) + + +def call(rows, label): + r = len(rows) + scalar = (1 << label) ^ (1 << ONE) + return tuple(tuple(((1 << ONE) if i == j else 0) ^ + (scalar if rows[i] >> j & 1 else 0) + for j in range(r)) for i in range(r)) + + +def scalar(rows): + return tuple(tuple((1 << ONE) if row >> j & 1 else 0 for j in range(len(rows))) + for row in rows) + + +def natural(mat): + """Coordinate-major natural representation, 2r by 2r.""" + r = len(mat) + result = [0] * (2*r) + for i, row in enumerate(mat): + for j, entry in enumerate(row): + small = tuple(xor(GROUP[g][k] for g in range(6) if entry >> g & 1) + for k in range(2)) + for k in range(2): + for l in range(2): + result[k*r+i] |= ((small[k] >> l) & 1) << (l*r+j) + return tuple(result) + + +def crossing(mat): + r = len(mat)//2 + return rank([row >> r for row in mat[:r]]), rank([row & ((1 << r)-1) for row in mat[r:]]) + + +def witnesses(): + count = 0 + for t in range(9): + for extra in range(3): + r = t+extra + for labels in ((A, B, A), (B, A, B)): + out = identity(r) + for j in range(t): + p = projector(r, 1 << j, 1 << j) + for label in labels: + out = matrix_mul(out, call(p, label)) + expected = tuple(tuple((1 << (SWAP if i < t else ONE)) if i == j else 0 + for j in range(r)) for i in range(r)) + need(out == expected, 'full formal attainment') + need(crossing(natural(out)) == (t, t), 'target per-label rank') + count += 1 + return count + + +def projection_checks(): + factors = 0 + for r in range(1, 6): + for u in range(1, 1 << r): + for v in range(1, 1 << r): + if (u & v).bit_count() % 2: + p = projector(r, u, v) + for label, expect in ((A, (1, 0)), (B, (0, 1))): + need(crossing(natural(call(p, label))) == expect, 'per-label increment') + factors += 1 + # Every free GL2 scalar and all twelve two-role factors, on both sides. + factors2 = [call(projector(2, u, v), label) for u in range(1, 4) + for v in range(1, 4) if (u & v).bit_count() % 2 for label in (A, B)] + for free in GROUP: + f = scalar(free) + need(crossing(natural(f)) == (0, 0), 'free scalar crossing') + for paid in factors2: + for mixed in (matrix_mul(f, paid), matrix_mul(paid, f)): + need(crossing(natural(mixed)) == crossing(natural(paid)), + 'free scalar preservation') + rng = Random(2026101514) + checked = 0 + for r in range(1, 7): + for trial in range(30): + out = identity(r) + counts = [0, 0] + for step in range(12): + if step % 3 == 0 and r > 1: + rows = [1 << i for i in range(r)] + i, j = rng.sample(range(r), 2) + rows[i] ^= 1 << j + nxt = scalar(rows) + else: + while True: + u, v = rng.randrange(1, 1 << r), rng.randrange(1, 1 << r) + if (u & v).bit_count() % 2: + break + label = rng.choice((A, B)) + counts[label == B] += 1 + nxt = call(projector(r, u, v), label) + before = natural(out) + out = matrix_mul(out, nxt) + now = natural(out) + need(now == binary_mul(before, natural(nxt)), 'natural product convention') + q0, q1 = crossing(now) + p0, p1 = crossing(before) + d0, d1 = crossing(natural(nxt)) + need(q0 <= p0+d0 and q1 <= p1+d1, 'subadditivity') + need(q0 <= counts[0] and q1 <= counts[1], 'prefix label bound') + checked += 1 + return {'paid_factors': factors, 'free_two_role_compositions': 144, + 'mixed_prefixes': checked} + + +def tariff_checks(): + weights = [Fraction(0), Fraction(1, 3), Fraction(1), Fraction(2), Fraction(7, 2)] + inequalities, sharp = 0, 0 + for t in range(9): + for a, b in product(weights, repeat=2): + lower = t*(2*min(a, b)+max(a, b)) + need(min(2*t*a+t*b, t*a+2*t*b) == lower, 'sharp weighted formula') + sharp += 1 + for na in range(t, 4*t+1): + for nb in range(t, 4*t+1): + if na+nb >= 3*t: + need(a*na+b*nb >= lower, 'weighted dual inequality') + inequalities += 1 + return {'rational_tariff_pairs': len(weights)**2, 'sharp_instances': sharp, + 'feasible_count_inequalities': inequalities, + 'example_t5_a1_b2': 20, 'example_t5_a0_b2': 10} + + +def controls(): + p = projector(2, 1, 1) + aa = matrix_mul(call(p, A), call(p, A)) + need(aa == identity(2), 'negative tariff identity loop') + need(2*Fraction(-1) < 0, 'negative tariff control') + out = identity(2) + for label in (A, B, A): + out = matrix_mul(out, call(p, label)) + corrupt = [list(row) for row in out] + corrupt[0][0] ^= 63 + corrupt = tuple(tuple(row) for row in corrupt) + need(corrupt != out and natural(corrupt) == natural(out), 'unfaithful natural control') + # A concrete weighted claim needs BOTH individual bounds and the total bound. + need(1*3+2*0 < 4, 'dropped b-bound control') + need(2*0+1*3 < 4, 'dropped a-bound control') + need(1*1+1*1 < 3, 'dropped total-bound control') + # A changed alphabet directly charging SWAP at 1 would violate 3t. + direct = call(p, SWAP) + need(direct == out and crossing(natural(direct)) == (1, 1), 'direct SWAP boundary') + need(matrix_mul(call(p, A), call(p, B)) != out, 'omitted attaining call') + return {'identity_negative_price_loop': True, 'natural_alias_detected_formally': True, + 'three_missing_inequality_controls': True, 'direct_swap_changed_alphabet': True, + 'omitted_attaining_call': True} + + +def compute(): + need(MUL[MUL[A][B]][A] == MUL[MUL[B][A]][B] == SWAP, 'label identity') + return dict(schema_version=1, scope='fixed nonnegative label tariffs; formal GL2 coordinate SWAP', + formula='minimum=t*(2*min(A,B)+max(A,B))', + formal_witnesses=witnesses(), projection=projection_checks(), + tariff=tariff_checks(), controls=controls()) + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--out', type=Path) + args = parser.parse_args() + result = compute() + text = json.dumps(result, indent=2, sort_keys=True)+'\n' + if args.out: + with args.out.open('x', encoding='utf-8', newline='\n') as f: + f.write(text) + else: + need(json.loads((HERE/'RESULT.json').read_text()) == result, 'complete receipt mismatch') + print('PASS_SWAP_WEIGHTED_TARIFF formal_witnesses=54 paid_factors=1302 mixed_prefixes=2160') + + +if __name__ == '__main__': + main()