Prove bipartite commutator incidence tariff

research/heisenberg-commutator-incidence-seedb054/OVERLAP.json

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18938788",
+  "claim_correction": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18938817",
+  "search": {
+    "command": "python3 scripts/find_overlap.py --refresh --json --task bit-new-register-model --limit 150 'H(2,2)' 'commutator incidence graph' 'bipartite commutator' 'commutator grid' 'K2,2' 'generalized Heisenberg' 'edge-multiplicity tariff' 'central commutator targets'",
+    "searched_at": "2026-10-15T02:24:38.270400+00:00",
+    "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE",
+    "coverage": {
+      "open_prs": {
+        "fetched_at": "2026-10-15T02:22:33.494118+00:00",
+        "complete_pagination": true,
+        "records": 485
+      },
+      "discussions": {
+        "fetched_at": "2026-10-15T02:24:38.270400+00:00",
+        "complete_pagination": true,
+        "records": 967
+      }
+    },
+    "warnings": [],
+    "exact_scope_matches": "The only exact-term remote match is this newly posted Cycle32 claim #18938788. No other H(2,2), K2,2, commutator-grid/incidence, or edge-multiplicity tariff overlap was found. A broad central-commutator phrase matched the completed UT3 handoff #1317 comment #18912406, a different group, target and cost."
+  },
+  "nearest_open_prs": [
+    {
+      "pr": 2175,
+      "head": "1d943bc9e0718c8a2f15e1d0a22b73ad528ef0ca",
+      "state": "OPEN",
+      "mergeable": "MERGEABLE",
+      "scope": "UT4 z/uz mixed central/noncentral endpoint; different two-edge path target."
+    },
+    {
+      "pr": 1816,
+      "head": "fb67c06c36bf3a5be26ab43fc81418b4bc7e748e",
+      "state": "OPEN",
+      "mergeable": "MERGEABLE",
+      "scope": "Two central UT4 targets; different alphabet and endpoint."
+    },
+    {
+      "pr": 2103,
+      "head": "43d2d1b1392709ff50d81e0dbdb7a557f88e1427",
+      "state": "OPEN",
+      "mergeable": "MERGEABLE",
+      "scope": "UT5 four-role mixed-root target; different group and single height-two endpoint."
+    },
+    {
+      "pr": 2248,
+      "head": "835bd7b1877f56d6d9f4eecd7d1ee32f31593e1e",
+      "state": "OPEN",
+      "mergeable": "MERGEABLE",
+      "scope": "Q8 three-role targets; claim released, different group and endpoint."
+    }
+  ],
+  "nearby_claims": [
+    {
+      "reference": "Discussion #1167 comment #18936773",
+      "status": "active at snapshot",
+      "scope": "complex-mechanisms S3 convolution rank-nine block; different track and decoder object."
+    },
+    {
+      "reference": "Discussion #2243",
+      "status": "released to PR #2248 by 2026-10-15 02:06 UTC",
+      "scope": "Q8 three-role target minima; distinct group and target."
+    },
+    {
+      "reference": "Discussion #2242",
+      "status": "released to PR #2246 by 2026-10-15 01:55 UTC",
+      "scope": "A5 conjugate five-cycle pair; distinct group and target."
+    }
+  ],
+  "candidates_considered": [
+    {
+      "scope": "R439 helper-star replacement H2/K contract",
+      "decision": "not selected",
+      "reason": "Several predecessor notes and helper-star/dirty-cut studies cover this local word."
+    },
+    {
+      "scope": "Another UT3 central commutator or small GL3/S3 census",
+      "decision": "not selected",
+      "reason": "All-register UT3 bounds and multiple S3/GL3 finite studies or claims cover the obvious variations."
+    },
+    {
+      "scope": "Bipartite central commutator incidence graph H(m,n), K2,2 cycle",
+      "decision": "selected",
+      "reason": "The merged UT4 model is a three-label path with two root target classes; the cycle adds four distinct central edge targets and supports a graph-incidence theorem."
+    }
+  ],
+  "scope_distinction": "All finite bipartite edge sets with independent central z_ij target spaces, arbitrary nonnegative edge multiplicities and arbitrary dirty register count; exact rank-one unit tariff. The smallest new cyclic instance is K2,2.",
+  "selected_frontier_changed": false
+}

