Prove the exact unequal-pivot Schur dimension law (no new κ)

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

@@ -0,0 +1,112 @@
+# Unequal scalar pivots and a prescribed product
+
+This proof was produced by Nick Petalas. Apache-2.0.
+
+Let K be any field and prescribe distinct nonzero p,q in K and h in K.
+For commuting idempotents P,Q with P11=p, Q11=q and (PQ)11=h, the least
+ambient dimension for Schur-commutator rank two is
+
+```text
+N(p,q,h) = 3 + [h in {0,p,q}] + [1-p-q+h != 0].              (1)
+```
+
+Brackets denote indicators of field equalities or inequalities. Every minimum
+is attained. The hypothesis p!=q is essential. This answers Open next question
+1 of Nick Petalas's #4771, whose equal-pivot theorem is a predecessor, not
+part of the new claim. The sector construction follows ssafwann's #4671 and
+Nick Petalas's #4746/#4771; the scalar factorization follows #4278.
+
+## Four sectors
+
+Let i:K -> V be coordinate inclusion and pi:V -> K coordinate projection.
+Write E00=(I-P)(I-Q), E10=P(I-Q), E01=(I-P)Q and E11=PQ.
+Their images Vj form a direct sum. Put Yj=Ej i and Xj=pi restricted to Vj.
+The four scalar products are
+
+```text
+t00=1-p-q+h,    t10=p-h,    t01=q-h,    t11=h.              (2)
+```
+
+Conversely, any four pairs of maps Xj,Yj with these products give pi i=1,
+since the products sum to 1. On their direct sum, take the diagonal
+projectors with sector eigenvalues 00,10,01,11. Choosing the first basis
+vector to be i(1) and the remaining vectors in ker pi realizes the prescribed
+coordinate entries. Thus sector constructions give actual full matrices.
+
+## Exact independence criterion
+
+The cited scalar factorization, valid for arbitrary nonzero p,q, uses
+
+```text
+A = [PQ i - (h/q)Q i, P i/p - Q i/q],
+B = [pi P/p - pi Q/q; -pi PQ + (h/q)pi Q].
+```
+
+Here pi A=0 and Bi=0. In coordinates V=i(K) direct-sum ker pi, AB induces
+the Schur commutator on ker pi. Its rank is two exactly when A and B both
+have rank two. A rank-two A is injective and a rank-two B is surjective;
+Bi=0 means B restricted to ker pi remains surjective.
+
+On each sector, A equals Yj times a row aj, and B equals a column bj times
+Xj, as follows:
+
+```text
+sector   aj                                      bj
+00       (0,0)                                   (0,0)^T
+10       (0,1/p)                                 (1/p,0)^T
+01       (-h/q,-1/q)                             (-1/q,h/q)^T
+11       ((q-h)/q,(q-p)/(pq))                    ((q-p)/(pq),-(q-h)/q)^T
+```
+
+Each bj is the same invertible rotation of aj, namely (a2,-a1)^T.
+Therefore the independence relations for A and B are identical, with Yj
+and Xj respectively deciding whether a direction occurs. The determinants
+of the pairs of rows are
+
+```text
+det(a10,a01)=h/(pq),
+det(a10,a11)=-(q-h)/(pq),
+det(a01,a11)=(p-h)/(pq).                              (3)
+```
+
+All three rows are nonzero because p,q are nonzero and distinct.
+
+If h is outside {0,p,q}, all three active products t10,t01,t11 are nonzero.
+Both maps in each sector are nonzero, and (3) guarantees independent
+directions. These three sectors each require one dimension.
+
+If h=0, sectors 10 and 01 have nonzero products but parallel directions.
+Sector 11 has zero product and its direction is independent of both.
+Consequently rank two for both factors is equivalent to X11 and Y11 both
+being nonzero. This sector requires two dimensions, in addition to the
+one-dimensional sectors 10 and 01.
+
+If h=p, sectors 01 and 11 have nonzero products but parallel directions.
+The independent direction is sector 10, whose product vanishes. Both
+X10 and Y10 must be nonzero. The required dimensions are again 1+1+2.
+
+If h=q, the same argument uses nonzero-product sectors 10 and 11 and
+zero-product sector 01. Both X01 and Y01 must be nonzero. These cases
+are disjoint because p and q are nonzero and distinct.
+
+Sector 00 has no effect on either rank. Its product t00 requires exactly
+one dimension when nonzero and can be omitted otherwise. Adding its
+contribution gives the lower bound (1).
+
+## Attainment
+
+A nonzero scalar product t is realized in dimension one by Y=(1), X=(t).
+A zero product for which both maps must be nonzero is realized in dimension
+two by Y=(1,0)^T, X=(0,1). Omit every other zero-product sector.
+These choices attain every sector lower bound above. Their products sum to
+1, so the coordinate construction following (2) applies. The independence
+conditions hold, hence the Schur commutator has rank two. This proves (1)
+over every field.
+
+For example, over F3, p=1,q=2 gives dimensions five, five and four at
+h=0,1,2 respectively. Over F5, p=2,q=3,h=4 gives dimension three.
+The equal-pivot rule cannot be reused: at h=p with p!=q it is just one
+zero-product sector, rather than the two required when p=q=h.
+
+This is a scoped algebraic theorem about one-coordinate Schur complements.
+It gives neither a header frequency nor a paid physical implementation.

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

