[chafreaky]

This refines PR #58's conditional witness by changing the order in which its compiler tries retired auxiliary slots:

$$ T(n)=O\left(n(\log n)^{1-\kappa}\right),\qquad \kappa=\frac{4764513337}{10^{14}}=4.764513337\times10^{-5}>2^{-15}. $$

The exponent saving is 0.290011% above #58 (475073569/10^13). The exact bit saving is 2382370177/50000000000000. The inherited analytic and fixed finite-alphabet multitape hypotheses remain unchanged.

Change

Try retired slots in descending current frame rank, breaking ties by slot ID. The previous order was ascending slot ID. The scalar graph, frame family, matching algorithm, legality checks, and same-frame synthesis are unchanged.

A slot can be reused only in a containing frame. Trying larger frames first is intended to preserve smaller-frame slots for later regions. This is a search heuristic. Correctness still follows from the checked containment and span conditions, explicitly paid clearing XORs, and the complete compute/scatter/uncompute word on arbitrary dirty state.

Quantity	PR #58	This PR
h=23 auxiliary roles	30,790	30,688
h=25 auxiliary roles	40,446	40,338
Physical wires W	150,593,466	150,167,598

The actual fixed-basis block profiles give rank 86,344,521,950, deficit 1,846,900, and maximum child width 529. All 4,073,300 data pairs, copied centers, paid endpoints, complex branch, and assembly interfaces remain charged. The original shared compiler remains byte-identical; a dedicated compiler module isolates this single scheduling change.

Verification

Independent replay of both selected words passes every source, target, and dirty basis vector in both orientations, reconstructs every frame transition from literal XOR incidences, and confirms exact fixed-I+J profiles with zero CRT disagreements. Exact rational checks prove all 47 assembly inequalities and seven margins, reject both next grid points, and exclude PR #58's complete network at the new bit saving. The pinned #58 certificate is retained for comparison.

The bounded search compared seven candidates per axis and all 49 pairings. This is not a global optimality claim. Fresh packaged regeneration passes both axes, every profile, and ten focused rejection/replay tests. Independent audit passes all 30 adversarial controls and all 51 source pins. The expanded current-main make verify completed successfully: 429 integrated tests, 28 restored research audits, and all 20 historical patch checks, with no generated-file drift. An independent review verified the upstream integration, source closure, unchanged mathematics, and completed receipt.

make joint-dual-verify
make verify

Tested current-main construction: 94c97bd367782c9530bee7c17d229bd4b1e0a2b7, incorporating main d55bcd62ceb8f322bcf311a5a66e94c3ac7724f0 and PR #58 head be5d3e6e39ad9a11372f168e37466af412e51e53. The proof and exact certificate are pinned to that tested construction; the completed verification receipt records the expanded run and preserves the earlier complete construction verification. The upstream merge preserves the original words, profiles, and exact arithmetic, and updates the Makefile/README source pins. This branch builds on PR #58. The finite certificate does not prove the inherited all-size framed-word transfer, residual compiler, finite-alphabet tape layout, analytic, routing, prime-selection, or recovery obligations.

Published-head CI: 20/20 checks passed on 21a121960644b8c6fdf9c06fe39dea1944dd2231 across Python 3.11, 3.13, 3.14 and the retained formal packages. The formal jobs cover their existing packages; they do not establish a new full formal multiplication theorem.

Attribution

This priority refinement and its checks were prepared by Chafik Boukhalfa with OpenAI Codex assistance. The compiler and paid reclamation are eumemic's PR #57, the dual-suffix graph is Rohan Gupta / gupt1156's PR #55 (Anthropic Claude assistance), and their prior checked composition is #58. Avi Eisenberg / ikeboy's #53 framework and all earlier source notices, licenses, and contributor credits remain. No imported algorithm is claimed as a new invention here.