[petalas]

Summary

For complete noncoordinate rank-one-idempotent pools over F2, prove that a three-dimensional off-diagonal pattern space with exactly one matrix-unit edge cannot have an irreducible five-dimensional joint image.

credited PR6782: joint-image dimension <= 5
new: dimension 5 forces the two-dimensional edge space to be invariant
therefore: an irreducible restricted pool has dimension <= 4

This scoped written proof answers CubeJerry's PR #6782, README open question 2. It uses that PR's edge-quotient lemma as a cited premise, without auditing or replaying its result. A separate explicit reducible pool attains joint-image dimension five. The proof and verifier were produced by Nick Petalas. Credit CubeJerry, Nick Petalas's #5921 fiber lemma, woklerx's #1456/#1846 framework and the retained scalar-register lineage.

Package: research/one-edge-pattern-reducibility/. Scientific base: 7c49fe32c55de02c2c873655c804b16e4c3fef0a. Direct predecessor: #6782 at 685457252b51b9c7932ece363365bdf0b12c9c31, with its proof URL and SHA256 in ORIGINS.json. Advance CLAIM.

Evidence

Before, the cited source left irreducible five-dimensional one-edge cores open. The new equality argument excludes every such core at arbitrary ambient width under the credited quotient premise.

Local CPython 3.12.15 normal and optimized checks pass. At fixed edge E01, complete equality-relevant enumeration finds 1030 one-edge spaces at width five and 6576 at width six, including respectively 30 and 328 dimension-five spaces. Every dimension-five space preserves the edge space. These are spaces with all three nonzero quotient cosets realized, not all pattern spaces or conjugacy classes. The complete five-projector equality fixture and seven negative controls pass.

Both registered checks passed locally, individually timed at 0.097s and 0.101s to check the replay budget. Package metadata, committed bytes and declared source history pass at 5dbf2c05220bea53d84b510efe5910c4cec8f182. Official export/input-coverage checks and both read-only Git-free direct replays pass. Syntax and indentation diagnostics pass. The verifier emits generated receipts bound to package-file SHA256 hashes.

Reproduce from the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/one-edge-pattern-reducibility/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/one-edge-pattern-reducibility/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/one-edge-pattern-reducibility
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/one-edge-pattern-reducibility --check-source-history

Any CPython 3.12 executable can replace this installation path. The standalone verifier uses only the standard library.

Limitations and unrun obligations

The claim type is a scoped proof with finite corroboration. The pending PR6782 edge-quotient lemma is an imported mathematical premise, not independently verified here. Its public proof is separately pinned in ORIGINS.json; it is neither an executable dependency nor part of the declared Git-history preflight.

The field is F2, the pattern dimension is three, and coordinate projectors are excluded. Additional coordinate calls or other patterns in a word can destroy the invariant edge space. Attainment of the irreducible dimension-four bound is not claimed. Lower-dimensional words, zero-edge pools, rational frames, native realization, arbitrary dirty-state restoration and complete physical/cost/precision/compiler/outer obligations remain open. No new κ, paid/target invoice, supplier admission, selected operator replay, proof-kernel result or complete multiplication theorem is claimed. The five selected assumptions remain.

Open next questions

• Can a one-edge core of dimension at most four yield a three-relation diagonal word with target rank above paid rank? First specify one scalar alphabet and relation lattice; the present pool theorem supplies neither chronology nor rational frames.
• What is the sharp irreducible joint-image bound for zero-edge three-dimensional pattern spaces? Start with one explicit configuration from PR6782 question 2; this proof needs a nonzero edge space.

Related open work

• Bound binary pattern cores and exclude the irreducible five-type saving (no new κ) #6782 supplies the edge-quotient premise, a distinct two-edge irreducible five-dimensional example and its word obstruction. This result closes its one-edge five-dimensional question without replaying those results.
• Prove the two-relation rank bound at arbitrary helper width (no new κ) #6777 proves the arbitrary-width two-relation word-rank bound. This package studies three-dimensional pattern pools and proves no word-rank inequality.

The post-CI related-work refresh read the eight other open account PRs created since the CLAIM, #6786 through #6793. None studies the same one-edge pattern-pool object or joint-image quantity, and no new same-quantity comparison is required.

CI notes

At head 5dbf2c05220bea53d84b510efe5910c4cec8f182, run 42222922550 passed both plan and replay (research/one-edge-pattern-reducibility). The registered package replay certified both normal and optimized finite checks. All local checks above also passed. CI execution does not establish the unbounded theorem or independently validate the imported edge-quotient premise.

Merge Danger

Door: two-way

Blast Radius: isolated

Adds only the seven files in research/one-edge-pattern-reducibility/.