Prove six-call two-SWAP cost with arbitrary address spectators

research/two-swap-address-spectators/README.md

@@ -0,0 +1,212 @@
+# Two swaps cost six calls with arbitrary address spectators
+
+**Scoped formal-model theorem.** For every finite address dimension `n>=2`
+and scalar register count `R>=2`, two coordinate-SWAP targets cost exactly
+six paid coordinate-CNOT calls, with free scalar mixing and arbitrarily many
+restored dirty registers. This closes both higher-dimension questions in
+[PR1495](https://github.com/CrocSwap/integer-mult-bounds/pull/1495)'s
+[finite certificate](../coordinate-cnot-address-spectator/README.md).
+It supplies no native implementation, multiplication supplier or new kappa.
+
+The new step is a row-write budget followed by a **parabolic subgroup
+projection**. The all-register two-coordinate obstruction is retained from
+commdata2338's [PR1414](https://github.com/CrocSwap/integer-mult-bounds/pull/1414).
+We also restate its six-call consequence using Ross Richardson's
+[cut corollary](../gl2-swap-cut-corollary/README.md) of
+[PR1989](https://github.com/CrocSwap/integer-mult-bounds/pull/1989), making
+the argument reviewable here without a finite word search.
+
+## Exact contract
+
+Work over `M_R(F2[GL_n(F2)])`. Address indices and scalar-register indices
+are separate and both start at zero. A paid call is
+
+```
+D_N(g) = I_R + ([g] + [I_n]) N,
+g = I_n + E_ij,  i != j,
+N = u v^T over F2,  v^T u = 1.
+```
+
+Every coordinate CNOT is allowed; each call has a rank-one idempotent scalar
+coupling and costs one. Scalar `GL_R(F2)` maps are free and may be interleaved.
+The complete endpoint is `T=diag([s],[s],[I_n],...,[I_n])`, where `s` swaps
+address coordinates zero and one and fixes the rest.
+
+Equality is coefficientwise in the full formal group algebra on arbitrary
+inputs. Extra registers are dirty and individually restored; off-diagonal
+couplings vanish. There are no free address maps, clean allocations, erasures
+or resets. Preparation and undo calls are charged. This explicit formal
+alphabet is distinct from a native pricing model or the older abelian model.
+
+## Proof
+
+**1. Normalize free scalar maps.** Commuting a scalar map past a paid call
+conjugates `N`, preserving rank one and idempotence. Gather all scalar maps
+into one residual factor. Augmentation sends every `[g]` to one and every
+paid call and the target to `I_R`. The residual scalar factor is therefore
+identity. Paid length and labels are unchanged. This normalization is credited
+to Gareth Davidson/PR1333 in PR1414.
+
+**2. Count writes to each address row.** Apply the natural representation,
+ordering the binary space by address blocks of size `R`. A call becomes
+`I_(nR)+E_ij tensor N`. For a prefix matrix `P`, left multiplication
+changes only block row `i`, by adding `N row_j(P)`. Each prefix is
+invertible: every gate squares to identity because `E_ij^2=0`. Thus
+`row_j(P)` has full row rank `R` and `rank(N row_j(P))=1`.
+
+If row `i` is written `c_i` times, telescoping its changes gives
+`rank(row_i(P_final-I))<=c_i`. If `c_i=1`, its unique nonzero rank-one
+change cannot disappear: calls targeting other rows leave it unchanged.
+A row that finishes unchanged is therefore never written or written at
+least twice. All dirty inputs are included.
+
+Let `E=diag(1,1,0,...,0)` on the scalar registers. The natural target is
+`I_(nR)+(s-I_n) tensor E`. Its two active address rows each have delta
+rank two; all other rows have delta zero. Hence
+
+```
+c_0 >= 2, c_1 >= 2;
+for i >= 2, either c_i=0 or c_i>=2.
+```
+
+A successful word of at most five calls **cannot write a spectator address
+row**, since that requires at least six calls. It may still read spectators:
+remaining calls may have `i<2,j>=2`.
+
+**3. Remove read-only spectators in the formal algebra.** All remaining
+labels belong to the subgroup
+
+```
+H = { [[A,B],[0,I_(n-2)]] : A in GL_2(F2), B arbitrary }.
+```
+
+Block multiplication shows that taking the upper-left block defines a group
+homomorphism `pi:H -> GL_2(F2)`. For `n=2` it is the identity.
+The inclusion `F2[H] -> F2[GL_n(F2)]` is injective: distinct group elements
+remain distinct formal basis vectors. The normalized word and target lie
+in this subalgebra, so their **formal** equality descends under the linear
+extension of `pi`.
+
+An active-to-active CNOT maps to a coordinate CNOT in `GL_2`. A read from a
+spectator maps to identity, making its paid factor `I_R`. Delete those
+identity factors. The resulting word has at most five legal calls for two
+swaps in the two-coordinate model, with the same projectors and dirty roles.
+
+This projection is invalid on all of `GL_n`: in dimension three,
+`g=I+E_02` and `h=I+E_21` have identity upper-left blocks, while `gh`
+has upper-left block `I_2+E_01`. Write exclusion must precede projection.
+Natural-image equality alone cannot justify this formal step either,
+because that representation has a nonzero algebra kernel.
+
+**4. Apply the two-coordinate obstruction.** PR1414's
+[PROOF.md](../coordinate-cnot-register-bound/PROOF.md) proves the six-call
+bound for every `R`. For completeness, the later PR1989 cut argument gives
+a short derivation. Order nonzero address vectors as `(0,1),(1,1),(1,0)`.
+The two CNOTs act as adjacent transpositions `(12),(23)`; their three-call
+swap is `(13)`. Act simultaneously on the six ordered pairs of distinct
+labels. On every scalar register, partition this basis into increasing
+pairs `H+` and decreasing pairs `H-`. Put `q(M)=rank M[H-,H+]`.
+Block multiplication and rank subadditivity give `q(UV)<=q(U)+q(V)`.
+
+Each adjacent transposition reverses exactly one increasing pair, so each
+paid rank-one factor has crossing rank one. Free scalar mixing has crossing
+rank zero. The swap reverses all three increasing pairs; on two registers
+its target has crossing rank six. Restored dirty registers contribute zero.
+Thus at least six paid calls are required, contradicting the projected word.
+This cut method and its all-register extension are credited to PR1989 and
+the retained corollary.
+
+**5. Attain six.** On scalar register zero use `a,b,a`, where
+`a=I_n+E_01,b=I_n+E_10`, with projector `E_00`. Repeat with projector
+`E_11` on scalar register one. Since `aba=s`, these six calls give the
+complete formal endpoint, fixing all other roles and address coordinates.
+
+The minimum is six by this uniform written argument, not extrapolation from
+finite checks. This does not classify shortest words: at length six the
+row counts `(2,2,2)` satisfy the necessary budget.
+
+## Reproduction and finite evidence
+
+Python 3.12 and its standard library suffice. From the repository root:
+
+```sh
+python -I -W error -B research/two-swap-address-spectators/verify.py
+python -I -O -W error -B research/two-swap-address-spectators/verify.py
+python -B scripts/research_package.py --package research/two-swap-address-spectators --check-only
+python -B scripts/research_package.py --package research/two-swap-address-spectators
+```
+
+The direct command prints
+`PASS_TWO_SWAP_ADDRESS_SPECTATORS finite_checks=passed uniform_minimum=6_by_written_proof no_new_kappa`.
+Use `--json` for recomputed evidence. Explicit exception checks survive
+optimized Python. No solver, network or predecessor code is imported.
+Four proof/model inputs are authenticated by SHA256 and Git blob hash;
+the registered runner checks historical provenance.
+
+The verifier checks deterministic eight-call prefixes for `n=2..6,R=2..5`,
+including involutions, independent matrix multiplication, row-rank budgets
+and nonzero single writes: 1,280 transitions, 5,120 row bounds and 2,656
+single-write checks. It exhausts 9,792 parabolic products at `n=3,4` and
+2,996 write-count vectors of length at most five for `n=2..8`. It checks 20 full
+formal six-call endpoints, their reversals and scalar conjugates, rejects
+all 120 single-call omissions, and detects 12 dirty-only faults missed by
+clean-input restrictions. Controls exhibit an invalid whole-group projection,
+a nonzero formal element with zero natural image, and the forbidden rank-two
+tariff under which three calls suffice.
+
+Author replay on Windows / CPython 3.12.0 / Git 2.47.1 passed both registered
+commands. The current schema's orientation command,
+`python -B scripts/research_selected_baseline.py`, also returned
+`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`: selected source bindings and exact
+metadata consistency only. The historical command printed in the original
+task card does not handle this selected productive-helper schema.
+
+This is a scoped proof with finite supporting checks, not Lean verification
+or independent human review. No selected-supplier cold replay, native
+rational-address compiler, hosting, precision/tape bound, recursive paid
+profile or outer analytic transfer is supplied. Selected kappa is unchanged.
+
+## Scope, overlap and credit
+
+Base: `cef4b52f2a59009865bf8eabde1be3f159063703`, current main at session
+entry; priority revision 7. Picker task `bit-new-register-model`, nonce
+`434b93a0ec53b6f1a0baea72e385b919`, scope key `7084092dd726e7ba1f2f`.
+[TASK.json](TASK.json) preserves the original card and the changed scope:
+a negative formal-model screen does not satisfy its native construction
+gate. We compare with PR1495's finite GL3 screen and the two-coordinate
+bounds, without rerunning the GL3 census or mixed-root tariff.
+
+The entry overlap snapshot covered 6,601 local README/TASK scope records,
+308 open PRs including drafts, and 4,006 Discussion records with complete
+pagination and no warnings (2026-10-23 02:29-02:31 UTC). Focused terms included
+`coordinate-cnot-address-spectator`, `address spectator` and `two swaps`.
+Coverage excludes arbitrary diffs, all closed-PR history and unpublished
+work; no-match is not novelty proof. Canonical coordination:
+[Discussion #1317](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19136566).
+
+Credit commdata2338 for PR1414's obstruction and PR1495's finite certificate
+and open questions; Gareth Davidson (@bitplane)/PR1333 for the restricted
+alphabet and normalization; Ross Richardson/PR1989 and the GL2 corollary
+for the cut theorem. Their notes retain Adam Gall, Cinna Davis and earlier
+cut-method credit. Credit eumemic/PR288, Ali Romman/PR468 and David Govea/PR720
+for the surrounding register-model and rational-address work. Source packages
+remain unchanged. The contribution here is uniform address-spectator
+elimination and its verifier, not the two-coordinate lower bound.
+
+Prepared for Mihir Srivastava (@mihir-s-05), with substantial OpenAI Codex
+assistance in proof development, coding, checking and writing. No independent
+human proof review or literature-priority claim is made. Apache-2.0.
+
+## Open next questions
+
+1. **Can three swaps benefit from spectator address coordinates?** The
+   two-coordinate minimum is nine, but the row budget permits an eight-call
+   candidate with counts `(3,3,2)`. First analyze the two spectator writes
+   and whether they can be eliminated. This note establishes neither such
+   a word's existence nor exclusion; a missing elimination lemma blocks
+   extending the argument.
+2. **Which native operation escapes the rank-one coordinate-CNOT tariff?**
+   First specify a complete arbitrary-input endpoint and implementation,
+   then charge preparation and restoration. Native realization and full
+   recursive accounting block transfer to the selected construction.
+   Further finite searches in the two-swap model proved here are unnecessary.

research/two-swap-address-spectators/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703",
+  "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/coordinate-cnot-address-spectator/README.md",
+      "usage": "input",
+      "git_blob": "15b3db71d9fc13b4e9806caf42dd56213936fc88",
+      "sha256": "f433d3891cdc88fb47e055c4246798980529268a9a17250574414f805935ddd5"
+    },
+    {
+      "path": "research/coordinate-cnot-register-bound/README.md",
+      "usage": "input",
+      "git_blob": "cdcc5a9e7f11ab3dbf7745a175ddcca208c68211",
+      "sha256": "e1666512fb71cf34c427c69ffb61a18b61e897a7f8f91f87820edf744e85a9fe"
+    },
+    {
+      "path": "research/gl2-swap-cut-corollary/README.md",
+      "usage": "input",
+      "git_blob": "c34c1460063ee4690c934d3c3fb3d81896f8931c",
+      "sha256": "3650918994be00323ccb61b75cdd81ecae47104a6e0765e319196618737949d9"
+    },
+    {
+      "path": "research/coordinate-cnot-register-bound/PROOF.md",
+      "usage": "input",
+      "git_blob": "68fee5b5ccff5329e27300e40dcbd483640dd6b7",
+      "sha256": "bcee89f92dcce8253bd7eae6e924ddff598c900da81979c6171a412f03d765e1"
+    }
+  ]
+}

