Prove the no-edge irreducible joint-image bound is 3.

research/no-edge-irreducible-image/README.md

@@ -0,0 +1,87 @@
+# No-edge irreducible joint image
+
+**Result.** For a complete no-edge pool of binary rank-one idempotents whose
+off-diagonal patterns span a space of dimension at most 3, the joint image is
+either of dimension at most 3, or of dimension 4 and reducible. Dimension 3
+is sharp at every ambient width. **No new κ.** The selected value remains
+`781451/250000000`.
+
+## Scope and evidence
+
+Catalogue card: `bit-new-register-model`, priority revision 8, base commit
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. Scope status: **changed**. The card
+asks for a new register alphabet. This package answers the scalar question left
+open by #6838: can such a pool act irreducibly on a four-dimensional joint
+image? It cannot. The reason is recorded in [TASK.json](TASK.json). The
+original native acceptance gate is unmet, and the selected frontier is
+unchanged.
+
+[PROOF.md](PROOF.md) is the all-width argument. It uses the fiber lemma from
+#5921 and the total-image bound dim V ≤ 4 from #6838 as inputs. The new step
+is the reducibility of every four-dimensional no-edge image, together with an
+explicit irreducible three-dimensional example. A four-pattern cap is handled
+by an idempotent gram matrix. Every other four-dimensional pool contains either
+a column triple, whose odd covectors span at most three dimensions, or a
+normal-form triple, which leaves an invariant line or hyperplane.
+
+The sharp example, on coordinates 0, 1, 2, 3, is
+
+```text
+N0 = e0 (e0+e1+e2)^T
+N1 = e1 (e0+e1+e3)^T
+N2 = e2 (e0+e2+e3)^T
+```
+
+Its pattern space is three-dimensional and contains no matrix unit. Both
+factors of every realizable projector are supported on these four coordinates,
+and the only realizable projectors are the three above. Their action on
+span(e0, e1, e2) has no invariant line or plane.
+
+[verify.py](verify.py) repeats the parts of the argument that are finite:
+all 168 elements of GL(3, 2), the exact pool on four coordinates and the
+one-bit extension, the seven four-point caps, and negative controls. The
+parity pool from #6838 is reducible. The normal-form triple by itself is
+reducible. Deleting one sharp projector leaves an invariant line. These checks
+do not replace the width-independent case analysis.
+
+Source pins are in [SOURCES.json](SOURCES.json). The catalogue and selected
+record are provenance at the base commit. Full Git history is needed to
+resolve them. Nothing here reruns the selected baseline as a scientific
+replay.
+
+## Reproduce
+
+From the repository root, with Python 3.12 and the standard library only:
+
+```sh
+python3 -B research/no-edge-irreducible-image/verify.py
+python3 -I -O -B research/no-edge-irreducible-image/verify.py
+python3 -B scripts/research_package.py --package research/no-edge-irreducible-image --check-only
+python3 -B scripts/research_package.py --package research/no-edge-irreducible-image
+```
+
+The verifier prints `PASS_NO_EDGE_IRREDUCIBLE_IMAGE`.
+
+## Open next questions
+
+1. **Word accounting after a valid split.** Does bound 3 improve the paid-rank
+   obstruction for a three-relation word once the relation, cube-span, and
+   coordinate-call hypotheses of #6777 and #6782 are in force? The scalar
+   theorem does not supply that split. The smallest next step is to state
+   those hypotheses and only then count endpoints.
+
+2. **Pattern dimension 4.** Does an irreducible no-edge pool of pattern
+   dimension 4 exist, and what is its joint-image dimension? The Fano-plane
+   case split stops at pattern dimension 3. #6838 already notes that the
+   parity construction one dimension higher has total joint image 5. The
+   smallest next step is to decide whether that example is irreducible.
+
+## Credit
+
+Nick Petalas, #5921, for the fiber lemma and the joint-image question.
+CubeJerry, #6838, for the sharp total-image bound 4 and for isolating the
+irreducible question; #6782 for the edge-quotient context. #6785 asks the
+zero-edge irreducible question and answers a different one-edge statement;
+its proof assumes a nonzero edge space. The relation-word setting of #6777
+is context, not a proof dependency. Prepared by unpaidmoon
+with substantial Cursor Grok assistance. New work is Apache-2.0.

research/no-edge-irreducible-image/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}

research/no-edge-irreducible-image/TASK.json

@@ -0,0 +1,78 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Sharp irreducible joint-image dimension of a complete no-edge binary rank-one idempotent pool whose off-diagonal pattern space has dimension at most 3.",
+  "scope_change_reason": "The card asks for a larger or nonabelian register alphabet. This package changes that premise to the scalar question left open by #6838, which is whether a complete no-edge pool of pattern dimension at most 3 can act irreducibly on a four-dimensional joint image. No new alphabet, word, or kappa is claimed. The same card was already moved to scalar pattern-pool questions by #5921 and #6838.",
+  "bottleneck_link": "Side result. An irreducible joint-image bound of 3, one below the sharp total-image bound 4, restricts the scalar pool before any chronological word or supplier search. The original native acceptance gate remains unmet.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the all-width irreducible bound and the sharp dimension-3 example are checked. Do not start word synthesis or a pattern-dimension-4 classification.",
+  "outcome": "completed",
+  "evidence": "PROOF.md shows that every no-edge pool of pattern dimension at most 3 is reducible whenever its joint image has dimension 4, and that dimension 3 is attained by an explicit irreducible three-projector pool at every ambient width. verify.py repeats the GL(3,2) classification, the sharp-example census, and the negative controls.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance with the case analysis, the GL(3,2) classification check, and the package verifier. Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "After a valid relation, cube-span, and coordinate-call split, does the irreducible bound 3 strengthen the paid-rank obstruction for a three-relation word?",
+      "why_it_matters": "The scalar pool bound does not by itself decide whether a concrete word saves a factor. #6838 left this as its second open question.",
+      "first_step": "State the exact split hypotheses from #6777 and #6782, then account for endpoints and paid rank using the irreducible image bound only where those hypotheses hold.",
+      "blocked_by": "The word-reduction hypotheses are not reproved in this package."
+    },
+    {
+      "question": "Does the irreducible joint-image bound stay 3 when the pattern space has dimension 4?",
+      "why_it_matters": "The no-edge argument uses dim P <= 3. #6838 notes that the parity construction one dimension higher has total joint image 5.",
+      "first_step": "Test whether that five-dimensional parity pool is irreducible, then look for an invariant-subspace argument that does not use a three-dimensional pattern space.",
+      "blocked_by": "Sections 4 through 7 use the Fano-plane structure of a three-dimensional pattern space."
+    }
+  ],
+  "coordination": {
+    "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166",
+    "question_source": "https://github.com/CrocSwap/integer-mult-bounds/pull/6838",
+    "depends_on": [
+      "https://github.com/CrocSwap/integer-mult-bounds/pull/5921",
+      "https://github.com/CrocSwap/integer-mult-bounds/pull/6838"
+    ]
+  }
+}

research/no-edge-irreducible-image/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "GL(3,2) no-edge basis classification, sharp three-projector pool, cap count, parity and normal-form negative controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same checks with assert statements disabled; the verifier raises SystemExit instead of using assert."
+    }
+  ]
+}