Prove sharp binary pattern-pool cardinality (no new κ)

research/pattern-pool-cardinality/PROOF.md

@@ -0,0 +1,134 @@
+# Sharp binary off-diagonal pool cardinality
+
+This scoped proof was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Model and theorem
+
+Let W>=1, and let V be a d-dimensional linear subspace of the zero-diagonal
+matrices in M_W(F2). Write off(N) for N with its diagonal deleted. Define
+
+```
+P(V) = {N : rank(N)=1, N^2=N, off(N) in V, off(N)!=0}.
+```
+
+These are scalar projectors, with no rational address frames or word order.
+In particular, coordinate projectors do not belong to P(V).
+Let R(V) be the nonzero elements of V which occur as off(N), and let e(V)
+count the matrix units E_ij in V with i!=j.
+
+**Theorem.** For every W and V,
+
+```
+|P(V)| = |R(V)| + e(V) <= 2^d + d - 1.
+```
+
+For every d>=1 and W>=d+1, some V attains equality. For d=0 the pool is
+empty. Thus the maximum over all ambient register counts is exactly
+2^d+d-1. This does not assert attainment at every smaller feasible W.
+
+## 1. All fibers of diagonal deletion
+
+**Lemma.** A realizable nonzero off-diagonal pattern has exactly one
+rank-one-idempotent lift, except when it is a matrix unit E_ab with a!=b.
+That pattern has precisely the two lifts
+
+```
+E_aa + E_ab = e_a (e_a+e_b)^T,
+E_bb + E_ab = (e_a+e_b) e_b^T.
+```
+
+To prove this, suppose distinct rank-one idempotents N and M have the same
+off-diagonal pattern. Then D=N+M is a nonzero diagonal matrix of rank at
+most two. A rank-one idempotent has trace one, so trace(D)=0 in F2.
+The number of nonzero diagonal entries of D is therefore even and at most
+two. It is exactly two, at positions a and b.
+
+Write N=x y^T and M=u v^T, with y^T x=v^T u=1. The rank-two image of D
+is contained in span(x,u), so that span equals span(e_a,e_b). Applying the
+same argument to D^T puts y and v in span(e_a,e_b). Both projectors are
+therefore supported on the same two-by-two coordinate block, and differ
+there by the identity.
+
+For completeness, the rank-one idempotents on that binary block are
+
+```
+[[1,0],[0,0]], [[0,0],[0,1]],
+[[1,1],[0,0]], [[0,1],[0,1]],
+[[1,0],[1,0]], [[0,0],[1,1]].
+```
+
+This list follows by taking nonzero x,y in F2^2 with y^T x=1.
+The only repeated nonzero off-diagonal patterns are the two single edges.
+Their displayed lifts work in every ambient dimension. Any third lift
+would, by the same argument with N, have to be in this list. This proves
+the lemma. The zero pattern has the W coordinate projectors as its lifts;
+its exclusion is essential.
+
+woklerx's PR1456 already proves uniqueness for cyclic patterns. The lemma
+retains that conclusion and treats every acyclic pattern and every
+ambient dimension as well. The rank and trace facts are standard linear
+algebra, not new methods claimed here.
+
+## 2. Exact count and upper bound
+
+Every pattern in R(V) contributes one projector. By the lemma, the only
+extra projectors are one additional lift for each E_ij in V. All these
+matrix units are realizable, so the exact count is |R(V)|+e(V).
+
+There are at most 2^d-1 nonzero vectors in V. Distinct off-diagonal matrix
+units are linearly independent, since they have disjoint one-entry
+supports. A d-dimensional V consequently contains at most d of them.
+The asserted upper bound follows.
+
+One consequence useful before a scalar-pool search is
+
+```
+dim(sum_{N in P(V)} im(N)) <= |P(V)| <= 2^d+d-1.
+```
+
+The joint image is invariant under every projector in the pool. If the pool
+is nonempty and W>2^d+d-1, it is a nonzero proper common invariant subspace.
+This is a necessary restriction on the pool alone. Adding coordinate
+projectors or other patterns to a chronological word can invalidate this
+particular invariant subspace.
+
+## 3. A family attaining the bound
+
+Use coordinates 0,1,...,d, padding by arbitrary further coordinates if
+W>d+1. Let
+
+```
+V = span(E_01, E_02, ..., E_0d).
+```
+
+For every nonempty subset J of {1,...,d}, the projector
+
+```
+N_J = e_0 (e_0 + sum_{j in J} e_j)^T
+```
+
+has off-diagonal pattern sum_{j in J} E_0j. Thus all 2^d-1 nonzero patterns
+in V are realized. Exactly d of them are single edges, and their second
+lifts are (e_0+e_j)e_j^T. These projectors are distinct and give precisely
+2^d-1+d elements of P(V), proving sharpness. The fiber lemma excludes
+additional lifts on padded coordinates.
+
+## Scope and predecessor boundary
+
+PR1456's open question asks for further pattern-space classification at
+relation nullity two. This result gives an exact all-dimension size bound
+before such a classification. PR1846's four-role flag and reducibility
+census is cited context, not a dependency of this proof and not replayed.
+Neither its flags nor any predecessor count is used above.
+
+The field is specifically F2. For example, over F7 the distinct matrices
+[[3,1],[1,5]] and [[5,1],[1,3]] are rank-one idempotents with the same
+two-edge cyclic pattern, so the fiber lemma does not carry over unchanged.
+The finite verifier checks this boundary literally.
+
+No rational-frame feasibility, two-relation word, native implementation,
+physical restoration, full cost invoice, supplier admission, improved kappa
+or complete multiplication theorem follows from this scalar count. The
+finite checks corroborate the written proof and do not establish its
+unbounded quantifiers by enumeration.