research/heisenberg-commutator-incidence-seedb054/PROOF.md

@@ -0,0 +1,128 @@
+# Bipartite commutator incidence tariff
+
+## Theorem
+
+Let `L` and `R` be finite index sets of sizes `m` and `n`, and let `E` be a
+bipartite edge set in `L × R`. For each edge `e=(i,j)`, choose a nonnegative integer multiplicity
+`p_e`, and put `P = sum_e p_e`. In the group algebra over `F2` of
+
+```text
+H(m,n) = { (u,v,Z) : u in F2^m, v in F2^n, Z in M_(m x n)(F2) }
+(u,v,Z)(u',v',Z') = (u+u', v+v', Z+Z'+u(v')^T),
+```
+
+write `x_i=(e_i,0,0)`, `y_j=(0,e_j,0)` and `z_ij=(0,0,E_ij)`. Thus
+`x_i y_j x_i y_j = z_ij`, and every `z_ij` is central. Let `r >= P`, assign
+disjoint sets `S_e` of `p_e` register coordinates, and let `P_e` be the
+diagonal projection onto `S_e`.
+
+The target is the diagonal matrix which has `[z_ij]` on the coordinates in
+`S_(i,j)` and the group-algebra identity on every other coordinate. A paid
+factor is
+
+```text
+D_N(g) = I_r + ([g]+[1]) N,
+g in {x_i : i in L} union {y_j : j in R},
+N in M_r(F2), rank(N)=1.
+```
+
+Arbitrary scalar `GL_r(F2)` maps may be interspersed for free, but the final
+target is expressed in the original coordinates. Each paid occurrence costs
+one. Every finite `r`, including arbitrary restored dirty spectators, has exact minimum
+
+```text
+4 P.
+```
+
+The smallest cyclic incidence instance is `K_(2,2)` with one target for each
+edge; it has four distinct central outputs and exact cost 16. The preceding
+UT4 shared-middle result has a two-edge path incidence pattern. This result
+extends that rank-nullity mechanism to arbitrary bipartite target graphs;
+`K_(2,2)` is its first cyclic case.
+
+## Attaining word and accounting
+
+For each edge `e=(i,j)` and each `t in S_e`, use the four factors
+
+```text
+D_(E_tt)(x_i) D_(E_tt)(y_j) D_(E_tt)(x_i) D_(E_tt)(y_j).
+```
+
+At coordinate `t` these multiply to `[x_i y_j x_i y_j]=[z_ij]` and act as
+identity at every other coordinate. Distinct diagonal supports do not
+interact. This gives exactly `4 p_e` paid calls on edge `e`, or `4P` total;
+every one of the four occurrences is charged. No scalar preparation, clean
+role, COPY, ERASE, or auxiliary operation is used.
+
+The call tariff is deliberately optimistic and complete only for this formal
+alphabet. It does not price a physical source/copy/frame/hosting/restoration/
+precision/interface implementation. Consequently it is not a selected
+supplier bill and supplies no `kappa` change.
+
+## Lower bound
+
+Free scalar `GL_r(F2)` maps may be normalized away. Push them through the paid
+factors by conjugation; a rank-one `N` remains rank one. Augmentation
+`[g] -> 1` sends every paid factor and the target to identity, so the
+remaining scalar map must itself be identity. It suffices to consider pure
+words in the displayed paid factors.
+
+Fix an active edge `(i,j)`. The map
+
+```text
+rho_ij(u,v,Z) = [[1, u_i, Z_ij], [0, 1, v_j], [0, 0, 1]]
+```
+
+is a group homomorphism to `UT3(F2)`: its top-right product term is exactly
+`u_i v'_j`. It sends `x_i` to `I+E12`, `y_j` to `I+E23`, all other listed
+generators to identity, and `z_kl` to `I+E13` exactly when `(k,l)=(i,j)`.
+The contragredient `rho_ij^vee(g)=(rho_ij(g)^(-1))^T` is also a homomorphism;
+it sends the same edge's central element to `I+E31`.
+
+Write each occurrence of a label `g` as `N_s=a_s b_s^T`. Let `X_g` have
+the `a_s` as columns and `Y_g` have the `b_s^T` as rows; their common inner
+dimension is the number `n_g` of occurrences of `g`.
+
+Under `rho_ij`, a factor labeled `x_i` contributes the block `E12 ⊗ N_s`,
+and a factor labeled `y_j` contributes `E23 ⊗ N_s`. Comparing the `(1,2)`
+block with the target forces `sum_(s:g_s=x_i) N_s=0`; similarly the `(2,3)`
+block forces `sum_(s:g_s=y_j) N_s=0`. For any active vertex one of its
+incident edges therefore gives
+
+```text
+X_g Y_g = 0,  rank(X_g) + rank(Y_g) <= n_g.             (1)
+```
+
+The `(1,3)` block of the natural representation is the ordered sum
+`sum_(s<t, g_s=x_i, g_t=y_j) N_s N_t`, which must equal `P_(i,j)`.
+Consequently `im(P_(i,j))` is contained in `im(X_(x_i))` and
+`row(P_(i,j))` is contained in `row(Y_(y_j))`. The `(3,1)` block in the
+contragredient representation gives the reverse ordered sum equal to the
+same `P_(i,j)`. Hence `im(P_(i,j))` is also contained in `im(X_(y_j))`, and
+its row space is contained in `row(Y_(x_i))`.
+
+More explicitly, for every left vertex `i`, the disjoint target coordinate
+sets on incident edges give
+
+```text
+rank(X_(x_i)) >= sum_(j:(i,j) in E) p_(i,j),
+rank(Y_(x_i)) >= sum_(j:(i,j) in E) p_(i,j).
+```
+
+For every right vertex `j` the analogous two inequalities hold with the
+column sum `sum_i p_(i,j)`. Equation (1) therefore implies
+
+```text
+n_(x_i) >= 2 sum_j p_(i,j),
+n_(y_j) >= 2 sum_i p_(i,j).
+```
+
+Summing over all label vertices counts every edge multiplicity once at each
+endpoint, so the number of paid factors is at least `2(2P)=4P`. Labels not
+incident to a target edge only add nonnegative calls. The explicit word
+attains the bound, proving exactness for every finite bipartite graph and all
+finite dirty register counts.
+
+The argument uses only necessary homomorphic images for its lower bound; the
+upper word is separately checked in the full formal group algebra. No
+finite-address test is used to infer the universal statement.

