Repository navigation
Conditional κ = 0.001625715867072461: jp8-heavy exact owner map on the PR604 cold-ended witness - #614
Merged
Conversation
…the PR604 cold-ended witness
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Conditional κ = 0.001625715867072461. This is +3.51e-7 over PR610 (0.00162536523418317) and +3.43e-6 over our PR609. The conservative model gives 0.001625715864253489.
This PR uses DreamingOfClouds' PR604 cold-ended provider words (
complex-571-cold14ataf8c23b: 14 cold factory-scratch helpers per call ending at 4-dimensional frames, on our PR601 witness) unchanged. Code,cold_endstep, controls and verifier are PR604's, byte for byte. Only the dispatch and literal owner map change:The second provider sits at an even stage on purpose. PR604's
wrong_selected_callassembly control needs each provider's first call to have another provider's call at the same stage parity, and a dispatch with atm3 at stages 0 and 1 fails that control. Because ck is not dispatched, ck is removed from the SPEC's providers and build, as the verifier requires: they must equal the dispatched set. The 114 assembly controls and 23 audit mutations are the full two-provider sets, and strict mode rejects every one.All of PR604's soundness argument applies unchanged. An owner map changes only which helper sits in which owner slot, and PR604's strict physical owner audit, invoice and assembly re-check it from scratch.
Declarative inputs ship in this first commit:
data/WITNESS.json(inputs only);data/EXPECTED.json(expected values, generated by recomputation with generic tools extended to PR604'scold_endstep);data/cand.json(the search-side candidate, package-relative);data/search/(the warm-start map and plan, PR604's template plan, the LP pattern sets and the dispatch);Rebuilding
data/PLAN.jsonfrom the solver output reproduces it byte for byte. One inherited SPEC value is corrected:entering_helper_rolesgoes from 16344 (stale since PR601) to the audited 16584. PR604'sverify.pydoes not read this key.Verification
research/complex-571-cold14-f6/verify.sh /tmp/complex-571-cold14-f6 .. # SOURCE_ROOT holds worktrees pr568 pr569 pr571 pr575 pr583 at the pinned commitsLocal result (Windows, CPython 3.11.11): the commit was preflighted from a fresh clone first (committed blobs equal the MANIFEST, every file LF, pin check passes,
spec.py checkOK). The official run from that clean clone of6cfd7e2then gavePASS_COLD14_NATIVE_COMPLEX_AND_CITED_BIT, κ 0.001625715867072461, 42/42 stages exit 0, 439 s, with no reused baseline or locals. The receipt records MANIFEST sha256 e373aa05…, equal to the committed MANIFEST. Separately, a strict generic verify fromdata/WITNESS.json+data/EXPECTED.jsonpassed (41/41 stages, same κ).GitHub CI has not run, and I make no claim about it.
Credits
cold_end, verifier changes and package), PR599, PR509 and PR516 (Lean).AI disclosure and authorship: Claude Opus 5.5 (Anthropic), running in the omp coding harness, found this dispatch and owner map, built the declarative inputs and prepared the PR. 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 builds on PR604, which is not merged. It is finite exact evidence, not an unconditional theorem, a complete Lean proof, or a practical speedup.