Exclude irreducible five-dimensional one-edge binary pattern pools

research/one-edge-pattern-reducibility/ORIGINS.json

@@ -0,0 +1,11 @@
+{
+  "source_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/6782",
+  "source_author": "CubeJerry",
+  "source_head": "685457252b51b9c7932ece363365bdf0b12c9c31",
+  "question": "README.md, Open next questions, question 2: irreducible five-dimensional one-edge cores",
+  "proof_url": "https://github.com/CubeJerry/integer-mult-bounds/blob/685457252b51b9c7932ece363365bdf0b12c9c31/research/bit-three-relation-core/PROOF.md",
+  "proof_sha256": "1fad3fa92b26bcd290b179ee3b714c3d25017bc63fa2439124e2e10ddb2c374c",
+  "imported_result": "Section 3 edge-quotient bound: one quotient image dimension per nonzero pattern coset; zero-coset images lie in the edge endpoint space.",
+  "status": "Cited mathematical premise, not independently audited or replayed. Pending public source is not a Git-history dependency or executable input of this package.",
+  "credit": "CubeJerry for the edge-quotient result and explicit one-edge question; Nick Petalas PR5921 for the diagonal-deletion fiber lemma; woklerx PR1456/1846 and the retained scalar-register lineage."
+}

research/one-edge-pattern-reducibility/PROOF.md

