[krzysztofwojt]

Change and mathematical scope

Proves the exact prescribed-boundary Schur minimum over every field for arbitrary invertible block pivots A,B and arbitrary product block H. The matrices A,B,H need not commute. For commuting idempotents P,Q with P11=A, Q11=B, (PQ)11=H, the least ambient dimension attaining Schur-commutator rank 2d is

n_min = 3d + rank(I-A-B+H)
           + nullity(A-H) + nullity(B-H) + nullity(H).

The proof extends the six-map criterion to noncommuting pivots, derives componentwise sector lower bounds and constructs a pair attaining all four bounds and both minimum input ranks simultaneously. An explicit pairwise-noncommuting rational/ternary example attains n=6 at d=2.

This resolves Open next question 1 of #4774 and #4785 and strengthens their requested unequal-scalar-block scope. It does not claim #4597's existing ordered factor identity as new. The contribution is a written algebraic theorem with finite corroboration, not a proof-kernel or independently human-accepted theorem. No physical supplier, priced header or new kappa; the selected frontier is unchanged.

Task and overlap

• Package: research/arbitrary-pivot-schur-minimum.
• Fresh canonical-main base: 81e9bd69e4a5b00ba9c713a1620e36d576d5522e; contribution head: 2839d35e58b3285a1992a3ecbae2809ebef7661b.
• Task formal-interface-lemma, priority revision 7, scope changed to an explicitly open algebraic side question. The original card remains in TASK.json. This settles a dimension obstruction; it does not discharge a physical interface or alter a multiplication ledger.
• Canonical advance claim: Discussion #5121, with handoff pointer.
• Exact predecessor scientific heads: Prove the sharp 2d block Schur commutator bound (no new kappa) #4597 dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb; Prove the exact unequal-pivot Schur dimension law (no new κ) #4774 a012548529a25a103345e8e8a8afa707a2b3a3e6; Prove the exact scalar-block Schur dimension formula (no κ) #4785 1c9996b87d497a1690630302a0ac65748affbf16. SOURCES.json additionally binds the cited documents at the base. Predecessor censuses are not re-audited.

Before claiming: 307 open PRs, 4,260 Discussion records and all 6,824 pinned-main README/TASK notes were searched. Before submission: a complete refreshed snapshot covered 311 open PRs and 4,281 Discussion records; targeted all-state Schur searches, newer PRs, recent #1166 handoffs, claim replies and this account's recent topics were also checked. Refreshed main 20a1e31bc6009b9b3f4d084bbaadc6350e34fcba leaves the priorities, catalogue, selected result and cited scientific inputs unchanged. No same-scope predecessor or active claim was found in this coverage. Unpublished work and arbitrary PR diffs remain outside that statement.

Validation

Python 3.12.12, standard library only. Passed:

python3.12 -B scripts/research_package.py --package research/arbitrary-pivot-schur-minimum
python3.12 -B scripts/check_research_commit.py --package research/arbitrary-pivot-schur-minimum --check-source-history

The manifest runs both checkers normally and under -O, each with -I -W error -B:

• Primary: 1,386 exact constructed cases across F_2,F_3,F_5,F_7,Q and d=2,3,4, plus two explicit examples. All 576 binary d=2 input triples are covered; the ternary exhaustive component has 8 noncommuting pivot pairs times all 81 H. Checks include full idempotence/commutation, prescribed blocks, literal Schur products, ordered factors, the six-map criterion and attaining ranks/dimensions.
• Independent bitset implementation: all 576 binary fixtures, including 288 noncommuting A,B inputs and 180 pairwise-noncommuting A,B,H inputs; no primary-code imports.
• Six deficient-map controls, two singular-pivot rejections, seven independent corruption/coverage controls. Each H/B-inverse order mutation is detected on 1,017 primary cases.
• Committed-byte and source-history preflight: 9 package files. Official export and integrity check passed. All four direct commands then passed from a fresh read-only Git-free extraction with PATH=/nonexistent; all 10 exported files, including the receipt, remained byte-identical.

Export SHA256: 10575b7c972d21007a7bc06e6f4e60741f7db463036f155ea3714dc7b63a0dc1.
Export receipt SHA256: d3788b5d506d3e2997228668ee35043798db715ed20e9a2107309352dee57564.

The computations corroborate the construction; minimality over all fields comes from PROOF.md, not finite enumeration. No full selected replay, physical admission, or Lean build was run.

Hosted CI limitation: run 39937792203, bound to contribution head 2839d35e58b3285a1992a3ecbae2809ebef7661b, fails the planning job's onboarding helper tests; hosted package replay is skipped. Its eight failures were independently reproduced on untouched main 20a1e31bc6009b9b3f4d084bbaadc6350e34fcba: seven historical-source-role assertions stop on working source drift: scripts/check_research_commit.py, and the standalone cp1252 overlap fixture omits research_package. The existing open repair #5123 addresses those fixture failures. This PR changes none of those files.

All four registered package commands also pass locally at GitHub's exact test merge a947b106c5dd9f784689d3f01b88791696d77dc0, using the newer main helpers. That sparse isolated worktree remains clean. This is a local test-merge replay, not a green hosted CI claim.

Credit

Krzysztof Wojt, with substantial OpenAI Codex assistance; bounded Luna assistance for overlap inventories and the separate binary implementation, reviewed and run by the primary author process. New work Apache-2.0. Nick Petalas #4774/#4785 supplies the open questions, #4771/#4746 the scalar/identity predecessors, and #4597/#4278 the ordered factorizations. ssafwann #4657/#4671 supplies the sector/split method. Ryanson Jonathan #4609/#4617 and lee-phys #4634 retain earlier sharpness credit. Nick Petalas #4259/#4228, Cinna Davis, source527, commdata2338 and Jose Manuel retain the request/normalizer lineage, detailed in the README. No historical priority is claimed for the underlying linear algebra.

Open next questions

The package questions separate nonmaximal Schur ranks from physical realization. A bounded next step is a fixed-boundary d=2 binary rank-two classification; the maximal-rank criterion does not decide it. Turning the ternary n=6 witness into a useful header first requires an actual caller and a complete resource bill. Neither follow-up is claimed here.