research/pattern-pool-cardinality/README.md

@@ -0,0 +1,117 @@
+# A sharp size bound for binary scalar pattern pools
+
+For every d-dimensional off-diagonal pattern space over F2, the pool of
+rank-one idempotents with a nonzero pattern has at most `2^d+d-1` elements,
+independently of the number of registers. A common-row construction attains
+the bound whenever at least d+1 registers are available. In particular,
+two-dimensional spaces have at most five noncoordinate projectors.
+
+Claim type: scoped written mathematical proof with finite exact corroboration.
+This contribution was produced by Nick Petalas. Apache-2.0. Independent human
+and formal proof-kernel review are unclaimed.
+
+[PROOF.md](PROOF.md) gives the complete argument. Deleting the diagonal has
+one lift per realizable nonzero pattern, except a single directed edge has
+two. A d-dimensional space contains at most d distinct edge patterns. The
+exact count is the number of realized nonzero patterns plus the number of
+matrix units in the space. No predecessor scientific suite is imported or run.
+
+## Evidence and reproduction
+
+The read-only standard-library verifier enumerates binary projectors on five
+and six registers. A separate oracle tries every diagonal completion for
+every realized pattern, including the zero-pattern boundary. It also checks
+all pairs of distinct realized five-register patterns, explicit attaining
+stars through dimension ten with padded spectators, and semantic controls.
+These checks corroborate the new proof, rather than reproducing the
+four-register flag classification.
+
+Local CPython 3.12.15 checks pass for 2,501 noncoordinate projectors,
+141,888 diagonal completions, 110,685 spanning pairs and 55 attaining star
+shapes containing 4,237 literal projectors. Five malformed dimensions and
+seven semantic control groups pass. Three disposable optimized-code mutants
+reject a missing edge charge, missing second lifts and admitted nilpotents.
+The two registered commands took 0.305 and 0.261 seconds in individual local
+runs, below their 120-second limits. These timings check the replay budget.
+
+From the repository root, run:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/pattern-pool-cardinality/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/pattern-pool-cardinality/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/pattern-pool-cardinality
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/pattern-pool-cardinality --check-source-history
+```
+
+Any CPython 3.12 executable may replace this installation path. A direct run
+prints `PASS_PATTERN_POOL_CARDINALITY` followed by a generated JSON receipt
+with exact counts and SHA256 hashes of all six package files. Save stdout
+outside the checkout. There is no handwritten scientific receipt. Direct
+replay works without Git or network; provenance validation needs full Git
+history. The verifier does not read predecessor files at runtime.
+
+## Sources, scope and stopping decision
+
+The source question is the Open next questions section of woklerx's
+[PR1456](https://github.com/CrocSwap/integer-mult-bounds/pull/1456), at
+`83b6ad2ace819a96128131a3600ee914a66dd0dd`. Its cyclic-pattern uniqueness
+argument and arbitrary-role Laurent method retain their credit. Ali Romman,
+eumemic and the register-model lineage remain predecessor credit.
+woklerx's [PR1846](https://github.com/CrocSwap/integer-mult-bounds/pull/1846)
+supplies the separate finite four-role flag classification. Neither result
+is audited here. Exact retained source blobs are pinned in SOURCES.json.
+
+Base canonical main is `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority
+revision eight. The selected-baseline metadata control passed. The card is
+changed to a scalar reconstruction side result. It supplies a bounded pool
+before word synthesis, and meets no native supplier acceptance gate.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217787)
+records this scope. Stop at the sharp size theorem; no word search is reserved.
+
+The joint image of the pool has dimension at most its size, giving a proper
+common invariant subspace when the ambient dimension exceeds the bound and
+the pool is nonempty. Coordinate projectors are excluded. Interleaving them
+can destroy this particular invariant subspace. This does not eliminate a
+complete two-relation word or extend the rational span-six obstruction of
+PR5231, which has different premises and a different conclusion.
+
+Entry searches covered live open PR bodies, recent account PRs, active
+Discussions and the latest handoff comments, the cached card search, merged
+pattern/dihedral searches, and all main package READMEs for distinctive
+pattern/fiber/count terms. The cached helper reports sparse local omissions;
+Git searches cover committed READMEs, not arbitrary nested code, unpublished
+work or every historical PR body. No match is not proof of novelty.
+
+The selected frontier is unchanged. Rational address frames, chronology,
+full native/physical/precision/tape/ownership costs, independent targets,
+compiler admission and the complete multiplication theorem remain outside
+scope. No Lean, Docker, historical scientific replay or selected operator
+replay is run. The universal result rests on the written proof.
+
+## Open next questions
+
+- Which pattern spaces attain the maximum? Begin by imposing equality in
+  both the realized-pattern and edge counts, then classify the resulting
+  directed-edge sets. This could remove redundant extremal search families;
+  the present proof supplies an attaining family without classifying all of them.
+- What is the sharp joint-image dimension at fixed d? The cardinality bound
+  gives a finite ambient threshold for irreducible pools, but can be loose.
+  Start with d=2 and retain every possible diagonal lift. Adding coordinate
+  gates to full words is a separate obstacle.
+
+Structured questions and blockers are in TASK.json.
+
+## Verifier implementation limits
+
+All loops have fixed finite domains. Exhaustive oracle widths are five and
+six; stars use at most eleven registers and dimension ten. The plane pass
+accepts at most 500 realized patterns and counts spanning pairs, not distinct
+planes. No recursion, subprocess, network or scientific output write occurs.
+Python dynamically allocates bounded tuples/maps; static allocation is not
+available in this runtime. At most the fixed projector/fiber tables, a
+64-completion oracle set and one star of at most 1,033 projectors are live.
+Functions are below sixty physical lines. Explicit exception checks survive
+optimized execution, and registered commands make warnings errors. Package
+hashing reads exactly six bounded source files.
+Syntax compilation and the standard-library indentation check pass. No
+dedicated linter is installed on this host.

