Prove the exact scalar-block Schur dimension formula (no κ)

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

@@ -0,0 +1,159 @@
+# Exact dimension for a common scalar block
+
+This proof was produced by Nick Petalas. Apache-2.0.
+
+Let K be any field, d >= 1, lambda in K nonzero and H in M_d(K).
+Consider commuting idempotents P,Q on K^n whose first d-by-d blocks are
+both lambda I_d and whose product PQ has first block H. Let S,Z be the
+two Schur complements after deleting those first d coordinates. Then the
+least n permitting rank(SZ-ZS)=2d is exactly
+
+```text
+n_min(lambda,H) = 3d + rank((1-2lambda)I+H)
+                       + 2 nullity(lambda I-H) + nullity(H).       (1)
+```
+
+Every minimum is attained over K, without diagonalizability assumptions
+on H. This answers Open next question 2 of Nick Petalas's #4771. The
+identity-block result of #4746 and ssafwann's #4671, and the scalar-block-size
+one result of #4771, are cited predecessors. The new part is the common
+nonidentity scalar block with an arbitrary prescribed matrix product.
+
+## Compression and the full-rank criterion
+
+Put U=K^d, V=K^n. Let i:U -> V be coordinate inclusion and pi:V -> U
+coordinate projection, so pi i=I. The joint eigenspace projectors are
+
+```text
+E00=(I-P)(I-Q), E10=P(I-Q), E01=(I-P)Q, E11=PQ.
+```
+
+They give a direct sum V=V00+V10+V01+V11 in every characteristic. Set
+Y_j=E_j i:U -> V_j and X_j=pi restricted to V_j:V_j -> U. Write
+
+```text
+D=lambda I-H,   T0=(1-2lambda)I+H,
+a=nullity(H),  b=nullity(D),  c=rank(T0).
+```
+
+Compression gives
+
+```text
+X00 Y00=T0,  X10 Y10=D,  X01 Y01=D,  X11 Y11=H.             (2)
+```
+
+In particular, their sum T0+2D+H is I. The signed joint-sector method
+comes from ssafwann's #4671 and Nick Petalas's #4746. Here the products
+and the rank argument retain lambda throughout.
+
+Use Nick Petalas's ordered block Schur identity from #4597, with equal
+pivot blocks lambda I. Its ambient factors are
+
+```text
+A=[PQ i-Q i H/lambda, (P-Q)i/lambda] : U^2 -> V,
+B=[pi(P-Q)/lambda; -pi PQ+H pi Q/lambda] : V -> U^2.
+```
+
+We have pi A=0 and Bi=0. Since V=i(U) direct-sum ker pi, the Schur
+commutator is the product of A in ker pi coordinates and B restricted to
+ker pi. Thus its rank is 2d exactly when A is injective and B is onto.
+In joint-sector coordinates,
+
+```text
+A(x,y) = (1/lambda)(0, Y10 y, -Y01(Hx+y), Y11 D x),
+B(v00,v10,v01,v11)
+       = (1/lambda)(X10 v10-X01 v01,
+                     H X01 v01-D X11 v11).                    (3)
+```
+
+**Criterion.** Rank(SZ-ZS)=2d if and only if Y10,Y01,Y11 are injective
+and X10,X01,X11 are onto.
+
+For necessity, rank 2d forces A injective. If Y10 z=0, (2) implies
+Dz=0, hence Hz=lambda z. Equation (3) then gives A(z,-lambda z)=0,
+so z=0. If Y01 z=0, the same product equation gives Dz=0 and
+A(z,0)=0, hence z=0. If Y11 z=0, (2) gives Hz=0. Thus
+Dz=lambda z and again A(z,0)=0, hence z=0. This proves all three
+injections. Apply the same necessity argument to the dual commuting
+projectors with inclusion pi* and projection i*. Their commutator has
+the same rank, and their sector inclusion ranks are the ranks of X_j*.
+Consequently the three X_j are onto.
+
+For sufficiency, A(x,y)=0 first gives y=0 by injectivity of Y10.
+The other two sectors give Hx=Dx=0. Since H+D=lambda I and lambda
+is nonzero, x=0. Thus A is injective. If a covector (u,v) annihilates B,
+surjectivity of X10 gives u=0. Surjectivity of X01 and X11 then gives
+vH=vD=0, hence lambda v=0 and v=0. Thus B is onto. As Bi=0,
+its restriction to ker pi is onto too. Their product has rank 2d,
+proving the criterion.
+
+## Lower bound and attaining construction
+
+Let r_j=dim V_j. For every active sector 10,01,11, the criterion and
+the rank inequality for a product imply
+
+```text
+rank(X_j Y_j) >= rank X_j + rank Y_j - r_j = 2d-r_j.
+```
+
+Equation (2) therefore gives the componentwise necessary bounds
+
+```text
+(r00,r10,r01,r11) >= (c,d+b,d+b,d+a).                         (4)
+```
+
+Their sum is (1). Also rank P=r10+r11 and rank Q=r01+r11 are
+each at least 2d+a+b. These input-rank bounds can be attained together
+with all four sector bounds.
+
+For an arbitrary d-by-d matrix T, let N_T have columns forming a
+complement to im T in U. On a space of dimension d+nullity(T) put
+
+```text
+X_T=[T N_T],     Y_T=[I;0].
+```
+
+Then X_T Y_T=T, X_T is onto and Y_T is injective. Use this for T=D
+in sectors 10 and 01 and for T=H in sector 11. In sector 00 take any
+rank factorization T0=X00 Y00 through dimension c, including dimension
+zero if T0=0. Stack the Y maps to form i and concatenate the X maps to
+form pi. By (2), pi i=T0+2D+H=I.
+
+On this direct sum let P0 and Q0 act by their sector eigenvalues 00,
+10,01,11. Complete i to a coordinate basis M=[i N], where N is a basis
+of ker pi. This is invertible because pi i=I. Then
+
+```text
+P=M^-1 P0 M,    Q=M^-1 Q0 M
+```
+
+are commuting idempotents with the prescribed leading blocks and product.
+All six active maps have full rank, so (3) proves sharpness. The dimension
+is exactly c+2(d+b)+(d+a). This proves (1) and simultaneous attainment
+of (4) and both input-rank bounds over every field.
+
+## Specializations and a nondiagonal example
+
+At lambda=1, c=rank(H-I)=d-b, so (1) reduces to the predecessor
+identity-pivot formula 4d+a+b. At d=1 it reduces to all three cases
+of the predecessor scalar formula in #4771. These are calibration
+specializations, not new results.
+
+For a new nondiagonal instance, over F5 take
+
+```text
+lambda=2,   d=2,   H=[[3,1],[0,3]].
+```
+
+Here T0=[[0,1],[0,0]] has rank one, while H and D=2I-H are
+invertible. Thus the exact minimum is seven, with sectors (1,2,2,2),
+input ranks four and Schur-commutator rank four. Replacing this Jordan
+block by 3I gives minimum six. A nondiagonal nilpotent part can therefore
+change the minimum even when H and lambda I-H have the same nullities.
+The construction above realizes both cases directly.
+
+This is a scoped algebraic proof, not a complete multiplication theorem.
+It supplies neither header frequencies nor a paid header producer or
+consumer. Unequal block pivots, general coefficient rings, subsequent
+Schur-state transitions, precision, restoration and stock remain separate
+obligations. Independent human and formal proof-kernel review are unclaimed.

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

