Skip to content

Prove five weight-(2,2,2) column-column orbits and infinitude beyond them (no κ) - #286

Draft
unpaidmoon wants to merge 1 commit into
cursor/upstream-e545235-base-7526from
cursor/column-column-plane-orbits-7526
Draft

unpaidmoon wants to merge 1 commit into
cursor/upstream-e545235-base-7526from
cursor/column-column-plane-orbits-7526

Conversation

@unpaidmoon

Copy link
Copy Markdown
Owner

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. One column plane is classified by a sorted triple of nonnegative integers α ≤ β ≤ γ with α+β ≥ 2. The nonzero weights are α+γ, β+γ, and α+β. There are infinitely many triples.
  • Exhaustive finite census. When both planes have weights (2, 2, 2), there are exactly five orbits: mutual cross (support 6), hooked overlap (support 6), one-sided placement (support 7, pool B of Show two dimension-6 no-edge pools outside the three printed coordina… CrocSwap/integer-mult-bounds#7221), shared foot (support 7), and the printed disjoint pair (support 8). Each such plane is the even-weight code on a 3-set, and the pair support has size 6, 7, or 8. The case split in PROOF.md is the completeness argument. Labeled counts on widths 6, 7, and 8 are 900, 2100, and 1120; widths 5 and 9 contribute 0.
  • Proof of infinitude. With only minimum weight at least 2 required, duplicating one coordinate of the printed pair in pairs of fresh coordinates gives support sizes 8+2k for every k ≥ 0. These are distinct orbits. Pool W of Show two dimension-6 no-edge pools outside the three printed coordina… CrocSwap/integer-mult-bounds#7221, with weights (2, 2, 4) and (2, 2, 2), is a further orbit and collapses if its repeated type is deleted, so it is not one of those duplications.

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 card bit-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:

python3 -B research/column-column-plane-orbits/verify.py
python3 -I -O -B research/column-column-plane-orbits/verify.py
python3 -B scripts/research_package.py --package research/column-column-plane-orbits --check-only
python3 -B scripts/research_package.py --package research/column-column-plane-orbits

Observed locally: PASS_COLUMN_COLUMN_PLANE_ORBITS, PASS_PACKAGE_METADATA_AND_PINS, and PASS_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 in PROOF.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

  1. After deleting, in pairs, every coordinate that duplicates another coordinate in both planes, which orbits still have two minimum-weight-at-least-2 planes? The doubling family reduces to the printed row. Pool W collapses. The first step is one repeated type in a plane whose three type counts are positive.
  2. Is every dimension-6 pool built from two normal-form triples, or from one normal-form triple and one column triple, a coordinate permutation of the witness printed in Prove a no-edge pattern-dimension-4 pool has total image at most 6. CrocSwap/integer-mult-bounds#7139? That is question 2 of Show two dimension-6 no-edge pools outside the three printed coordina… CrocSwap/integer-mult-bounds#7221 and is not taken here.

Workflow feedback (optional)

The open-question list in CrocSwap#7221 was specific enough to finish in one session. No separate workflow note.

Open in Web Open in Cursor 

…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
cursor Bot changed the base branch from main to cursor/upstream-e545235-base-7526 November 11, 2026 13:44
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