Prove optimal spectator gathers with overlapping neighborhoods (no κ)

research/optimal-spectator-gather/PROOF.md

@@ -0,0 +1,152 @@
+# Optimal overlap-aware spectator gathers
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and result
+
+Partition a finite binary address into N neighborhoods of K coordinates each.
+All neighborhoods use the same offset convention. Let A and B be sets of h
+neighborhoods, with c=|A intersection B|. Write S and T for their full sets of
+hK binary coordinates. The input is the complete binary rectangle, with arbitrary
+payloads, preceding fibers and arbitrary correlations between all coordinates.
+
+The completed operator on each active neighborhood is the same operator U.
+The assignment of source neighborhoods to target neighborhoods is free, while
+all K offsets within each neighborhood must be preserved. This is appropriate
+for the common completed kernels in zxv's PR6070 global-H interface. It is a
+changed assignment policy, not a new proof of its router or callee.
+
+**Theorem.** There is a gather P sending S to T that moves exactly
+
+    2K(h-c) binary coordinate positions
+
+and is a product of exactly
+
+    h-c whole-neighborhood swaps = K(h-c) binary-coordinate swaps.
+
+Both counts are minimum, simultaneously. The binary-coordinate lower bounds
+hold even if a competing coordinate permutation is allowed to split or reorder
+neighborhoods, provided it still sends the complete set S onto T.
+
+The theorem is an exact optimum in a coordinate-permutation model. A
+coordinate swap is one transposition of two binary address positions. It is
+not a claim about a minimum CNOT count, adjacent tape movements, arbitrary
+linear charts, native recursive children or a complete physical invoice.
+
+## Construction and lower bound
+
+Put L=A minus B and E=B minus A. They have the same cardinality m=h-c.
+Choose any bijection f:L to E. Exchange neighborhood a with neighborhood f(a),
+offset by offset, for each a in L. Fix every other coordinate.
+
+These exchanges have disjoint endpoints. They map A onto B, fix A intersection B
+pointwise, fix every coordinate outside their symmetric difference and form an
+involution. They move 2Km positions and use Km disjoint coordinate transpositions.
+The deterministic implementation pairs the two sorted difference lists.
+
+Let sigma be any coordinate permutation with sigma(S)=T. Every coordinate of
+S minus T must move: fixing one would leave a coordinate outside T in sigma(S).
+Every coordinate of T minus S must also move: if fixed, its unique preimage
+would lie outside S. Thus at least |S symmetric-difference T|=2Km positions move.
+
+The support of a word of l coordinate transpositions is contained in their
+2l endpoints. Consequently l>=Km. The construction attains both lower bounds.
+The same endpoint argument on neighborhood indices proves the m-swap lower
+bound when each instruction exchanges two complete neighborhoods. This proof
+works for every finite N,K,h and every overlap, including A=B, when no routing
+is needed. The executable API requires h>=1; the empty case is trivial.
+
+The use of disjoint transpositions and elementary support counting is standard.
+The new contribution is the optimal assignment at this spectator gather
+boundary, its executable constructor and its exact before/after application.
+The original sparse-extension theorem already allows arbitrary bijections.
+Its general extension and support-routing cost are not claimed again here.
+
+## Arbitrary-input operator boundary
+
+For any common linear operator U on one K-bit neighborhood, let U_A be the
+product of its copies on A. Disjoint copies commute. Because P preserves every
+neighborhood's offsets and sends A bijectively onto B,
+
+    P inverse * U_B * P = U_A.
+
+One can check this on basis tensors and extend linearly. It holds on all
+payloads, including correlated dirty spectator data. No separability of the
+actual input or zero workspace is assumed. P inverse=P, so the exact same
+finite swap word restores the layout.
+
+The hypothesis that the kernels are identical matters. Distinguishable jobs
+must follow their own assignment constraints; a shared neighborhood may then
+have to move. Offsets matter too: the implementation preserves them even for
+an operator that treats different offsets differently. The finite checks use
+both exact phase-sensitive Gaussian columns and a nonsymmetric, nonseparable
+four-entry neighborhood operator.
+
+## The spectator-row wrapper
+
+Retain PR6070's row, front, active and back field capacities and its complete
+nested stock Q. Suppose the source neighborhoods are aligned to the same K-bit
+grid as the target active slots. Replace only its ordered exposure permutation
+by P above. The active target slots and every field capacity are unchanged.
+
+Every source coordinate maps into T. Therefore every preimage of a physical
+position outside T is a genuine source spectator. This includes the complete
+row prefix and compact controls, even if they originally intersect S. The
+original wrapper's one whole-row padding and its row-independent completed
+callee can consequently be used with the same declared contracts.
+
+On a completed exact return, restrict to the original rows, then apply P again.
+The result is U_A. For surrounding coarse-dependent diagonals D1,D2, the result
+is exactly D2 U_A D1. The second diagonal must still wait for padding removal
+and inverse exposure. This proof does not assume that a diagonal commutes with
+exposure or with internal row mixing.
+
+This is a local replacement implication under PR6070's stated completed-callee,
+paid-router, ownership, precision, padding-disposal and tape hypotheses. It
+does not discharge those hypotheses or any selected framework assumption.
+No predecessor scientific replay is needed or claimed for this implication.
+
+Under the retained support-router theorem, substitute k=2K(h-c) in its cost
+
+    O(V (k+1)^(1-a_BIT) polylog(p) + poly(p)).
+
+When c=0 this equals the previous 2Kh upper bound. When overlap is present it
+can be smaller. The ordered construction can also already be optimal on some
+inputs; no strict gain is claimed for every gather. When c=h the exposure is
+identity and its routing can be omitted. No asymptotic exponent improvement
+or fully priced supplier gain follows from these local counts alone.
+
+## A strict before/after example
+
+In the PR6070 layout take h=3, Q=3, G>=1 and K=128G. The row, front and back
+widths are all K. The target block indices are B={2,3,4}; choose A={0,2,3}.
+Enough trailing spectator capacity is retained.
+
+The ordered gather maps 0 to 2, 2 to 3, 3 to 4 and closes with 4 to 0. At each
+of the K offsets it is a four-cycle. Hence it moves 4K coordinates and its
+shortest coordinate-transposition word has length 3K. The usual cycle-count
+lower bound follows because a transposition changes the number of cycles by
+at most one; each four-cycle can be built with three transpositions.
+
+The new gather simply exchanges blocks 0 and 4. It moves 2K coordinates and
+uses K coordinate transpositions, both optimal by the theorem. Blocks 2 and 3
+stay fixed. The original row block 0 receives the old block 4, which is a
+source spectator. All three original kernel jobs are still delivered.
+
+The verifier constructs and enumerates both actual sparse permutations.
+An encoded fixture has log2(p)=32, G=134, K=17152 and enough ambient reservoir
+and suffix capacity. Its counts are 68608 to 34304 moved coordinates and
+51456 to 17152 coordinate swaps. It is an encoded geometry, not an exported
+production caller or execution of its enormous tensor. Small exact complete
+row fixtures separately execute padding, dirty internal row cycling, return,
+inverse exposure and both surrounding diagonals.
+
+## Verification boundaries
+
+The all-parameter theorem is the written proof above. Exhaustive enumeration
+through seven neighborhood positions independently minimizes over every
+permutation, including permutations moving unrelated spectators. The exact
+operator checks corroborate the new implementation and boundary. They do not
+formally prove the universal result or accept the inherited multiplication
+framework. Unaligned source neighborhoods, different active operators, physical
+router lowering and actual production-call installation remain open.

