Prove five-call optimum for three GL2 swaps at scalar-rank cap two

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.

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

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

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