@@ -0,0 +1,132 @@
+# Exact Schur dimension for unequal scalar pivots
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with finite corroboration. Over every field,
+let P,Q be commuting idempotents with distinct nonzero scalar leading entries
+p,q and prescribed leading product entry h. The exact least ambient dimension
+attaining Schur-commutator rank two is
+
+```text
+N(p,q,h) = 3 + [h in {0,p,q}] + [1-p-q+h != 0].
+```
+
+Brackets denote indicators. Every minimum is attained by explicit matrices.
+Over F3, p=1,q=2 gives minima five, five and four at h=0,1,2 respectively.
+Over F5, p=2,q=3,h=4 gives dimension three.
+
+This answers Open next question 1 of
+[PR #4771](https://github.com/CrocSwap/integer-mult-bounds/pull/4771), head
+`22cb0bda57237d39d0e6944b232447d3a2809311`. That equal-pivot classification
+is cited, not audited. Equality of pivots is a real boundary: at h=p with
+p!=q, just one zero-product sector requires two dimensions; at p=q=h,
+the predecessor requires two such sectors. No new kappa is claimed.
+
+## Proof and evidence
+
+[PROOF.md](PROOF.md) decomposes the commuting idempotents into four joint
+eigenspaces, with compressed products `(1-p-q+h,p-h,q-h,h)`. The three
+active directions have pair determinants `h/(pq)`, `-(q-h)/(pq)` and
+`(p-h)/(pq)`. Away from the three endpoints, their nonzero products force
+rank two. At each endpoint, the missing independent direction requires a
+two-dimensional zero-product sector. This proves the lower bound and gives
+an attaining construction over every field.
+
+The standalone verifier constructs full matrices for all **1,140** distinct
+nonzero pivot/product triples over F3,F4,F5,F7,F8,F9. It checks idempotence,
+commutation, both pivots, the product entry, literal Schur multiplication,
+commutator rank and the scalar factorization. F4,F8,F9 use polynomial
+quotient fields, not arithmetic modulo their orders.
+
+A separate optimization enumerates **14,270** scalar vector pairs and
+**3,528** sector-map patterns. Every minimum agrees. Dimensions zero, one
+and two realize every possible zero/nonzero scalar-map type, so this covers
+the sector optimization rather than truncating an ambient-matrix search.
+Eight rejection controls cover all three missing required endpoint sectors,
+zero/equal pivots, an out-of-field product, a nonfield order and a mutated
+projector. Explicit exceptions keep checks active under optimized Python.
+
+The finite-field and matrix helpers are adapted from Nick Petalas's #4771
+verifier, with exact provenance in SOURCES.json. The new constructions,
+parameter domain and optimization implement the unequal-pivot theorem.
+No predecessor executable is imported or invoked at runtime.
+
+## Reproduction
+
+From the repository root, using CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/unequal-pivot-schur-dimension/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/unequal-pivot-schur-dimension/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/unequal-pivot-schur-dimension
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/unequal-pivot-schur-dimension --check-source-history
+```
+
+Any CPython 3.12 interpreter can replace the local interpreter path. The direct
+verifier writes nothing and prints `PASS_UNEQUAL_PIVOT_SCHUR_DIMENSION`, the
+counts above and a generated SHA256 receipt for all six package files.
+Metadata and source-history checks are separate from mathematical acceptance.
+Each registered command has a 60-second timeout. Local measured durations were
+0.113 seconds ordinary and 0.115 seconds optimized on CPython 3.12.15.
+These are check durations, not performance comparisons.
+
+The selected source-binding orientation passed after its inputs were
+materialized. Current guidance replaces the card's historical first command
+with `scripts/research_selected_baseline.py`. This checks metadata only.
+
+## Scope and implementation bounds
+
+The proof covers one-coordinate deletion, distinct nonzero scalar pivots and
+commuting field idempotents. Equal pivots are credited predecessor work.
+Larger prescribed product blocks, nonfield rings and later elimination
+states remain outside scope. Header production/frequency, physical caller,
+restoration, stock, precision and the complete consumer bill are unknown.
+No supplier admission, selected-frontier change or complete multiplication
+theorem is supplied. Independent human and formal proof-kernel review are
+unclaimed. No Lean, Docker or selected operator replay was run.
+
+The verifier has no recursion, subprocess, callback or generated code. Its
+six fixed field domains have order at most nine; matrices have at most five
+rows, helper capacities permit six rows, and elimination has at most twelve
+columns. Scalar vector scans total at most 1+9^2+9^4 iterations per field; each pattern product
+has four factors of at most four types, and receipts read six files of at
+most 100,000 bytes each. No result matrices accumulate across triples.
+Functions stay below 60 physical lines. Both registered modes use warnings
+as errors. No external static analyzer is installed or claimed.
+
+Power of Ten rule 3 deviation: CPython and its standard library allocate
+dynamically. The fixed domains and stated collection limits bound live data,
+but do not prohibit allocation after initialization. The verifier owns no
+external mutable resources. Reassess capacities before exposing search sizes
+as external inputs.
+
+## Open next questions
+
+1. Determine the least dimension for unequal scalar block pivots pI_d,qI_d
+   and prescribed leading product H. Begin with a nondiagonal 2-by-2 H.
+   Scalar nonvanishing no longer determines sector-map ranks; no block theorem
+   is provided here.
+2. Count complete headers realizing one prescribed unequal-pivot profile.
+   Begin with the F3 p=1,q=2,h=2 construction and specify the weighted header
+   ensemble. Existence alone does not give frequency or paid production cost.
+
+Structured questions, first steps and blockers are in [TASK.json](TASK.json).
+
+## Credit and task scope
+
+Nick Petalas's #4771 supplies the explicit open question, equal-pivot theorem
+and finite-field/matrix helpers. Nick Petalas's #4746 and ssafwann's
+#4671/#4657 supply earlier identity-pivot sector constructions. Nick
+Petalas's #4278/#4597 supplies scalar and ordered block factorizations.
+Ryanson Jonathan's #4609/#4617 and lee-phys's #4634 supply preceding
+small-field and block sharpness examples. 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
+question. It settles a new prescribed-boundary minimum without extending a
+physical construction. Canonical main, source pins and overlap limitations
+are recorded in TASK.json and SOURCES.json.
+
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131498).

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

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "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/scalar-pivot-schur-dimension/README.md",
+      "usage": "provenance",
+      "git_blob": "7ccd8ef743a665e4177cbc712da78ec58da0e83a",
+      "sha256": "326fbbab0d25a94113e4ede541873025209a26ac3d3171b2c4ea48189982dad0"
+    },
+    {
+      "path": "research/scalar-pivot-schur-dimension/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "ebfb0d1b1c57651a0a34434ca42aec05e4ddc6b6",
+      "sha256": "c3573842b497de3b41d4cd5b6ef72edfee8e4cc968acfdfc27bfcbb5b3ca09d2"
+    },
+    {
+      "path": "research/scalar-pivot-schur-dimension/verify.py",
+      "usage": "provenance",
+      "git_blob": "dcaacaee1b8b36bc1afcac1f192d1d7d3aba00ca",
+      "sha256": "136cf14c409556a76b344aa99ba3ef58c8612d7cd87f7ea456ecd97181cfb76a"
+    },
+    {
+      "path": "research/schur-commutator-criterion/README.md",
+      "usage": "provenance",
+      "git_blob": "6b37342de04f5c42c198dd6ba14cea9845be6f05",
+      "sha256": "5616da2e708a8425f1bf0bf5c89c236ef8ed0a23d0544d30ae2142ffe167dc01"
+    }
+  ]
+}