[petalas]

Result

Claim type: scoped exact minimum in the formal integer-shear register model of #3905. It combines a finite certificate with a cited written theorem. There is no new κ, supplier or selected-frontier change.

#3905 (1337isnot1337) proves that diag([B],[e]), with B = X^2Y^2 = [[5,2],[2,1]], costs four calls with labels X^{±1}, Y^{±1} and factors I + ([g]+[e])N, where N is a rank-one idempotent over F2. Its Open next question asks whether diag([B],[B^{-1}]) can share factors across roles and cost fewer than the eight calls of the coordinate-projector word.

It cannot. The exact minimum is eight calls.

• Lower bound. Over F2 the Research: exact four-call minimum for an integer-shear target #3905 factor equals the gate (I-N)[e] + N[g] of Ali Romman's merged research/group-subproduct-cover (Prove the all-group rank-one triple floor with free scalar workspace #5394). Its cover theorem (cited, not audited) says the paid count equals the least length of one label word whose ordered subproducts contain every target label. The new step is a complete census of all 87,381 shear words of length 0–8. No word of length at most seven has both B and B^{-1} among its ordered subproducts. The lower bound therefore holds for any F2 frame rank, interleaved scalar maps and finite dirty workspace.
• Upper bound. D_{E11}(X)^2 D_{E11}(Y)^2 D_{E22}(Y^{-1})^2 D_{E22}(X^{-1})^2 = diag([B],[B^{-1}]) is an exact identity in M2(F2[G]) using rank-one frames, two dirty roles, no scratch and no cleanup.
• Census facts: B and B^{-1} each have exactly one four-letter word (XXYY, yyxx). Exactly 124 words of length eight cover both. In 54 of them, a B mask and a B^{-1} mask share a position. Positions can be shared at length eight, but sharing never shortens the word.

Package: research/sl2z-inverse-pair-cover/.

Evidence and reproduction

From the repository root, with CPython 3.12 (locally ~/git/integer-mult-bounds/.venv/bin/python3.12, CPython 3.12.15):

python3.12 -W error -B research/sl2z-inverse-pair-cover/verify.py
python3.12 -W error -O -B research/sl2z-inverse-pair-cover/verify.py
python3.12 -B scripts/research_package.py --package research/sl2z-inverse-pair-cover
python3.12 -B scripts/check_research_commit.py --package research/sl2z-inverse-pair-cover --check-source-history

Local results at 362cead4c481b2d9856baa07b711687425cfe002:

PASS_SL2Z_INVERSE_PAIR_COVER legal_factors=24 census_words=87381 max_both_cover_below_8=0 length8_both_covers=124 overlapping_mask_covers=54 geodesics=1+1 minimum_calls=8 controls=11 no_new_kappa
PASS_REGISTERED_RESEARCH_PACKAGE research/sl2z-inverse-pair-cover outcome=completed
PASS_RESEARCH_COMMIT_BYTES ... "package": "research/sl2z-inverse-pair-cover" ...
PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check)

Each VERIFY command takes about one second. The verifier also checks the gate identity for all 24 legal factors, 16 dirty columns, eight single-deletion controls, a reorder control, and a sharing control in which {B, X^2} has a four-letter cover. A random support-lemma check runs 40 circuits with arbitrary F2 frames and interleaved scalar matrices. A separate breadth-first cover-number routine agrees with the census.

Limitations and unrun obligations

• The lower bound for arbitrary frames and workspace relies on Prove the all-group rank-one triple floor with free scalar workspace #5394's written proof, which was not re-checked. The census itself is complete for the four-label alphabet through length eight.
• Group labels are formal basis elements. Native conversion of the shear action, physical cost, recursive moment and supplier admission are unpriced (see Prove commutative caller obstruction for the integer-shear target #3937, Prove minimum binary carrier and native XOR bill for the integer-shear target #3947, Prove faithful integer-shear words fail the supplier moment test. #4126, Price integer transvections on the shear target B^k. #4146).
• The result covers only the four-label alphabet. A larger alphabet can change the cover number.
• No Lean, Docker, independent human or formal-kernel review.

Open next questions

1. Is the paid count of diag([B^k],[B^{-k}]) exactly 8k for every k ≥ 2? A first step is a pruned census for k = 2 up to length 15, or a no-sharing lemma built from the shortest words for B^{±k}.
2. Does the eight-call minimum survive when S = XY^{-1}X, or any single extra label, is added to the paid alphabet? A first step is a five-label census through length seven. Each added label also needs its own native price.

Related open work

• Research: exact four-call minimum for an integer-shear target #3905 (1337isnot1337): source model, four-call single-target theorem, and the question answered here. This package cites it and does not change it.
• Prove prime-exponent group labels need one rank unit per target (no new κ) #6008 (this account, opened after this claim): prime-exponent group labels, rank units per target, in the same Prove the all-group rank-one triple floor with free scalar workspace #5394 subproduct-cover framework. Different groups and charge; there is no shared number to compare.
• Prove exact eight-call tariff for four inverse C3 targets (no κ) #5963: inverse C3 targets in a different group and alphabet. There is no shared number to compare.

Credit

The package was produced by Nick Petalas. It builds on 1337isnot1337 (#3905, the model and the question) and Ali Romman (#5394, the cover theorem). The register-model lineage that #3905 credits (#288, #203) is retained.

CI notes

All checks passed at 362cead4c481b2d9856baa07b711687425cfe002: plan and replay (research/sl2z-inverse-pair-cover), run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40585729674.