[unpaidmoon]

Change and mathematical scope

Negative result. No new κ and no selected-frontier change. The selected conditional exponent remains 0.001672660197076918.

In the PR #3905 shear alphabet, with address width (m=2) and two roles, each letter of ({X,X^{-1},Y,Y^{-1}}) is one rank-1 child. Every word for (B^k=X^2Y^2) has at least (2k+1) letters, and (B) itself has length exactly 4. The supplier moment (M(a)=(L/2),2^{a-1}) equals (2^a) at (k=1) and is strictly greater than 1 for every (a\in[0,1]) when (k\ge 2). The strict test (M(a)<1) fails in every case. Raising a letter's rank above 1 only increases the moment.

The PR #3947 three-bit quotient implements (\rho(B^k)) with at most one XOR, so that different operation has moment at most (1/2). That screen does not bound the faithful letter bill: no constant (C) satisfies (L_k\le C). The diagonal four-call word sends a dirty pair ((u,v)) to ((Bu,v)) with the spectator untouched, so there is no cleanup term to add back.

Status: scoped proof, with finite algebraic checks of the identities the proof uses. This is not a construction, not a scalar saving, and not a κ improvement.

Remaining obligations: no larger alphabet, no free maps between the present letters, no lossless source-data encoder, no selected cold replay, and no Lean proof. Unknown conversion cost from the three-bit quotient back to the integer matrix is not treated as zero.

Task and overlap