research/heisenberg-commutator-incidence-seedb054/README.md

@@ -0,0 +1,91 @@
+# Exact tariff for a bipartite commutator grid
+
+**Exact abstract construction and lower bound; no new `kappa`.** In the
+class-two group `H(m,n)` with generators `x_i` and `y_j`, let each selected
+edge `(i,j)` carry `p_ij` distinct dirty target roles for the central
+commutator `z_ij=x_i y_j x_i y_j`. Among paid factors
+`I+([g]+[1])N`, for the listed generators and arbitrary rank-one binary
+matrices `N`, the exact minimum is `4 Σ p_ij` for every finite number of
+dirty registers. The direct edgewise word attains this bill; the proof shows
+that no labels can be shared across the bipartite incidence pattern to reduce
+it. The first cyclic case `K2,2` has four distinct outputs and exact cost 16.
+
+The object extends the shared-middle rank-nullity pattern of the three-label
+UT4 path result to a complete bipartite commutator incidence model. One
+`UT3(F2)` quotient per active edge and its contragredient expose each edge
+target. For each generator, the disjoint
+incident target spaces force matching column and row span dimensions; one
+rank-nullity inequality per generator sums to `4 Σ p_ij`. The complete
+parameterized proof is in [PROOF.md](PROOF.md).
+
+## Cost and limits
+
+The local tariff counts every rank-one factor occurrence in the direct word.
+The model permits arbitrary free scalar
+`GL_r(F2)` mixing and normalizes it by augmentation; it has arbitrary dirty
+register inputs and no free address maps, clean roles, COPY, or ERASE. These
+are formal group-algebra calls only. Source access, physical frame changes,
+hosting, copying, restoration, precision, interfaces, supplier realization,
+and recursive-moment charges have no representation here. The exact local
+minimum is therefore not a supplier improvement or a selected-`kappa`
+change.
+
+The pinned research baseline returned `PASS_RESEARCH_BASELINE_BINDINGS_ONLY`
+and identifies the complex supplier as currently binding. That is a source
+binding/arithmetic check only; this package does not replay or modify the
+selected supplier.
+
+The verifier constructs the 256-element `H(2,2)` multiplication table,
+checks each of four edge quotients and its dual on all 256-squared group-pair
+inputs, verifies the
+16-call `K2,2` word in the full formal algebra, checks a weighted six-target
+instance, rejects each one-call omission, and rejects a changed edge label.
+It does not search for words: the all-finite-graph lower bound comes from the
+written quotient/rank-nullity proof.
+
+## Reproduce
+
+From repository root, using Python 3.12 and the standard library:
+
+```sh
+python3 scripts/research_package.py --package research/heisenberg-commutator-incidence-seedb054 --check-only
+python3.12 scripts/research_package.py --package research/heisenberg-commutator-incidence-seedb054
+```
+
+Direct local check, also using only the standard library:
+
+```sh
+python3 -I -B research/heisenberg-commutator-incidence-seedb054/verify.py
+```
+
+Expected result:
+
+```text
+PASS_HEISENBERG_BIPARTITE_COMMUTATOR group=256 edge_quotient_pairs=262144 K22_targets=4 calls=16 omission_controls=16 dirty_spectator=preserved weighted_targets=6 calls=24 wrong_label=rejected
+```
+
+The assigned base is `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. Exact
+predecessor file hashes and historical catalogue/selected provenance are in
+[SOURCES.json](SOURCES.json); the required replay inputs are declared in
+[VERIFY.json](VERIFY.json). The fresh complete overlap snapshot and nearby
+claims are in [OVERLAP.json](OVERLAP.json). The scope claim was posted at
+[Discussion #1167, comment #18938788](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18938788).
+
+## Open next questions
+
+Can one of these abstract central-commutator words be embedded in a concrete
+bit supplier with a complete favorable source, frame, copy, hosting,
+restoration, precision, and interface bill? A feasible first step is to map
+one `H(2,2)` label operation to a pinned supplier boundary and charge every
+role transition. The blocker is that no such implementation or recursive
+profile is supplied here.
+
+## Attribution
+
+The normalized register model and the preceding shared-middle UT4 tariff are
+credited to their cited authors and [merged UT4 mixed-root package](../ut4-mixed-root-tariffs/README.md).
+The new statement is the bipartite graph incidence tariff, with `K2,2` as its
+first cyclic case. Prepared by OpenAI Codex with substantial GPT-6 assistance
+in selection, derivation, exact implementation, verification, and writing;
+no independent human review or proof-kernel verification is claimed.
+Apache-2.0.

research/heisenberg-commutator-incidence-seedb054/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "e8870e5917057d59b730eb14721a778639eca050",
+      "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"
+    },
+    {
+      "path": "research/bit-three-register-lower-bound/README.md",
+      "usage": "input",
+      "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79",
+      "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd"
+    },
+    {
+      "path": "research/ut4-mixed-root-tariffs/PROOF.md",
+      "usage": "input",
+      "git_blob": "633a7d5137ad13fafe719cc042099977ad1f96e5",
+      "sha256": "c0def58338a69a57ac95f1d32a744993aa07656c46eba88a99354b276917bd8e"
+    },
+    {
+      "path": "research/ut4-mixed-root-tariffs/README.md",
+      "usage": "input",
+      "git_blob": "bf7625fd94664ed9945509b255e575fb1e01c30a",
+      "sha256": "4a66cf146138eaf0b9459c8c49e6fd08d485f12abfb7f288d9e18c14ef849be0"
+    }
+  ]
+}