From 6f43f8941fbe73ce411fa4698b8c0d96fb938e9e Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 21:25:38 -0500 Subject: [PATCH] Prove bipartite commutator incidence tariff --- .../OVERLAP.json | 90 +++++++ .../PROOF.md | 128 ++++++++++ .../README.md | 91 +++++++ .../SOURCES.json | 36 +++ .../TASK.json | 125 ++++++++++ .../VERIFY.json | 23 ++ .../verify.py | 227 ++++++++++++++++++ 7 files changed, 720 insertions(+) create mode 100644 research/heisenberg-commutator-incidence-seedb054/OVERLAP.json create mode 100644 research/heisenberg-commutator-incidence-seedb054/PROOF.md create mode 100644 research/heisenberg-commutator-incidence-seedb054/README.md create mode 100644 research/heisenberg-commutator-incidence-seedb054/SOURCES.json create mode 100644 research/heisenberg-commutator-incidence-seedb054/TASK.json create mode 100644 research/heisenberg-commutator-incidence-seedb054/VERIFY.json create mode 100644 research/heisenberg-commutator-incidence-seedb054/verify.py diff --git a/research/heisenberg-commutator-incidence-seedb054/OVERLAP.json b/research/heisenberg-commutator-incidence-seedb054/OVERLAP.json new file mode 100644 index 0000000000..05e2a541b8 --- /dev/null +++ b/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 +} diff --git a/research/heisenberg-commutator-incidence-seedb054/PROOF.md b/research/heisenberg-commutator-incidence-seedb054/PROOF.md new file mode 100644 index 0000000000..8cbd78b379 --- /dev/null +++ b/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= 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. diff --git a/research/heisenberg-commutator-incidence-seedb054/README.md b/research/heisenberg-commutator-incidence-seedb054/README.md new file mode 100644 index 0000000000..af9d60e661 --- /dev/null +++ b/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. diff --git a/research/heisenberg-commutator-incidence-seedb054/SOURCES.json b/research/heisenberg-commutator-incidence-seedb054/SOURCES.json new file mode 100644 index 0000000000..1cd7887095 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/heisenberg-commutator-incidence-seedb054/TASK.json b/research/heisenberg-commutator-incidence-seedb054/TASK.json new file mode 100644 index 0000000000..d4f0d81308 --- /dev/null +++ b/research/heisenberg-commutator-incidence-seedb054/TASK.json @@ -0,0 +1,125 @@ +{ + "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": "For every finite bipartite graph with edge multiplicities p_ij, in the formal F2[H(m,n)] register model with labels x_i,y_j and rank-one paid matrices, determine the exact minimum call count for the diagonal family of independently supported central commutators z_ij=x_i y_j x_i y_j. Claim: exactly 4 sum(p_ij), for every finite dirty register count. The concrete first cyclic case is K2,2 with four unit targets and exact cost 16.", + "scope_change_reason": "The chooser card is a generic new-register construction. Local and live overlap show extensive prior UT3/UT4 path, UT4 central, UT5 mixed-root, Q8 and A5 work. I changed the object to the bipartite commutator-incidence group H(m,n), whose K2,2 target has a cycle of four distinct central roots; the intended new content is the all-graph incidence lower bound and its attaining exact word.", + "bottleneck_link": "A sharp formal bit-call tariff is a structural input for future bit mechanisms. The selected conditional result is currently complex-bound; this abstract theorem has no supplier realization or immediate kappa effect.", + "budget_minutes": 60, + "stop_rule": "Prove the edgewise natural/contragredient quotient and rank-nullity bound for all finite bipartite graphs and multiplicities; exactly verify the K2,2 unit instance, one weighted instance, and declared corruption controls in the full formal algebra. Do not launch a word search or extend to other groups. Reserve the final quarter for verification, metadata, overlap refresh, and handoff.", + "outcome": "completed", + "evidence": "Written theorem gives n_x_i >= 2 sum_j p_ij and n_y_j >= 2 sum_i p_ij, hence at least 4P calls; edgewise four-call words attain 4P. The exact H(2,2) verifier checks all 262144 ordered group pairs under each of four quotient and dual homomorphisms, the full 16-call K2,2 word, a 24-call weighted six-target word, all 16 one-call omissions, and a wrong-label control.", + "author": "OpenAI Codex", + "ai_assistance": "Substantial OpenAI Codex GPT-6 assistance in scope selection, exact derivation, implementation, verification and writing; no independent human review or proof-kernel verification.", + "open_questions": [ + { + "question": "Can one of these abstract central-commutator words be embedded in a concrete bit supplier with a favorable complete paid profile?", + "why_it_matters": "Only a realized supplier boundary with all source, copy, frame, hosting, restoration, precision, interface and recursive charges can alter the selected conditional moment.", + "first_step": "Choose one H(2,2) label and map its action to a pinned concrete supplier boundary, preserving arbitrary dirty inputs and charging every role transition.", + "blocked_by": "This package contains no physical/compiler realization, hosted replay, or recursive profile for the formal labels." + } + ], + "assignment_seed": "b054c63f8969592c7c1608ddeee294e9", + "assignment_track": "bit-mechanisms", + "selector_scope_key": "7f5f4426ef796683c485", + "selector_method": "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "catalogue_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18938788", + "claim_correction_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18938817", + "predecessors": [ + { + "reference": "research/ut4-mixed-root-tariffs", + "status": "merged predecessor; three-label path with two noncentral root target classes" + }, + { + "reference": "PR #2175", + "head": "1d943bc9e0718c8a2f15e1d0a22b73ad528ef0ca", + "status": "open; UT4 z/uz mixed central/noncentral target tariff" + }, + { + "reference": "PR #1816", + "head": "fb67c06c36bf3a5be26ab43fc81418b4bc7e748e", + "status": "open; two central UT4 targets, every finite role count" + }, + { + "reference": "PR #2103", + "head": "43d2d1b1392709ff50d81e0dbdb7a557f88e1427", + "status": "open; UT5 four-role mixed-root target" + }, + { + "reference": "PR #2248", + "head": "835bd7b1877f56d6d9f4eecd7d1ee32f31593e1e", + "status": "open handoff checked live; Q8 three-role minima, distinct group/target" + }, + { + "reference": "Discussion #1167 comment #18936773", + "status": "active claim; complex-mechanisms S3 convolution rank-nine block, distinct object and track" + } + ], + "candidate_scopes": [ + { + "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; not a new construction scope." + }, + { + "scope": "Another UT3 central commutator or small GL3/S3 target census", + "decision": "not selected", + "reason": "All-register UT3 bounds, S3 short-layer work, and current adjacent claims/PRs already cover the obvious variants." + }, + { + "scope": "Bipartite central commutator incidence graph H(m,n), K2,2 cycle", + "decision": "selected", + "reason": "Four distinct central edge outputs form a cycle beyond the merged three-label UT4 path; exact edgewise quotient proof is not present in the refreshed overlap sources." + } + ], + "selector_note": "A preliminary chooser invocation accidentally ran from the preceding PR worktree and its assignment was discarded after detecting a base mismatch. This package pins the fresh accepted draw produced in the dedicated selector worktree at exact main base 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2.", + "baseline": { + "status": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "binding_primitive": "complex", + "selected_kappa": "836330098538459/500000000000000000", + "scope": "Selected source bindings and arithmetic only; not a supplier verification or full cold replay." + } +} diff --git a/research/heisenberg-commutator-incidence-seedb054/VERIFY.json b/research/heisenberg-commutator-incidence-seedb054/VERIFY.json new file mode 100644 index 0000000000..fe8ee54dbe --- /dev/null +++ b/research/heisenberg-commutator-incidence-seedb054/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md", + "research/ut4-mixed-root-tariffs/PROOF.md", + "research/ut4-mixed-root-tariffs/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Checks H(2,2) group law and all four edge quotient/contragredient homomorphisms on all 256 squared group pairs; verifies the full formal K2,2 direct word, a weighted six-target word, every one-call omission, and a wrong-label control." + } + ] +} diff --git a/research/heisenberg-commutator-incidence-seedb054/verify.py b/research/heisenberg-commutator-incidence-seedb054/verify.py new file mode 100644 index 0000000000..785ccb3479 --- /dev/null +++ b/research/heisenberg-commutator-incidence-seedb054/verify.py @@ -0,0 +1,227 @@ +#!/usr/bin/env python3 +"""Exact small-instance checks for the bipartite commutator tariff.""" + +from itertools import product + + +M = N = 2 +GROUP_SIZE = 1 << (M + N + M * N) +UNIT = 1 +ZERO = 0 + + +def split(g): + return g & 3, (g >> 2) & 3, (g >> 4) & 15 + + +def outer(u, v): + z = 0 + for i in range(2): + for j in range(2): + if ((u >> i) & 1) and ((v >> j) & 1): + z ^= 1 << (2 * i + j) + return z + + +def group_mul(g, h): + u, v, z = split(g) + u2, v2, z2 = split(h) + return (u ^ u2) | ((v ^ v2) << 2) | ((z ^ z2 ^ outer(u, v2)) << 4) + + +def basis(g): + return 1 << g + + +def ring_mul(a, b): + out = 0 + aa = a + while aa: + xa = aa & -aa + ga = xa.bit_length() - 1 + aa ^= xa + bb = b + while bb: + xb = bb & -bb + gb = xb.bit_length() - 1 + bb ^= xb + out ^= basis(group_mul(ga, gb)) + return out + + +def matrix_mul(a, b): + r = len(a) + out = [[ZERO for _ in range(r)] for _ in range(r)] + for i in range(r): + for k in range(r): + if a[i][k] == ZERO: + continue + for j in range(r): + if b[k][j] != ZERO: + out[i][j] ^= ring_mul(a[i][k], b[k][j]) + return out + + +def identity_matrix(r): + return [[UNIT if i == j else ZERO for j in range(r)] for i in range(r)] + + +def xgen(i): + return 1 << i + + +def ygen(j): + return 1 << (2 + j) + + +def zgen(i, j): + return 1 << (4 + 2 * i + j) + + +def rho(g, i, j): + u, v, z = split(g) + return ( + (1, (u >> i) & 1, (z >> (2 * i + j)) & 1), + (0, 1, (v >> j) & 1), + (0, 0, 1), + ) + + +def dual_rho(g, i, j): + u, v, z = split(g) + a = (u >> i) & 1 + b = (v >> j) & 1 + c = (z >> (2 * i + j)) & 1 + return ( + (1, 0, 0), + (a, 1, 0), + (c ^ (a & b), b, 1), + ) + + +def mat3_mul(a, b): + return tuple( + tuple(sum(a[i][k] * b[k][j] for k in range(3)) & 1 for j in range(3)) + for i in range(3) + ) + + +def target_matrix(multiplicities, r=None): + target_roles = sum(sum(row) for row in multiplicities) + if r is None: + r = target_roles + assert r >= target_roles + out = identity_matrix(r) + role = 0 + for i in range(2): + for j in range(2): + for _ in range(multiplicities[i][j]): + out[role][role] = basis(zgen(i, j)) + role += 1 + return out + + +def direct_word(multiplicities): + factors = [] + role = 0 + for i in range(2): + for j in range(2): + for _ in range(multiplicities[i][j]): + for g in (xgen(i), ygen(j), xgen(i), ygen(j)): + factors.append((g, role)) + role += 1 + return factors + + +def run_word(factors, r): + result = identity_matrix(r) + for g, role in factors: + factor = identity_matrix(r) + # D_{E_role,role}(g) has the basis element [g] in that diagonal slot. + factor[role][role] = basis(g) + result = matrix_mul(result, factor) + return result + + +def check_group_and_quotients(): + groups = range(GROUP_SIZE) + # The cocycle identity certifies associativity of the declared multiplication. + for u, u1, u2, v1, v2 in product(range(4), repeat=5): + left = outer(u, v1) ^ outer(u ^ u1, v2) + right = outer(u1, v2) ^ outer(u, v1 ^ v2) + assert left == right + + for g in groups: + u, v, z = split(g) + inv = u | (v << 2) | ((z ^ outer(u, v)) << 4) + assert group_mul(g, inv) == 0 + assert group_mul(inv, g) == 0 + for i, j in product(range(2), repeat=2): + central = zgen(i, j) + assert group_mul(g, central) == group_mul(central, g) + + assert len({zgen(i, j) for i, j in product(range(2), repeat=2)}) == 4 + for i, k in product(range(2), repeat=2): + assert group_mul(xgen(i), xgen(k)) == group_mul(xgen(k), xgen(i)) + for j, l in product(range(2), repeat=2): + assert group_mul(ygen(j), ygen(l)) == group_mul(ygen(l), ygen(j)) + + pairs_checked = 0 + for i, j in product(range(2), repeat=2): + for g in groups: + for h in groups: + gh = group_mul(g, h) + assert rho(gh, i, j) == mat3_mul(rho(g, i, j), rho(h, i, j)) + assert dual_rho(gh, i, j) == mat3_mul(dual_rho(g, i, j), dual_rho(h, i, j)) + pairs_checked += 1 + + for k, l in product(range(2), repeat=2): + expected = ((1, 0, 1), (0, 1, 0), (0, 0, 1)) if (i, j) == (k, l) else ((1, 0, 0), (0, 1, 0), (0, 0, 1)) + expected_dual = ((1, 0, 0), (0, 1, 0), (1, 0, 1)) if (i, j) == (k, l) else ((1, 0, 0), (0, 1, 0), (0, 0, 1)) + assert rho(zgen(k, l), i, j) == expected + assert dual_rho(zgen(k, l), i, j) == expected_dual + + for i, j in product(range(2), repeat=2): + x, y, z = xgen(i), ygen(j), zgen(i, j) + assert group_mul(group_mul(group_mul(x, y), x), y) == z + assert group_mul(x, x) == group_mul(y, y) == 0 + return pairs_checked + + +def main(): + pair_checks = check_group_and_quotients() + + grid = ((1, 1), (1, 1)) + factors = direct_word(grid) + target = target_matrix(grid) + assert len(factors) == 16 + assert run_word(factors, 4) == target + assert run_word(factors, 5) == target_matrix(grid, 5) + + omission_controls = 0 + for k in range(len(factors)): + shortened = factors[:k] + factors[k + 1 :] + assert run_word(shortened, 4) != target + omission_controls += 1 + + wrong = list(factors) + wrong[0] = (xgen(1), wrong[0][1]) + assert run_word(wrong, 4) != target + + weighted = ((2, 1), (0, 3)) + weighted_factors = direct_word(weighted) + weighted_r = sum(sum(row) for row in weighted) + assert len(weighted_factors) == 4 * weighted_r == 24 + assert run_word(weighted_factors, weighted_r + 2) == target_matrix(weighted, weighted_r + 2) + + print( + "PASS_HEISENBERG_BIPARTITE_COMMUTATOR " + f"group={GROUP_SIZE} edge_quotient_pairs={pair_checks} " + f"K22_targets=4 calls=16 omission_controls={omission_controls} " + "dirty_spectator=preserved weighted_targets=6 calls=24 " + "wrong_label=rejected" + ) + + +if __name__ == "__main__": + main()