Prove sharp asymmetric coordinate-SWAP tariffs with dirty spectators

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.

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
+  }
+}

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."
+    }
+  ]
+}

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"
+  }
+}

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."
+    }
+  ]
+}