[unpaidmoon]

Change and mathematical scope

A complete no-edge pool of binary rank-one idempotents whose off-diagonal pattern space has dimension 4 has joint image of dimension at most 6. Dimension 6 is attained, and the action is reducible there. The largest irreducible joint image therefore has dimension at most 5. The pool in CrocSwap#7094 attains 5 and is rechecked here.

This is a scoped all-width proof, together with an exhaustive census of the 5005 six-point subsets of F2^4 and an exhaustive census of the 168 elements of GL(3,2). It is not a search. No new κ. The selected frontier stays 781451/250000000.

The result uses completeness, the absence of matrix units, and pattern dimension exactly 4. It does not bound pattern dimension 5, and it does not price a word.

Task and overlap

Base commit: f16923d466a6aba912299882e0545564d2ba7bb2.

Task card: bit-new-register-model, priority revision 8. Scope status: changed. The card asks for a new register alphabet. This package answers the open question of CrocSwap#7094: whether a complete no-edge pool of pattern dimension 4 can act irreducibly on a joint image of dimension 6 or more. The answer is no. The same card was already moved to scalar pattern-pool questions by CrocSwap#5921, CrocSwap#6838, CrocSwap#6921, CrocSwap#6962, and CrocSwap#7094.

Nearest overlap, from a search on 2026-11-10 of 406 open and 6175 closed PR records and 7014 discussion records:

• Prove sharp binary pattern-pool cardinality (no new κ) CrocSwap/integer-mult-bounds#5921 is the fiber lemma (Nick Petalas).
• Prove sharp zero-edge image bound four and universal rank-three bound six (no new κ) CrocSwap/integer-mult-bounds#6838 is the total-image bound 4 for pattern dimension at most 3, including Lemma 3 (CubeJerry).
• Prove the no-edge irreducible joint-image bound is 3. CrocSwap/integer-mult-bounds#6921 classifies no-edge triples and proves the irreducible bound 3.
• Show the no-edge irreducible bound fails in pattern dimension 4. CrocSwap/integer-mult-bounds#6962 attains irreducible dimension 4.
• Show a no-edge pattern-dimension-4 pool has irreducible joint image 5. CrocSwap/integer-mult-bounds#7094 attains irreducible dimension 5 and leaves dimension 6 open. Head b5f0a0df3d22e8ad40d67d6be4d1c7ff24d180c5.
• Bound binary pattern cores and exclude the irreducible five-type saving (no new κ) CrocSwap/integer-mult-bounds#6782 is the edge-quotient bound and Exclude irreducible five-dimensional one-edge binary pattern pools CrocSwap/integer-mult-bounds#6785 is a one-edge exclusion. Neither is this no-edge dimension-4 question.

No match is not a novelty certificate. Open upstream PRs through CrocSwap#7105 do not take this question. The original native acceptance gate remains unmet.

Validation

Evidence class: a written all-width proof. The finite parts are the six-point census and the GL(3,2) census, both exhaustive on finite domains, plus complete pool scans of four explicit witnesses. Those scans are not a search over all four-dimensional pattern spaces.

From the repository root, Python 3.12, standard library only:

python3 -B research/no-edge-dim4-image-at-most-six/verify.py
python3 -I -O -B research/no-edge-dim4-image-at-most-six/verify.py
python3 -B scripts/research_package.py --package research/no-edge-dim4-image-at-most-six --check-only
python3 -B scripts/research_package.py --package research/no-edge-dim4-image-at-most-six

The verifier prints PASS_NO_EDGE_DIM4_IMAGE_AT_MOST_SIX. Both registered commands passed in this environment.

Not run: Lean, Docker, the selected-baseline scientific replay, and any enumeration of all 4-dimensional pattern spaces. The selected record was read only to confirm κ is unchanged.

Credit

The fiber lemma is Nick Petalas, CrocSwap#5921. The total-image bound and Lemma 3 are CubeJerry, CrocSwap#6838. The triple classification and the irreducible bound 3 are CrocSwap#6921. The dimension-4 irreducible 4-cycle is CrocSwap#6962. The dimension-5 witness rechecked here is CrocSwap#7094. Prepared by unpaidmoon with substantial Cursor Grok assistance. New work is Apache-2.0.

Open next questions

1. Does a complete no-edge pool of pattern dimension 5 still have total joint image at most 6, and can its irreducible image exceed 5? The parity construction one dimension higher already has total image 6, and the edge-quotient bound only gives 31.
2. Is every dimension-6 pool a coordinate permutation of one of the three witnesses? The dimension bound does not need that list.
3. After a valid relation split, does irreducible dimension at most 5 change a three-relation paid-rank obstruction? This remains question 1 of Prove the no-edge irreducible joint-image bound is 3. CrocSwap/integer-mult-bounds#6921. The split hypotheses are not proved here.

Workflow feedback (optional)

CrocSwap#7094 named the missing dimension exactly, which kept the session on one bound instead of a new alphabet. A link to the feedback discussion is enough: CrocSwap#1200