research/optimal-spectator-gather/README.md

@@ -0,0 +1,111 @@
+# Optimal overlap-aware spectator gathers
+
+A freely assigned gather for identical, aligned K-bit kernels needs exactly
+`2K(h-c)` moved coordinates and `K(h-c)` binary-coordinate swaps, where h
+neighborhoods are active and c source neighborhoods already coincide with target
+neighborhoods. The constructor fixes the overlap and exchanges the two difference
+sets. Both counts are proved optimal, even against arbitrary coordinate
+permutations sending the full source set onto the target set.
+
+This contribution was produced by Nick Petalas. Claim type: scoped proof with
+finite exact corroboration. No new kappa or completed supplier is claimed.
+
+The new assignment improves one routing step of zxv's
+[PR6070 spectator-row wrapper](https://github.com/CrocSwap/integer-mult-bounds/pull/6070).
+Its ordered assignment can move shared neighborhoods unnecessarily. In the
+explicit h=3, Q=3, K=128G layout, moved support falls from 4K to 2K and the
+shortest coordinate-swap word from 3K to K. The same complete active slots,
+stock, dirty-input operator and inverse-restoration boundary are retained.
+[PROOF.md](PROOF.md) states the exact changed contract and optimality argument.
+
+`gather.py` constructs the new involution. `verify.py` enumerates a separate
+permutation oracle and interprets complete exact operators. It imports no
+predecessor verifier and does not rerun or audit the source theorem.
+
+## Evidence
+
+The normal local checker passes:
+
+- 5,913 permutations and 695,482 subset images, covering all 4,706 equal-size
+  source/target-set pairs through seven neighborhood positions;
+- 3,878 complete exact Gaussian basis columns, including both offsets of
+  two-bit neighborhoods, and 93 nonsymmetric whole-neighborhood fixtures;
+- three complete spectator-row fixtures with arbitrary dirty payloads,
+  whole-row padding, internal row cycling, inverse exposure and surrounding
+  coarse-dependent diagonals;
+- one encoded layout with K=17152, reducing moved support 68608 to 34304 and
+  shortest coordinate swaps 51456 to 17152;
+- 13 malformed-input/capacity rejections and two semantic scope controls.
+
+Every reported count is generated by the checker. Its JSON output also binds
+all package files by SHA256. There is no hand-authored mathematical receipt.
+[VALIDATION.md](VALIDATION.md) records verification and implementation limits.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/optimal-spectator-gather/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/optimal-spectator-gather/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/optimal-spectator-gather
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/optimal-spectator-gather --check-source-history --check-modes
+```
+
+Any CPython 3.12 path can replace the local path. Expected scientific status:
+`PASS_OPTIMAL_SPECTATOR_GATHER`. The registered runner and publication preflight
+have their own separate PASS markers.
+
+## Scope and limitations
+
+This is a local routing construction and exact optimum. It permits a changed
+assignment among identical completed kernels. A fixed ordered assignment,
+unaligned neighborhoods, distinguishable operators, CNOT counts, adjacent tape
+movements and arbitrary linear encoders are different optimization problems.
+The executable planner has explicit finite resource caps; the proof has no
+size cap. Literal vector execution is limited to 16 address bits.
+
+The source's paid support-router theorem can use the smaller moved support.
+A complete physical invoice, actual global-H production event, supplier,
+rounded-callee/padding-disposal proof, native/compiler closure and outer
+multiplication theorem remain unimplemented. All five selected assumptions
+remain. The selected conditional kappa stays .003125804. No full selected cold
+replay, Lean, Docker, independent human or formal proof-kernel review is claimed.
+
+## Open next questions
+
+1. Export one literal global-H call whose source and target neighborhoods share
+   a K-grid. Count their overlap and lower this exact gather through the paid
+   support router. Actual physical layout, complete stock and callee return
+   evidence are prerequisites; these fixtures are not that installation.
+2. For unaligned complete neighborhoods, determine an exact offset-preserving
+   assignment and completion objective. Start with two overlapping grids and
+   state which chunk boundaries the physical callee requires. The present
+   aligned proof must not be transferred without that contract.
+
+## Related open work
+
+No open PR specifically optimizing the moved-coordinate support of this
+aligned spectator gather was identified in the live open-title/body and
+main/merged searches. PR6070 is a merged cited predecessor. Search caps,
+sparse local notes and unpublished work limit that coverage. No additional
+computation was run to check another contributor's mathematical result.
+
+## Credit and provenance
+
+Credit zxv's PR6070 for the spectator placement, row-independent completed-call
+contract and installation question. The arbitrary S-union-T extension and paid
+support-router theorem are retained predecessor work, including Vlado
+Vojdanovski's PR1673, Jeremy Kothe's PR1758, Chafik Boukhalfa's PR1786 and their
+compact-layout/support-audit lineage. Retain PR4359's stock and precision
+framework and the selected P104/helper/native/compiler contributors. Elementary
+permutation support and cycle facts are standard background. This package
+claims the optimal assignment at this boundary and its constructor/application,
+not a new general theory of permutations or a predecessor supplier result.
+
+Canonical base is a5bff3bf133e482541c09eba4e773884bdb2b1b7, priority revision 8.
+SOURCES.json pins the retained source bytes as provenance. They are not imported
+by the new verifier. The card is explicitly changed to this local constructive
+step; it does not discharge an inherited assumption at a production caller.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19272318)
+sets this same scope. Apache-2.0.

research/optimal-spectator-gather/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/spectator-row-reservoir/README.md",
+      "usage": "provenance",
+      "git_blob": "5af75bdb7fd55ba8a810ff9e035d50dcdbcd06a1",
+      "sha256": "408e3ef76487a7dc43832d73bfb5b9fcc33c8cafd4e9078f40dc3f0887090a59"
+    },
+    {
+      "path": "research/spectator-row-reservoir/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "000c4e5ddf1446b11ee15679bf4238bec77760c8",
+      "sha256": "a895844a13bd747dccd64eb260dc30a0e7bb77cb66269f82ef5f5aeda2d9c782"
+    },
+    {
+      "path": "research/spectator-row-reservoir/verify.py",
+      "usage": "provenance",
+      "git_blob": "a5e05c3856779c8469d178b1210090553243b9cd",
+      "sha256": "0e15cea067c77b1653822359cb06680581ac1ba3d9f87474bc8da11f5f71f7e9"
+    },
+    {
+      "path": "research/kappa-observation-integration/release-work/current/package/vendor/pr1673/capped-phase-fusion/SUPPORT-ROUTER.md",
+      "usage": "provenance",
+      "git_blob": "4f39fa9eaf553d1df5111de8c19bcf5bf9829c2b",
+      "sha256": "6ddb322e11883c1177ba6cd1a77d23a1dac827d7290b32eaf642457b1d762a54"
+    }
+  ]
+}