Conditional κ = 0.001601159251759369: improved literal owner map for the three-provider PR571 prefix witness

[jeremykothe2]

Summary

Conditional κ = 0.001601159251759369. This is +6.92e-8 over our PR576 (0.00160109005167629), +4.77e-7 over PR571 and +3.89e-7 over PR575. The conservative model gives 0.001601159248973933.

This is the same three-provider construction as PR576 (same providers, dispatch and code) with an improved literal owner map found by literal large-neighbourhood search. Only data/PLAN.json, data/OWNERS.json.gz, data/WITNESS-SPEC.json and MANIFEST.json differ from PR576's package.

The construction keeps DominikScholz's PR571 joint-prefix word and adds three providers:

• P571 is PR571's prefix width-seven word, unchanged. It runs on 54 calls.
• P571K is PR571's prefix word plus 12 further PR568-style multi-cut cold kernels, which take 12 helpers from width nine to eight. It runs on calls 0–7. Eight of the kernels are A-first kernels that become legal only after PR569's promotions raise their first frames to rank two. The other four are B-first kernels.
• E8 is PR568's eight-cold eight-pivot provider. It runs on 10 calls: 8, 13, 17, 26, 36, 41, 45, 48, 53 and 54.

A new literal owner map hosts all 72 calls. The paid profile is {1:169688,2:40193,3:26376,4:13824,5:4032,6:4032,8:576,30:1,48:1817}.

How it was found

• The kernels came from an exact sparse dyadic relation search (Rust, i128 replay). Each one was rebuilt with PR568's build_multicut_kernels.py, with an exact zero dirty response.
• An LP/MILP packing screen chose the dispatch.
• The owner map comes from a fixed-dispatch per-window MILP, warm-started from PR571's owner map. It used lazy cross-time Hall cuts and a local-repair sub-MIP that frees only the windows that cannot yet be decomposed, followed by Kőnig realization.

Package

research/complex-571-three-provider-f1/ contains 16 files. PR568 (research/complex-multicold, 71c99ac) and PR571 (research/structural-gain, b7bdc5a) are pinned external sources, and nothing is copied from them.

The global stage is driven by data. code/ reads every expected value from data/WITNESS-SPEC.json: providers, dispatch, the owner and plan hashes, the profile and κ. It recomputes each value from the words, owners and engines and compares it with the spec. No witness constants appear in code. The audit and assembly mutation controls are generated per provider: 31 owner mutations and 147 assembly controls, each of which must be rejected.

Verification

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

git fetch origin pull/568/head:pr568 pull/571/head:pr571
git worktree add --detach ../pr568 71c99ac935a33bb7b59a1b4a7af8725a939b0b90
git worktree add --detach ../pr571 b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3
python3 -B research/complex-571-three-provider-f1/verify.py --work /tmp/571-3prov \
  --multicold ../pr568/research/complex-multicold \
  --structural-gain ../pr571/research/structural-gain

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

• the full PR558 replay;
• the E8 build with all of PR568's omission controls;
• the P571 local, rebuilt from PR571's pinned word and checked byte for byte against PR571's retained local;
• P571K, built from PR571's word with PR568's constructor, followed by 48 multi-cut omission controls;
• the native chain and exact phase edges for all three providers;
• the spec-driven bind, the owner audit (31 mutants), a fresh invoice, both exact moment engines, the 47 strict outer inequalities for each model, the 147 assembly controls and the phase-timing controls.

Local result (Windows, CPython 3.11.11): PASS_PR571_PREFIX_WORD_PREFIXK_AND_PR568_EIGHT_COLD_THREE_PROVIDER_NATIVE_COMPLEX_AND_CITED_BIT, κ 0.001601159251759369, 31/31 stages exit 0, 353 s. The verified package tree is byte-identical to this commit.

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

Credits

• DominikScholz: PR571 (the joint prefix, its composition and global code) and PR569 (the width-seven promotions, which also make the eight A-first kernels legal).
• jon314159: PR575 and PR567.
• jeremykothe2: PR576 and PR574 (the three-provider construction this map hosts).
• chafreaky: PR572 and PR551.
• 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 kernel search, 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 2aacc1f2edae76fc963699be5cfaf31bcf3ef56b is incorporated in the reviewed family through #588, published in 9594b61.

Retains the three-provider scalar mechanism while changing the literal assignment. Assess the resulting reconstructed idle profile, not solver-reported objective alone.

Preserved implementation and research:

• research/complex-571-three-provider-f1

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.