Conditional κ = 0.001596133352130093: seven more cold-kernel helpers on PR564

[jeremykothe2]

Summary

This is a small extension of eumemic's PR564. It raises the conditional κ from 0.001593134158181640 to 0.001596133352130093 (+2.999e-6). Nearly all of the construction and all of the verification machinery come from the earlier PRs credited below.

PR564 (following PR561) makes one width-nine helper per complex call "cold". An exact dyadic donor relation cancels its dirty response, so it enters at rank one and its residual width drops from nine to eight. This PR finds seven more such helpers per provider, for eight in total. Then it re-solves the owner packing for the new width inventory. Most of the gain comes from the repacking, as in PR564.

This PR adds a single self-contained package, research/complex-multicold/, on top of current main. It vendors PR558 and PR559 unchanged, as PR564 does. Its new and changed parts relative to PR564's research/complex-allcold/ are these 16 files:

• New:
  • code/build_multicut_kernels.py
  • code/audit_multicold_controls.py
  • data/{ZERO,FOUR,EIGHT}-MULTICOLD.json
• Changed:
  • verify.py
  • code/assemble.py
  • code/assembly_controls.py
  • code/audit_allcold.py
  • code/bind_providers_portable.py
  • data/OWNERS.json.gz
  • data/PLAN.json
  • proof/CONSTRUCTION.md
  • README.md, NOTICE.md, MANIFEST.json

All other files are byte-identical to PR564's package.

Construction

A B-first width-nine helper is untouched before its first original gate. Up to that point it holds only its initial dirt. Its cancelling gates donor += -q·pivot @E can therefore sit at different cuts, with each donor at a cut where its frame fits (cur ⊆ E ⊆ next). The dirty response is zero exactly when the sum, over donors, of q times that donor's suffix column at its cut equals the pivot's column. PR564's search used a single cut and finds no new relations. The multi-cut search finds seven:

• Helper-donor kernels: helpers 282, 294 and 306 (registers 506@[24], 518@[30], 530@[30]). Local profile delta: {1:+1,2:+2,3:-2}.
• Target-donor kernels: helpers 271, 283, 295 and 307 (registers 495@[24], 507@[24], 519@[30], 531@[30]). These are placed only after the centre scatter, mirroring the post-centre gauge compensation. Local profile delta: {1:+3,2:+1,3:-2}.

Each of the 16 post-centre helpers needs one specific partner as its split donor. They pair up as (494,566), (506,578), (518,542), (530,554), (495,567), (507,579), (519,543) and (531,555). So this family supports at most eight cold helpers per word. We found no kernel by any of these mechanisms for the 276 helpers first touched before the centre.

Overlap with PR567. PR567 (jon314159), opened shortly before this PR, independently found one of these seven kernels: helper 294 (register 518@[30], split donor 542). It places that kernel at a single cut, where we use multiple cuts. The other six kernels and the eight-helper owner repacking are not in PR567.

PR562's 15/2/55 dispatch is unchanged. The width inventory becomes {4:p,5:56-p,8:164,9:284}. The owner assignment was found as follows:

• an aggregate CP-SAT model with per-call Hall conditions, adapted from higherbeing's open allocator;
• then a per-pattern Kőnig edge colouring, as in the existing partial-own-coordinated script.

Neither tool is an admission dependency; the verifier checks the literal assignment. The idle profile is {1:93,2:93,3:2118,7:1,48:1713}, compared with PR564's {3:2364,7:172,48:1668}.

The paid profile is {1:167741,2:31741,3:34502,4:13696,5:4032,6:4032,7:1,8:576,48:1713}. The figures are: live stock 7168, physical stock 7682, rank mass 520704, deficit 2560. The complex rate is b = 0.00159868506668458107128. eumemic's unchanged PR543 bit supplier gives c = 0.001653826988146798944268, so the complex side binds. A conservative complex model gives κ = 0.001596133349380077.

Verification methodology

python3 -B research/complex-multicold/verify.py --work /tmp/multicold-replay

