Classify exact Schur dimensions for prescribed scalar pivots (no κ)

research/scalar-pivot-schur-dimension/PROOF.md

@@ -0,0 +1,142 @@
+# Exact scalar-pivot dimension
+
+This proof was produced by Nick Petalas. Apache-2.0.
+
+Let K be any field, let lambda be nonzero, and prescribe h in K. Among
+commuting idempotents P,Q on K^n with P11=Q11=lambda and (PQ)11=h, let
+N(lambda,h) be the least n for which their one-coordinate Schur complements
+have commutator rank two. Then
+
+```text
+                    4 + [1-2lambda != 0],  h=0,
+N(lambda,h) =       5 + [lambda != 1],     h=lambda,
+                    3 + [1-2lambda+h != 0], otherwise.
+```
+
+The brackets denote the indicator of a field inequality. The first two cases
+are disjoint because lambda is nonzero. Every minimum is attained. Matrices
+need not be symmetric. This is a scalar-pivot theorem, not a theorem about a
+prescribed matrix product for a larger deleted block.
+
+## Sector compression
+
+Put U=K, V=K^n. Let i:U -> V be coordinate inclusion and pi:V -> U the
+coordinate projection. Since pi i=1, V=i(U) direct-sum ker pi.
+The four joint eigenspace projectors are
+
+```text
+E00=(I-P)(I-Q), E10=P(I-Q), E01=(I-P)Q, E11=PQ.
+```
+
+These mutually annihilating projectors sum to I in every characteristic. Set
+Vj=im Ej, rj=dim Vj, Yj=Ej i and Xj=pi restricted to Vj. Their products are
+
+```text
+t00=X00 Y00=1-2lambda+h,
+t10=X10 Y10=lambda-h,
+t01=X01 Y01=lambda-h,
+t11=X11 Y11=h.                                      (1)
+```
+
+They sum to 1. Conversely, any such four pairs of maps with these products
+give pi i=1. Equip their direct sum with diagonal P0,Q0 having eigenvalues
+00,10,01,11. Complete i to a basis [i N], with N a basis of ker pi.
+Conjugation into this basis gives commuting idempotents with exactly the
+required coordinate pivots and leading product. This standard sector
+construction is the predecessor method of ssafwann's #4671 and Nick Petalas's
+#4746. The products and sharpness conditions below change with lambda.
+
+## Rank-two criterion
+
+Use the scalar factorization from Nick Petalas's #4278, with equal pivots
+lambda. Its ambient factors are
+
+```text
+A = [PQ i - (h/lambda)Q i, (P-Q)i/lambda] : K^2 -> V,
+B = [pi(P-Q)/lambda; -pi PQ + (h/lambda)pi Q] : V -> K^2.
+```
+
+They satisfy pi A=0 and Bi=0. The Schur commutator is the product of A's
+coordinates in ker pi and B's restriction to ker pi. Therefore it has rank
+two exactly when A has rank two and B has rank two. Indeed, a rank-two A is
+injective and a rank-two B is onto. The identity Bi=0 and the displayed direct
+sum imply that B restricted to ker pi is still onto.
+
+For each sector, A is Yj times the following row, and B is the following
+column times Xj:
+
+```text
+sector     row for A                         column for B
+00         (0,0)                             (0,0)^T
+10         (0,1/lambda)                      (1/lambda,0)^T
+01         (-h/lambda,-1/lambda)             (-1/lambda,h/lambda)^T
+11         ((lambda-h)/lambda,0)             (0,-(lambda-h)/lambda)^T
+```
+
+Since the sectors form a direct sum, rank A is the span dimension of the
+listed rows whose Yj is nonzero. Similarly, rank B is the span dimension of
+the listed columns whose Xj is nonzero. There is no cross-sector cancellation.
+
+If h is neither 0 nor lambda, all three active products in (1) are nonzero.
+Thus Xj and Yj are nonzero in sectors 10,01,11. The 10 and 01 rows are
+independent since h!=0; the corresponding columns are also independent.
+Both factors automatically have rank two.
+
+If h=0, A's first column is supported only in sector 11. It is nonzero
+exactly when Y11 is nonzero. The nonzero products t10=t01=lambda already
+give the second independent direction. The dual statement for B requires
+X11 nonzero. Hence sharpness is exactly X11!=0 and Y11!=0.
+
+If h=lambda, A's first column is supported only in sector 01. Its 01 row
+is proportional to (lambda,1), whereas its only possible independent row is
+the 10 row. The 11 row vanishes. Therefore rank A=2 exactly when Y01 and
+Y10 are both nonzero. Dually, rank B=2 exactly when X01 and X10 are both
+nonzero. The nonzero t11=lambda already ensures a nonzero 11 sector.
+
+These are exact replacement criteria for the identity-pivot six-map argument;
+they do not assume that all three sectors always require both maps.
+
+## Lower bounds and attainment
+
+One scalar compressed product t!=0 needs at least one dimension. If t=0
+and both X and Y must be nonzero, at least two dimensions are necessary:
+nonzero maps between one-dimensional spaces have nonzero product.
+If neither map is required, a zero product needs no dimension.
+
+For h outside {0,lambda}, sectors 10,01,11 each need one dimension, and
+sector 00 needs exactly [1-2lambda+h!=0]. This gives the third case.
+For h=0, sectors 10,01 need one each, sector 11 needs two, and sector 00
+needs [1-2lambda!=0]. This gives the first case.
+For h=lambda, sectors 10,01 need two each, sector 11 needs one, and sector
+00 needs [1-lambda!=0]. This gives the second case.
+
+Attain all these bounds by choosing, independently in each sector,
+
+```text
+nonzero t:                  Y=(1),       X=(t),
+zero t, both maps required: Y=(1,0)^T,   X=(0,1),
+zero t, no maps required:   zero-dimensional sector.
+```
+
+The products are (1), so their sum is 1 and the coordinate construction
+above applies. Each stated sharpness criterion holds. This proves existence
+at exactly the lower bound over every field, and completes the proof.
+
+## Consequences and boundary
+
+For a nonidentity scalar pivot lambda, the prescribed product h=lambda
+forces dimension six. Thus substituting lambda into the old identity-pivot
+formula, which would predict five for an endpoint product, is invalid.
+For example, over F3, lambda=h=2 has exact minimum six, whereas h=0 or h=1
+with the same pivot has exact minimum four.
+
+The generic minimum three occurs exactly when h=2lambda-1 avoids 0 and
+lambda. Such lambda exists over every finite field with at least four
+elements. F2 and F3 give minima five and four respectively when lambda,h
+are unrestricted. The F2/F3/F5 unrestricted minima were already established
+by Ryanson Jonathan's #4609. The contribution here is the exact dependence
+on both prescribed scalar values over every field.
+
+No header frequency, later Schur-state law, physical caller, supplier
+admission, new kappa or complete multiplication theorem follows. Uniform
+physical and analytic costs remain separate unknown obligations.

