Prove square-zero is necessary for the borrowed shear tariff: non-square-zero endpoints need 6 shears (no new κ)

research/borrowed-shear-general-endpoint/README.md

@@ -0,0 +1,152 @@
+# Square-zero is necessary for the borrowed-space shear tariff
+
+**Scoped proof with exact finite census; no new κ.**
+
+Ali Romman's [PR #5640](https://github.com/CrocSwap/integer-mult-bounds/pull/5640)
+(`research/borrowed-space-shear-tariff`) proves that a square-zero update
+`diag(I+N, I_q)` of rank r costs exactly `2 ceil(r/q) + 2` cross-bank shears
+with q arbitrary dirty borrowed coordinates. Its lower bound holds for every
+endpoint `diag(T, I_q)`, but its attaining word needs `N^2 = 0`. This package
+answers what happens for a general endpoint.
+
+**Theorem.** Over any field K, for any n, q >= 1 and any n by n matrix T, if a
+word in the PR #5640 alphabet implements `diag(T, I_q)` using at most two
+gathers, or at most two scatters, then `(T - I)^2 = 0`.
+
+**Corollary.** If `(T - I)^2 != 0` and `r = rank(T - I)`, every implementing
+word has at least `max(ceil(r/q)+1, 3)` gathers and as many scatters, so at
+least
+
+    max(2 ceil(r/q) + 2, 6) shears.
+
+When `r <= q` the PR #5640 count of four shears cannot be attained by any
+non-square-zero T. The extra cost is exactly two shears in every domain
+enumerated below.
+
+**Finite census (exact minima).** A breadth-first search over the whole group
+generated by the alphabet gives the exact minimum for every reachable endpoint
+in six domains. Every one equals
+
+    tariff(T) = 2 ceil(r/q) + 2            if (T - I)^2 = 0,
+    tariff(T) = max(2 ceil(r/q) + 2, 6)     otherwise.
+
+| field | n | q | group order | square-zero endpoints | non-square-zero endpoints |
+|---|---|---|---:|---:|---:|
+| F2 | 2 | 1 | 168 | 3 (min 4) | 2 (min 6) |
+| F2 | 2 | 2 | 20,160 | 3 (min 4) | 2 (min 6) |
+| F2 | 3 | 1 | 20,160 | 21 (min 4) | 98 (min 6), 48 (min 8) |
+| F3 | 2 | 1 | 5,616 | 8 (min 4) | 15 (min 6) |
+| F5 | 2 | 1 | 372,000 | 24 (min 4) | 95 (min 6) |
+| F2 | 3 | 2 | 9,999,360 | 21 (min 4) | 98 (min 6), 48 (min 6) |
+
+The last row comes from the opt-in NumPy script; the others come from the
+registered standard-library verifier. Each reachable set is all of `SL(n, F_p)`.
+The F2, n=q=2 row is the smallest case where the square-zero formula fails: its
+two non-square-zero endpoints have `r = 2 = q`, so the rank bound allows 4, but
+6 are needed. On F2, n=3, q=2 the rank-3 endpoints meet the rank bound 6 exactly.
+So the 6-shear floor and the rank bound both bind there, at different endpoints.
+
+## Proof
+
+Write the current state as `x = X x0 + Y z0`, `z = C x0 + D z0`, starting from
+`(X,Y,C,D) = (I,0,0,I)`. A gather `G(A)` sets `C += A X`, `D += A Y`. A scatter
+`S(B)` sets `X += B C`, `Y += B D`. The endpoint requires `X = T`, `Y = 0`,
+`C = 0`, `D = I`.
+
+Adjacent gates of one kind merge (`G(A)G(A') = G(A+A')`). So every word with at
+most two gathers is `S(B0) G(A1) S(B1) G(A2) S(B2)`, with some matrices
+possibly zero. Its states are, in order:
+
+    S(B0): X = I,           Y = B0
+    G(A1): C = A1,          D = I + A1 B0
+    S(B1): X = I + B1 A1,   Y = B0 + B1 (I + A1 B0)
+    G(A2): C = A1 + A2 (I + B1 A1)
+           D = I + A1 B0 + A2 Y
+    S(B2): X = I + B1 A1 + B2 C,  Y = Y + B2 D.
+
+The endpoint gives `C = 0` after `G(A2)`, so `A1 = -A2 (I + B1 A1)` and the
+final data block is `T = I + B1 A1`. Expand `A2 Y` with `C = 0`:
+
+    A2 Y = A2 (I + B1 A1) B0 + A2 B1 = -A1 B0 + A2 B1,
+
+so `D = I` forces `A2 B1 = 0`. Multiply `A1 = -A2 (I + B1 A1)` on the right by
+B1: `A1 B1 = -A2 B1 - (A2 B1) A1 B1 = 0`. Hence
+
+    (T - I)^2 = B1 (A1 B1) A1 = 0.
+
+The final `Y = 0` only fixes B2 and adds no constraint. For words with at most
+two scatters, use the PR #5640 transpose-reversal. Transposing the complete
+matrix product and reversing its order gives a word for `diag(T^T, I_q)` with
+gathers and scatters exchanged. Then `(T^T - I)^2 = ((T - I)^2)^T = 0`.
+
+The corollary combines this with the PR #5640 bound `k, l >= ceil(r/q)+1`.
+The argument uses the restoration of arbitrary dirty borrowed inputs (`D = I`).
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and only the standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/borrowed-shear-general-endpoint
+python3.12 -I -W error -B research/borrowed-shear-general-endpoint/verify.py
+python3.12 -I -O -W error -B research/borrowed-shear-general-endpoint/verify.py
+```
+
+The verifier prints a JSON `RESULT` payload and `PASS_BORROWED_SHEAR_GENERAL_ENDPOINT`;
+it takes about 21 seconds locally. For each of the five standard-library domains it:
+
+- enumerates the full group by breadth-first search, so each distance is an
+  exact minimum over all words;
+- checks every endpoint `diag(T, I_q)` against the tariff above;
+- replays one shortest witness word per endpoint as a literal (n+q)-square
+  matrix product and checks it equals `diag(T, I_q)`, including the dirty
+  borrowed columns;
+- checks that every shortest non-square-zero witness has at least three
+  gathers and three scatters, as the theorem requires.
+
+Controls: the square-zero-only formula `2 ceil(r/q)+2` is refuted on exactly the
+two F2, n=q=2 non-square-zero endpoints, and a witness with one corrupted
+coefficient fails to replay. All checks are explicit and survive `-O`.
+
+The F2, n=3, q=2 row needs NumPy and about 70 seconds and 40 MB of distance table.
+It is not registered in VERIFY.json:
+
+```sh
+python3.12 -B -I research/borrowed-shear-general-endpoint/extended_census.py
+```
+
+It passed locally with NumPy 2.5.4 (`PASS_EXTENDED_CENSUS`, group order 9,999,360,
+168 endpoints, 0 mismatches). That row is local evidence only; CI does not run it.
+
+## Limits
+
+The theorem is a written proof checked by its author only; human and formal
+proof-kernel review are unclaimed. The census covers only the six listed
+domains. **No general upper bound is proved for non-square-zero T.** Whether
+`max(2 ceil(r/q)+2, 6)` is attainable for every T over every field is open.
+The clean-borrowed-coordinate variant, coefficient costs, precision and the
+translation-kernel extension of PR #5640 are not treated. This is a side
+result in the same alphabet. It changes no κ, selected frontier, physical
+supplier or caller bill.
+
+## Open next questions
+
+- **Is `max(2 ceil(r/q)+2, 6)` always attainable?** It is exact in every
+  enumerated domain. A proof would complete the tariff for general endpoints
+  in this alphabet. First step: build a six-shear word `GSGSGS` for an
+  arbitrary `T` in `SL(n, K)` when `q >= n`. Then try to splice it with the
+  grouped PR #5640 word for larger r. Blocker: the PR #5640 cross-products
+  `L_i V_j = 0` fail for non-square-zero factors, so a new invariant is needed.
+- **Which endpoints are reachable at all?** Each shear has determinant one, so
+  `det T = 1` is necessary. Each census domain reaches all of `SL(n, F_p)`. A
+  general proof for every field and every q is not supplied here.
+- **Does the clean-borrowed tariff `2 ceil(r/q)+1` show the same square-zero
+  gap?** The transpose argument is unavailable there, as PR #5640 notes. The
+  one-sided gather argument above may still apply.
+
+## Credit
+
+Produced by Nick Petalas. Ali Romman (@aliromman, PR #5640) supplies the
+alphabet, the rank lower bound, the transpose-reversal argument and the
+square-zero construction that this package extends. Dugongue (PR #5634)
+supplies the reader-recoding application that motivated PR #5640. Apache-2.0.

research/borrowed-shear-general-endpoint/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}

research/borrowed-shear-general-endpoint/TASK.json

@@ -0,0 +1,107 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact borrowed-space cross-bank shear tariff for a general endpoint diag(T, I_q) in the PR #5640 alphabet: a written proof that at most two gathers or at most two scatters force (T-I)^2 = 0, so non-square-zero endpoints need at least max(2 ceil(r/q)+2, 6) shears, plus exact breadth-first minima on six small prime-field domains.",
+  "scope_change_reason": "The card asks for a missing interface implication. PR #5640 proves its tariff only for square-zero updates although its lower bound applies to every endpoint; this package settles the square-zero dependence of the lower bound. It is a written mathematical side result, not a Lean formalization or a selected-caller binding.",
+  "bottleneck_link": "Side result: it prices reader recoding with borrowed dirty coordinates when the update is not square-zero. It changes no complete signed bill, kappa or selected frontier.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the lower-bound theorem and the exact census once every enumerated minimum matches; leave the general attaining construction as an open question.",
+  "outcome": "partial",
+  "evidence": "README.md proof; verify.py exhaustive BFS minima and witness replays on F2 (n,q)=(2,1),(2,2),(3,1), F3 (2,1), F5 (2,1); opt-in extended_census.py on F2 (3,2), local only.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is max(2 ceil(r/q)+2, 6) attainable for every non-square-zero endpoint over every field?",
+      "why_it_matters": "It would complete the exact borrowed-space tariff for general endpoints in this alphabet.",
+      "first_step": "Construct a six-shear GSGSGS word for arbitrary T in SL(n,K) with q >= n, then splice with the grouped PR #5640 word for larger r.",
+      "blocked_by": "The PR #5640 condition L_i V_j = 0 fails for non-square-zero factors; no replacement invariant is known."
+    },
+    {
+      "question": "Is every T in SL(n,K) reachable for every field and every q >= 1?",
+      "why_it_matters": "det T = 1 is necessary; reachability decides where the tariff is finite.",
+      "first_step": "Prove that the alphabet generates the block-unipotent subgroup and contains diag(SL(n,K), I_q).",
+      "blocked_by": "Only the six enumerated domains are checked here."
+    },
+    {
+      "question": "Does the clean-borrowed count 2 ceil(r/q)+1 have the same square-zero gap?",
+      "why_it_matters": "Clean scratch is a separate alphabet use in PR #5640.",
+      "first_step": "Redo the two-gather state calculation with z0 = 0 and without the transpose argument.",
+      "blocked_by": "The transpose-reversal argument does not apply to clean coordinates."
+    }
+  ]
+}

research/borrowed-shear-general-endpoint/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Exact BFS shear minima on five prime-field domains against the general-endpoint tariff, literal witness replays, gather/scatter counts and two rejecting controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Same exact checks under optimized Python; all checks are explicit."
+    }
+  ]
+}

research/borrowed-shear-general-endpoint/extended_census.py

@@ -0,0 +1,72 @@
+#!/usr/bin/env python3
+"""Opt-in NumPy census over F2 (default n=3, q=2): exact minima for every diag(T, I_q).
+
+Not registered in VERIFY.json; run with an interpreter that has NumPy.
+"""
+import itertools, sys
+import numpy as np
+from collections import Counter
+n, q = map(int, sys.argv[1:3]) if len(sys.argv) > 2 else (3, 2); m = n + q; M = (1 << m) - 1
+def pack(cols): return sum(c << (i*m) for i, c in enumerate(cols))
+I = pack([1 << i for i in range(m)])
+gens = []  # (kind, matrix) kind 'G': for x-col j list of z-cols a ; 'S': for z-col a list of x-cols i
+for vals in itertools.product((0,1), repeat=q*n):
+    if not any(vals): continue
+    gens.append(('G', [[a for a in range(q) if vals[a*n+j]] for j in range(n)]))
+    gens.append(('S', [[i for i in range(n) if vals[a*n+i]] for a in range(q)]))
+dist = np.full(1 << (m*m), 255, dtype=np.uint8); dist[I] = 0
+front = np.array([I], dtype=np.uint64); d = 0
+while front.size:
+    d += 1
+    cols = [(front >> np.uint64(c*m)) & np.uint64(M) for c in range(m)]
+    new = []
+    for kind, spec in gens:
+        nc = list(cols)
+        if kind == 'G':
+            for j in range(n):
+                for a in spec[j]: nc[j] = nc[j] ^ cols[n+a]
+        else:
+            for a in range(q):
+                for i in spec[a]: nc[n+a] = nc[n+a] ^ cols[i]
+        v = nc[0].copy()
+        for c in range(1, m): v |= nc[c] << np.uint64(c*m)
+        new.append(v)
+    cand = np.unique(np.concatenate(new))
+    cand = cand[dist[cand] == 255]
+    dist[cand] = d; front = cand
+def rank2(rows):
+    rows = list(rows); r = 0
+    for bit in range(n):
+        piv = next((i for i in range(r, len(rows)) if rows[i] >> bit & 1), None)
+        if piv is None: continue
+        rows[r], rows[piv] = rows[piv], rows[r]
+        for i in range(len(rows)):
+            if i != r and rows[i] >> bit & 1: rows[i] ^= rows[r]
+        r += 1
+    return r
+def matmul(A, B):  # row bitmask matrices n x n: row i bit j
+    return [ (lambda ri: __import__('functools').reduce(lambda acc, k: acc ^ (B[k] if ri >> k & 1 else 0), range(n), 0))(A[i]) for i in range(n)]
+stats = Counter()
+for Tbits in range(1 << (n*n)):
+    Trows = [(Tbits >> (i*n)) & ((1 << n) - 1) for i in range(n)]
+    # column j of full matrix: bits i of rows
+    cols = [sum(((Trows[i] >> j) & 1) << i for i in range(n)) for j in range(n)] + [1 << (n+a) for a in range(q)]
+    dd = int(dist[pack(cols)])
+    if dd == 255: continue
+    N = [Trows[i] ^ (1 << i) for i in range(n)]
+    r = rank2(N); P = N; nil = None
+    for e in range(1, n+2):
+        if not any(P): nil = e; break
+        P = matmul(P, N)
+    N2 = matmul(N, N)
+    stats[(r, rank2(N2), nil, dd)] += 1
+bad = 0
+for (r, r2, nil, dd), cnt in sorted(stats.items(), key=lambda kv: (kv[0][0], kv[0][1], kv[0][2] or 99, kv[0][3])):
+    base = 2 * (-(-r // q)) + 2 if r else 0
+    want = base if r2 == 0 else max(base, 6)
+    bad += cnt * (dd != want)
+    print("r=%d rank((T-I)^2)=%d nilpotency_index=%s minimum=%d tariff=%d : %d" % (r, r2, nil, dd, want, cnt))
+print("group_order", int((dist != 255).sum()), "endpoints", sum(stats.values()), "mismatches", bad)
+if bad:
+    raise SystemExit("FAIL: tariff mismatch")
+print("PASS_EXTENDED_CENSUS")