[jeremykothe2]

Summary

Conditional κ = 0.001601486955392486. This is +2.27e-7 over PR579 (0.001601260169988325) and +3.28e-7 over our PR578. The conservative model gives 0.001601486952579549.

This PR combines three existing providers with one new provider:

• ck (66 calls): PR576's provider. It is PR571's joint-prefix word plus the 12 extra PR568-style multi-cut cold kernels.
• atm3 (5 calls, new): the same word plus 40 width-5→4 entrance promotions on the A entrances, built with PR569's unchanged build_entrance_promotions.py. The 12 kernels are re-applied after the promotions, and they still give an exact zero dirty response.
• jp8 (1 call): PR575's plain joint-prefix provider, rebuilt from PR575's unchanged build_joint_prefix.

A new literal owner map hosts all 72 calls. The paid profile is {1:174540,2:40064,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-free4f/ contains 17 files. Four 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).

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 or joint_prefix, 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
for n in 568:71c99ac935a33bb7b59a1b4a7af8725a939b0b90 569:897213a855b7fb8a1b8b0e552a2f5c42e6c1b326 \
         571:b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3 575:eac6f7e; do git worktree add --detach ../pr${n%%:*} ${n#*:}; done
python3 -B research/complex-571-free4f/verify.py --work /tmp/571-free4f \
  --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

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): PASS_FREE4F_NATIVE_COMPLEX_AND_CITED_BIT, κ 0.001601486955392486, 38/38 stages exit 0, 371 s. A fresh clone of this commit is byte-identical to the verified package tree, its committed blobs equal its MANIFEST, and its pin check passes. A second official run from that clean clone of commit 747ec97 also passed: PASS_FREE4F_NATIVE_COMPLEX_AND_CITED_BIT, κ 0.001601486955392486, 38/38 stages exit 0, 371 s.

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

Credits

• chafreaky: 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 promotion search, the screening, the owner solve, 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 747ec97129eb85b1e57bf73c934400fe08a8c6cd is incorporated in the reviewed family through #588, published in 9594b61.

The #587 fixture reconstructs this exact declared witness twice (generation and strict replay) and compares all published expected construction/provider/global fields. This is the proposed execution coverage for #582, not a claim to have run its original standalone driver. Full fixture completion and input binding remain required.

Preserved implementation and research:

• research/complex-571-free4f

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.