[petalas]

Result

Scoped proof with an exact finite census; no new κ. Claim type: written proof (author-checked) plus finite certificate.

Ali Romman's #5640 proves the sharp borrowed-space tariff 2⌈r/q⌉+2 cross-bank shears for a square-zero update diag(I+N, I_q). Its lower bound holds for every endpoint diag(T, I_q), but its attaining word needs N² = 0.

Theorem. Over any field, if a word in the #5640 alphabet (gathers z += A x, scatters x += B z, arbitrary dirty borrowed inputs restored) implements diag(T, I_q) with at most two gathers or at most two scatters, then (T−I)² = 0.

Corollary. A non-square-zero T with r = rank(T−I) needs at least max(2⌈r/q⌉+2, 6) shears. When r ≤ q, the four-shear count from #5640 is unattainable.

Census. Breadth-first search over the whole generated group gives exact minima. In every domain below, each of the 319 standard-library endpoints and 168 NumPy endpoints equals 2⌈r/q⌉+2 when square-zero and max(2⌈r/q⌉+2, 6) otherwise:
F2 (n,q) = (2,1), (2,2), (3,1); F3 (2,1); F5 (2,1); plus F2 (3,2) with NumPy (group order 9,999,360). The smallest case where the square-zero formula fails is F2, n = q = 2: two endpoints with r = 2 = q cost 6, not 4.

The proof is five lines of state algebra: D = I forces A₂B₁ = 0, then C = 0 forces A₁B₁ = 0, and T − I = B₁A₁. It is in research/borrowed-shear-general-endpoint/README.md.

Evidence and reproduction

Interpreter: CPython 3.12.15 (~/git/integer-mult-bounds/.venv/bin/python3.12), standard library only for registered checks.

python3.12 -B scripts/research_package.py --package research/borrowed-shear-general-endpoint
python3.12 -B scripts/check_research_commit.py --package research/borrowed-shear-general-endpoint --check-source-history
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

Local results: PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=partial (two registered commands, about 22 s each); PASS_RESEARCH_COMMIT_BYTES. The verifier replays one shortest witness per endpoint as a literal (n+q)-square matrix product, including the dirty columns. It checks that every non-square-zero witness has at least three gathers and three scatters. Two controls must reject: the square-zero-only formula, refuted on exactly two F2 n = q = 2 endpoints, and a witness with one corrupted coefficient.

Opt-in, local only (not in VERIFY.json; needs NumPy, about 70 s): python3.12 -B -I research/borrowed-shear-general-endpoint/extended_census.py → PASS_EXTENDED_CENSUS, 168 endpoints, 0 mismatches (NumPy 2.5.4).

Limits

• No general upper bound is proved for non-square-zero T. Attainability of max(2⌈r/q⌉+2, 6) beyond the six domains is open.
• The census covers only the listed domains. The F2 (3,2) row is local evidence only.
• The clean-borrowed variant, coefficient costs, precision and the translation-kernel extension of Sharp borrowed-space shear tariff with an attaining translation-kernel compiler #5640 are not treated.
• Human and formal proof-kernel review are unclaimed. No κ, selected-frontier, supplier or caller-bill change.

Open next questions

• Is max(2⌈r/q⌉+2, 6) attainable for every non-square-zero T over every field? First step: a six-shear GSGSGS word for arbitrary T ∈ SL(n,K) with q ≥ n.
• Is every T ∈ SL(n,K) reachable for every field and every q? Each shear has determinant one, so det T = 1 is necessary. Every enumerated domain reaches all of SL(n, F_p).
• Does the clean-borrowed count 2⌈r/q⌉+1 show the same square-zero gap? The transpose argument is unavailable there.

Related open work

No open PR studies the borrowed-space shear alphabet or its tariff. Searches for "borrowed shear", "square-zero" and "cross-bank shears" across open PRs found none. Rechecked before DONE: the open PRs this account opened after the CLAIM (#5961–#5969, #5971) study other objects, and none computes this tariff.

CI notes

All checks passed for head 622c4f56bc8e1d440c725cf87b991ae965132378: plan and replay (research/borrowed-shear-general-endpoint) in run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40541238332. The opt-in F2 (3,2) NumPy census is not part of CI.

Credit

Produced by Nick Petalas. Ali Romman (#5640) supplies the alphabet, the rank lower bound, the transpose-reversal argument and the square-zero construction. Dugongue (#5634) supplies the reader-recoding application behind #5640.