Repository navigation
Prove the sharp paid-moment floor for independent four-cycles. - #6514
Open
unpaidmoon wants to merge 1 commit into
Open
unpaidmoon wants to merge 1 commit into
unpaidmoon wants to merge 1 commit into
Conversation
Every induced four-cycle on the retained 640-input centre graph raises the paid moment by at least 2(1+7^theta-8^theta) for 0<theta<1, with helper targets fixed. One cycle attains the bound. No kappa change. Prepared by unpaidmoon with substantial Cursor Grok assistance. Co-authored-by: unpaidmoon <unpaidmoon@users.noreply.github.com>
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.
Change and mathematical scope
Every induced four-cycle on the retained 640-input centre graph raises the complete paid moment by at least
2(1+7^theta-8^theta) > 0for0<theta<1, when its four empty charts move independently to nontrivial one-transvection neighbours and every helper target stays fixed. One cycle attains the bound for every such theta. This is a scoped proof with an exact finite certificate. It is not a κ improvement. The selected frontier stays κ = 781451/250000000 from PR6030.The componentwise prefix floor is
(2,2,2,2,2,2,2,0,0). The attaining cycle has vertices10875,10876,10898,10899, walked as(10875,10876,10899,10898), with label 59 at each vertex. Its histogram change is{0:-2,1:2,7:2,8:-2}. The four internal edges stay at rank 0. All 408 productive helper targets and the zero independent centre reward stay fixed. Unknown native, delivery, and restoration costs are outside this bill; the paid side is already strictly worse.Remaining obligations: five-contact blocks, changed routes, changed helper targets, native delivery, restoration, compiler closure, and any decoder of the selected PR6030 word. No supplier is admitted.
Task and overlap
Base:
7c49fe32c55de02c2c873655c804b16e4c3fef0a.Session r86 takes item 9 of the ordered eligible list published with #6337, after dropping delivered handoffs and work already on main, in open PRs, or on a fork
cursor/*branch:p104-side-correction,coverage-law-change).bit-helper-contract).bit-new-register-model.r437-carrier-integration.complex-rank-shape-decoder.complex-new-helper-inventory.#6336 already proved the four-contact tree theorem on this card and left the 62 induced four-cycles unpriced. This package answers that open question. It is distinct from the tree certificate: the tree transform does not apply once a chord identifies two contacts, and the cycle partition is new. Scope is changed. The priced object is the historical retained-centre graph under independent one-transvection charts. PR5693 and PR5698 are different coframe contracts and are not the alphabet used here.
The overlap search on 2026-11-02 covered local notes at this base, open upstream PRs, and discussions. No open PR prices these cycles. The nearest closed predecessor is #6336.
Validation
Python 3.12, standard library, from the repository root:
Observed:
PASS_INDEPENDENT_CENTRE_FOUR_CYCLESwith minima2,2,2,2,2,2,2,0,0, 62 cycles, and 558 literal prefix checks; the same marker under-O;PASS_REGISTERED_RESEARCH_PACKAGEwith outcomenegative-result;PASS_RESEARCH_COMMIT_BYTES. The selected-binding orientation returnedPASS_RESEARCH_BASELINE_BINDINGS_ONLY. That command is not a supplier replay.Not run: native amplitudes, a physical caller, restoration, rounding, a compiler closure, the selected cold replay, Lean, and an outer theorem. All five selected framework assumptions remain.
Credit
Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.
Credit unpaidmoon / PR6336 for the four-contact census, the tree theorem, and the cycle question; Nick Petalas / PR6306 for the three-contact theorem and the paired transform; unpaidmoon / PR6289 for the independent chart question; Chris R / Clear1nsight / PR4867 and PR4888 for the retained graph; Cinna Davis, Cao Yifan, and David Ganz / Dugongue for the retained-centre, native-word, and chart-neighbour lineage. Predecessor files are unchanged.
Open next questions
Can a five-contact tree, or a changed route or helper target, produce a favourable complete bill on this graph? Every connected four-contact block is now priced, and each raises the paid moment, so this is a new endpoint problem. Internal degree is at most 3. Family status treats the four-contact obstruction as a stop. See
research/independent-centre-four-cycles/README.md.Workflow feedback
The filtered order recorded in #6337 made the parallel item numbers repeatable. A one-line pointer from
current-priorities.mdto that filtered list would make the next handoff check easier.