research/two-swap-address-spectators/TASK.json

@@ -0,0 +1,70 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703",
+  "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 six-call cost of two coordinate swaps for arbitrary finite address dimension n>=2 and arbitrary scalar register count R>=2, with restored dirty roles.",
+  "scope_change_reason": "The assigned card seeks a native escape. This bounded negative formal-model result instead resolves the two higher-dimensional questions in PR1495 using a row-write budget and subgroup projection; no native supplier is claimed.",
+  "bottleneck_link": "Side result on the bit-mechanisms track: excludes address-spectator or dirty-role enlargement as a two-swap saving in this exact tariff. It does not discharge the selected supplier obligations or change kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the uniform proof, exact finite controls, registered replay and publication checks. Do not extend into a larger word census or native construction round.",
+  "outcome": "negative-result",
+  "evidence": "README.md gives the uniform proof; verify.py checks finite row-budget, parabolic-projection and full formal-endpoint fixtures with explicit failure controls. VERIFY.json registers normal and optimized replay.",
+  "author": "Mihir Srivastava, with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance for repository orientation, proof development, implementation, finite verification, writing and GitHub coordination. No independent human review claimed.",
+  "open_questions": [
+    {
+      "question": "Can three swaps benefit from spectator address coordinates?",
+      "why_it_matters": "The two-coordinate minimum is nine; an eight-call count vector (3,3,2) is not excluded by this row budget.",
+      "first_step": "Analyze two writes to a spectator row and whether a formal endpoint forces an eliminable subword, before any bounded search.",
+      "blocked_by": "No elimination argument for a spectator row written twice; no eight-call candidate or exclusion supplied."
+    },
+    {
+      "question": "Which native operation can escape the rank-one coordinate-CNOT tariff?",
+      "why_it_matters": "A changed formal price is irrelevant to the selected construction without a complete native implementation and paid profile.",
+      "first_step": "Specify a complete arbitrary-input endpoint and price all preparation and restoration for the proposed changed operation.",
+      "blocked_by": "Native realization and full recursive accounting remain absent."
+    }
+  ]
+}

research/two-swap-address-spectators/VERIFY.json

@@ -0,0 +1,39 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/coordinate-cnot-address-spectator/README.md",
+    "research/coordinate-cnot-register-bound/README.md",
+    "research/gl2-swap-cut-corollary/README.md",
+    "research/coordinate-cnot-register-bound/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Finite row-write ranks, subgroup projection, full formal witnesses, omitted calls, dirty-only faults, rank-two tariff and natural-image alias controls; source hashes."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Finite row-write ranks, subgroup projection, full formal witnesses, omitted calls, dirty-only faults, rank-two tariff and natural-image alias controls; source hashes."
+    }
+  ]
+}