research/pattern-pool-cardinality/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/bit-one-relation-any-registers/README.md",
+      "usage": "provenance",
+      "git_blob": "7453a3f10c9cbaad746f108dc65dcfc514d0fdb5",
+      "sha256": "1f2899320e646a4158531c3f8260ba32b4761ae883fdb5bce4d3e3b0a4d8cb8c"
+    },
+    {
+      "path": "research/bit-one-relation-any-registers/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "9b42c6cd2e93514bd8c5247e2ef2d516d6603ae6",
+      "sha256": "38805f881d0bd625418fd8bdc9410d06fe3873374db9678c722d13abd3bfe392"
+    },
+    {
+      "path": "research/bit-four-role-two-patterns/README.md",
+      "usage": "provenance",
+      "git_blob": "e79087d9cd8f4473e6e48fa4e521902b7809f3a4",
+      "sha256": "e4ee830e783b20bfb0886ae8c91133a6138157ed5dcaac90ce16ddc616c8d49f"
+    },
+    {
+      "path": "docs/research/current-priorities.md",
+      "usage": "provenance",
+      "git_blob": "6f5d40d13d8f3bdc12ce7954c8c3eb4ab1f8be91",
+      "sha256": "70f61c8d140ae6e892f2b8f065bba4eae3e76f7a8f55f632fd4e2f9f34039bdc"
+    }
+  ]
+}