Prove nonmaximal Schur-commutator ranks form an interval with a sharp binary dimension law (no new κ)

research/schur-intermediate-ranks/PROOF.md

@@ -0,0 +1,164 @@
+# Nonmaximal Schur-commutator ranks for prescribed pivots
+
+Nick Petalas. Apache-2.0.
+
+This answers, in part, Open next question 1 of Krzysztof Wojt's
+[PR #5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128)
+(`research/arbitrary-pivot-schur-minimum`). Its sector factorization, the maps
+`L,R` of its equations (4), (7), (8) and its rank-`2d` minimum are cited, not
+rechecked. Sections 1–4 are an all-field proof. Section 5 is a finite
+certificate.
+
+## 0. Setting
+
+Let K be a field, d >= 1, A,B in GL_d(K), H in M_d(K). Put
+
+```
+T00 = I-A-B+H,  T10 = A-H,  T01 = B-H,  T11 = H,   nu_j = nullity T_j.
+```
+
+Consider commuting idempotents P,Q in M_n(K) with `P11=A`, `Q11=B`,
+`(PQ)11=H`, Schur complements S, Z as in #5128, and ρ = rank(SZ-ZS).
+
+## 1. Reduction to two block subspaces
+
+By #5128 §3–4, such pairs are exactly the choices of sector spaces V_j and maps
+`Y_j: U -> V_j`, `X_j: V_j -> U` with `X_j Y_j = T_j` (U = K^d); then
+n = Σ dim V_j. By #5128 (5), (7), (8),
+
+```
+SZ-ZS  ~  L R,   L = Y G,   R = G' X,
+```
+
+with `Y = diag(Y10,Y01,Y11)`, `X = diag(X10,X01,X11)` and fixed maps
+
+```
+G(x,y)    = (A^-1 y, -B^-1(Hx+y), (I-B^-1 H)x + (A^-1-B^-1)y),
+G'(a,b,c) = (A^-1 a - B^-1 b + (A^-1-B^-1)c,  H B^-1 b + (H B^-1 - I)c).
+```
+
+The 00 sector does not enter L or R. Put `M = G G'` on U^3,
+`I = im X = ⊕ I_j` and `N = ker Y = ⊕ N_j`. Then `I_j ⊇ im T_j`,
+`N_j ⊆ ker T_j`, and
+
+```
+ρ = rank(Y M X) = dim(M I + N) - dim N =: f(I,N).                (1)
+```
+
+**Cost.** For fixed (I_j, N_j) the least dim V_j is
+`dim I_j + (d - dim N_j) - rank T_j`. Sylvester's inequality gives the lower
+bound. For attainment, write T_j = σφ with σ a basis of im T_j, add
+coordinates ψ reading a complement of N_j in ker T_j, and add columns τ
+completing σ to a basis of I_j:
+
+```
+Y_j = [φ; ψ; 0],   X_j = [σ, 0, τ].
+```
+
+Then `X_j Y_j = T_j`, `im X_j = I_j`, `ker Y_j = N_j`. The 00 sector costs
+at least rank T00, attained by a rank factorization. Hence
+
+```
+n_min(ρ) = rank T00 + Σ nu_j + min{ dim I - dim N : f(I,N) = ρ },     (2)
+```
+
+the minimum over block subspaces `im T_j ⊆ I_j`, `N_j ⊆ ker T_j`. Any larger
+n is reached by padding the 00 sector.
+
+## 2. Unit steps
+
+Enlarging I by one dimension, or shrinking N by one, raises the cost in (2)
+by exactly one and changes f by 0 or +1. For I this is immediate from (1).
+For N' ⊂ N of codimension one, `dim(MI+N')` falls by at most one while
+`dim N'` falls by exactly one. Every admissible (I,N) is reached from
+`(im T, ker T)` by such steps. Consequences:
+
+* The least dimension at any rank is `n0 = rank T00 + Σ rank T_j`. At n0 the
+  rank is forced: `ρ0 = f(im T, ker T) = rank(T M T)`, with
+  `T = diag(T10,T01,T11)`.
+* Every feasible rank lies in [ρ0, 2d]. If ρ is feasible at n, so is every
+  rank in [ρ0, ρ]: a step chain to the attaining pair passes through each
+  value. Thus **the ranks feasible at dimension n form the interval
+  [ρ0, ρmax(n)]** for n >= n0, and none are feasible below n0.
+* `n_min(ρ) >= n0 + (ρ - ρ0)`.
+
+## 3. Deficiency identity
+
+Let `a = Σ (d - dim I_j)` and `b = Σ dim N_j`. Then
+
+```
+rank R = 2d - a,     rank L = 2d - b.                            (3)
+```
+
+*R.* A row pair (u,v) annihilates R exactly when
+`Φ(u,v) = (uA^-1, (-u+vH)B^-1, u(A^-1-B^-1) - v + vHB^-1)` lies in
+`⊕ I_j^⊥` (#5128 (8)). Φ is injective because G' is onto. Each pure
+covector lies in im Φ:
+
+```
+w(A-H)=0:  Φ(wA, w)  = (w, 0, 0),
+w(B-H)=0:  Φ(0, w)   = (0, w, 0),
+wH=0:      Φ(0, -w)  = (0, 0, w).
+```
+
+Since `I_j ⊇ im T_j`, `I_j^⊥` lies in the left kernel of T_j. Hence
+`⊕ I_j^⊥ ⊆ im Φ`, the annihilator of R has dimension exactly a, and
+`rank R = 2d - a`.
+
+*L.* `ker L = G^-1(N)`. Each pure vector of `⊕ ker T_j` lies in im G:
+
+```
+(A-H)z=0:  G(-z, Az) = (z, 0, 0),
+(B-H)z=0:  G(z, 0)   = (0, -z, 0),
+Hz=0:      G(z, 0)   = (0, 0, z).
+```
+
+G is injective, so `dim ker L = dim N = b`.
+
+From (3), `2d - a - b <= ρ <= 2d - max(a,b)`. In particular
+`a + b <= 2(2d - ρ)`. The cost in (2) equals `rank T00 + Σ nu_j + 3d - a - b`,
+and `nmax = 3d + rank T00 + Σ nu_j` is #5128's formula. Therefore
+`n_min(ρ) >= nmax - 2(2d - ρ)`.
+
+## 4. All-field theorem
+
+For every field, d, A,B in GL_d(K) and H in M_d(K):
+
+```
+feasible ranks at n = [ρ0, ρmax(n)]        (n >= n0; empty below n0),
+n0 = rank T00 + Σ rank T_j,     ρ0 = rank(T M T),
+n_min(ρ) >= max( n0 + ρ - ρ0,  nmax - 2(2d - ρ) ),   ρ0 <= ρ <= 2d.   (4)
+```
+
+Both bounds are tight at their endpoints: n_min(ρ0) = n0 and
+n_min(2d) = nmax (#5128). Also `2d - 2Σ nu_j <= ρ0 <= 2d - Σ nu_j`, by (3)
+at a = b = Σ nu_j.
+
+Equality in (4) for all fields and all d is **not** proved here. Attainment
+needs a pair with a = b and `im R ∩ ker L = 0` at every intermediate rank, plus
+efficient unit steps below the crossover. Section 5 certifies equality only
+for d = 2 over F2.
+
+## 5. Finite certificate: d = 2 over F2
+
+`verify.py` enumerates all 576 triples A,B in GL_2(F2), H in M_2(F2)
+(288 with AB != BA). For each it enumerates every admissible block pair
+(I,N) and computes (1) and (2) exactly. It checks (3) and the sandwich on
+every enumerated pair, and checks that equality holds in (4) for every ρ.
+For every triple and every feasible rank it then assembles a literal pair
+P,Q at the claimed least n, recomputes the Schur complements from the matrix
+entries, and checks idempotence, commutation, the three blocks and the rank.
+That is 2,496 literal witnesses.
+
+Outcome: ρ0 is 0 for 408 triples, 2 for 144 and 4 for 24; there are 16
+distinct profiles. Rank two, the first step named in #5128, is feasible at
+n exactly when ρ0 <= 2 and `n >= max(n0 + 2 - ρ0, nmax - 4)`. The 24 triples
+with ρ0 = 4 are those with T10, T01, T11 all invertible. They admit only
+rank 4, at n = n0 = nmax.
+
+## 6. Boundary
+
+This concerns one common deletion with invertible pivots over a field. It
+gives no header count, physical header producer or consumer, dirty-owner
+restoration, precision, stock, recursive compilation or outer transfer. No
+kappa changes.

research/schur-intermediate-ranks/README.md

@@ -0,0 +1,115 @@
+# Nonmaximal Schur-commutator ranks for prescribed pivots
+
+**Scoped all-field proof plus an exact finite certificate. No new kappa.**
+Produced by Nick Petalas. Apache-2.0.
+
+Krzysztof Wojt's [PR #5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128)
+(`research/arbitrary-pivot-schur-minimum`) finds the least dimension n at which
+commuting idempotents P,Q with prescribed invertible pivots `P11=A`, `Q11=B`
+and product block `(PQ)11=H` reach Schur-commutator rank 2d. Its Open next
+question 1 asks which smaller ranks are feasible at each ambient dimension. It
+names d=2 over F2, rank two, as a first step. This package answers that first
+step for every rank and proves an all-field lower bound.
+
+## Result
+
+Write `T00=I-A-B+H`, `T10=A-H`, `T01=B-H`, `T11=H`, `nu_j = nullity T_j`,
+`nmax = 3d + rank T00 + Σ nu_j` (#5128), and
+
+```
+n0   = rank T00 + rank T10 + rank T01 + rank T11,
+rho0 = rank(T M T),   T = diag(T10,T01,T11),
+```
+
+where `M = G G'` is built from #5128's ordered factors (PROOF.md §1).
+
+**Theorem (every field, every d; [PROOF.md](PROOF.md)).**
+
+1. No pair exists below n0. At n0 the rank is forced to rho0.
+2. For n >= n0, the feasible ranks form the interval `[rho0, rhomax(n)]`.
+   Ranks below rho0 never occur.
+3. For rho0 <= rho <= 2d,
+   ```
+   n_min(rho) >= max( n0 + rho - rho0,  nmax - 2(2d - rho) ).
+   ```
+   Both terms are tight at their endpoints: `n_min(rho0)=n0` and
+   `n_min(2d)=nmax`.
+
+The second term comes from a new deficiency identity. If the sector images
+lose total dimension a and the sector kernels have total dimension b, then
+`rank R = 2d-a` and `rank L = 2d-b` exactly. Hence
+`2d-a-b <= rho <= 2d-max(a,b)`.
+
+**Finite certificate (d=2, F2).** Equality holds in (3) for all 576 triples
+`A,B in GL_2(F2)`, `H in M_2(F2)`, 288 of them with AB != BA. rho0 is 0 for
+408 triples, 2 for 144 and 4 for 24, with 16 distinct profiles. For the first
+step named in #5128: rank two is feasible at n exactly when rho0 <= 2 and
+`n >= max(n0+2-rho0, nmax-4)`. The 24 triples with T10, T01, T11 all
+invertible admit only rank four.
+
+Example: A=B=H=I gives the profile n = 2, 4, 6, 8, 10 for rho = 0..4, so each
+extra rank costs two dimensions. Profiles with crossover, such as
+n = 3, 4, 5, 7, 9, show both terms of the maximum binding.
+
+## Evidence
+
+[verify.py](verify.py) is standard-library only. For each triple it enumerates
+every admissible block pair `im T_j ⊆ I_j`, `N_j ⊆ ker T_j` and computes
+the exact least dimension of every rank. On every enumerated pair it checks
+`rank R = 2d-a`, `rank L = 2d-b` and the sandwich bound. It checks the closed
+law for every triple. For every triple and every feasible rank, it then
+assembles a literal pair P,Q at the claimed least n. It recomputes S and Z from
+the matrix entries and checks idempotence, commutation, all three prescribed
+blocks and the rank: 2,496 literal witnesses. Four seeded controls must be
+rejected: a slope-one-only law, the rank-2d formula used at every rank, a
+corrupted P entry and a wrong prescribed H.
+
+The exhaustive minimum is complete for d=2 over F2 because of the reduction
+in PROOF.md §1. Every pair arises from sector factorizations, and the cost
+of each (I,N) choice is its proved minimum.
+
+## Reproduce
+
+From the repository root (any CPython 3.12; about 2 s each):
+
+```sh
+python3.12 -I -W error -B research/schur-intermediate-ranks/verify.py
+python3.12 -I -O -W error -B research/schur-intermediate-ranks/verify.py
+python3.12 -B scripts/research_package.py --package research/schur-intermediate-ranks
+python3.12 -B scripts/check_research_commit.py --package research/schur-intermediate-ranks --check-source-history
+```
+
+Expected final line: `PASS_SCHUR_INTERMEDIATE_RANKS_D2_F2`, with
+`rows_sha256 e18d15092793582f8d16939086fb512563ecbffc95e0f537ddece6873232dc81`.
+
+## Limitations
+
+Equality in the lower bound is proved only for d=2 over F2. For other d and
+fields it is a bound, not a formula. The theorem concerns one common deletion
+with invertible pivots. It gives no header frequency, physical producer or
+consumer, dirty-owner restoration, precision, stock or outer transfer. The
+selected frontier and kappa are unchanged. No independent human or formal
+proof-kernel review is claimed.
+
+## Open next questions
+
+1. **Does equality hold for every d and field?** Equality would give a closed
+   form for the whole trade-off and complete #5128's question 1. First step:
+   run the same reduction for d=2 over F3 and d=3 over F2. Then try a two-phase
+   chain: single efficient steps up to the crossover, followed by paired I/N
+   steps that keep `im R ∩ ker L = 0`. Blocker: over small fields that
+   transversality might fail for every admissible choice.
+2. **Is there a closed form for rho0?** The ranks of the T_j alone do not fix
+   it in the binary data. Begin with the proved sandwich
+   `2d - 2Σ nu_j <= rho0 <= 2d - Σ nu_j` and find the extra invariant.
+
+## Credit
+
+Produced by Nick Petalas. Krzysztof Wojt's #5128 supplies the arbitrary-pivot
+sector factorization, the ordered maps L, R and the rank-2d minimum, and poses
+the question answered here. These are cited, not rechecked. The earlier
+Schur-family lineage credited in that package keeps its credit: ssafwann's
+#4657/#4671 sector and split-factor method, Nick Petalas's #4597/#4746/#4771/
+#4774/#4785, Ryanson Jonathan's #4609/#4617 and lee-phys's #4634. The new work
+is the reduction to block subspace pairs, the unit-step interval theorem, the
+deficiency identity with its lower bound, and the d=2 binary certificate.

research/schur-intermediate-ranks/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "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/arbitrary-pivot-schur-minimum/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c7d58883b4df5ddab4f237a521458b7f506b3617",
+      "sha256": "77118415edf74aa4b6a49c94cb735913ad08377802ab44f3f51f66531b46593a"
+    }
+  ]
+}

