[aliromman]

A joint frame refit of the exact PR6453 or PR6529 scalar word cannot give a large gain through the fixed PR6398 mixed caller. The new rational certificate excludes kappa >= 0.003293 through the retained .0034 BIT cap, leaving less than 0.143% headroom over PR6529's reported .003288299. This is a scoped negative result, not a new kappa.

A second theorem makes child-size searches finite for any root with the stated fresh-stage and whole-idle bill, including coupled sites. Every favorable raw-budget search can cap each binary child at 22 leaves for .003293 <= kappa <= .0034, or 21 leaves from .00332118199 onward. The proof bounds each child increment and prunes one leaf; it does not assume the existing six-field root. See PROOF Section6.

The newer PR6545 reports .00329394 through a changed caller boundary. It is outside the fixed-root ceiling. No gain from that separate work is claimed here. Applying the general child cap to it requires checking the stated billing contract.

The domain permits every simultaneous binary contact subspace in F2^9, including subspaces absent from the source. Helper input and output frames can change; every lost helper credit is charged. It keeps the scalar events, main boundaries, public forward moves and owned reverse moves. Different leaves can choose different frame assignments and either source word. The fixed mixed root permits every positive child size and every binary tree.

The exact models contain 119,534 and 119,463 inequalities. Four rounded rational duals, with their full residual corrections, bound the paid-minus-helper tariff and its derivative. Possible native savings are below .053864 and .053888 per call. For each source, 4,851 binary splits and 4,656 finite root choices pass the exclusion; a concave decreasing tail covers every larger tree. A uniform derivative bound extends the failure through .0034. All native jobs, changed helper targets, queries and idles are in the raw bill. Extra ordinary/compiler/outer fees are granted zero cost for this negative bound; no positive construction or full supplier admission is inferred.

Only research/p104-monotone-frame-ceiling/ is added. Start with PROOF.md and verify.py. Exact pending-source words, root contract and notices are retained with their original head/path/blob/SHA256 pins. The offline checker needs only Python 3.12 and the standard library:

python3.12 -B scripts/research_package.py --package research/p104-monotone-frame-ceiling

Both registered modes pass, with both source callers as positive controls and fifteen semantic rejection controls. Five separate optimized-process corruptions are rejected. All 25 committed file bytes/modes, official export integrity, and both read-only Git-free empty-PATH replays pass. The full scientific addendum was frozen at f94fc3f; only scope and validation prose changed afterward. Hosted planning and the complete registered replay both pass at final head 9de3f9183a242715b664ae8747a8540bf6cc38e5 in run41579083999. The completed replay log contains both exact proof passes and the registered-package pass. Final-head export integrity also passes; independent scientific review remains pending. The checkout is shallow; full-history ancestry, Lean, Docker and full native/selected cold replay are unclaimed.

Canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority 8 and selected PR6030 were refreshed before submission. The live PR6529 head remains 44b0d0e8961201ac1656490b4384a7752e1cd9c5. The current 490-PR/6,483-Discussion cache and active claims were checked. General coframes, period-six callers, scalar-word edits and intermediate retirement are separate scopes. This proof does not cover those changed contracts. The user's large complete kappa objective remains unmet; the selected frontier is unchanged.

New source-specific model, proof and checker: Ali Romman with substantial OpenAI Codex assistance; no subagents. Credit Erwan L./PR6453, Rohan Arun/PR6399/6417, DreamingOfClouds/PR6375, Ali Romman/PR6398/6529, Cinna Davis, David Arias, Gareth Davidson, Jacob Alan Sussman, zxv, Cao Yifan and all retained native/compiler/analytic authors. Weak duality and subspace dimension inequalities are classical. Original notices remain byte-exact. Apache-2.0.

Canonical claim and continuation.