Conditional κ = 0.001602080856660739: PR583 frame coalescences on the PR582 three-provider witness

[jeremykothe2]

Summary

Conditional κ = 0.001602080856660739. This is +4.19e-7 over PR583 (0.001601661522127798) and +5.94e-7 over our PR582. The conservative model gives 0.00160208085385131.

This PR applies chafreaky's PR583 six A-prefix frame coalescences (twelve rank-1 payments become six rank-2 payments per call) to the PR582 witness. They go on both kernel-carrying providers:

• ck, 66 calls: PR576's provider (PR571's joint-prefix word plus 12 PR568-style multi-cut cold kernels), plus the six coalescences.
• atm3, 5 calls: the same word plus 40 width-5→4 entrance promotions on the A entrances (PR569's constructor), plus the six coalescences, which apply unchanged.
• jp8, 1 call: PR575's plain joint-prefix provider. It has no coalescible gates.

Frame changes only: scalar operations, helper widths and PR582's literal owner map are all unchanged. The coalescences are applied by PR583's own unchanged build_frames.py constructor, pinned as an external source, with its omission and over-promotion controls. The paid profile is {1:173688,2:40490,3:23928,4:14024,5:4038,6:4032,8:576,30:1,48:1857}.

How it was found

• An LP/MILP screen over free dispatch of {ck, atm3, jp8, e8} gave an upper bound of 0.0016015477. The integer solution chose 66/5/1.
• The owner map comes from an exact-window MILP with the dispatch fixed, warm-started from PR571's owner map. Every solution of that model expands literally through Kőnig colouring, and HiGHS solved it to optimality.

Package

research/complex-571-free4fc/ contains 19 files. Five sources are pinned externally by manifest and file hashes, and nothing is copied from them:

• PR568 (research/complex-multicold, 71c99ac);
• PR569 (research/larger-gain, 897213a);
• PR571 (research/structural-gain, b7bdc5a);
• PR575 (research/complex-joint-prefix, eac6f7e);
• PR583 (research/kernel-frame-coalescing, 89be768).

The package is fully data-driven. data/SPEC.json describes each provider as a typed chain of build steps (pinned base word, then promote, greedy_kernels, joint_prefix or frame_coalesce, each with its paired omission and coverage audits), plus the dispatch, the owner and plan hashes, and every expected value. The single verify.py and code/ contain no witness constants. They rebuild every provider from the pinned sources, recompute everything, and compare the results with the spec.

Verification

PR568, PR569, PR571 and PR575 are not merged, so fetch their pinned commits first:

git fetch origin pull/568/head:pr568 pull/569/head:pr569 pull/571/head:pr571 pull/575/head:pr575 pull/583/head:pr583
for n in 568:71c99ac935a33bb7b59a1b4a7af8725a939b0b90 569:897213a855b7fb8a1b8b0e552a2f5c42e6c1b326 \
         571:b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3 575:eac6f7e 583:89be768; do git worktree add --detach ../pr${n%%:*} ${n#*:}; done
python3 -B research/complex-571-free4fc/verify.py --work /tmp/571-free4fc \
  --source multicold=../pr568/research/complex-multicold \
  --source larger_gain=../pr569/research/larger-gain \
  --source structural_gain=../pr571/research/structural-gain \
  --source joint_prefix=../pr575/research/complex-joint-prefix \
  --source frame_coalescing=../pr583/research/kernel-frame-coalescing

Add --check-pins to check only the package and source pins.

verify.py uses only the standard library. It runs:

• the full PR558 replay;
• each provider's build chain, with all of its omission controls (PR568 multi-cut kernels, PR569 promotions, PR575 joint-prefix coverage and rank-five audits);
• the native chain and exact phase edges for all three providers;
• binding, the physical owner audit (31 mutants), a fresh invoice, both exact moment engines, the 47 strict outer inequalities for each model, 147 assembly controls, and the phase-timing controls.

Local result (Windows, CPython 3.11.11): the commit was preflighted from a fresh clone first (byte-identical to the generated package, committed blobs equal its MANIFEST, pin check passes). The official run from that clean clone then gave PASS_FREE4FC_NATIVE_COMPLEX_AND_CITED_BIT, κ 0.001602080856660739, 40/40 stages exit 0, 393 s.

GitHub CI has not run, and I make no claim about it.

Credits

• chafreaky: PR583 (the six frame coalescences this PR stacks) and PR579 (the 48/24 mix of PR576 kernel calls and PR575 calls showed that kernel calls should dominate), plus PR577, PR572 and PR551.
• jon314159: PR575 (the joint prefix in all calls) and PR567.
• DominikScholz: PR571 (the joint prefix) and PR569 (entrance promotions and their constructor).
• jeremykothe2: PR576, PR578 and PR574.
• eumemic: PR564, PR561, PR562, PR558, PR550, PR543, PR507.
• rohanarun: PR559.
• Dugongue: PR552 and PR514.
• icekylinx: PR535 and PR531.
• DreamingOfClouds: PR484.
• higherbeing: the open allocator.
• lydakis: PR275.
• Douglas Colkitt / CrocSwap: maintenance.
• The original OpenAI Weighted dual-suffix carriers: conditional κ = 7.9961717358e-5 #109 framework.

AI disclosure and authorship: Claude Opus 5.5 (Anthropic), running in the omp coding harness, did the work for this PR: the stacking, the screening, the spec-driven package and this description. Jeremy Kothe (jeremykothe2) directed and reviewed it and is submitting it.

Scope

The result is conditional on the inherited all-size compiler, common-label/mutable-source realization, whole-call hosting, precision/tape/exact recovery, analytic transfer and the bit H1–H5 assumptions. It is finite exact evidence. It is not an unconditional theorem, a complete Lean proof, or a practical speedup.

[Mister-Meeseeks]

Thank you @jeremykothe2. This contribution at e580557d85eb8b8a100361926252d120eb447a44 is incorporated in the reviewed family through #588, published in 9594b61.

Applies six coalescences to each prefix provider selected by the free4f owner map. Width equality permits testing the same map but does not waive fresh local phase, global binding or invoice checks. Historical PR569 source pin requires an explicit source override.

Preserved implementation and research:

• research/complex-571-free4fc

The family review and individual disposition record the scope, evidence and attribution. Parallel and intermediate contributions remain credited even where a later composition has a stronger bound. The published multiplication bound remains conditional on the documented compiler, realization, hosting and analytic assumptions; these finite checks are not a full Lean multiplication proof.