@@ -0,0 +1,143 @@
+# Exact Schur dimension for a common scalar block
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with finite corroboration. For every field K,
+every nonzero lambda in K and every prescribed H in M_d(K), d >= 1, the least
+ambient dimension of commuting idempotents P,Q with common leading blocks
+lambda I_d, leading product block H and Schur-commutator rank 2d is
+
+```text
+n_min(lambda,H) = 3d + rank((1-2lambda)I+H)
+                     + 2 nullity(lambda I-H) + nullity(H).
+```
+
+Every minimum is attained by the construction in [PROOF.md](PROOF.md), including
+nondiagonal and nondiagonalizable H. The four minimal joint-sector dimensions
+are `(rank((1-2lambda)I+H), d+b, d+b, d+a)`, where `a=nullity(H)` and
+`b=nullity(lambda I-H)`. Both input projectors simultaneously have minimum
+rank `2d+a+b`.
+
+This answers Open next question 2 of
+[PR #4771](https://github.com/CrocSwap/integer-mult-bounds/pull/4771), pinned at
+`22cb0bda57237d39d0e6944b232447d3a2809311`. That package treats scalar block
+size one. Nick Petalas's #4746 and ssafwann's #4671 treat identity blocks.
+Their results are cited inputs and specializations, not audit targets. The new
+result allows a nonidentity scalar block and an arbitrary matrix product H.
+No new kappa or selected-frontier change is claimed.
+
+For example, over F5 with lambda=2 and `H=[[3,1],[0,3]]`, the exact minimum
+is seven, with sectors `(1,2,2,2)`, input ranks four and Schur-commutator
+rank four. For the diagonal product `H=3I_2` the minimum is six. Both H and
+`2I-H` are invertible in both examples. The nilpotent part changes the
+00-sector rank, which the identity-pivot formula does not capture.
+
+## Evidence and reproduction
+
+The proof specializes the ordered block identity of #4597 and proves that
+sharpness is equivalent to injectivity and surjectivity of all six active
+sector maps. The rank inequality bounds each sector separately. A split
+factorization attains all four bounds and both input ranks simultaneously.
+The proof holds over every field; the finite checks are corroboration.
+
+The independently written standard-library verifier imports no predecessor
+executable. It constructs full P,Q and directly checks idempotence,
+commutation, both scalar block pivots, the prescribed product block, Schur
+idempotence, rank drops, the ordered commutator factorization, the six-map
+criterion, the ambient minimum and both input ranks. Its executed domains are:
+
+- All 3,446 pairs `(lambda,H)` with nonzero lambda and every two-by-two H over
+  F2,F3,F4,F5, respectively 16, 162, 768 and 2,500 constructions.
+- All 210 scalar pairs over F2,F3,F4,F5,F7,F8,F9, including direct numerical
+  comparison with #4771's piecewise scalar specialization.
+- 482 additional Jordan and companion-style constructions at d=2,3 over
+  those seven fields. These overlap the exhaustive domains where applicable.
+- An independent enumeration of 45,900 full-rank factor pairs over F2,
+  finding the exact minimum middle dimension for each of the 16 two-by-two
+  compressed products. This corroborates the sector cost, rather than
+  enumerating all ambient commuting projector pairs.
+- Six premise-preserving missing-map controls and five malformed-input
+  controls. The former retain commuting idempotents and the prescribed
+  compressed products while lowering one necessary injection or surjection.
+- All 1,808 field triples test associativity and distributivity; every nonzero
+  element has its inverse checked. F4,F8,F9 use irreducible polynomial
+  quotients, rather than arithmetic modulo their orders.
+
+Two explicit checks compare the nondiagonal seven-dimensional F5 example
+with its six-dimensional diagonal control. The generated stdout receipt binds
+all six package files by SHA256. The verifier writes nothing into the checkout.
+
+From the repository root, with CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/scalar-block-schur-dimension/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/scalar-block-schur-dimension/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/scalar-block-schur-dimension
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/scalar-block-schur-dimension --check-source-history
+```
+
+The scientific marker is `PASS_SCALAR_BLOCK_SCHUR_DIMENSION`. A different
+CPython 3.12 path may replace the local path. All checks use explicit exceptions
+and remain active under optimized Python. Metadata and source-history checks
+are separate from mathematical verification. The selected source-binding
+orientation passed; no selected scientific replay was run.
+
+## Scope and code constraints
+
+This is one deletion with equal nonzero scalar block pivots, field coefficients
+and commuting idempotents. It gives no complete-header count, later-state law,
+coefficient-ring theorem or arbitrary-block-pivot dimension minimum. Header
+production, selection/emission, dispatch, dirty restoration, precision, stock
+and the complete physical consumer costs remain unknown. No physical supplier
+admission or complete multiplication theorem follows. Independent human and
+formal proof-kernel review are unclaimed. Lean, Docker and selected cold replay
+were not run.
+
+The verifier has fixed domains, fields of order at most nine, deleted blocks
+of size at most three and constructed matrices of size at most 18. Matrix
+operations enforce a 24-row, 48-column capacity, including augmented elimination.
+The largest exhaustive target scan has 625 matrices per pivot, and the factor
+census retains at most 210 full-rank maps and 16 minima. Only the current full
+construction and counters persist across target scans. All calls are direct;
+there is no recursion, subprocess, callback chain or generated code. Functions
+stay below 60 physical lines. Warnings are errors in both registered commands;
+syntax, function lengths and dynamic-code calls are inspected locally. No
+external static analyzer is installed or claimed.
+
+Power of Ten rule 3 deviation: CPython arithmetic and tuples allocate during
+execution, so this standalone verifier cannot prohibit dynamic allocation.
+The fixed field, matrix, census and six-file receipt capacities bound its live
+data. Both registered modes exercise these bounds, and explicit controls reject
+an oversized matrix and invalid target shapes. The deviation is confined to
+this verifier; reassess storage and input validation before adding larger
+domains or an external parameter interface. It owns no external mutable resource.
+
+## Open next questions
+
+1. Determine the prescribed-H minimum for unequal scalar block pivots pI_d
+   and qI_d at d>=2. This would separate equality of the pivots from their
+   scalarity. Start with the two ambient factors and an H with an eigenvalue
+   at one pivot but not the other. The scalar unequal-pivot question is
+   separately claimed and is not delivered here.
+2. Count complete headers attaining one nonidentity scalar-block profile.
+   Feasibility alone gives no frequency or paid header cover. Start with the
+   F5 profile `(1,2,2,2)`, d=2, lambda=2 and the fixed Jordan product above.
+   A joint factorization count and the producer/consumer bill remain open.
+
+## Credit and task scope
+
+Nick Petalas's #4771 supplies the explicit open matrix-product question and
+scalar predecessor; #4746 supplies the all-field identity-pivot predecessor.
+ssafwann's #4671/#4657 supplies the binary fixed-H theorem, six-map method
+and split-sector construction. Nick Petalas's #4597/#4278 supplies the ordered
+block and scalar Schur factorizations. Ryanson Jonathan's #4609/#4617 and
+lee-phys's #4634 supply earlier 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
+question. It resolves a prescribed-boundary dimension question without auditing
+another contributor or expanding a physical construction. Exact source pins,
+overlap coverage, the advance claim and preserved checkout state are recorded
+in TASK.json and SOURCES.json. No predecessor file or credit line is changed.

research/scalar-block-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/all-field-identity-schur/README.md",
+      "usage": "provenance",
+      "git_blob": "c3a64475cc52ba7025d57d2c1a810a35c563ca40",
+      "sha256": "e702c6e05e3283363294ed10a1b9bc4b589c46cc2fb7df198ec9c6841ec78f78"
+    },
+    {
+      "path": "research/block-schur-commutator/README.md",
+      "usage": "provenance",
+      "git_blob": "79790ccea54cfea1aab611768927651a81f2fb18",
+      "sha256": "945c1420fe9fb5c26dec49e7d6005d77382ca9dc6ca0f424d8baa1500bfc092c"
+    }
+  ]
+}