Research theorem: exact paid cost for binary affine register words

[bitplane]

Change and mathematical scope

In an explicit nonabelian binary-affine address model, noncommuting labels and arbitrarily many restored dirty registers cannot reduce the direct paid-call bill. The exact minimum for diag([g_1],...,[g_w],1,...,1), with g_i=(A_i,b_i), is sum rank_F2([A_i-I|b_i]).

The complete alphabet is formal F2[AGL_d(F2)] register words, free scalar GL_r(F2) basis changes, and unit paid calls I+([g]-1)N with binary rank-one idempotent N and rank-one homogeneous affine displacement. Nonzero translations are paid units; no address map is free. Every extra register must be restored on arbitrary dirty inputs. The attaining construction uses no extra register or scalar preparation. This is an optimistic screening model; real scalar work/storage and physical interfaces still need their own bill.

The written proof normalizes free scalar maps by augmentation, derives the lower bound from a homogeneous representation, and constructs an attaining factorization in the formal group algebra for every address dimension. A concrete triple of mutually noncommuting dimension-three targets requires nine paid calls for any restored dirty-register count; its nine-call formal construction with a fourth dirty register is checked.

This changes the address group and price rule from the card's rational abelian starting model. It does not reduce rational frames modulo two, prove a selected-supplier improvement, or claim a universal barrier for every nonabelian model. No kappa, frontier, physical supplier or multiplication-runtime improvement is claimed. The proof is written, not Lean-verified.

Task and overlap

• Base and refreshed main: bce54fb3f895cbe5cd4c0eb477c3afeed100190f; the patch applies cleanly. No guidance or selected inputs changed.
• One OS nonce 5d737eb3d3ab653b8a6a9411d0753d36 selected bit-mechanisms, card bit-new-register-model, scope key 7084092dd726e7ba1f2f, priority revision 2. Scope is refined to the complete binary-affine alphabet and arbitrary restored register count.
• PR468/720 concern the rational abelian three-register model; PR288 has related rank methods and a different nonabelian solvable-quotient setting; PR836 gives a complex/unitary obstruction. Their exact context and heads are recorded in SOURCES.json / OVERLAP.json.
• PR1194/1306 already cover the other suggested helper-contract card's immediate questions, so those investigations were not repeated.
• Final live overlap: 818 open PRs and 67 Discussion records, complete pagination, 2026-10-13 22:49 UTC. This is bounded overlap evidence, not a novelty certificate. Claim: Binary affine addresses: exact paid-call floor with arbitrary dirty registers #1317 .

Only research/binary-affine-register-bound/ and its dedicated full-census workflow are added.

Validation

python3 -I -B research/binary-affine-register-bound/verify.py --full --work /tmp/binary-affine-full

Python 3.12+ and C++17 are required. The independent C++ Cayley BFS visits all 323,930 affine maps through dimension four and 72,642,074 directed transitions, without rank pruning. Python checks every distance, reachable state and explicit attaining factorization. The dimension-four histogram is [1,225,11830,124200,186304]. This enumerates address maps; the unlimited-register conclusion comes from the proof, not a claim to have enumerated all register circuits.

Additional evidence: 44,020 elementary rank checks; 96 exact formal words / 576 prefixes; 56 formal identities; 32 larger fixtures through dimension 32; seven boundary controls and five package tests. Controls distinguish dirty-helper correctness, noncommuting order, omitted calls, underpriced rank-two operations, translation offsets and the nonfaithfulness of the natural representation on the group algebra. Five packaging tests cover source/certificate/distance corruption, isolated read-only relocation and output preservation.

Registered Python 3.12 replay passed. A complete read-only exported replay under isolated optimized Python 3.14 rebuilt the C++ checker and produced the same canonical receipt, with all 14 input files unchanged:
e95e3af2f484cb03f600c8d669354465f4812a1316e842e248fc81a48d5a30d0.

The generic hook runs quick coverage only, explicitly omitting the full dimension-four native census; the dedicated workflow runs --full. Selected-record/source/provenance checks pass. Hosted CI is separate from these local results. No selected supplier cold replay, physical/native supplier, hosting, precision/tape/compiler or outer analytic admission was performed.

Credit

Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance in proof, implementation, validation and writing; no subagent or independent human review. Apache-2.0; predecessor files/notices are unchanged. Credit eumemic, Ali Romman (PR468), David Govea (PR720), the retained rank-method lineage, and the helper-contract predecessors listed in the README.

The rank and reflection-length methods are classical; the proof credits Huang/Lewis/Reiner and delMas/Lewis with primary references. No new reflection-length principle or literature priority is claimed. The contribution is the explicit register-model cost statement, complete attaining construction, boundary audit and independent exhaustive certificate.

Open next questions

A smaller coordinate-only paid alphabet can make direct target lengths exceed this rank floor; a dimension-three target with that gap is a concrete next search. Separately, any proposed physical escape should name the primitive/free-operation hypothesis it changes and price the full boundary. Natural representation equality alone cannot certify a formal word.

Proof, package README, and observed validation.

[Mister-Meeseeks]

100-PR batch review at 7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2.

Merged to main, preserving the original contributor commits and package attribution.

Reviewed scope: Exact paid-call cost in the formal binary affine register model with arbitrary restored dirty registers and free scalar mixing. Representation-rank lower bound and explicit all-dimension attaining factorization, corroborated by full native finite BFS; not the rational-address supplier model.

The pinned scoped command passed; the batch ledger contains its command, input hashes, environment and log. This incorporates the research/tooling contribution and does not change the selected κ or discharge the inherited multiplication-theorem assumptions.

Batch review, attribution and evidence. Thank you for the contribution.