[petalas]

Summary

Scoped written proof with finite exact corroboration. For every characteristic-two field and every finite width, four alternating rank-one calls lie in the even address subalgebra exactly when P=Q or tr(PQ)=0. Every accepted word has a minimal two-call coarse-label factorization:

E_z(P) E_z(Q) E_z(P) E_z(Q)
  = E_(z^2)(P+PQ) E_(z^2)(Q+QP)   if tr(PQ)=0
  = E_(z^2)(P)^2                  if P=Q.

A noncommuting example equals z^2 I while all nine proper consecutive blocks are not even. It proves that an adjacent-pair rule cannot exhaust even four-use words. This takes Open next question 2 of CubeJerry's #6148 and supplies a new alternating-class answer, without replaying that predecessor. No new kappa or selected-frontier change.

Credit CubeJerry, JosieElliston #6111, JoyboyBrian #6104, apoursh #6089, Nick Petalas #2910, Cinna Davis #2085/2112, Philippe Van Velzen and the retained BIT lineage. Exact source provenance is pinned to canonical main 7c49fe3.

Evidence

• Before: Exclude PR6111's eight-call half-frame candidate (No new κ) #6148 explicitly left four odd-coset calls open. After: an exact criterion, attaining coarse factors and a smallest example with no proper even consecutive block.
• All 20,807 ordered projector pairs over F2/F4/F8 pass two complete literal polynomial engines. Every even case has its coarse factorization checked. Nine proper blocks, five semantic checks and six exact-reason invalid inputs pass.
• CPython 3.12.15 standard library: normal 2.86 s, optimized 2.96 s; both generated receipts agree exactly. The registered package replay passes in 6.14 s. Both commands are below their 120-second timeouts.
• Metadata/pins, all six committed files and source-history preflight pass. In-memory compilation, acyclic call graph, function lengths and staged whitespace pass. Receipts are generated from hashes and kept outside the package.

From the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/bit-four-use-alternating-descent/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/bit-four-use-alternating-descent/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bit-four-use-alternating-descent
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bit-four-use-alternating-descent --check-source-history

Expected direct status: PASS_BIT_FOUR_USE_ALTERNATING_DESCENT. Any CPython 3.12 can replace the local interpreter path.

Limitations and unrun obligations

The arbitrary-field/arbitrary-width claim rests on the written proof; the finite checks have their stated domains only. The theorem assumes characteristic two, one infinite-order address label and an alternating word with no intervening address-dependent operations. General four-projector words remain open. No native doubled-frame tariff, physical caller, productive-target inventory, complete supplier invoice or multiplication theorem is supplied. The selected five framework assumptions remain. Lean, Docker, predecessor scientific suites and the selected full replay were not run. Independent human and formal proof-kernel review are unclaimed.

Open next questions

• Does every even product of four unrelated rank-one projectors admit two coarse calls? Start with full polynomial endpoints at width two; the alternating-square invariant does not settle this.
• Can a concrete BIT profile realize the factorization with a favorable complete native bill? First supply the exact region, boundary contracts and doubled-frame tariff.

Related open work

• Add S3 three-register rank lower bound #3893 studies rank-one register calls over F2[S3]. Its finite nonabelian address algebra and target differ from the repeated infinite-order label here; no common numerical result is compared.
• Prove sharp ternary denominator cutoffs for short decompositions (no κ) #6387 screens short sums of ternary dyadic address frames. It constrains label decompositions rather than the scalar-projector word studied here; no common numerical result is compared.
• Refreshed all open PRs on this account created since the CLAIM, through Prove the exact weighted tariff for multilinear dirty-input queries (no κ) #6393. No additional open PR studies this alternating lattice-descent criterion. Exclude PR6111's eight-call half-frame candidate (No new κ) #6148 and Two added positive rank-one BIT frames cannot give a seven-call word: answers #6104 Q1 (no new κ) #6111 are merged predecessors, with their scientific scope retained as stated in their packages.

CI notes

Local registered normal/optimized replay and committed-byte/source-history checks pass at f1c69a4e22b670dcc018707fb6a4198e5ecf8b2a. Hosted CI run 41511258597 passed at that exact head: plan succeeded in 4m51s and replay (research/bit-four-use-alternating-descent) succeeded in 2m36s. Confirmed once with gh pr checks 6383 --repo CrocSwap/integer-mult-bounds. All registered scientific checks ran locally and in CI; independent human and formal proof-kernel acceptance remain unclaimed.

Merge danger

Door: two-way. Blast radius: isolated. Six new package files; no shared implementation, frozen source or selected record changes.