Skip to content

Prove the sharp paid-moment floor for independent four-cycles. - #6514

Open
unpaidmoon wants to merge 1 commit into
CrocSwap:mainfrom
unpaidmoon:cursor/centre-four-cycle-invoice-5f1b
Open

unpaidmoon wants to merge 1 commit into
CrocSwap:mainfrom
unpaidmoon:cursor/centre-four-cycle-invoice-5f1b

Conversation

@unpaidmoon

@unpaidmoon unpaidmoon commented Nov 3, 2026 •

Copy link
Copy Markdown
Contributor

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) > 0 for 0<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 vertices 10875,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:

  1. Complex helpers (p104-side-correction, coverage-law-change).
  2. BIT (bit-helper-contract).
  3. New decoders and interfaces.
  4. Supplier audit.
  5. All-size audit.
  6. Verification tooling.
  7. bit-new-register-model.
  8. r437-carrier-integration.
  9. This package. complex-rank-shape-decoder.
  10. 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:

python3 -W error -B research/independent-centre-four-cycles/verify.py
python3 -W error -O -B research/independent-centre-four-cycles/verify.py
python3 -B scripts/research_package.py --package research/independent-centre-four-cycles
python3 -B scripts/check_research_commit.py --package research/independent-centre-four-cycles --check-source-history

Observed: PASS_INDEPENDENT_CENTRE_FOUR_CYCLES with minima 2,2,2,2,2,2,2,0,0, 62 cycles, and 558 literal prefix checks; the same marker under -O; PASS_REGISTERED_RESEARCH_PACKAGE with outcome negative-result; PASS_RESEARCH_COMMIT_BYTES. The selected-binding orientation returned PASS_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.md to that filtered list would make the next handoff check easier.

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>
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.

2 participants