Repository navigation
Prove five weight-(2,2,2) column-column orbits and infinitude beyond them (no κ) - #286
Draft
unpaidmoon wants to merge 1 commit into
Draft
unpaidmoon wants to merge 1 commit into
unpaidmoon wants to merge 1 commit into
Conversation
…them. Classify F2 column planes of minimum weight at least 2 whose image spaces meet only at 0. The weight-(2,2,2) case is an exhaustive five-orbit census; the wider family is infinite by an explicit doubling construction. No kappa change. Co-authored-by: unpaidmoon <unpaidmoon@users.noreply.github.com>
cursor
Bot
changed the base branch from
main
to
cursor/upstream-e545235-base-7526
November 11, 2026 13:44
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
Proof and exhaustive finite census, with no κ change. The selected frontier stays
363005817/100000000000.Over F2, a column plane is a 2-dimensional space supported off its column, with every nonzero vector of weight at least 2. Its image is the column plus that plane. This package classifies pairs of such planes whose image spaces meet only at 0, up to coordinate permutation.
PROOF.mdis the completeness argument. Labeled counts on widths 6, 7, and 8 are 900, 2100, and 1120; widths 5 and 9 contribute 0.This does not classify the normal-normal or mixed geometries, and it does not list every minimum-weight-at-least-2 orbit. No word is priced. The five framework assumptions of the selected record are unchanged.
Task and overlap
Base commit
e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8. Catalogue cardbit-new-register-model. Scope status: changed. The card asks for a new register alphabet. This package answers open question 1 of CrocSwap#7221, which is the column-column half of the coordinate classification left open by CrocSwap#7139. The same card was already moved to this scalar pattern-pool model by CrocSwap#5921, CrocSwap#6838, CrocSwap#6921, CrocSwap#6962, CrocSwap#7094, CrocSwap#7138, CrocSwap#7139, and CrocSwap#7221.Nearest work: CrocSwap#7138 prints one weight-(2, 2, 2) column-column witness; CrocSwap#7139 asks whether every dimension-6 pool is a coordinate permutation of one of three witnesses; CrocSwap#7221 separates two further pools, W and B, and leaves the orbit list open. This package takes that list. It does not take question 2 of CrocSwap#7221.
Upstream main was re-fetched at submission and was still
e54523517d0f03e58352e647c403a5af3e525a57. A GitHub search of open PR titles and bodies on 2026-11-11 found this question only in CrocSwap#7138, CrocSwap#7139, and CrocSwap#7221.Validation
Python 3.12, standard library only. From the repository root:
Observed locally:
PASS_COLUMN_COLUMN_PLANE_ORBITS,PASS_PACKAGE_METADATA_AND_PINS, andPASS_REGISTERED_RESEARCH_PACKAGE. The verifier exhausts the weight-(2, 2, 2) domain, rejects two overlaps excluded by the case split, checks the doubling family for k = 0 through 4, and checks pool W. It does not enumerate planes of unbounded support; infinitude is the explicit family inPROOF.md. The selected baseline was not replayed. No Lean, Docker, or historical suite was run.Credit
The fiber lemma is Nick Petalas, CrocSwap#5921. The total-image bound and Lemma 3 are CubeJerry, CrocSwap#6838. The triple classification is CrocSwap#6921. The dimension-4 irreducible 4-cycle is CrocSwap#6962. The dimension-5 witness is CrocSwap#7094. The weight-1 bound and its printed dimension-6 column witness are CrocSwap#7138. The three printed dimension-6 witnesses are CrocSwap#7139. The question answered here, and pools W and B, are CrocSwap#7221. Prepared by unpaidmoon with substantial Cursor Grok assistance. New work is Apache-2.0. Independent human and formal proof-kernel review are unclaimed.
Open next questions
Workflow feedback (optional)
The open-question list in CrocSwap#7221 was specific enough to finish in one session. No separate workflow note.