Research: body-dependent BIT stock cutoff and fixed-point counterexample

[thakrarsagar]

PR2324 leaves open whether its prescribed borrowing reserve can be reduced to the actual post-borrow body. This research note proves the conditional row-divisibility implication, gives the sharp uniform fit cutoff 245773 for the changed reserve, and supplies an exact counterexample to equality-based fixed-point selection. The original reserve's 311311 theorem remains unchanged.

The new stock is K(w)^D(floor((e-k)/w)). A monotone inequality search supplies the least conservative borrowing witness and keeps k=O(w log e). At width 245772, the certified prime 15*2^78+1 makes every strictly-less-than-half borrowing choice fail. At width 273158, the equality iteration cycles 122886 ↔ 131078; the least feasible inequality witness is 122887.

Scope: scoped mathematical audit/research note, conditional on PR2234's complete physical row/caller contracts. No new multiplication exponent, full caller implementation, selected-stage stock identification, or frontier change. The proof retains all high matrix fibres, complete child stock, pointwise row restoration, two-call reuse, padding restriction, remainder/high-part work and the uniform borrowing charge.

Pins and overlap: base/refreshed canonical main 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2, priority revision 4, OS seed 60. Jose Manuel PR2234 at d047ef86fbc5b1614d3d8e2b8d3441413beab73f; Aakash PR2324 at 0ec8a26572069b6109decadd488b9770944a4296. Both heads rechecked unchanged. Original source documents and notice are retained byte for byte with Git/SHA256 pins. Final overlap covers 551 open PRs and 1062 Discussion/comment/reply records with complete pagination and no warnings; arbitrary diffs remain outside coverage. EdDiboi's concurrent original-stock prime-regime claim is distinct and credited in TASK.json. Canonical claim.

Reproduce:

python3.12 -Werror -B scripts/research_package.py --package research/bit2234-body-stock-audit

Passed locally on Linux x86_64 / CPython 3.12.15: exact source-bound receipt; independent full-GL integer products at depths 15/16; bottom-up coverage of all 1048575 positive widths below 2^20; 13 tests normally and with -O, including source/receipt/type corruption, prime, strict-fit, rounding, arbitrary-row restoration and no-fixed-point controls. Package metadata/pins, selected source-binding baseline and staged whitespace checks pass. The all-width theorem rests on the written proof; finite tests do not establish physical caller assumptions. No full selected cold replay, Lean proof, independent human review or hosted-CI success is claimed.

Prepared by Sagar Thakrar (@thakrarsagar) with substantial OpenAI Codex assistance, including separate source-contract, exact-product and test review. Jose Manuel supplies the caller/K/D/ordinary-wrapper contracts; Aakash supplies the predecessor theorem, dyadic-tail method and concrete handoff. The retained NOTICE and README preserve the selected BIT and stock-audit lineage. New work is Apache-2.0. Open next questions concern physical contract admission and formalizing the row/padding implication; neither requires changing the selected frontier.