Scoped negative result: rank-two obstruction for 78 CK cleanup pairs

research/complex-ck-cleanup-fusion/CLAIM.md

@@ -0,0 +1,37 @@
+# Sprint claim
+
+- Track: complex supplier. OS assignment seed: 20.
+- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`.
+- Start: 2026-10-13 04:26:40 UTC. Expected finish: 05:16:40 UTC.
+- Object: the selected #626 CK provider's full-frame scalar cleanup.
+- Hypothesis: same-source, same-target additions separated only by commuting
+  operations can be combined at their later position without changing the
+  complete dirty-input map or increasing the absolute prefix envelope.
+- Method: exhaust the pair domain in this one cleanup word, then apply a
+  deterministic fixed-point fusion pass and exactly replay both orientations.
+  Seed 20 selects CK by parity. Full-frame cleanup is selected after excluding
+  the already-claimed factory and B-frame tasks.
+- Deliverable: exact local circuit evidence, a reproducible checker, source pins,
+  negative controls, and a scoped result. No new kappa is assumed.
+- Candidates considered: raw factory resynthesis, selected B-frame reassignment,
+  and cleanup fusion. #681 and #698 cover the first two. #696 lowers individual
+  unchanged macros; this experiment changes the cleanup macro word. #687 changes
+  a raw K-triangle read order. No pending result is a dependency.
+- Coordination: GitHub's pinned-issue query returned an empty list. No separate
+  issue was opened. Open PRs were inspected through #700 before this local claim.
+- Scope: only this research package. Keep upstream, accepted supplier sources,
+  selected certificates, ownership, frame paths, and recursive profiles unchanged.
+- Substantial OpenAI Codex assistance is used for research, code, and writing.
+
+Status: completed, 2026-10-13 04:44 UTC. The initial commuting search found no
+candidate among all 78 pairs. One refinement computed the complete conjugated
+shear: every pair has a certified rank-two defect in both orientations. No
+single rank-one replacement can work anywhere among the unchanged middle gates
+on arbitrary register inputs. This is a scoped negative result, with no kappa
+claim and no fixed-point optimization run.
+
+Result: [research note](README.md), [exact certificate](CERTIFICATE.json), and
+[review branch](https://github.com/thakrarsagar/integer-mult-bounds/tree/research/complex-ck-cleanup-fusion/research/complex-ck-cleanup-fusion).
+Reproduce with `python3 -B research/complex-ck-cleanup-fusion/verify.py`.
+Expected: `PASS_CK_CLEANUP_RANK_TWO pairs=78 rank=2 columns=312 controls=8`.
+The final verification and overlap record is in [VALIDATION.md](VALIDATION.md).

research/complex-ck-cleanup-fusion/README.md

@@ -0,0 +1,205 @@
+# Rank-two obstruction to CK cleanup pair fusion
+
+**Status: scoped negative result. No new supplier or kappa.**
+
+The selected #626 CK provider has 8,309 full-frame cleanup operations,
+including 8,186 additions and 123 nonzero scalings. Exactly 78 pairs of additions
+have the same ordered target and source registers. For every such pair, removing
+the two endpoints while retaining the intervening word creates a defect of rank
+two. Consequently, **no single addition, scaling, or other rank-one update can
+replace the pair at any position among the unchanged intervening gates**.
+
+This is a statement about the complete rational map on arbitrary register inputs.
+It allows any coefficient and any target/source for the proposed replacement.
+It does not rule out changing intermediate gates, using multiple replacement
+gates, exploiting restricted inputs, or resynthesizing a larger circuit.
+
+## Reproduce
+
+From the repository root, with Python 3.11 or later:
+
+```sh
+python3 -B research/complex-ck-cleanup-fusion/verify.py
+```
+
+Expected:
+
+```text
+PASS_CK_CLEANUP_RANK_TWO pairs=78 rank=2 columns=312 controls=8
+```
+
+The command needs only the standard library and committed files. It performs
+no network access or file writes. It checks source pins, the binding to the
+selected CK specification, every cleanup register's full-frame boundary,
+complete pair coverage, all 156 forward/dual witnesses, and the committed
+certificate. Checks stay enabled with `python3 -O`.
+
+`verify.py` is the authoritative entry point for source pins and all certificate
+metadata. `check_columns.py` also runs separately, without checking those pins.
+It checks all 624 minor entries by
+replaying 312 basis columns. This is an independent arithmetic implementation,
+not an independent human review. It uses dense vectors and literal inverse
+and forward scalar operations; it imports no code from the sparse conjugation
+checker. The main command additionally checks the recorded support sizes and
+conjugation factors. Neither implementation replays all 716 columns of the
+complete supplier. Two columns suffice for each nonzero minor.
+
+## Exact finite statement
+
+Use column vectors and let an addition be
+`A(t,s,a) = I + a e_t e_s^T`, with `t != s` and `a != 0`.
+For a repeated pair at cleanup indices `i < j`, put
+
+```text
+E = e_t e_s^T
+M = the product of cleanup gates strictly between i and j
+P = (I + b E) M (I + a E)
+u = M e_t
+v^T = e_s^T M^-1
+D = P M^-1 - I
+  = a (u + b e_t u_s) v^T + b e_t e_s^T.
+```
+
+Every middle gate is invertible. All additions have distinct registers, and all
+scalings have a nonzero coefficient. Thus the inverse used here exists.
+
+Choose `r != t` with `u_r != 0` and `c != s` with `v_c != 0`. The determinant
+of the minor of `D` on ordered rows `[t,r]` and columns `[s,c]` is
+
+```text
+det D[[t,r],[s,c]] = a b u_r v_c != 0.
+```
+
+The expression for `D` is a sum of two rank-one matrices, so its rank is
+exactly two. Such `r,c` exist for every one of the 78 pairs. The certificate
+records the four minor entries, their determinant, the two exterior factors,
+and the support sizes. These are rational identities and remain nonzero over
+the complex numbers.
+
+For a proposed insertion position, split the unchanged middle word as `M=Y X`.
+A replacement `R` would have to satisfy `P=Y R X`, hence
+
+```text
+R - I = Y^-1 (P - M) X^-1.
+```
+
+Multiplying by invertible matrices preserves rank. Therefore `rank(R-I)=2` at
+every insertion position. A single addition or scaling has `rank(R-I) <= 1`,
+so it cannot work. This also excludes arbitrary rank-one updates, which are
+more permissive than the supplier's actual scalar gate set.
+
+The backward orientation replaces each chronological gate by its inverse
+transpose, keeping the gate order. The checker recomputes the witnesses in that
+orientation rather than assuming the forward minors also work. Independently,
+`P^-T - M^-T = P^-T (M-P)^T M^-T` shows that the defect rank is preserved.
+
+For example, pair `[17,24]` consists of additions from register 236 to register
+230 with coefficients `-2` and `1`. The forward minor on rows `[230,231]` and
+columns `[236,230]` is
+
+```text
+[-1   1]
+[ 2  -1]
+```
+
+Its determinant is `-1`. The corresponding dual minor also has determinant
+`-1`. All indices are zero-based within the pinned cleanup list.
+
+## Experiment and coverage
+
+OS randomness produced assignment seed **20**, selecting the complex-supplier
+track and, by parity, CK rather than JP8. The three candidate tasks were factory
+resynthesis, B-frame reassignment, and cleanup pair fusion. Concurrent #681 and
+#698 already cover the first two, so this experiment uses the cleanup circuit.
+
+The initial test allowed moving an addition across individually commuting gates
+to merge it with another addition on the same ordered registers. All 78 pairs
+have blockers. That failed search alone says nothing about collective
+cancellation within the middle word. The one refinement was to compute the
+complete conjugated shear and an exact rank minor. It proves the stronger
+fixed-middle obstruction above, including middle words whose individual gates
+do not commute with the endpoint.
+
+The completed domain consists of **every pair of distinct additions with the
+same ordered target and source in this one cleanup word**, with both
+orientations checked. Pair generation stops after exhausting the list. There
+is no sampling, timeout, or random search beyond the assignment choice. No
+fixed-point fusion pass is needed because no first fusion in this class exists.
+Pairs with different endpoint registers are outside this domain.
+
+Even granting a replacement arbitrary coefficients, an arbitrary rank-one map,
+and free placement/source access does not overcome the rank defect. No proposed
+circuit reaches the cost-accounting stage. Frame changes, wrappers, restoration,
+recursive children, ownership, and the selected bit supplier therefore retain
+their original costs. Cleanup arithmetic simplification alone would not change
+the recursive rank histogram in any case.
+
+## Controls
+
+Five semantic controls check the distinction between a blocker and a proof:
+
+- A commuting middle addition permits a rank-one combined update.
+- A noncommuting source scaling by two still permits a combined coefficient
+  `3/2`; it must not be classified as a rank-two obstruction.
+- A reverse-direction middle addition has the exact minor determinant `-1`.
+- Opposite endpoint coefficients around that middle addition do not cancel.
+- Two inverse middle additions cancel collectively and permit fusion, despite
+  each being an individual commutation blocker.
+
+The direct-column checker also rejects three altered certificates: a changed
+minor entry, a flipped dual endpoint coefficient, and an omitted pair. A
+recomputed certificate must match every field of the committed evidence.
+
+## Provenance, relation to other work, and limits
+
+Base commit: `66849e1475c930fd7732b1a0067ffee7e1e95f60`.
+The accepted result at this base is conditional
+`kappa=51110230636731/31250000000000000`, from #626 with #543.
+The actual construction and scope are identified by
+[the selected record](../../certificates/selected-result.json) and
+[the maintainer review](../../docs/research/community-k492-review.md).
+[SOURCES.json](SOURCES.json) records exact dependency heads and file hashes.
+The compressed word is bound by its decompressed-payload hash, so gzip metadata
+and compression versions do not affect equality.
+
+Credit belongs to Jeremy Kothe's #622 K-triangle construction, Chafik Boukhalfa's
+#626 selected owner package, DreamingOfClouds' cold-helper and native-verifier
+work, icekylinx's scalar factory/direct-delivery lineage, Dugongue's coordinate
+and rank-sector work, eumemic's retained #543 bit supplier, and the predecessors
+credited in the selected review. The original source files and notices remain
+unchanged.
+
+Related pending work is credited without treating its titles as accepted results:
+
+- Evan McKinney's [#271](https://github.com/CrocSwap/integer-mult-bounds/pull/271)
+  simplifies bit cleanup sandwiches and changes helper endpoints. Its field,
+  circuit, and allowed rewrite differ from this fixed complex cleanup test.
+- eumemic's [#411](https://github.com/CrocSwap/integer-mult-bounds/pull/411)
+  resynthesizes complex target prefixes and recomputes dirty responses.
+- [#681](https://github.com/CrocSwap/integer-mult-bounds/pull/681) resynthesizes an
+  eight-register raw factory window. This does not contradict the narrower
+  two-endpoint, unchanged-middle obstruction.
+- [#687](https://github.com/CrocSwap/integer-mult-bounds/pull/687) examines raw
+  K-triangle read relocation; [#698](https://github.com/CrocSwap/integer-mult-bounds/pull/698)
+  optimizes B frames at fixed gate order; [#696](https://github.com/CrocSwap/integer-mult-bounds/pull/696)
+  lowers the primitives implementing unchanged complex macros.
+- Concurrent [#710](https://github.com/CrocSwap/integer-mult-bounds/pull/710),
+  prepared for Sagar Thakrar with Codex assistance, uses exact conjugation to
+  shorten the bit supplier's R420 cleanup. It was discovered during the final
+  overlap refresh. Its joint two-sandwich rewrite over F2 changes five gates
+  to three; this rational CK census excludes only two endpoints becoming one
+  update with their middle fixed. The two results are compatible.
+
+None of those pending packages is imported or needed to reproduce this result.
+The accepted providers, `upstream/`, selected frontier, and global accounting
+are unchanged. No optimality claim is made for CK, JP8, the whole cleanup word,
+or broader circuit synthesis. All-size compilation, common-label and
+mutable-basis realization, hosting, residual, precision/tape, recovery, and
+analytic-transfer assumptions of the selected construction remain inherited.
+This finite certificate and written rank argument are not a Lean proof or a
+verification of the complete multiplication theorem.
+
+Prepared for **@thakrarsagar**, with substantial **OpenAI Codex assistance** in
+research, code, mathematical analysis, verification, and writing. A second Codex
+agent supplied the independent column implementation and reviewed the rank
+argument. New material is under the repository's [Apache-2.0 license](../../LICENSE).

research/complex-ck-cleanup-fusion/SOURCES.json

@@ -0,0 +1,13 @@
+{
+  "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60",
+  "selected_pr626_head": "660de893d27bb7abd1d5b01b1640207528a5c851",
+  "reviewed_pr622_head": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6",
+  "retained_pr543_head": "2065fe4f72a914d907f1046603f5a36f17018535",
+  "files": {
+    "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53",
+    "research/complex-k492-owner-repair/data/SPEC.json": "2a2577ac526535826fed9d5f7f83f6e2e0ec058a146c64f7286720b995fa2323",
+    "research/complex-k492-owner-repair/code/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805",
+    "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz": "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7"
+  },
+  "hash_convention": "SHA256 of exact file bytes; for .gz, SHA256 of the decompressed payload."
+}

research/complex-ck-cleanup-fusion/VALIDATION.md

@@ -0,0 +1,61 @@
+# Validation receipt
+
+Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`.
+Local environment: macOS 26.5.2 arm64; Python 3.14.8 and Python 3.11.15.
+Verification started at approximately 2026-10-13 04:39 UTC, after the completed
+bounded experiment and before submission. The original maximum work budget
+was 50 minutes, with completion permitted earlier.
+
+Passed:
+
+- `python3 -B research/complex-ck-cleanup-fusion/verify.py`.
+- `python3 -O -B research/complex-ck-cleanup-fusion/verify.py`, with all checks
+  still active. Both print `PASS_CK_CLEANUP_RANK_TWO pairs=78 rank=2 columns=312 controls=8`.
+- Independent direct-column checker, including optimized Python execution:
+  78 pairs, both orientations, 312 columns, 624 exact minor entries.
+- Python 3.11.15 optimized replay from a minimal temporary checkout containing
+  only this package and the four pinned inputs, at a path containing spaces,
+  invoked while the working directory was `/`.
+- Recompressing the input with gzip level 1 and a different timestamp preserves
+  acceptance. Changing the decompressed input, supplier SPEC bytes, or certificate
+  support metadata causes rejection in the temporary checkout.
+- `make selected-record-check` passes with the unchanged accepted rational kappa,
+  source inventory, and proof-supplement checks.
+- Staged whitespace checks and local documentation links pass. The diff contains
+  only this package; upstream main still has the recorded base commit.
+
+The package's five semantic controls and three certificate-mutation controls run
+on every normal invocation. They distinguish individual commutation blockers
+from complete-middle rank obstructions and detect bad minor entries, dual signs,
+and coverage. Two additional Codex workers reviewed the same narrowly claimed
+scope. One supplied the independent arithmetic implementation; another reported
+no mathematical or code blocker for the full-register-space statement. This is
+AI-assisted review, not independent human review.
+
+The full repository `make verify`, selected cold supplier regeneration,
+global invoice/assembly replay, Lean, and remote Linux CI were not run for this
+isolated research addition. No selected construction, generator, production
+verifier, or source input changes. The result does not claim a faster
+implementation, smaller recursive moment, or larger kappa.
+
+Final overlap review inspected 531 open PRs through #712 and refreshed the pinned
+issue query, which remained empty. In particular, #710's new bit-cleanup
+conjugation construction is credited in the README and does not establish the
+CK rank-two census. #705 concerns determinant obstructions for Clifford register
+paths and is a different search class. Exact inspected heads for related work:
+
+| PR | Head |
+| --- | --- |
+| #271 | `ebc1defe8c13f39f86e5901c3437c1be52886a2b` |
+| #411 | `f58d95f2c5da03445e704ea9c72cc55df9e68190` |
+| #681 | `80d4edbc2d53f058787cb5c43bd0fc22c7e7fdff` |
+| #687 | `82bbb9c3ac34540f196410d137ebc59d9c2c43a9` |
+| #696 | `5a3f983715027c4fd83f50bc9001d4b18463bed1` |
+| #698 | `ab78f797cffcbeddbb17a7eb069741085ffe3351` |
+| #705 | `eeb0cd605415a73b792915aaa9185000f293c84a` |
+| #710 | `d97c8d20a8b885271a24c5a4e8446ac7f5697d5c` |
+
+An immediate pre-submission refresh covered 535 open PRs through #716.
+#713/#716 concern R420 target-basis compensation; #714 concerns clean product-shear
+checkpoints; #715 concerns mixed E8 ports. None studies this fixed CK cleanup
+pair domain.