Repository navigation
Conditional κ = 0.001602278921983212: two gate-move frame coalescences on PR584 - #588
Conversation
…83 six plus two gate-move coalescences) on the PR582 three-provider witness
…d PR586 controls (same kappa)
|
Thank you @jeremykothe2. This contribution at Gate moves pass pairwise transvection commutation; raising frames follows moves, cleanup regenerated and responses invariant. Must still validate native frames/phases/owner contracts and full bill. Full original cold replay passed with all provider chains; the integrated public cold command is running separately. Preserved implementation and research: 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. |
|
Independent check: the ck, atm3 and jp8 words are coalescence-optimal under single gate moves and frame changes. I rebuilt the three provider words from the pinned sources (ck content sha
So the next local-word tick needs a transformation other than reordering commuting gates and sliding frames along the existing chains. For orientation, the paid climbs of ck by (section, class, rank): A-phase helpers rank 1 14 %, B-phase helpers rank 1 13 % and rank 2 13 %, B-phase targets rank 1 8 %, final helper climbs 8→9 5 %. Script: |
Summary
Conditional κ = 0.001602278921983212. This is +1.98e-7 over our PR584 and PR586 (0.001602080856660739) and +6.17e-7 over PR583. The conservative model gives 0.001602278919174953.
This PR is PR584 plus two new frame coalescences in block 25 of the A prefix, on both kernel-carrying providers (ck, 66 calls; atm3, 5 calls):
x491 += x490at frame [25]) commutes past A34 and A35, which share its source 490 but have different targets. Moved after them, it can be raised to frame [96,25].PR583's search missed these because neither gate was its pivot's last gate. Each merge turns two rank-1 payments into one rank-2 payment per call, so the change is {1:−4, 2:+2} per call on top of PR583's six coalescences. Scalar operations and responses are unchanged, as are helper widths and PR582's literal owner map.
The moves are applied by a new typed build step,
gate_move_coalesce(code/build_gate_moves.py). For every move it checks commutation, unchanged dirty responses and widths, and the cleanup rule. It has omission, over-promotion and unmoved-raise controls, and each control must be rejected. The paid profile is{1:173404,2:40632,3:23928,4:14024,5:4038,6:4032,8:576,30:1,48:1857}.How it was found
Package
research/complex-571-free4fc8/contains 22 files. Five sources are pinned externally by manifest and file hashes, and nothing is copied from them:research/complex-multicold,71c99ac);research/larger-gain,897213a);research/structural-gain,b7bdc5a);research/complex-joint-prefix,eac6f7e);research/kernel-frame-coalescing,89be768).The package is fully data-driven.
data/SPEC.jsondescribes each provider as a typed chain of build steps (pinned base word, thenpromote,greedy_kernels,joint_prefix,frame_coalesceorgate_move_coalesce, each with its paired omission and coverage audits), plus the dispatch, the owner and plan hashes, and every expected value. The singleverify.pyandcode/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:
Add
--check-pinsto check only the package and source pins.verify.pyuses only the standard library. It runs: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_FREE4FC8_NATIVE_COMPLEX_AND_CITED_BIT, κ 0.001602278921983212, 42/42 stages exit 0, 391 s.Update (commit 6d0e53b, same κ): the package is hardened with PR586's portable decompressed-content identity checks and controls (3 recompressions accepted; 27 semantic and 27 reference/metadata mutations rejected), and its width metadata is now recomputed from the actual widths. Owner map, profile and κ are unchanged. The official run from a clean clone of 6d0e53b passed:
PASS_FREE4FC8B_NATIVE_COMPLEX_AND_CITED_BIT, κ 0.001602278921983212, 43/43 stages exit 0, 445 s.GitHub CI has not run, and I make no claim about it.
Credits
AI disclosure and authorship: Claude Opus 5.5 (Anthropic), running in the omp coding harness, did the work for this PR: the coalescence search, the gate-move build step, 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.