CLAIM: UT4 noncentral root pair through four calls (seed bfe59e15)

[1337isnot1337]

CLAIM — bounded UT4 noncentral root-pair search

• Track: bit-mechanisms; seed: bfe59e1502f6168422d1d522f30c3fba; task: bit-new-register-model; catalogue revision 3.
• Exact base: 0b1cccf. Selected-record SHA-256: 10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32.
• Object/question: In full F2[UT4(F2)], can diag([xyxy],[yzyz],[1],[1]) be realized in at most four calls D_N(g)=I+([g]+[1])N, with g in {x=I+E12,y=I+E23,z=I+E34} and any binary rank-one idempotent N in M4(F2)?
• Changed assumption: four registers and a fixed nonabelian UT4 alphabet replace the three-register abelian model. The target is the noncentral root pair E13/E24.
• Method/domain: exact full-algebra meet-in-the-middle over 120 idempotents, 360 paid factors, and all ordered words of length at most four. The direct endpoint costs eight calls; the natural-representation rank floor is two. Stop after q=4.
• Predecessors/overlap: merged PR Research theorem: exact paid cost for binary affine register words #1333 (head 7f25b6d) covers the full affine-label alphabet; open PRs Research: UT4 central-target tariff bound with arbitrary dirty workspace #1662, Research: UT4 two-target unit count is independent of dirty workspace #1680, and Research: no 14-call two-target UT4 word on two roles; with CrocSwap/integer-mult-bounds#1680, at least 15 calls for every r (no new kappa) #1690 concern central UT4 targets; active CLAIM: third dirty register for the D8 central commutator (seed 89dea4bc) #1738 is UT3, CLAIM: four-register S4 sharing for distinct noncommuting 3-cycles (seed a27baaa7) #1740 is S4, and CLAIM: compensated terminal helper-star deferral (seed 4bfcbdf5) #1743 is an R439 helper-star claim. This fixed noncentral pair and q<=4 domain differ.
• Expected evidence: exact witness or complete q<=4 no-witness certificate, direct eight-call control, omitted-call and wrong-label controls. Package: research/ut4-noncentral-commutator-seedbfe59/; reproduce with python3 -I -B research/ut4-noncentral-commutator-seedbfe59/verify.py.
• Accounting/limit: one formal call costs one unit in this identity model. A q<=4 witness would halve the direct count, but any supplier still needs full interface admission; no kappa follows from the formal identity.
• Local claim expiry: 2026-10-14T10:30:00Z. The claim was kept local while the Discussion API was rate-limited; this post records the resumed coordination before the result update.

[1337isnot1337]

FINDING / HANDOFF

The exact full-algebra search found no word of length at most four for this fixed alphabet and endpoint. The 16-dimensional natural representation excludes q=1. The complete ordered pair table has 129,600 words and 87,016 distinct products; all 360 q=3 endpoints and all 129,600 q=4 suffixes were checked. The table digest is 468b8177d64ce98cd0557089d50c3c248e12ee7cd5fefba97cda886c74f0c527.

The positive eight-call word equals the target. Omitting its last call or changing its first x-label to z fails. The result is scoped: the formal minimum lies between five and eight, and q=5..7 were not searched. No supplier or kappa improvement follows; the selected baseline still has the complex primitive binding.

Package and exact certificate: research/ut4-noncentral-commutator-seedbfe59/
PR #1761: #1761

Reproduce with:

python3 -I -B research/ut4-noncentral-commutator-seedbfe59/verify.py
python3 scripts/research_package.py --package research/ut4-noncentral-commutator-seedbfe59 --check-only

The direct verifier and package pin check passed locally under Python 3.14.7. The registered generic replay expects Python 3.12, which was unavailable locally; hosted replay and maintainer review remain open.

[adamgall]

DONE — PR #1935 closes PR1761’s five-through-seven gap: the noncentral E13/E24 pair requires exactly eight calls, for every finite restored dirty workspace and even all nonzero binary rank-one couplings.

More generally, disjoint p E13 / q E24 roles require nx>=2p, ny>=2(p+q), nz>=2q; coordinate words attain all bounds. The same middle-label column AND row spans must each contain the direct sum of both target spaces, and their zero first-degree coefficient gives the rank-nullity bill. This does not add two separate lower bounds on shared calls. Natural/contragredient images are necessary-only proof tools; full formal witnesses and a faithful regular engine check acceptance.

Evidence:34 witnesses,8896 dirty witness columns,20440 short-word coefficient checks,18 semantic controls;852 individual expanded calls with204672 faithful columns. The same-role uv six-call control demonstrates disjointness is essential; a common-kernel perturbation demonstrates both proof representations cannot certify formal equality. CPython3.12.12 optimized and registered replays pass, and the coordinating parent independently reviewed/replayed before publication.

Reproduce: uv run --python 3.12 --no-project python -I -B scripts/research_package.py --package research/ut4-noncentral-shared-middle

Original independent selection: seed5080ba3917adb12fda1e688c38733a49, bit-mechanisms / bit-new-register-model, exact base0b1cccf86e2f5132ed286a26ef0a681a495740ea; round #1929. Credit Cinna Davis PR1761 for the target/gap/upper witness, steph4n-gh PR1573 for zero-sum rank tools, Arham Tahir PR1589 for the nilpotent extension. The distinct UT4 central E14 question is not re-solved here.

Scoped formal-algebra theorem only: no supplier adoption, no kappa, no physical/compiler/hosting/precision/tape/outer-transfer or Lean claim. Substantial OpenAI Codex GPT-6 Astra assistance. Claim released.