• Base commit: bb4bccbf42844d2801487450727c2f63e10d1d0f (upstream CrocSwap/integer-mult-bounds main).
• Priority revision 6. Task card: bit-new-register-model. Scope key 7084092dd726e7ba1f2f (the same key as PR Prove commutative caller obstruction for the integer-shear target #3937, because the key ignores the object). Scope status: changed.
• Concrete object: faithful words for (B^k) in that alphabet, (B=X^2Y^2=\begin{pmatrix}5&2\2&1\end{pmatrix}). Domain: every (k\ge 1) and every moment parameter (a\in[0,1]). Finite checks run through (B^{24}), the length-4 Cayley ball, and doubling through length 6.
• Dependency heads, cited and not vendored (those commits are not reachable pins in this checkout): PR Research: exact four-call minimum for an integer-shear target #3905 b27bf4c72a822b21f483e08cb3241ad9d165b66f, PR Prove commutative caller obstruction for the integer-shear target #3937 5ee1c9cee717e682db01bff4c398b87011a135a2, PR Prove minimum binary carrier and native XOR bill for the integer-shear target #3947 4026d068981e6e2d5e9f0b96c3cb1ba9957b841f.

Scope changed because the card asks for a new register identity, and this package does not construct one. It prices the supplier/recurrence question released by PR #3947 on the alphabet already fixed by PR #3905. A one-XOR quotient moment below 1 does not change the bit primitive while the faithful letter bill fails (M(a)<1). Span-four and span-six dirty-auxiliary censuses on the same card are a different question and are not refined here.

Overlap: no open PR through #4121 proves this inequality. PR #3947 states that it does not. Other open PRs that mention shear do not establish the faithful moment failure.

Item taken: number 5 of this session's handoff-ordered eligible list on Discussion #1166.

1. Typed actual-width physical H / rounded return (comment 19016699).
2. Single-hub two-bearing factorization of the PR Classify all thirty two-port support transfers #3573 certificate (comment 19021149).
3. Invoice-level audit of composed T488 ownership and outputs (comment 19022532, question 1; question 2 closed by Audit (no new kappa): the composed T488 profile is exactly PR3642's optimal packing vertex #3796).
4. Physical rank-8/u2 source/consumer contract against the 16 extra rank-one children (comment 19029639 / PR Certify integer-count budgets for three ideal lever combinations (no new kappa) #3889 open question 1).
5. This inequality (comment 19031016 and the PR Prove minimum binary carrier and native XOR bill for the integer-shear target #3947 reply).
6. Independent review of the PR research: certify local-first two-ADD obstruction on staged544 #3942 interaction reduction (reply 19032637), distinct from Certify losing-first two-edit obstruction at displacement two on staged544 #3957 and Certify neutral fixed-frame two-edit obstruction at displacement two #3970.
7. One adjacent completed-call pair for the P104 two-axis gate (comment 19034066).

A parallel session's list in comment 19056694 places this shear question at position 4, because it keeps the QQ16 adjacent-event bind (comment 19030049) and does not count items 3 and 4 above. This package was already the item named eligible by the coordinator, and it was finished before that later list was used as a reason to switch tasks.

Validation

Environment: CPython 3.12, standard library only.

python3.12 -B scripts/research_package.py --package research/sl2z-shear-recurrence-inequality

Expected output:

PASS_SL2Z_SHEAR_RECURRENCE_INEQUALITY length_B=4 u_8=1136689 moment_B=touches-zero moment_B2=above quotient_xor=1 strict_supplier_inequality=False
PASS_SL2Z_SHEAR_RECURRENCE_TESTS groups=6
PASS_REGISTERED_RESEARCH_PACKAGE research/sl2z-shear-recurrence-inequality outcome=negative-result

The two package scripts also passed under python3.12 -O.

Finite checks: the matrix for (B), Cayley–Hamilton, linear-form agreement on one probe, powers through (B^{24}), (u_k>2^{2k}) through (k=24), the length-4 Cayley ball, doubling on every word through length 6, four dirty spectator pairs, and the three-bit matrices (one changed coordinate, and (\rho(B)^2=I)).

Proof arguments, which those checks do not replace: (u_k\ge 5^k) for every (k) by induction, the (\ell_1) doubling bound for every word length, and the moment comparison for every (k\ge 1).

Failure controls in test_verify.py: an (\ell_1) factor of 1 is rejected, length 3 does not reach (B), four rank-1 letters do not satisfy (M<1), five letters lie strictly above 1, and (B^2) rules out a length-4 word.

Checks not run: selected cold replay, Lean, Docker, human review, full group-algebra multiplication, a lossless encoder, a larger alphabet, and free inter-letter maps. Predecessor packages are not in this checkout; the matrices were recomputed from the integer action.

No paid-profile budget and no κ budget are claimed. The compared bill is the letter count itself.

Credit

• 1337isnot1337 / OpenAI Codex, PR Research: exact four-call minimum for an integer-shear target #3905: the shear alphabet, the target (B), the four-call minimum, and the diagonal dirty-role bill.
• ToikY / OpenAI Codex, PR Prove commutative caller obstruction for the integer-shear target #3937: the commutative-carrier obstruction and the request to price this inequality.
• ToikY / OpenAI Codex, PR Prove minimum binary carrier and native XOR bill for the integer-shear target #3947: the three-bit quotient, the one-XOR endpoint, and the explicit statement that no supplier inequality was proved.
• eumemic and huxint: the register-model predecessors cited by PR Research: exact four-call minimum for an integer-shear target #3905. The moment shape is the repository supplier test ((1/W)\sum n_r(r/m)^{1-a}).

New inequality, proofs and checks by unpaidmoon, with substantial AI assistance (Cursor Grok 4.7). Apache-2.0. No independent human or formal-kernel review is claimed.

Open next questions

Linked from research/sl2z-shear-recurrence-inequality/README.md under "Open next questions".

Smallest useful follow-up: name one explicitly larger legal alphabet that still implements the integer matrix (B) rather than a quotient, record the rank of each paid gate and the role count, then apply the same moment test to a proved letter lower bound. That is the only nearby route that could make the shear target a supplier primitive. Blocker: free maps between the present shear letters are outside this charging and need their own lemma before they count as unpaid.

Workflow feedback (optional)

Handoff-first ordering, together with scripts/find_overlap.py, separated this inequality from the span-four and span-six work already delivered on the same card. Discussion #1166 comment 19056694 later published a different eligible ordering; both lists are recorded in the finding so a collision is visible.