Review the common-map tensor-pairing bound independently.

research/tensor-pairing-common-map-review/README.md

@@ -0,0 +1,118 @@
+# Independent review of the common-map tensor-pairing bound
+
+**Audit confirmation. No new decoder, supplier or kappa.** Selected conditional
+kappa stays `0.001672660197076918`.
+
+This package re-derives the argument in sections 2–5 of
+[PR #3928](https://github.com/CrocSwap/integer-mult-bounds/pull/3928), head
+`2b2daaecac95e1048923d22fda51ccd01780565f`, the review requested by
+[discussion comment 19030180](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19030180).
+It does not import that pull request's code. The claim under review stands:
+no counterexample turned up.
+
+## What was checked
+
+Let `G0 = [[2, 1], [1, 2]]` and `G4 = G0` tensored with itself four times,
+indexed by 4-bit words. Then `G4[i, j] = 2^(4 - d(i, j))`. The pairing
+`B[i, j] = (G4[i, j] + 1) mod 2` is 0 exactly on the complement `j = i xor 15`,
+and 1 elsewhere, including the diagonal.
+
+Over `F2`, `B` squares to the identity. Both scanners multiply the 16 by 16
+matrix; the primary also row-reduces it. The rank is 16. A bilinear pairing of
+9-bit labels has matrix rank at most 9, for any source map, reader map and
+bilinear form. The full sixteen-point pairing therefore does not embed in the
+nine-bit alphabet.
+
+For a principal set `S`, write `p` for the number of included complement pairs
+and `s` for the number of singletons. The primary scanner checks all 65,536
+subsets. The rank is `2p` when `s = 0` and `2p + 1` when `s > 0`. The largest
+set with rank at most 9 has size 12.
+
+A common injective map into norm-2 E8 root lines is stricter. Distinct lines
+have doubled inner products in `{-4, 0, 4}`; the scanner checks every pair
+among the 120 lines. Pairing 1 forces orthogonality and pairing 0 forces inner
+product `±1`. The complement relation is a matching, so the real Gram matrix
+is block diagonal with blocks `[2]` and `[[2, ε], [ε, 2]]`, `ε ∈ {-1, 1}`.
+Those blocks have eigenvalues 2, and 1 and 3. The Gram matrix is positive
+definite of rank `|S|`. The roots lie in `R^8`, so `|S| ≤ 8`.
+
+The bound is attained by eight explicit roots in the 112-line complement of
+the coordinate frame `{±e_{2i} ± e_{2i+1}}` (eight lines). Their within-pair
+products are `±1` and every cross-pair product is 0, matching `B` on tensor
+indices `(0, 15, 1, 14, 2, 13, 3, 12)`.
+
+## Scalar mismatch
+
+The predecessor identity is `D T^T = 2 G4`. Indices 0 and 1 are a cross pair
+of this witness, so the root Gram entry is 0, but `G4[0, 1] = 8`. The required
+coefficient is 16. Dividing the Gram by 8 leaves coefficient 2, still not 0.
+Restricting the tensor factors to this geometric witness does not give the
+tensor scalar identity. The second scanner recomputes the same three numbers.
+
+## Scope challenges that did not become counterexamples
+
+Injectivity is necessary for the eight-point statement. Tensor indices
+`(0, 15, 1, 2, 3, 4, 5, 6, 7)` preserve `B` when 0 and 15 go to the distinct
+lines `e0 - e2` and `e0 - e3` and the other seven indices share the line
+`e1 - e4`. All three lines lie in the 112-line complement. Dropping
+distinctness really does admit nine indices.
+
+Different source and reader maps are outside the Gram argument. The proof
+already says so. The size-12 rank-screen witness is not a missed common-map
+embedding: its four singleton rows, restricted to the set, are identical, and
+the restricted pairing has rank 9. Equal rows of a rank-9 Gram matrix
+`A H A^T` force those labels to coincide once `H` is invertible and the rows
+of `A` span `F2^9`. Separately, indices
+`(0, 15, 1, 14, 2, 13, 3, 12, 4)` do have nine distinct rows and nine distinct
+abstract labels `(508, 506, 496, 488, 448, 416, 256, 128, 511)`. E8 geometry,
+not binary rank, is what excludes that nine-point set.
+
+## What was not checked
+
+PR #3566's root-to-port bijection and the selected archive's port labels were
+not re-derived. "Attained at selected port indices 0, 76, 28, 86, 103, 17, 10,
+11" remains a claim of PR #3928. This review shows the eight roots lie in the
+standard 112-line complement, which is the geometric model of P112, not that
+those integers are the archive's port numbers.
+
+No separate-map search, no dirty-input decoder, no COPY bill, no supplier and
+no new kappa. The eight-term all-pairs floor is untouched.
+
+## Reproduce
+
+Python 3.12, standard library, from the repository root:
+
+```sh
+python3.12 -B research/tensor-pairing-common-map-review/verify.py
+python3.12 -B research/tensor-pairing-common-map-review/independent.py
+python3.12 -B research/tensor-pairing-common-map-review/test_verify.py
+python3.12 -B scripts/research_package.py --package research/tensor-pairing-common-map-review
+```
+
+Expected markers:
+
+```text
+PASS_TENSOR_PAIRING_COMMON_MAP_REVIEW full_rank=16 subsets=65536 rank_screen_max=12 common_map_cap=8 witness_gram_rank=8 scalar_before=16 scalar_normalized=2 root_entry=0 abstract_labels=9 noninjective_indices=9 no_new_kappa
+PASS_TENSOR_PAIRING_COMMON_MAP_REVIEW_INDEPENDENT square=I16 witness_cross=0 coefficient=16 normalized=2 labels=9 no_new_kappa
+PASS_TENSOR_PAIRING_COMMON_MAP_REVIEW_TESTS controls=3
+```
+
+Ordinary replay is read-only. On CPython 3.12.3 the three direct commands
+finished in under a second.
+
+## Open next questions
+
+1. Can two different 9-bit maps embed one principal set of size 9 through 12
+   and still match `2 G4`? The common-map cap does not forbid it. A first step
+   is one fixed nine-point index set. A label pair is not yet a decoder.
+2. Do other common injective eight-point witnesses also miss `2 G4` on a cross
+   pair, or is the mismatch special to this frame? Classifying them needs the
+   PR #3566 port pin before the selected labels can be cited.
+
+## Credit
+
+The theorem and the eight-root witness are ToikY's PR #3928, following
+homelab-05 / 1337isnot1337 PR #3895 and Gonzalo Mier's PR #3566 port bijection.
+The E8 frame convention follows the retained P112 model. This re-derivation
+was prepared by unpaidmoon with substantial Cursor Grok assistance. It is not
+an independent human or formal-kernel review. Apache-2.0.

research/tensor-pairing-common-map-review/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/tensor-pairing-common-map-review/TASK.json

@@ -0,0 +1,78 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md",
+      "research/selected-k8-unrestricted-ends/README.md",
+      "research/eisenstein-reduction-copy-floor/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Independently confirm or refute the common injective E8 bound and the normalized scalar mismatch for the sixteen-point tensor pairing, without importing PR #3928.",
+  "scope_change_reason": "The card asks for a larger-rank local decoder. This session takes the released tensor-pairing handoff instead: the proposed rank-16 block is already obstructed at the nine-bit label embedding, so the useful result is a separate check of that obstruction rather than another decoder search.",
+  "bottleneck_link": "Rank-16 delivery is a 2.31x ideal lever only when a local word can actually emit those children. A common injective E8 map of this pairing stops at eight points, and the full sixteen-point pairing has F2 rank 16, so it is not a nine-bit bilinear form.",
+  "budget_minutes": 60,
+  "stop_rule": "Confirm sections 2-5 of the claimed argument with two scanners and three rejecting controls, or stop at the first counterexample. Do not search a new decoder or price a separate-map embedding.",
+  "outcome": "completed",
+  "evidence": "verify.py census and E8 witness; independent.py square, Gram and labels; test_verify.py controls",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance in the independent re-derivation, checks and write-up. No independent human or formal-kernel review.",
+  "open_questions": [
+    {
+      "question": "Can different source and reader maps embed a principal subset of size 9, 10, 11 or 12 while preserving the scalar identity 2G4?",
+      "why_it_matters": "The eight-point cap uses one common map. The binary rank screen still allows size 12, but only as a necessary condition.",
+      "first_step": "Fix one principal index set of size 9 and search for two 9-bit label maps whose bilinear pairing equals B_S and whose factors reproduce 2G4 on that set.",
+      "blocked_by": "A passing label pair is not a decoder until dirty inputs, frames, restoration and the recursive bill are priced."
+    },
+    {
+      "question": "Does any common injective eight-point witness satisfy the restricted tensor scalar identity, or do they all repeat the cross-pair mismatch?",
+      "why_it_matters": "This review shows one attaining geometric witness fails the identity. It does not classify the other eight-point maps.",
+      "first_step": "Enumerate sign patterns and orthogonal frames inside the 112-line complement and compare each cross-pair Gram entry with 2G4.",
+      "blocked_by": "The selected port-index bijection of PR #3566 was not re-derived here, so a port-labeled census needs that source pin first."
+    }
+  ]
+}