research/scalar-pivot-schur-dimension/README.md

@@ -0,0 +1,139 @@
+# Exact Schur dimension for a prescribed scalar pivot and product
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with finite corroboration. Let P,Q be
+commuting idempotents over any field, with the same nonzero scalar first
+entry lambda and prescribed first entry h of PQ. The least ambient dimension
+in which their one-coordinate Schur complements have commutator rank two is
+
+```text
+                    4 + [1-2lambda != 0],  h=0,
+N(lambda,h) =       5 + [lambda != 1],     h=lambda,
+                    3 + [1-2lambda+h != 0], otherwise.
+```
+
+Here brackets mean the indicator of a field inequality. Every minimum is
+attained by the explicit sector construction in [PROOF.md](PROOF.md).
+In particular, a nonidentity pivot with h=lambda requires exactly six
+dimensions. Over F3, lambda=h=2 requires six, while the same pivot with
+h=0 or h=1 requires four. Nonidentity pivots therefore change the endpoint
+dimension law, rather than simply replacing the symbol 1 in the old formula.
+
+This answers the scalar part of Open next question 1 in
+[PR #4746](https://github.com/CrocSwap/integer-mult-bounds/pull/4746), pinned at
+`5f014560d6225cae17598ac479fb29d2947d8e6b`. Its identity-pivot formula,
+ssafwann's binary theorem in #4671 and Ryanson Jonathan's earlier unrestricted
+small-field minima in #4609 are predecessor results, not new claims here.
+The new result is the exact dependence on both prescribed scalars, including
+the replacement sharpness criterion, over every field. No new kappa.
+
+## Evidence and reproduction
+
+The written proof decomposes the commuting projectors into their four joint
+eigenspaces. The compression products are
+`(1-2lambda+h,lambda-h,lambda-h,h)`. Nick Petalas's #4278 factorization
+reduces sharpness to two explicit rank-two conditions. Their zero-product
+sectors need two dimensions precisely in the endpoint cases above.
+
+The independently written standard-library verifier imports no predecessor
+executable. It constructs actual P,Q and checks idempotence, commutation,
+both pivots, the prescribed product, direct Schur multiplication and the
+ordered factor identity. It covers every nonzero lambda and every h over
+F2,F3,F4,F5,F7,F8,F9, totaling **210 parameter pairs**. This includes the
+known identity-pivot specialization as a calibration case.
+
+A separate finite optimization enumerates **14,291 scalar vector pairs**
+through sector dimensions zero, one and two, recording every possible
+zero/nonzero map type and its minimum dimension. It evaluates **1,212
+four-sector patterns** and matches the formula in all 210 cases. Two
+dimensions suffice to realize any scalar map type, as explained in the
+proof; this is not a truncated search over ambient matrices.
+
+Seven controls detect omitted necessary zero-product sectors in both
+endpoint cases, a zero pivot, an incorrect sector sign, a mutated projector,
+a singular coordinate basis and an unsupported nonfield order. F4,F8,F9
+use polynomial quotient fields, not arithmetic modulo their orders. All
+checks remain enabled under optimized Python.
+
+From the repository root, using CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/scalar-pivot-schur-dimension/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/scalar-pivot-schur-dimension/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/scalar-pivot-schur-dimension
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/scalar-pivot-schur-dimension --check-source-history
+```
+
+Another CPython 3.12 path may replace the local path. The direct verifier
+writes nothing and emits `PASS_SCALAR_PIVOT_SCHUR_DIMENSION` with a generated
+receipt binding all six package files by SHA256. The metadata runner and
+publication preflight are separate from the mathematical claim.
+
+The selected source-binding orientation passed after its declared inputs
+were materialized. Its source hashes and budget metadata are consistent;
+no selected scientific replay was run. The card's historical first command
+has been replaced by `scripts/research_selected_baseline.py` in current
+repository guidance.
+
+## Scope and code constraints
+
+The theorem concerns one scalar deletion, equal nonzero pivots and commuting
+idempotents over a field. Unequal pivots, larger deleted blocks with prescribed
+matrix product, coefficient rings, later-state transitions and header
+probabilities are outside scope. Producer selection, header emission,
+dispatch, dirty restoration, stock, precision and the complete consumer
+cost are unknown. No physical supplier admission, selected-frontier change
+or complete multiplication theorem is claimed. Independent human and formal
+proof-kernel review are unclaimed. Lean, Docker and selected cold replay were
+not run. All registered local checks are required before publication.
+
+The fixed verifier uses seven fields of size at most nine. Matrices have at
+most six rows, elimination at most twelve columns, and vector scans at most
+q^4=6561 iterations per field. Each pattern product has four finite factors,
+each containing at most four map types. Only counters, small field tables
+and the current construction persist. There is no recursion, subprocess,
+code generation or user-controlled input. Functions stay below 60 physical
+lines. Explicit exceptions enforce bounds and invariants under -O. Warnings
+are errors in both registered commands; syntax and function lengths are
+also inspected locally. No external static analyzer is installed or claimed.
+
+Power of Ten rule 3 deviation: CPython arithmetic, iterators and collections
+allocate dynamically. This bounded standalone verifier cannot prohibit
+runtime allocation. The fixed field, vector, matrix and six-file receipt
+capacities bound live data; no state accumulates across the 210 cases.
+Both registered modes exercise the bounds and seven rejection controls.
+Reassess fixed storage and input validation before adding larger domains
+or an external parameter interface. The deviation is confined to this
+verifier, which owns no external mutable resources.
+
+## Open next questions
+
+1. Determine the minimum for unequal nonzero scalar pivots p,q with
+   prescribed h. The same four-sector method starts with products
+   `(1-p-q+h,p-h,q-h,h)`, but its independent-direction cases need a new
+   classification. This would separate equality of pivots from scalarity.
+2. Determine the prescribed-matrix-product minimum for a common nonidentity
+   scalar block lambda I_d. Start with one nondiagonal H; scalar sector-map
+   nonvanishing no longer determines rank. This theorem gives no all-d bound.
+3. Count complete headers for one fixed nonidentity scalar profile. Dimension
+   feasibility does not provide frequency or a paid header producer. Specify
+   the header ensemble before deriving a count or claiming a physical gain.
+
+## Credit and task scope
+
+Nick Petalas's #4746 supplies the explicit open question and all-field
+identity-pivot predecessor. ssafwann's #4671/#4657 supplies the binary
+dimension theorem, six-map method and split sector construction.
+Nick Petalas's #4278/#4597 supplies the scalar and ordered block Schur
+factorizations. Ryanson Jonathan's #4609/#4617 and lee-phys's #4634 supply
+preceding small-field and unrestricted-block sharpness constructions.
+Nick Petalas's #4259/#4228 retains the laminar-header and single-request
+context. Cinna Davis supplies the BIT request setting; source527,
+commdata2338 and Jose Manuel retain the normalizer lineage credit.
+
+The formal-interface-lemma card is explicitly changed to this algebraic
+side theorem. The work supplies a new prescribed-boundary dimension law,
+without auditing another contributor or expanding a physical mechanism.
+Exact citations, source provenance, overlap coverage, the advance claim and
+the preserved checkout state are recorded in TASK.json and SOURCES.json.

research/scalar-pivot-schur-dimension/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/schur-commutator-criterion/README.md",
+      "usage": "provenance",
+      "git_blob": "6b37342de04f5c42c198dd6ba14cea9845be6f05",
+      "sha256": "5616da2e708a8425f1bf0bf5c89c236ef8ed0a23d0544d30ae2142ffe167dc01"
+    }
+  ]
+}