Repository navigation
Conversation
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.
Scoped negative result: after PR #5350's 151-ADD compression, no forward single-level drop in the PR #5426 move class lowers the complete paid moment for
99/100 <= t <= 1. This completes Nick Petalas's released handoff and closes a specific route to reduce fragmentation. No new kappa or selected-frontier change.Proof and exact scope, complete receipt, verifier, source pins, and registered commands are pinned to
c9f27ddbee648bc190696ecfcd2370fbf4b55d3c.All 518,315 plans across 2,526 levels are accounted for: 513,971 fail a necessary dependency condition, 4,336 fail acyclicity, and eight survive. Every surviving plan has the same exact paid delta:
The exponent interval is certified with integer arithmetic, using
100^100 > 9*97^100. Every productive endpoint remains fixed. Omitting the centre constraint admits 51 cheaper moves; that is a relaxed control, not a supplier construction.The new checker independently builds the static operation/level graph and runs Kahn deletion for every plan that passes dependency pruning. It agrees with the retained dynamic method on all 4,344 exact-model and 4,341 relaxed-model candidates. The package imports PR #5426's source parser and option definitions; it does not claim independent coverage of those semantics. Complete feasible histograms include all 632 fields, partner insertions and changed centre ranks. The corrected cost expression was already in the handoff; the contribution is its completed source-bound receipt and independent graph check.
Reproduction and evidence
Python 3.12, standard library only, from the repository root:
Expected markers:
PASS_COMPRESSED_WORD_DROP_INVOICE,PASS_REGISTERED_RESEARCH_PACKAGE, andPASS_RESEARCH_COMMIT_BYTES.Local checks run on macOS arm64 with CPython 3.12.13: the complete normal and optimized registered replays; exact source and generated-word hashes; every feasible histogram; static/dynamic graph agreement; centre-free control; false climb-rank, cycle, withdrawn-expression and missing-centre-charge rejection. Metadata and all 11 committed package/input files pass. All declared source commits are ancestors. The official export passes integrity and coverage for all five inputs. A separate full direct replay also passed with CPython 3.15.2. Hosted CI will be reported separately.
The base and all five consumed source files are pinned to canonical main
7c49fe32c55de02c2c873655c804b16e4c3fef0a. This is the historical PR #4610/PR #5350 word, not selected PR #6030. Priority revision 8 guides the task. Current selected kappa remains0.003125804, with all five framework assumptions retained.Scope and credit
The proof fixes the operation set, native maps, coefficients, field endpoints, monotone chains and centre delivery at frame zero. It removes one level at a time; revisiting fields and native-warp frames remain fixed. It covers the forward direction only. Simultaneous removals, a new scalar word or changed centre delivery require a new complete cost calculation. No native-phase, compiler, precision, stock, BIT, outer or selected cold replay was run. No independent human or formal proof-kernel review is claimed.
Mark / @Matarener supplied the move model, original-word result and compressed-word question in PR #5426. @ahrazzle supplied the compressed word in PR #5350, using Cinna Davis / @1337isnot1337's methods from PR #4692. Cao Yifan / @intqwq supplied the native word in PR #4610. @DreamingOfClouds supplied fragmentation accounting in PR #5226. Nick Petalas / @petalas supplied the corrected unpublished lead in the linked handoff. Credit also Dugongue, zxv, Jacob Alan Sussman and the retained centre/native/controller lineage. Source notices remain intact. Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0.
Advance claim. Live PR bodies and all paginated Discussions were checked, with relevant source notes read from pinned main. Sparse local notes, arbitrary historical diffs and unpublished work remain coverage limits. This is one scoped contribution, not one result per candidate or control. Open next: one fully priced coupled removal, outside the exhausted single-level class.