Skip to content

Certify exact paid costs for compressed-word single-level drops (no new κ) - #6475

Open
aliromman wants to merge 1 commit into
CrocSwap:mainfrom
aliromman:codex/hundred-consecutive-results
Open

aliromman wants to merge 1 commit into
CrocSwap:mainfrom
aliromman:codex/hundred-consecutive-results

Conversation

@aliromman

Copy link
Copy Markdown
Contributor

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:

{1:-1, 4:-1, 5:+1, 8:-1, 9:+1}
9^t + 5^t - 8^t - 4^t - 1 > 29/50 > 0

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:

python3.12 -B scripts/research_package.py --package research/compressed-word-drop-invoice
python3.12 -B scripts/check_research_commit.py --package research/compressed-word-drop-invoice --check-source-history

Expected markers: PASS_COMPRESSED_WORD_DROP_INVOICE, PASS_REGISTERED_RESEARCH_PACKAGE, and PASS_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 remains 0.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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant