[petalas]

Summary

Scoped algebraic proof with finite corroboration. For commuting field idempotents with distinct nonzero scalar leading entries p,q and prescribed leading product h, the exact least ambient dimension attaining Schur-commutator rank two is

N(p,q,h) = 3 + [h in {0,p,q}] + [1-p-q+h != 0].

Every minimum is attained. Over F3, p=1,q=2 gives dimensions five, five and four at h=0,1,2. Over F5, p=2,q=3,h=4 gives dimension three.

This answers Open next question 1 of #4771, head 22cb0bda57237d39d0e6944b232447d3a2809311. Its equal-pivot theorem is cited rather than audited. The new unequal-pivot case needs one two-dimensional zero-product sector at each endpoint, while the predecessor p=q=h case needs two. The formula includes a lower bound and an explicit attaining construction over every field.

Only research/unequal-pivot-schur-dimension/ is added. The contribution was produced by Nick Petalas. Credit Nick Petalas #4771/#4746/#4278/#4597, ssafwann #4671/#4657, Ryanson Jonathan #4609/#4617, lee-phys #4634, and the retained BIT/header lineage detailed in the package. The finite-field and matrix helpers are adapted from #4771 with exact source provenance; no predecessor executable is invoked at runtime. No new kappa or selected-frontier change.

Advance claim. The formal-interface-lemma card is explicitly changed to this algebraic side question. Base is canonical main 624de9dc66858af0945e5f8a0942488d62280d43, priority revision 7.

Evidence

Before: #4771 explicitly leaves unequal pivots open. After: PROOF.md classifies the three active sector directions, gives the exact zero-product dimension charges, and constructs attaining matrices.

• All 1,140 parameter triples over F3,F4,F5,F7,F8,F9 pass literal checks of idempotence, commutation, prescribed pivots/product, direct Schur multiplication, commutator rank and the scalar factorization.
• A separate exact optimization enumerates 14,270 scalar vector pairs and 3,528 sector-map patterns. Every minimum agrees. Dimensions zero, one and two realize every scalar-map zero/nonzero type; this is not an ambient-matrix truncation.
• Eight rejection controls cover three missing required endpoint sectors, invalid zero/equal pivots, an invalid product, a nonfield order and a mutated projector. The checks remain enabled under optimized Python.
• Both registered commands pass on CPython 3.12.15. Measured local durations are 0.113 seconds ordinary and 0.115 seconds optimized, against separate 60-second timeouts. These are check durations, not speed comparisons.
• Package metadata/replay, six-file committed-byte/source-history preflight, export integrity, and an optimized read-only Git-free export replay pass on a012548529a25a103345e8e8a8afa707a2b3a3e6. All seven exported files, including the export receipt, remain unchanged.
• Syntax/function-capacity inspection passes; the longest function has 33 lines. Both registered commands use warnings as errors. The bounded CPython allocation deviation is documented. No external static analyzer is installed or claimed.
• The selected source-binding orientation passes after sparse inputs are materialized. This is metadata orientation, not a selected scientific replay.

From the repository root:

/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

Expected markers are PASS_UNEQUAL_PIVOT_SCHUR_DIMENSION, PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed, and PASS_RESEARCH_COMMIT_BYTES. Any CPython 3.12 interpreter can replace the local path. The verifier writes no files and generates a receipt bound to all six package files. Publication ancestry checks require full Git history.

Optional committed export and offline integrity check, choosing an unused output path:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/export_research_package.py export --package research/unequal-pivot-schur-dimension --ref a012548529a25a103345e8e8a8afa707a2b3a3e6 --output /tmp/unequal-pivot-schur.tar
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/export_research_package.py check /tmp/unequal-pivot-schur.tar

Limitations and unrun obligations

The universal claim rests on the written algebraic proof, with finite corroboration. It covers one-coordinate deletion, commuting field idempotents, and distinct nonzero pivots. Larger prescribed matrix products, coefficient rings and later elimination states are outside scope. Header production/frequency, physical caller, restoration, precision, stock and the complete consumer bill remain unknown. No supplier admission or complete multiplication theorem follows.

Independent human and formal proof-kernel review are unclaimed. Lean, Docker and selected scientific cold replay were not run. Every registered local check ran.

Related open work

This account's open PRs created since the CLAIM at 2026-10-22 19:43:47 UTC were refreshed before DONE. The five other newly opened PRs were read for overlap.

• Prove the binary pair-versus-singleton full-guard inequality (no κ) #4777 studies three orthogonal corank-one requests over F2 and a full-guard probability inequality. F2 has only one nonzero scalar, so it has no parameter pair with p!=q in this theorem; there is no overlapping numerical minimum to compare.
• Prove all-field negative correlation for one-way full guards (no κ) #4778 studies all-field full-guard correlation for one-way coupled, noncommuting requests. This theorem assumes commuting idempotents and computes minimum dimension, so the input domains and numerical quantities are disjoint.

The other new account PRs #4776, #4780 and #4781 study right-vector target reachability or factor counts over coefficient algebras; they do not assert this Schur dimension or an overlapping numerical minimum. The merged predecessor #4771 fixes equal pivots, also a disjoint parameter domain. Its equal-pivot theorem and explicit unequal-pivot open question retain their credit.

At initial publication no same-object open PR appeared in the live Schur title/body search. Canonical-main README and merged-PR searches were refreshed before committing. Sparse local notes, unpublished work and arbitrary code diffs remain outside the completeness claim; TASK.json records that earlier coverage and exact source pins.

Open next questions

1. Determine the least dimension for unequal scalar block pivots pI_d,qI_d and prescribed product H, beginning with a nondiagonal 2-by-2 H. Scalar nonvanishing no longer determines sector-map ranks.
2. Count complete headers for a prescribed unequal-pivot profile, beginning with F3 p=1,q=2,h=2 after specifying the weighted header ensemble. Existence alone gives neither frequency nor a paid producer.

CI notes

Both hosted checks passed on contribution head a012548529a25a103345e8e8a8afa707a2b3a3e6 in run 39843460454: plan in 3m10s and the registered research/unequal-pivot-schur-dimension replay in 1m9s. The registered replay runs both ordinary and optimized verification commands. All registered local checks, committed-byte/source-history preflight and Git-free export replay also passed. This records execution of the scoped package checks, not independent human or formal proof-kernel acceptance of the universal theorem.

Merge danger

Door: two-way. Blast radius: package. This isolated research addition changes no shared implementation, frozen evidence or selected-frontier file.