research/tensor-pairing-common-map-review/VERIFY.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": ["{python}", "-B", "{package}/verify.py"],
+      "timeout_seconds": 120,
+      "checks": "Kronecker Gram, F2 square identity, all 65536 principal ranks, E8 112-line witness, nine labels, size-12 row obstruction and noninjective control"
+    },
+    {
+      "argv": ["{python}", "-B", "{package}/independent.py"],
+      "timeout_seconds": 60,
+      "checks": "Separate square identity, witness Gram and frozen nine-label pairing"
+    },
+    {
+      "argv": ["{python}", "-B", "{package}/test_verify.py"],
+      "timeout_seconds": 120,
+      "checks": "Three rejecting controls: broken complement, nonzero cross Gram entry, altered label"
+    }
+  ]
+}

research/tensor-pairing-common-map-review/independent.py

@@ -0,0 +1,100 @@
+#!/usr/bin/env python3
+"""Second reading of the pairing identity, witness Gram and nine labels.
+
+No function in this file is imported from verify.py. The census of all
+65536 principal sets stays in that file.
+"""
+
+PASS = (
+    "PASS_TENSOR_PAIRING_COMMON_MAP_REVIEW_INDEPENDENT "
+    "square=I16 witness_cross=0 coefficient=16 normalized=2 labels=9 no_new_kappa"
+)
+
+WITNESS = (
+    (0, 0, 0, 0, 0, 2, -2, 0),
+    (0, 0, 0, 0, 0, 2, 0, -2),
+    (0, 0, 0, 2, -2, 0, 0, 0),
+    (0, 0, 2, 0, -2, 0, 0, 0),
+    (1, -1, -1, -1, -1, 1, 1, 1),
+    (1, -1, 1, 1, 1, -1, -1, -1),
+    (1, 1, -1, -1, -1, -1, -1, -1),
+    (1, 1, 1, 1, 1, 1, 1, 1),
+)
+TENSOR_INDEX = (0, 15, 1, 14, 2, 13, 3, 12)
+LABELS = (508, 506, 496, 488, 448, 416, 256, 128, 511)
+NINE_INDEX = TENSOR_INDEX + (4,)
+
+
+def need(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def pairing_from_formula():
+    table = []
+    gram = []
+    for i in range(16):
+        grow = []
+        brow = []
+        for j in range(16):
+            value = 2 ** (4 - (i ^ j).bit_count())
+            grow.append(value)
+            brow.append((value + 1) & 1)
+        gram.append(grow)
+        table.append(brow)
+    return gram, table
+
+
+def square_identity(pairing):
+    for i in range(16):
+        for j in range(16):
+            total = 0
+            for k in range(16):
+                total ^= pairing[i][k] & pairing[k][j]
+            need(total == int(i == j), "square")
+
+
+def dot(left, right):
+    return sum(a * b for a, b in zip(left, right))
+
+
+def witness_and_scalar(gram, pairing):
+    matrix = [[dot(left, right) // 4 for right in WITNESS] for left in WITNESS]
+    for i in range(8):
+        for j in range(8):
+            if i // 2 != j // 2:
+                need(matrix[i][j] == 0, "cross")
+            elif i != j:
+                need(abs(matrix[i][j]) == 1, "pair")
+            else:
+                need(matrix[i][j] == 2, "norm")
+            need(
+                ((matrix[i][j] + 1) & 1) == pairing[TENSOR_INDEX[i]][TENSOR_INDEX[j]],
+                "pairing",
+            )
+    for sign in (-1, 1):
+        determinant = 4 - sign * sign
+        need(determinant == 3, "block")
+    need(gram[0][1] == 8 and matrix[0][2] == 0, "mismatch")
+    need(2 * gram[0][1] == 16, "raw coefficient")
+    return matrix
+
+
+def nine_labels(pairing):
+    for i, left in enumerate(NINE_INDEX):
+        for j, right in enumerate(NINE_INDEX):
+            bit = (LABELS[i] & LABELS[j]).bit_count() & 1
+            need(bit == pairing[left][right], "label")
+    need(len(set(LABELS)) == 9, "distinct")
+
+
+def main():
+    gram, pairing = pairing_from_formula()
+    square_identity(pairing)
+    witness_and_scalar(gram, pairing)
+    nine_labels(pairing)
+    print(PASS)
+
+
+if __name__ == "__main__":
+    main()