The verifier is PR564's, extended to cover the new kernels. It uses the standard library only, and assertions must stay enabled. In order, it:

1. Rebuilds frozen PR558, the four-pivot source and PR564's three one-cold words, with their cold-kernel omission controls.
2. Applies the seven multi-cut kernels to each provider word. It checks:
   • exact zero dirty response by forward replay;
   • legal frame chains;
   • the pinned profile delta.
     It runs 32 omission controls per provider: every new gate alone and every whole kernel, in both orientations. Each must fail.
3. Re-runs the inherited 44-kernel and promotion omission audits on each final word, then checks:
   • all 728 scalar columns in both orientations;
   • all 504 dirty helpers restored;
   • both reflected ledgers;
   • all 2929 phase edges and 224 endpoint adapters per provider;
   • the normalized wrappers.
4. Binds the three providers and checks the physical owner assignment:
   • all 36,288 helpers have a single whole owner;
   • 3,209 chart types;
   • 27,679 cross-replica roles;
   • 4,018 idle remainders;
   • 16 controller mutants, each of which must be rejected.
5. Emits a fresh invoice and runs both exact assembly models with 54 malformed-receipt controls. Two rational moment engines reject the adjacent supplier endpoint. It also runs seven bootstrap levels and 47 strict outer inequalities, with next-grid and parameter controls.

Verification results

All runs were local, on Windows with Python 3.11.

Run	Tree	Status	κ	Steps	Time
1	stacked on PR564 (aa70965)	PASS_THREE_PROVIDER_048_MULTICOLD_NATIVE_COMPLEX_AND_CITED_BIT	1596133352130093/10^18	42/42 exit 0	357 s
2	same package, independent worktree	same PASS	same	42/42 exit 0	356 s
3	this PR's tree (main db0e57b + 71c99ac)	same PASS, process exit 0	1596133352130093/10^18	42/42 exit 0	353 s

The paid profile in every run equals the one stated above. GitHub CI has not run, and I make no claim about it.

Credits

This builds directly on:

• eumemic:
  • PR564 (all-call cold kernels, c18417b), the base of this work.
  • PR561 (the cold-kernel idea).
  • PR562 (zero/four/eight providers and owners).
  • PR558 (rank-five pivots).
  • PR550 (rank-five trace expansion).
  • PR543 (bit supplier, cited).
  • PR507 (partial-own factory).
• jon314159: PR567 (independently found the register-518 cold kernel, posted first).
• rohanarun: PR559 (native complex moment).
• Dugongue: PR552 (collective hyperplane waves) and PR514 (asynchronous whole owners).
• chafreaky: PR551 (subspace16 complex).
• icekylinx: PR535 (post-centre rank-four kernels), PR531, and the compiler and controller.
• DreamingOfClouds: PR484 (shared-donor kernels and entrance gauges).
• higherbeing: the open allocator.
• lydakis: PR275 (finite assembly and E8 verification).
• Douglas Colkitt / CrocSwap: maintenance and the review framework.
• The authors of the original OpenAI Weighted dual-suffix carriers: conditional κ = 7.9961717358e-5 #109 framework, on which all of this is conditional.

All vendored packages, notices, licenses and AI disclosures are unchanged.

AI disclosure and authorship: Claude Opus 5.5 (Anthropic), running in the omp coding harness, did the work for this PR. A small team of Claude agents found the seven multi-cut kernels, wrote the constructor and omission audit, solved the new owner assignment, built and verified the package, and drafted this description. Jeremy Kothe (jeremykothe2) directed and reviewed the work 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 71c99ac935a33bb7b59a1b4a7af8725a939b0b90 is incorporated in the reviewed family through #588, published in 9594b61.

Multi-cut donors read a pivot that retains its initial dirt before its original touch. Cancellation is an exact sum of dyadic response columns at their own cuts. Target donors and helper donors require their individual chronology; complete scalar restoration, native phases and allocation are checked separately.

Preserved implementation and research:

• research/complex-multicold

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.