research/schur-intermediate-ranks/TASK.json

@@ -0,0 +1,81 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Which Schur-commutator ranks below 2d are feasible, and at which least ambient dimension, for commuting idempotents with prescribed invertible pivots A,B and product block H (Open next question 1 of PR #5128)?",
+  "scope_change_reason": "The card asks for decoder/coframe changes with a full signed moment. This package answers a structural open question posed by PR #5128 in the Schur block-deletion family, which bounds the rank available to such a decoder request. It does not price a decoder.",
+  "bottleneck_link": "Side result. It gives the exact rank/dimension trade-off for one Schur deletion request, which a header or decoder design would need before pricing. It does not change any supplier bill or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at an all-field lower bound and an exact d=2 F2 certificate; list general attainment as open rather than extending the search.",
+  "outcome": "partial",
+  "evidence": "PROOF.md proves, over every field, that feasible ranks at each n form an interval [rho0, rhomax(n)] and n_min(rho) >= max(n0+rho-rho0, nmax-2(2d-rho)). verify.py certifies equality for all 576 triples at d=2 over F2, with 2,496 literal commuting idempotent witnesses and 4 rejected controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does equality n_min(rho)=max(n0+rho-rho0, nmax-2(2d-rho)) hold for every d and every field?",
+      "why_it_matters": "It would give a closed form for the whole rank/dimension trade-off, completing PR #5128 Open next question 1.",
+      "first_step": "Run the same exhaustive reduction for d=2 over F3 and d=3 over F2, then try a two-phase step chain: efficient single steps up to the crossover, then paired I/N steps keeping im R and ker L transverse.",
+      "blocked_by": "Over small fields the transversality im R ∩ ker L = 0 may fail for every admissible choice; no general argument is given."
+    },
+    {
+      "question": "Is there a closed form for rho0 = rank(T M T) in terms of A,B,H?",
+      "why_it_matters": "rho0 is the forced rank at the absolute minimum dimension n0; ranks alone of the T_j do not determine it (d=2, F2 data).",
+      "first_step": "Compare rho0 against the sandwich 2d-2*sum(nu_j) <= rho0 <= 2d-sum(nu_j) on the 576 binary triples and identify the extra invariant.",
+      "blocked_by": "None known."
+    }
+  ]
+}