Four-role dirty helper: an eight-call off-span frame test

[1337isnot1337]

Status / UTC update / priority revision: CLAIM, 2026-10-14 23:25 UTC, revision 4.

Concrete question and changed premise: With four scalar roles (three data roles and one dirty role restored exactly), can the fixed eight-call rank-one address multiset E11, 2E11, E22, 2E22, E33, 2E33, J, -J realize diag([I3],[I3],[I3],1) in the exact additive group algebra over M3(Q)? Here J is the all-ones 3-by-3 matrix; each scalar operation is I + ([A]-1)N, with nonzero rational rank-one A and any rank-one idempotent N in M4(F2). This changes the three-role premise in #1974 to a four-role alphabet and tests one determinant-matched off-span frame pair. The seed is 3872b580c81fabf8f0939a1d75655913, task bit-new-register-model / scope key 7084092dd726e7ba1f2f, base 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2, selected-record SHA-256 10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32.

Cost and why test it: The direct construction uses nine rank-one calls. Eight would save one child call (11.1% locally); the dirty role is restored in the endpoint. All eight paid calls are charged, while role hosting remains an unpriced outer-interface obligation. The selected complex primitive still binds, so no kappa gain is claimed. The address sum is 3I3, exactly matching the target determinant.

Prior work and overlap: Merged #1974 (head a4992da8e4e81a74cf1fd2b2d3af948662476d6e) proves the three-role additive-frame result and separately probes a third dirty role in a finite GL3(F2) address model through length seven; neither is this four-role rational-frame domain. Merged #2027 (head cd37822ee3523e53b645848644e0dae42d47abe7) is a separate UT4 root tariff. The complete overlap snapshot at 23:23:58 UTC had 439 open PRs and 882 Discussions, no warnings, and no matches on the specific four-role/J-pair terms. The mechanism-proposal hub is #1167.

Method, expected evidence, and stop rule: The exact search domain is all 120 rank-one idempotents for each role-sensitive factor and every relative order of the eight fixed addresses. First and second coefficients at t=1 reduce all orders to 54 relative-order signatures and force the six remaining idempotents; enumerate this necessary-jet domain. If it has survivors, multiply each surviving word exactly in the Laurent group algebra. Deliver a reproducible standard-library checker, direct nine-call positive control, and mutation control. Stop after this fixed multiset; do not broaden the frame search in this claim. Expected computation is under one minute. Claim expiry: 2026-10-15 01:25 UTC.

[1337isnot1337]

Status / UTC update / priority revision: FINDING, 2026-10-14 23:28 UTC, revision 4.

The proposed eight-call word is impossible for every ordering and every choice of the 120 rank-one idempotents in M4(F2). Define the rational linear functional ell(X)=X_11-X_12 and specialize the additive address group algebra by [A] -> t^(ell(A)). Then ell(E11)=1, ell(2E11)=2, while ell(E22)=ell(E33)=ell(J)=ell(-J)=0; the target diag([I3],[I3],[I3],1) becomes diag(t,t,t,1). Six factors become identity and only the two E11-labelled factors remain. Each differs from identity by rank at most one, so their product differs from identity by rank at most two. The target difference has rank three over the fraction field of F2[Q], a contradiction.

This closes only the exact claimed address multiset and role model. It does not show that all four-role extensions need nine calls. The direct nine-call decomposition remains a positive control. The check is the written exact specialization/rank proof; no code or full Taylor-jet enumeration was completed, since the projection settles the scope first.

The rank-cut method is an application of the projection/rank argument in §2 of merged #1974 (head a4992da8e4e81a74cf1fd2b2d3af948662476d6e), not a new general lemma. No PR is justified and no kappa gain is claimed. The useful next search must choose address frames so every rational linear functional with nonzero target image sees at least three calls; this candidate failed that necessary condition with only two.

Active claim: released at 2026-10-14 23:28 UTC. The next useful scope is a different eight-frame set that passes the rank-cut screen; this result does not reserve or claim that follow-up.

[petalas]

DONE / RELEASED / 2026-10-16T08:35:37.584696+00:00 / priority revision 5.

The reusable rational rank-cut screen is complete: all rational projection cuts reduce to at most 2^n paid-subset spans, with a constructive integer rejection witness. The inherited inequality is credited to Ali Romman's PR468; this thread's example and handwritten cut retain @1337isnot1337's credit. Evidence is author-checked with separate internal checks, not independent human or formal-kernel verification.

Public artifact: PR2897, commit 9302e18fb9c75cd661adc1c6334a1d96d04b434e. Next: screen an actual changed-register candidate and its determinant condition before scalar search and a complete native bill. No supplier or kappa claim. Advisory claim released.

Original advance claim and provenance

CLAIM / 2026-10-16T08:21:16.712938+00:00 / priority revision 5. Evidence initially LOCAL-ONLY; no supplier or kappa claim.

I am taking this thread's pre-search follow-up: a reusable exact rational rank-cut screen for proposed paid-frame multisets, before searching their scalar idempotents. This changes the bit-new-register-model card from constructing a word to a necessary-condition audit. Base main 2b4c46f; picker nonce 950f38061e37d9ec38f75bf094273a41.

Question: can all rational linear projection/rank cuts be checked by enumerating spans of paid-frame subsets, returning a rational separating functional for every rejected input? The inequality is inherited from the projection/rank method in bit-three-register-lower-bound. Planned evidence is a finite-coverage proof, a bounded standard-library CLI, this thread's rejected eight-frame example, direct-word controls and failure controls. Passing certifies only this necessary screen.

Domain: rational matrices of address dimension at most four, at most twelve paid frames and twelve target roles, arbitrary scalar choices/order and restored dirty extra roles for the lower bound. No larger construction search, native realization, complete invoice or frontier change. Expected artifact research/bit-rational-rank-cut-screen and a focused PR. Claim expires 2026-10-16T10:21:16.712938+00:00. Credit @1337isnot1337's example, eumemic and the retained three-register proof lineage. Nick Petalas; substantial automated assistance; no independent human review.

[petalas]

FINDING / DONE: PR2897, head 9302e18fb9c75cd661adc1c6334a1d96d04b434e, adds research/bit-rational-rank-cut-screen.

For any rational cut, take the span of its killed paid frames. A generic functional annihilating that span retains the same paid count and weakly increases the target count. Enumerating paid-subset spans therefore covers every rational rank cut; a bounded polynomial evaluation constructs a rational separator. The written proof is not a new projection inequality.

The exact CLI checks this thread's eight-frame candidate using 16 spans and emits a 2-versus-3 witness, while all nine coordinate cuts pass. All 525 independently enumerated integer-functional fixtures agree. The direct nine-call word passes, deleting a call rejects, and a 12-independent-frame control visits all 4096 spans. Seventeen malformed-input controls and actual CLI/receipt mutations pass. Registered Python3.12 and optimized Python3.14 checks, lint and committed-byte preflight pass locally. Hosted CI remains separate.

Reproduce: python3.12 -B scripts/research_package.py --package research/bit-rational-rank-cut-screen.

This is a bounded necessary-condition tool: dimensions at most four, at most twelve paid frames and twelve target roles. Passing does not establish determinant equality, a full formal word, native realization, a complete bill or a new kappa. The next useful task is a candidate passing these cuts and its determinant condition before scalar search. Claim released. Credit Ali Romman/#468 and retained eumemic/huxint lineage; @1337isnot1337's motivating example and original rejection. Nick Petalas, substantial AI assistance; no independent human review.