Finite bit construction: certify R439 matching floor and save 31 further ADDs

[bitplane]

Finite bit-circuit construction and exact restricted-class cost bound. The complete R439 word costs 11,949 ADDs, saving 31 beyond PR926 while reducing both positive prefix maxima. An independent integer certificate proves an 11,948-ADD floor for disjoint helper pairs around the frozen PR915 target basis. The candidate is within one ADD of that floor and fits the existing precision ceilings. Whether some arithmetic optimum also meets those ceilings remains open. No new kappa is claimed.

The complete D bill is 199 + 306 + 4,719 + 306 + 199 = 5,729 ADDs. The saving is 1,259 beyond PR915 and 12,356 against selected PR589. Every preparation/restoration operation is paid. All non-D fields, every register's ordered MOVE path, all COPY/ERASE records, 439 helpers, nine rank-seven totals and rank mass 5,129 are retained.

The matching certificate checks both orientations of all 96,141 unordered pairs, using 439 vertex prices and 19 odd-set prices. Its doubled upper bound is 2,520; an explicit matching saves 1,260, proving equality. No solver is needed for default verification. The class fixes the target basis, disjoint helper recipe, direct middle injections and unchanged suffix; it excludes general XOR circuits and overlapping basis changes.

All three nominated arithmetic optima need 193 nine-stage prefix bits. The declared follow-up exhausts their 598 single-pair deletions, pricing 601 complete words in both directions; 17 fit both caps. The selected deletion loses one ADD of saving and gives F = 70,083, B = 10,548,832, and a 101-bit local bound. Its nine-stage estimate uses 87.43% of the 192-bit ceiling, compared with PR926's 99.925%. The exact precision-constrained minimum in this fixed class is either 11,948 or 11,949; failure of three optima is not an exclusion of every optimum.

Reproduce with Python 3.12+, C++17 and Boost headers:

python3 -I -B research/r439-helper-matching/verify.py
python3 -I -B research/r439-helper-matching/test_package.py

Complete receipts match on ordinary CPython 3.14.4 and isolated optimized CPython 3.12.3 from a minimal read-only closure. Checks include every dual inequality, all 601 priced words, 14,390,692 literal positive instructions, 48,729 direct mixed-matrix coefficients, and 661 separate input columns in both D directions for five words. Original E8/frame/endpoint checks and fresh unchanged native 5/9/11-stage checks pass on 883/1,327/1,549 formal columns per word. All 240 omitted-bridge controls, 19 local controls and 8 package tests pass. Optional NetworkX 3.6.1 nomination reproduces every committed field. Selected-record checks pass before and after rebase; staged whitespace passes.

The floor calibration passes the original local 104-bit checks but is explicitly rejected by the source-bound 192-bit nine-stage invoice expression. The original H2 and literal K extractor remain false for the four changed words, with their predicates unchanged. Integration requires acceptance of the semantic D boundary, changed whole-hosted emission/audit, complete finite/precision invoices and outer assembly. Common-label realization and analytic assumptions remain inherited. Full repository/cold supplier suites, a full formal multiplication theorem and measured runtime improvement are not claimed.

Research base: 91a2094. Publication base after rebase: 47481c8. All 14 consumed source files are byte-identical across the update. Main now selects PR890, conditional kappa 0.001661957774647029, retaining PR589; that intervening improvement is not attributed to this work. Only research/r439-helper-matching/ is added. Seed 4 selected the bit-supplier track; the local claim records the three tasks, bounded search and scope. A 708-open-PR refresh through #937 found no competing certificate for this graph. PR933 and PR936 concern different frame/order or phase-A synthesis classes; their savings are not composed.

Credit Sagar Thakrar's PR716/817 for prior fixed-basis matching certificates, PR915 for the frozen target basis and PR926 for the greedy comparator. Exact source snapshots and notices are retained. Credit also remains with Scott Woolsey Biggart, Greer Guthrie, Mikhail R. Gadelha, commdata2338, DreamingOfClouds, eumemic and the native verification lineage. The matching method and odd-set inequalities are classical; optional discovery credits NetworkX, Jack Edmonds and Zvi Galil. Prepared for Gareth Davidson (@bitplane) with substantial OpenAI Codex assistance, Apache-2.0; no independent human review claimed.

Published head: 8af7833. Mathematical implementation: 34f7eff; the final commit changes only the local claim to record the result/link and refreshed publication context. The remote OPEN state, exact head and 33-file package scope were verified. All five hosted workflows on that head report action_required; no hosted CI pass is claimed. Research-artifact workflow. The immediate post-submission queue through #943 contains distinct fanout, decoder, Fourier and complex-owner contributions; none is composed here.