@@ -0,0 +1,142 @@
+# One edge cannot support an irreducible five-dimensional pool
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Statement and imported premise
+
+Work over F2. Let P be a three-dimensional space of zero-diagonal W-by-W
+matrices. Its complete noncoordinate pool is
+
+```
+C(P) = {xy^T : y^T x = 1, off(xy^T) in P, off(xy^T) != 0}.
+V = sum_{N in C(P)} im(N).
+```
+
+Suppose P contains exactly one off-diagonal matrix unit p=E_ab. Put
+E=span(e_a,e_b), and let pi be the coordinate projection deleting a and b.
+The pool preserves V, so its restrictions to V are well defined.
+
+**Theorem.** If dim V=5, every N in C(P) preserves E. More precisely,
+each N either has image contained in E or annihilates E. Consequently
+the restricted pool is reducible. Every irreducible restricted pool with
+these hypotheses has dim V<=4.
+
+The proof uses the following result of CubeJerry's
+[PR6782, Section 3](https://github.com/CubeJerry/integer-mult-bounds/blob/685457252b51b9c7932ece363365bdf0b12c9c31/research/bit-three-relation-core/PROOF.md).
+Let P0=span(p). Projectors whose patterns lie in P0 have image in E.
+For each nonzero coset alpha of P/P0, the images modulo E of all pool
+members in that coset span a space of dimension at most one. Thus
+
+```
+dim V <= dim E + 2^(3-1)-1 = 5.
+```
+
+This edge-quotient result is a cited mathematical premise, not a new
+result or an independently audited claim of this package. Its proof builds
+on Nick Petalas's PR5921 diagonal-deletion fiber lemma and the retained
+woklerx pattern-space lineage. Exact citation metadata is in ORIGINS.json.
+
+## Proof of the new theorem
+
+The two lifts of p are e_a(e_a+e_b)^T and (e_a+e_b)e_b^T.
+Their images span E, so E is contained in V.
+
+There are exactly three nonzero cosets alpha_1, alpha_2, alpha_3 of P/P0,
+and their sum is zero. If dim V=5, then dim pi(V)=3. The three at-most-one-
+dimensional quotient image spaces must therefore be nonzero and linearly
+independent. Choose N_i=x_i y_i^T from coset alpha_i, for i=1,2,3.
+The vectors pi(x_1), pi(x_2), pi(x_3) are linearly independent.
+
+Since the three cosets sum to zero,
+
+```
+off(N_1+N_2+N_3) in P0.
+```
+
+In particular the block with rows outside {a,b} and columns in {a,b}
+vanishes. Let X have columns pi(x_i), and let Y have rows y_i restricted
+to E. That block equation is XY=0. The three columns of X are independent,
+so X is injective and Y=0. Each selected N_i annihilates E.
+
+Now take any N=xy^T in C(P). If pi(x)=0, its image is contained in E.
+Otherwise its pattern lies in some alpha_i. The imported quotient result
+and the fact that the field is F2 give pi(x)=pi(x_i): a one-dimensional
+binary space has only one nonzero vector. The off-diagonal difference of
+N and N_i lies in P0. Its outside-row/E-column block is therefore
+
+```
+pi(x_i) (y|E + y_i|E)^T = 0.
+```
+
+Here pi(x_i) is nonzero and y_i|E=0. It follows that y|E=0, so N
+annihilates E. This proves the asserted dichotomy for every pool member.
+
+Thus the nonzero two-dimensional space E is a common invariant subspace
+strictly inside the five-dimensional V. The restricted pool is reducible.
+Combining this exclusion with the imported upper bound five proves the
+irreducible upper bound four. This does not assert that four is attained.
+
+## A reducible pool attaining joint-image dimension five
+
+The conclusion is reducibility, not a smaller unrestricted joint-image
+bound. Here is a concrete attaining example on coordinates 0,...,5:
+
+```
+P = span(E01, (e3+e4)e2^T, (e4+e5)e2^T).
+```
+
+Exactly one nonzero element of P is a matrix unit, namely E01.
+The three nonzero patterns supported in column 2 each have exactly two
+rows in {3,4,5}. Their unique idempotent lifts are
+
+```
+(e2+e3+e4)e2^T, (e2+e4+e5)e2^T, (e2+e3+e5)e2^T.
+```
+
+For a direct completeness argument, the two prescribed rows force the
+covector to be e2, and idempotence forces the coordinate-2 entry of the
+image vector to be one. No pattern obtained by adding E01 to one of these
+three column patterns is realizable: entries (0,1) and (i,2), i>=3,
+would force the absent off-diagonal entry (0,2) in a rank-one matrix.
+Together with the two lifts of E01, these are the complete five members.
+
+The last three image vectors are independent. Their sum is e2, and none
+is zero or equal to another. Their span is disjoint from span(e0,e1).
+Hence dim V=2+3=5. All five projectors preserve E=span(e0,e1), as required.
+Padding by zero coordinates gives the same example at every W>=6.
+
+## What the finite enumeration covers
+
+The verifier enumerates all binary rank-one idempotents at W=5 and W=6,
+excluding zero off-diagonal patterns. It fixes the unique directed edge
+to E01, which any other directed edge can reach by permuting coordinates.
+
+For each realized pattern q, remove its E01 bit to obtain its quotient
+key. Every equality case has all three nonzero quotient cosets realized,
+by the imported quotient bound. It therefore occurs among triples of
+distinct realized keys q,r,q+r. Ordering q<r<q+r counts each such quotient
+plane once. Their inverse images under deletion of the E01 bit are
+exactly the spaces span(E01,q,r). Testing all seven nonzero patterns
+retains precisely the spaces with one edge. The verifier reconstructs
+their complete pools, computes each joint-image rank and checks the
+edge-space action for every dimension-five case.
+
+The resulting counts concern spaces with all three nonzero quotient
+cosets realized. They are not counts of every three-dimensional pattern
+space. They count representatives with fixed edge E01, not conjugacy
+classes. Finite enumeration corroborates the written argument; it does
+not prove the theorem at unbounded W.
+
+## Boundary of the result
+
+The field is F2, the pattern dimension is three, and the pool is complete
+and excludes coordinate projectors. Adding other patterns or coordinate
+calls to a word need not preserve E. The theorem concerns the restrictions
+to the joint image, not a cost-free physical change of basis.
+
+The remaining one-edge active dimensions at most four, zero-edge pools,
+three-relation diagonal words, rational frame realization, arbitrary dirty
+helpers, chronological restoration, native operators and complete recursive
+invoices are separate questions. No supplier, saving in kappa, selected-
+frontier change or complete multiplication theorem is claimed.

research/one-edge-pattern-reducibility/README.md

@@ -0,0 +1,128 @@
+# One-edge five-dimensional binary pools are reducible
+
+This scoped proof and its standalone verifier were produced by Nick Petalas.
+Apache-2.0. Independent human and formal proof-kernel review are unclaimed.
+
+For a three-dimensional binary off-diagonal pattern space containing exactly
+one matrix-unit edge E_ab, the complete noncoordinate rank-one-idempotent pool
+cannot act irreducibly on a five-dimensional joint image. If that image has
+dimension five, every pool member preserves span(e_a,e_b). Thus an irreducible
+restricted pool has active dimension at most four. Attainment at four is not
+claimed. A separate reducible example attains joint-image dimension five.
+
+This answers the one-edge irreducible classification question in
+[CubeJerry's PR6782](https://github.com/CrocSwap/integer-mult-bounds/pull/6782),
+README open question 2. The [proof](PROOF.md) builds on that contribution's
+edge-quotient lemma. The new step studies equality in its bound; the lemma
+and its prior bound are credited premises, not reverified deliverables.
+There is no new kappa or supplier admission.
+
+## Evidence
+
+The claim type is a scoped written proof with finite exact corroboration.
+The universal argument holds at every ambient width under the credited
+edge-quotient premise. The verifier imports no predecessor code and reads
+no external scientific input.
+
+At widths five and six it enumerates every fixed-edge pattern space capable
+of attaining the bound. Equality requires all three nonzero quotient cosets
+to be realized. The complete pools of these spaces are reconstructed from
+all binary rank-one idempotents, and every dimension-five edge action is
+checked exactly.
+
+| Ambient width | One-edge spaces with all three quotient cosets realized | Dimension-five spaces | Those preserving the edge space |
+| --- | ---: | ---: | ---: |
+| 5 | 1030 | 30 | 30 |
+| 6 | 6576 | 328 | 328 |
+
+These are spaces with edge fixed to E01, not conjugacy classes or counts of
+all pattern spaces. [PROOF.md](PROOF.md) explains the complete enumeration
+of the relevant domain. The five-projector equality fixture is reconstructed
+by a separate direct space check. Seven controls exercise dependent generators,
+multiple edges, missing members, an extra coordinate projector, an unsupported
+width and two explicit edge-space leakage cases.
+
+Every direct run prints `PASS_ONE_EDGE_PATTERN_REDUCIBILITY` and a generated
+JSON receipt with recomputed counts and SHA256 hashes of package files. No
+handwritten scientific receipt is supplied.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/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 the installation path. The last command
+requires the package to be committed. The standalone verifier also runs without
+Git, network or the rest of the repository.
+
+Local CPython 3.12.15 runs passed normally and optimized, as did both registered
+commands and the package metadata check. Individual direct runs took 0.097 and
+0.101 seconds; these single-run measurements check the replay budget, not a
+performance improvement. Syntax compilation and indentation diagnostics passed.
+
+[SOURCES.json](SOURCES.json) pins the merged catalogue, selected record and
+PR5921 proof context as historical Git provenance. [ORIGINS.json](ORIGINS.json)
+separately pins the pending PR6782 proof by public URL, exact head and SHA256.
+That cited mathematical premise is not imported by the finite verifier or
+included in the Git-history preflight. No claim of independent verification
+of PR6782 is made. The public proof must be consulted to assess the imported
+lemma.
+
+## Scope and limitations
+
+The card `bit-helper-contract` is changed to an algebraic side question from
+another contributor. The required selected-baseline command passed with
+`PASS_RESEARCH_BASELINE_BINDINGS_ONLY`; it authenticates metadata, not operators.
+The selected record remains at `781451/250000000` under its five assumptions.
+The direct construction, three-relation word problem and complete BIT moment
+requested by the card remain unproved here.
+
+The field is F2 and the pool is complete. Coordinate projectors are excluded.
+Interleaving extra coordinate calls or other patterns can destroy the invariant
+edge space. The result supplies neither a free physical basis transformation
+nor a word-rank saving. Rational frames, arbitrary dirty-state restoration,
+native realization, full cost/precision/tape/ownership accounting, compiler and
+outer admission remain separate. No selected operator replay, Lean or Docker
+run is supplied. The finite census does not establish unbounded quantifiers.
+
+The verifier uses explicit checks that stay active under optimized Python.
+All loops have fixed finite domains, with at most 2010 noncoordinate projector
+records and at most 2010 quotient keys. Each pair loop has at most 2,019,045
+iterations. There is no recursion. Python allocates managed objects during
+enumeration; this is a bounded-domain deviation from fixed-allocation practice.
+The negative-control callbacks have five fixed targets and no shared mutable
+state. No dedicated linter is installed; warning-as-error execution, syntax and
+indentation diagnostics are used for this isolated Python file.
+
+## Related open work
+
+- [#6782](https://github.com/CrocSwap/integer-mult-bounds/pull/6782) supplies the
+  edge-quotient bound, a distinct two-edge five-dimensional irreducible example,
+  its word obstruction and the explicit one-edge question. This package closes
+  that one-edge five-dimensional irreducible case without replaying its results.
+- [#6777](https://github.com/CrocSwap/integer-mult-bounds/pull/6777) proves a
+  two-relation word-rank bound at arbitrary scalar width. The present result
+  concerns three-dimensional pattern pools and proves no word-rank inequality.
+
+Merged PR5921 supplies the fiber/cardinality context and PR1456/1846 the earlier
+pattern-space framework. They retain their original credit. CubeJerry's new
+edge-quotient theorem is the direct predecessor. The broader register-model
+lineage credits David Govea, Ali Romman, woklerx and eumemic.
+
+## Open next questions
+
+- Can a one-edge core of dimension at most four yield a three-relation diagonal
+  word with target rank exceeding paid rank? First specify one remaining scalar
+  alphabet and its relation lattice. Chronological synthesis and rational frames
+  are absent here, so the pool result alone cannot answer this.
+- 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 depends on a nonzero edge space and gives no zero-edge classification.
+
+Structured first steps and blockers are in [TASK.json](TASK.json).

research/one-edge-pattern-reducibility/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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"
+    },
+    {
+      "path": "research/pattern-pool-cardinality/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "4fce5d3b6a9c810cfd4d298b209dbd51cefa173c",
+      "sha256": "47ebe562180c7276bbf0636e9ba3aa1a84f8962ff8b60b3b2fb30cee4514e989"
+    },
+    {
+      "path": "research/pattern-pool-cardinality/README.md",
+      "usage": "provenance",
+      "git_blob": "ae404ea1d8a65f3c48b9817e7664c17abc4bf736",
+      "sha256": "f677bf62dc68c67c267a60c625e4555e428b9fc290fda4033cd9eb0cb06ae3b0"
+    }
+  ]
+}