Prove exact mixed GL2 tariffs for disjoint address blocks

research/mixed-gl2-block-tariff/README.md

@@ -0,0 +1,185 @@
+# Exact mixed GL2-block tariffs in larger address spaces
+
+**Scoped formal-model theorem; no new kappa.** Fix disjoint pairs of address
+coordinates. A diagonal register target can use any of the six `GL_2(F2)`
+operators on each pair, with different choices on different registers.
+Its exact cost is the sum of the block tariffs
+
+```text
+label:    e  a  b  ab  ba  s=aba
+cost:     0  1  1   2   2     3.
+```
+
+This remains true in every ambient `GL_n(F2)` that contains the pairs, even
+when the circuit uses arbitrary coordinate CNOTs between pairs or with
+address spectators. Free scalar register mixing and any finite number of
+restored dirty registers are allowed.
+
+The dimension-two mixed tariff is already a corollary of Ross Richardson's
+[PR #1989](https://github.com/CrocSwap/integer-mult-bounds/pull/1989), through
+the `GL_2(F2)=S_3` bridge in
+[PR #2415](https://github.com/CrocSwap/integer-mult-bounds/pull/2415).
+This contribution extends the averaged row-order method of
+[PR #4950](https://github.com/CrocSwap/integer-mult-bounds/pull/4950) from
+identical swaps to all six block labels and sums over disjoint pairs.
+It does not claim a new dimension-two lower bound. The selected kappa remains
+`60403/20000000`; no physical supplier is supplied.
+
+## Model and theorem
+
+Let `n>=2` and let `B_j=(p_j,q_j)` be fixed pairs with disjoint coordinate
+sets in `{0,...,n-1}`. For each target register `r` and block `j`, select
+`g_(r,j)` from `GL_2(F2)`. Its embedding acts on the two coordinates of `B_j`
+and fixes all other coordinates. The register target `g_r` is the product
+of these embeddings. They commute because the pairs are disjoint.
+Other register targets and all unused address coordinates are identity.
+
+Work in the formal group algebra `M_R(F2[GL_n(F2)])`. Every register input
+is arbitrary. The endpoint is `diag([g_1],...,[g_t],1,...,1)`, with every
+extra register restored and no off-diagonal residue. Paid units are
+
+```text
+I_R + ([c]+1)N,
+```
+
+where `c` is any coordinate CNOT in the ambient address space, and `N` is
+any binary scalar rank-one idempotent. Each unit costs one. Free scalar
+`GL_R(F2)` maps may occur anywhere. There are no other free address maps,
+clean allocations or uncharged restoration calls.
+
+**Theorem.** For every finite `R>=t`, the exact paid-call minimum is
+`sum_(r,j) ell(g_(r,j))`, with `ell` given by the table above.
+The empty target uses the empty word. The statement covers arbitrary
+intermediate scalar projectors and cross-pair address calls; only the
+required final target has the block form.
+
+## Proof
+
+Use the left regular representation of `G=GL_n(F2)`. For each total order
+`<` on the nonzero binary vectors and pair `(p,q)`, let
+
+```text
+A_(p,q) = {x in G : row_p(x) < row_q(x)}.
+```
+
+On all `R` registers, take the crossing rank from this address cut to its
+complement. Block multiplication gives `q(MN)<=q(M)+q(N)`. A free scalar
+map has crossing rank zero. A paid call has crossing block
+`P_c[A^c,A] tensor N`, so its crossing rank is `out_A(c)`, since `rank(N)=1`.
+A diagonal target has the sum of its register crossing ranks. These facts
+hold in the formal algebra and do not assume commuting projectors.
+
+Average each cut over all total orders. Write `u=|G|/6`.
+A CNOT writing neither coordinate of a pair changes neither selected row,
+so its charge in that cut is zero. If it writes the first row, denote the
+old rows by `x,y` and the new row by `z`. The three vectors are distinct:
+rows of an invertible matrix are independent, and a sum of two rows is
+neither zero nor any original row. The event that the cut is left is
+`x<y<z`, which has probability `1/6`. If it writes the second row, the
+leaving event is `z<x<y`, with the same probability. This holds for a read
+inside the pair, in another pair or at an address spectator.
+
+Thus a call contributes `u` to the averaged cut of its written coordinate's
+pair, if there is such a pair, and zero to every other pair. Disjointness
+makes the sum of all paid charges at most `u`. In particular, reading from
+another pair does not charge its cut: that pair's rows do not change.
+
+For a target block, put `z=x+y`. With
+`a=[[1,1],[0,1]]` and `b=[[1,0],[1,1]]`, products act rightmost first.
+The output rows and numbers of leaving orders among the six orders of
+`x,y,z` are:
+
+| Label | Output rows | Leaving orders |
+| --- | --- | ---: |
+| e | x,y | 0 |
+| a | z,y | 1 |
+| b | x,z | 1 |
+| ab | y,z | 2 |
+| ba | z,x | 2 |
+| s=aba | y,x | 3 |
+
+Each averaged target charge is `u*ell(g)`. Other blocks in the same register
+do not change this pair of rows. Summing over target registers and blocks
+therefore gives target crossing rank `u*sum ell(g_(r,j))`. Subadditivity
+bounds it by `u` times the total paid-call count. Since `u>0`, this proves
+the lower bound for arbitrary dirty workspace and ambient dimension.
+
+For the upper bound, use the direct two-generator word for each block on
+its own register with coordinate projector `E_rr`. Its length is `ell(g)`.
+The factors remain diagonal formal monomials, so the group identity is
+also a coefficientwise identity in the full formal algebra. Concatenate
+the words for all blocks and registers. This attains the lower bound and
+restores every unused register and coordinate. No unpaid cleanup is needed.
+
+## Consequences and boundary
+
+The heterogeneous target `diag([a],[b],[aba])` costs exactly five for all
+`n>=2` and any `R>=3`. The fixed-three-register search in
+[the retained heterogeneous-target note](../bit-mixed-transposition-triple/README.md)
+already found five at `n=2`. Its extra-register question is covered there by
+the inherited dimension-two cut theorem; the ambient-address extension here
+also rules out using other address coordinates to reduce that cost.
+
+The coordinate pairs must be disjoint. On one register, the product of the
+three swaps on `(01),(12),(02)` equals the swap on `(12)`. Its separate
+nine-call implementation can therefore be replaced by three calls. The
+verifier checks this literal counterexample and rejects overlapping pairs
+as input to the additive tariff. This is a one-register product; it is not
+the three-register mixed-swap target of the component-cut theorem.
+
+The theorem also retains the rank-one tariff, arbitrary-input endpoint and
+absence of free address transformations. It does not cover unequal or
+projector-dependent prices, a rank-two call charged as one, a restricted
+clean-input endpoint, or arbitrary overlapping block products.
+
+## Evidence and reproduction
+
+Use CPython 3.12 and the standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/mixed-gl2-block-tariff
+python3.12 -I -W error -O -B research/mixed-gl2-block-tariff/verify.py
+```
+
+Expected markers: `PASS_REGISTERED_RESEARCH_PACKAGE` and
+`PASS_MIXED_GL2_BLOCK_TARIFF costs=0,1,1,2,2,3 no_new_kappa`.
+Normal replay recomputes [RESULT.json](RESULT.json), writes no files and
+needs no Git or network. `--emit-receipt` emits JSON for explicit regeneration.
+The receipt binds all five source files by SHA-256.
+
+The checker compares the six crossing counts with independently computed
+`GL2` word lengths. It checks 80 actual coordinate-CNOT/basis cases over
+31,992 relative orders, including cross-pair reads and spectator writes.
+It exhausts all three-register single-block label triples and all two-register
+two-block label quadruples in the declared finite dimension/register grids:
+7,128 complete diagonal formal endpoints and 39,852 single-call omissions.
+Nine controls cover invalid contracts, empty targets, the five-call example
+and the overlapping-block counterexample.
+
+These particular upper words remain diagonal monomials. Their group labels
+are therefore sufficient to verify their full formal endpoints. This does
+not assert that natural matrices certify arbitrary group-algebra programs.
+The lower bound for all programs is the written regular-representation proof.
+No predecessor executable is imported.
+
+## Open next questions
+
+What is possible for overlapping target blocks? First specify the actual
+one-register product or multi-register endpoint; the example above shows
+that a list of local block prices need not add. No general cost law for
+that changed boundary is supplied here. Native realization, full supplier
+accounting and proof-kernel review remain separate obligations.
+
+## Credit and source pins
+
+Prepared for Ali Romman with substantial OpenAI Codex assistance. New work
+is Apache-2.0. Ross Richardson supplied the general inversion-sum theorem
+and the GL2 bridge; James Reed supplied the averaged spectator cut; Cinna
+Davis supplied the fixed-register heterogeneous question. Their retained
+notes credit Mihir Srivastava, commdata2338, Gareth Davidson and earlier
+register-model/cut contributors. All notices remain unchanged.
+The four source documents are provenance only, pinned in
+[SOURCES.json](SOURCES.json). Base:
+`f259dabc7d70e0db8d6d36bfda888f008bbfecc1`, priority revision 7.
+No independent human review, native/compiler admission, selected cold replay,
+full multiplier theorem or kappa improvement is claimed.

research/mixed-gl2-block-tariff/RESULT.json

@@ -0,0 +1,77 @@
+{
+  "ambient_paid": {
+    "cases": 80,
+    "relative_orders": 31992
+  },
+  "boundary_controls": 9,
+  "formal_diagonal_words": {
+    "endpoints": 7128,
+    "omissions": 39852,
+    "paid_calls": 39852
+  },
+  "no_new_kappa": true,
+  "schema": "mixed-gl2-block-tariff/v1",
+  "source_sha256": {
+    "README.md": "c261a4d289c61e31dc495303f22d994b506c87b2f03de308ed94435bd7a1a4e0",
+    "SOURCES.json": "0bf3f591df2bd72806d5087a421a7fdd4c248ae9bd356dbc92b8569da750fb32",
+    "TASK.json": "aea608cafc4e5ec31d8af1fa52c6615125cf909ae26e0d6e222378b00e777b4b",
+    "VERIFY.json": "491b483ee1214d957f4ded739810898d6e4978ff031337538ca2c966c880763b",
+    "verify.py": "b99269d958510a9f9cfde49a28b239d3e56d21ddba8a7e39a37b590cb44b1775"
+  },
+  "tariffs": {
+    "a": {
+      "cost": 1,
+      "leaving_orders": 1,
+      "orders": 6,
+      "rows": [
+        3,
+        2
+      ]
+    },
+    "ab": {
+      "cost": 2,
+      "leaving_orders": 2,
+      "orders": 6,
+      "rows": [
+        2,
+        3
+      ]
+    },
+    "b": {
+      "cost": 1,
+      "leaving_orders": 1,
+      "orders": 6,
+      "rows": [
+        1,
+        3
+      ]
+    },
+    "ba": {
+      "cost": 2,
+      "leaving_orders": 2,
+      "orders": 6,
+      "rows": [
+        3,
+        1
+      ]
+    },
+    "e": {
+      "cost": 0,
+      "leaving_orders": 0,
+      "orders": 6,
+      "rows": [
+        1,
+        2
+      ]
+    },
+    "s": {
+      "cost": 3,
+      "leaving_orders": 3,
+      "orders": 6,
+      "rows": [
+        2,
+        1
+      ]
+    }
+  }
+}

research/mixed-gl2-block-tariff/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1",
+  "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/bit-mixed-transposition-triple/README.md",
+      "usage": "provenance",
+      "git_blob": "44c449f37495b75cfda01a3293eca1e7e29633e9",
+      "sha256": "d394690ebf1905f3940e3a17662e1169bed68fe02304e2ed863f79c4ad093d5f"
+    },
+    {
+      "path": "research/gl2-swap-cut-corollary/README.md",
+      "usage": "provenance",
+      "git_blob": "c34c1460063ee4690c934d3c3fb3d81896f8931c",
+      "sha256": "3650918994be00323ccb61b75cdd81ecae47104a6e0765e319196618737949d9"
+    },
+    {
+      "path": "research/swap-row-order-cut/README.md",
+      "usage": "provenance",
+      "git_blob": "941c1eb4f2301023757c45bbe1bb767962065cd1",
+      "sha256": "a5e9661f5ffa504cafee1c9481f0a1072b98341f98a031a2b4d18bb8c4a9ef7c"
+    },
+    {
+      "path": "research/symmetric-adjacent-cut-bound/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "30dad3856246c9cef3b8014ee967dd545f3a092d",
+      "sha256": "008be68867a8e85f4e18455d206e03f20aebfc28e9f08efba576180e7e1edc50"
+    }
+  ]
+}

research/mixed-gl2-block-tariff/TASK.json

@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1",
+  "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 mixed GL2-block sum tariff for arbitrary ambient coordinate CNOTs, free scalar mixing and restored dirty registers.",
+  "scope_change_reason": "The dimension-two mixed tariff follows from PR1989. Extend PR4950 averaged row-order cuts to all six block operators and sums over disjoint coordinate pairs; do not repeat an old fixed-register search.",
+  "bottleneck_link": "Arbitrary address spectators and cross-pair reads/writes cannot reduce this complete formal paid-call bill. Native costs and supplier admission remain separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the uniform tariff proof, bounded exact checks and changed-premise control. No general formal-word census or native search.",
+  "outcome": "completed",
+  "evidence": "Six exact crossing tariffs and independent group word lengths; actual coordinate-CNOT order counts; exhaustive bounded diagonal upper words, call omissions and an overlapping-block counterexample.",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance for proof, implementation, verification and publication. No independent human or proof-kernel review.",
+  "open_questions": [
+    {
+      "question": "What cost is possible for target blocks whose coordinate sets overlap?",
+      "why_it_matters": "The disjoint-write accounting no longer applies, and an explicit one-register product can cancel from nine to three calls.",
+      "first_step": "Specify one overlapping target product and compare its actual endpoint with the formal cut charges.",
+      "blocked_by": "No general additive law is claimed for overlapping blocks."
+    }
+  ],
+  "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19139741",
+  "selection": {
+    "mode": "handoff-first",
+    "source_pr": 4950,
+    "source_head": "78dc9c12f46967df0d85594875a32a62b5639670",
+    "related_question": "research/bit-mixed-transposition-triple/README.md"
+  },
+  "overlap": {
+    "searched_at": "2026-10-23T06:47:45.225966+00:00",
+    "open_prs": {
+      "fetched_at": "2026-10-23T06:46:43.014855+00:00",
+      "complete_pagination": true,
+      "records": 318
+    },
+    "discussions": {
+      "fetched_at": "2026-10-23T06:47:45.121400+00:00",
+      "complete_pagination": true,
+      "records": 4130
+    },
+    "local_notes": 83,
+    "total_local_notes": 6710,
+    "limits": "Sparse omitted notes, arbitrary diffs and unpublished work. Related local proofs were read directly."
+  }
+}