diff --git a/research/schur-rank-attainment/.gitattributes b/research/schur-rank-attainment/.gitattributes new file mode 100644 index 0000000000..51d8b75fe1 --- /dev/null +++ b/research/schur-rank-attainment/.gitattributes @@ -0,0 +1,5 @@ +* text eol=lf +reference6031.py -text +reference6031.md -text +reference5128.md -text +reference6053.md -text diff --git a/research/schur-rank-attainment/AUDIT.md b/research/schur-rank-attainment/AUDIT.md new file mode 100644 index 0000000000..274636fe64 --- /dev/null +++ b/research/schur-rank-attainment/AUDIT.md @@ -0,0 +1,59 @@ +# Independent audit of PR6053 at an exact scientific head + +Target: apoursh, [PR6053](https://github.com/CrocSwap/integer-mult-bounds/pull/6053), +head **12385ca23315181e3d15eb23a2d9ffec65d9a909**. +Prepared for SHIN09-git with substantial OpenAI Codex assistance. Apache-2.0. + +## Why the scope changed + +At entry, the complete cached search identified the released questions in +PR6031 and no matching successor. Work began on a coordinate-minor attainment +argument and exact finite corroboration. A second complete live search found +PR6053, opened at 2026-10-28T03:27:51Z during the session. We inspected its exact +proof after finding that overlap. Its theorem is the same dimension law. + +The package therefore became a bounded audit of that exact source. No novelty, +priority or independent human review is claimed. The separately developed +coordinate-minor construction is retained as an alternate verification route. +This audit does not claim to re-run the original PR6053 program or its 886-case +inventory. The new verifier imports no PR6053 executable code. + +## Claims and separate evidence + +| Reviewed claim | Evidence here | +|---|---| +| Every intermediate rank attains the dimension bound | PROOF.md Sections 2–4 give a coordinate-minor deletion construction; it does not require the two-block normal form used by PR6053. | +| rho0 = rank((B-H) A^-1 (A-H)) + rank((A-H) B^-1 (B-H)) + 2 rank H - 2d | Evaluated independently on all 9,389 declared cases and compared to the lifted pairing, T G G' T, and (on finite census domains) the complete subspace oracle. | +| Sector admissibility and least dimension | Every chosen row/column is from the original sector basis. Exhaustive subspace profiles agree on 171,259 pairs. | +| Actual commuting-idempotent witnesses | 32,051 literal P,Q constructions pass an independent raw-matrix checker for idempotence, commutation, A/B/H blocks and Schur rank. | +| Ternary behavior, including odd minima | Complete d=2 F3 input coverage by 8,136 conjugacy representatives, covering all 186,624 raw triples. There are 288 representative cases with rho0=1. | +| Ordered factors and both cost slopes matter | Nine real source mutants are required to fail at the intended scientific checks; ten fixture/formula controls also fail as expected. | + +The structured rational/prime-field cases cover Q and F2,F3,F5,F7,F11 at +d=1..4. The d=3 binary family fixes one pivot pair and enumerates all H; +it does not replace PR6053's differently chosen d=3 cases or claim broader +coverage in every respect. Our total subspace-pair count is smaller than +PR6053's because its selected d=3 cases have different subspace inventories. + +## Written-argument review + +PR6053's six lifted spaces match the credited PR6031 deficiency identities. +The sign choice in the 01 right lift differs from our pure-sector convention +by a nonzero scalar, so it does not change the subspace or pairing rank. + +Its two nonzero cross blocks use disjoint sector row/column spaces. Thus their +within-sector reductions can be made independently; the paired-coordinate +and radical selections respect the original block constraints. Our arbitrary +coordinate-minor chain supplies another attainment argument without needing +that special pairing sparsity. + +For the closed rho0 formula, the block matrix [[F,H],[0,J]] has rank +d + rank(J A^-1 F) after adding the second block column to the first and +eliminating with A=F+H. Swapping F and J gives the ordered B expression. +Subtracting rank F and rank J yields the pairing ranks. Substitution into +rho0=2d-2nu+r gives the stated closed formula, with no commuting-factor step. + +No discrepancy was found in these arguments or the declared exact checks. +This is a review conclusion within the stated field/invertible-pivot/common- +deletion scope, not a machine-checked universal proof. Physical realization +and all supplier costs remain outside the audit. diff --git a/research/schur-rank-attainment/LICENSE b/research/schur-rank-attainment/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/schur-rank-attainment/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/schur-rank-attainment/OVERLAP.json b/research/schur-rank-attainment/OVERLAP.json new file mode 100644 index 0000000000..7e9fb8e5ac --- /dev/null +++ b/research/schur-rank-attainment/OVERLAP.json @@ -0,0 +1,608 @@ +{ + "schema_version": 1, + "question": "All-field and all-d attainment of PR6031's exact dimension lower bound for each Schur-commutator rank.", + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "initial_snapshot": { + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-28T03:04:21.841951+00:00", + "terms": [ + "schur-intermediate-ranks", + "nonmaximal Schur", + "intermediate Schur", + "n_min(rho)", + "rank/dimension trade" + ], + "coverage": { + "local": { + "head": "721c03822c421b7f7fcbb2598993b947c4d88419", + "records": 8350, + "head_records": 8348, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-28T02:58:52.008345+00:00", + "complete_pagination": true, + "records": 318 + }, + "discussions": { + "fetched_at": "2026-10-28T03:02:29.570584+00:00", + "complete_pagination": true, + "records": 5703 + }, + "closed_prs": { + "fetched_at": "2026-10-28T03:03:32.167844+00:00", + "complete_pagination": true, + "records": 5222 + } + }, + "local_records": 8350, + "warnings": [ + "open_prs: offline; cached data may miss current changes", + "discussions: offline; cached data may miss current changes", + "closed_prs: offline; cached data may miss current changes" + ], + "reference_terms": [], + "limits": "Remote PR scope includes open and closed/merged titles and bodies, with separate coverage and timestamps. State changes are deduplicated by latest PR update; snapshots are not atomic. Local coverage compares searched working-tree notes with regular note paths at coverage.local.head; it does not certify HEAD contents or historical coverage. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 8, + "matches": [ + { + "kind": "local-readme", + "title": "research/schur-intermediate-ranks/README.md", + "path": "research/schur-intermediate-ranks/README.md", + "sha256": "6c351f071a3ea6b5f92a2dd122a5613a18e4dd340153d4a1c9ab92db7cd7462e", + "matched_terms": [ + "schur-intermediate-ranks", + "nonmaximal schur", + "n_min(rho)" + ], + "score": 5, + "excerpt": "# Nonmaximal Schur-commutator ranks for prescribed pivots\n\n**Scoped all-field proof plus an exact finite certificate. No new kappa.**\nProduced by Nick Petalas. Apache-2.0.\n\nKrzysztof Wojt's [PR #5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128)\n(`research/arbitrary-pivot-schur-minimum`) finds the least dimension n at which\ncommuting idempotents P,Q with prescribed invertible pivots `P11=A`, `Q11=B`\nand product block `(PQ)11=H` reach Schur-commutator rank 2d. Its Open next\nquestion" + }, + { + "kind": "local-task", + "title": "research/schur-intermediate-ranks/TASK.json", + "path": "research/schur-intermediate-ranks/TASK.json", + "sha256": "27abe9dc1e3485f83d59b5ffb307d1ee55e19014d76b6908fe62843f7eb4e348", + "matched_terms": [ + "schur-intermediate-ranks", + "n_min(rho)", + "rank/dimension trade" + ], + "score": 5, + "excerpt": "coder request. It does not price a decoder.\",\n \"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.\",\n \"budget_minutes\": 60,\n \"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.\",\n \"outcome\": \"partial\",\n \"evidence\": \"PROOF.md proves, over" + }, + { + "kind": "pr", + "number": 6031, + "title": "Prove nonmaximal Schur-commutator ranks form an interval with a sharp binary dimension law (no new κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6031", + "head": "acc000f4edfa0b0c4a90b505c6e02a4c3572f74c", + "base": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "updated_at": "2026-10-28T00:39:50Z", + "draft": false, + "state": "closed", + "matched_terms": [ + "schur-intermediate-ranks", + "nonmaximal schur", + "n_min(rho)" + ], + "score": 5, + "excerpt": "forced to rho0 at n0. For n >= n0 the feasible ranks form the interval `[rho0, rhomax(n)]`, and\n `n_min(rho) >= max(n0 + rho - rho0, nmax - 2(2d - rho))`.\n The second term uses a new deficiency identity: `rank R = 2d - a` and `rank L = 2d - b`, where a and b are the sector-image and sector-kernel deficiencies.\n2. For d=2 over F2, equality holds for all 576 triples (288 with AB != BA). rho0 is 0, 2 or 4 for 408, 144 and 24 triples, with 16 profiles. Rank two is feasible at n exactly when rho0" + }, + { + "number": 1166, + "title": "Handoffs and requests for independent checks", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19230733", + "updated_at": "2026-10-28T00:39:51Z", + "matched_terms": [ + "schur-intermediate-ranks", + "n_min(rho)" + ], + "score": 2, + "excerpt": "scussions/1166#discussioncomment-19230456). Both hosted checks passed, `plan` and `replay (research/schur-intermediate-ranks)`, in [run 40607943406](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40607943406).\n\nResult: for prescribed invertible pivots A,B and product block H (Open next question 1 of #5128), over every field the feasible Schur-commutator ranks at each n >= n0 form an interval [rho0, rhomax(n)], and n_min(rho) >= max(n0+rho-rho0, nmax-2(2d-rho)). The second term come" + }, + { + "number": 5121, + "title": "DONE: exact Schur minima for arbitrary invertible pivots (#5128)", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5121", + "updated_at": "2026-10-23T10:23:40Z", + "matched_terms": [ + "nonmaximal schur" + ], + "score": 1, + "excerpt": "mission or new kappa. The selected frontier is unchanged.\n\nThe next useful mathematical question is nonmaximal Schur ranks at fixed A,B,H; a bounded d=2 binary rank-two classification is an initial test, not another replay of the maximal-rank theorem. Physical realization of the ternary witness requires an actual caller and a complete resource bill. Neither follow-up is claimed.\n\nNick Petalas #4774/#4785 supplies the open questions; #4771/#4746 the scalar/identity predecessors; #4597/#4278 the o" + }, + { + "number": 1166, + "title": "Handoffs and requests for independent checks", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19230456", + "updated_at": "2026-10-28T00:14:51Z", + "matched_terms": [ + "nonmaximal schur" + ], + "score": 1, + "excerpt": "CLAIM / complex-rank-shape-decoder, changed scope: nonmaximal Schur-commutator ranks for prescribed arbitrary pivots\n\nQuestion: Krzysztof Wojt's merged [PR #5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128) (research/arbitrary-pivot-schur-minimum) gives the least dimension for commutator rank 2d with prescribed invertible A,B and product block H. Its Open next question 1 asks which smaller Schur-commutator ranks are feasible at each ambient dimension, starting with d=2 over F2. Th" + }, + { + "kind": "local-task", + "title": "research/arbitrary-pivot-schur-minimum/TASK.json", + "path": "research/arbitrary-pivot-schur-minimum/TASK.json", + "sha256": "d18615b9ee1af54cc3e107c779edf9441572efa0a32432aad4ef19bdd4055413", + "matched_terms": [ + "nonmaximal schur" + ], + "score": 1, + "excerpt": " \"open_questions\": [\n {\n \"question\": \"For prescribed invertible A,B and arbitrary H, which nonmaximal Schur-commutator ranks are feasible at each ambient dimension?\",\n \"why_it_matters\": \"The six-map equivalence determines the maximal-rank boundary only; smaller ranks could have different dimension obstructions.\",\n \"first_step\": \"Classify rank-two residual commutators for d=2 over F_2 at fixed noncommuting A,B,H, with explicit finite scope before seeking a general theorem.\",\n " + }, + { + "kind": "pr", + "number": 5128, + "title": "Prove exact Schur minima for arbitrary invertible block pivots (no new κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5128", + "head": "2839d35e58b3285a1992a3ecbae2809ebef7661b", + "base": "20a1e31bc6009b9b3f4d084bbaadc6350e34fcba", + "updated_at": "2026-10-23T10:40:45Z", + "draft": false, + "state": "closed", + "matched_terms": [ + "nonmaximal schur" + ], + "score": 1, + "excerpt": "a3ecbae2809ebef7661b/research/arbitrary-pivot-schur-minimum/README.md#open-next-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.\n" + } + ] + }, + "interpretation": "Initial remote snapshots were fetched live this session, then searched offline without a second download. The offline warnings describe cache use. The 8 hits are predecessor notes, PR6031 and its handoffs, plus PR5128/5121 lineage; no matching successor was identified. This is a bounded overlap search, not a novelty certificate.", + "selected_handoff": { + "pr": 6031, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6031", + "head": "acc000f4edfa0b0c4a90b505c6e02a4c3572f74c", + "question": "Open next question 1: is the dimension lower bound attained for all fields and all d?", + "done_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19230733" + }, + "credit": [ + "Nick Petalas: PR6031 sector reduction, deficiency lifts and lower bounds.", + "Krzysztof Wojt: PR5128 ordered factorization and full-rank endpoint." + ], + "limitations": "PR titles/bodies and Discussion records, plus tracked README/TASK notes; not arbitrary source diffs, unpublished work or an atomic snapshot. A final live recheck is recorded separately in VALIDATION.json.", + "final_live_snapshot": { + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-28T03:41:37.743722+00:00", + "terms": [ + "schur-intermediate-ranks", + "Schur rank", + "nonmaximal Schur", + "intermediate Schur", + "rank attainment", + "defect pairing", + "coordinate-minor" + ], + "coverage": { + "local": { + "head": "721c03822c421b7f7fcbb2598993b947c4d88419", + "records": 8350, + "head_records": 8348, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-28T03:36:27.854921+00:00", + "complete_pagination": true, + "records": 326 + }, + "discussions": { + "fetched_at": "2026-10-28T03:40:15.455619+00:00", + "complete_pagination": true, + "records": 5709 + }, + "closed_prs": { + "fetched_at": "2026-10-28T03:41:36.142891+00:00", + "complete_pagination": true, + "records": 5222 + } + }, + "local_records": 8350, + "warnings": [], + "reference_terms": [], + "limits": "Remote PR scope includes open and closed/merged titles and bodies, with separate coverage and timestamps. State changes are deduplicated by latest PR update; snapshots are not atomic. Local coverage compares searched working-tree notes with regular note paths at coverage.local.head; it does not certify HEAD contents or historical coverage. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 31, + "matches": [ + { + "kind": "local-readme", + "title": "research/schur-intermediate-ranks/README.md", + "path": "research/schur-intermediate-ranks/README.md", + "sha256": "6c351f071a3ea6b5f92a2dd122a5613a18e4dd340153d4a1c9ab92db7cd7462e", + "matched_terms": [ + "schur-intermediate-ranks", + "nonmaximal schur" + ], + "score": 4, + "excerpt": "# Nonmaximal Schur-commutator ranks for prescribed pivots\n\n**Scoped all-field proof plus an exact finite certificate. No new kappa.**\nProduced by Nick Petalas. Apache-2.0.\n\nKrzysztof Wojt's [PR #5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128)\n(`research/arbitrary-pivot-schur-minimum`) finds the least dimension n at which\ncommuting idempotents P,Q with prescribed invertible pivots `P11=A`, `Q11=B`\nand product block `(PQ)11=H` reach Schur-commutator rank 2d. Its Open next\nquestion" + }, + { + "kind": "local-readme", + "title": "research/schur-rank-attainment/README.md", + "path": "research/schur-rank-attainment/README.md", + "sha256": "1d3a7cfe74a9f2f32b5b399637e522f96b9eb74a82b136baea93ba1483f574e0", + "matched_terms": [ + "schur rank", + "intermediate schur", + "defect pairing", + "coordinate-minor" + ], + "score": 4, + "excerpt": "# Every intermediate Schur rank attains the dimension lower bound\n\n**Scoped all-field proof with exact reproducible corroboration. No new kappa.**\nPrepared for SHIN09-git with substantial OpenAI Codex assistance. Apache-2.0.\n\nThis follows [Nick Petalas's PR6031](https://github.com/CrocSwap/integer-mult-bounds/pull/6031),\nOpen next question 1, and [Krzysztof Wojt's PR5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128).\nTheir sector reduction, ordered maps, deficiency lifts and lower " + }, + { + "kind": "pr", + "number": 6031, + "title": "Prove nonmaximal Schur-commutator ranks form an interval with a sharp binary dimension law (no new κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6031", + "head": "acc000f4edfa0b0c4a90b505c6e02a4c3572f74c", + "base": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "updated_at": "2026-10-28T00:39:50Z", + "draft": false, + "state": "closed", + "matched_terms": [ + "schur-intermediate-ranks", + "nonmaximal schur" + ], + "score": 4, + "excerpt": "nk two is feasible at n exactly when rho0 <= 2 and `n >= max(n0+2-rho0, nmax-4)`.\n\nProof: `research/schur-intermediate-ranks/PROOF.md`.\n\n## Evidence and reproduction\n\n`verify.py` uses only the standard library. For every triple it enumerates every admissible block-subspace pair and computes the exact least dimension for each rank. On every pair it checks the rank R/L identities and the sandwich bound, and it checks the closed law. It then builds 2,496 literal commuting idempotent pairs, one for " + }, + { + "number": 2372, + "title": "CLAIM: P112 arbitrary cross forms, Schur rank tradeoff and a formal COPY-floor interface (PR2294 open question 1)", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2372", + "updated_at": "2026-10-23T10:04:11Z", + "matched_terms": [ + "schur rank" + ], + "score": 3, + "excerpt": "CLAIM: PR2294's open two-call P112 arbitrary-cross-form problem: a Schur rank tradeoff and kernel-checked arithmetic interface for the 128 COPY floor\n\n**Status / UTC update / priority revision:** DONE / 2026-10-15 07:24 UTC / revision 4. Details in the comment below.\n**Concrete question and changed premise:** PR #2294's open question: for arbitrary cross forms, does a Schur rank tradeoff strengthen the two-call 128 COPY floor, with a kernel-checked count interface?\n**Established result and evide" + }, + { + "number": 2372, + "title": "CLAIM: P112 arbitrary cross forms, Schur rank tradeoff and a formal COPY-floor interface (PR2294 open question 1)", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2372#discussioncomment-18943441", + "updated_at": "2026-10-15T07:24:54Z", + "matched_terms": [ + "schur rank" + ], + "score": 3, + "excerpt": "DONE: [PR #2395](https://github.com/CrocSwap/integer-mult-bounds/pull/2395), head `361de309e5fc05f83862f0b6c611210eda9837a1` on base `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`.\n\n**Result:** a stronger answer to PR #2294's open arbitrary-cross-form question. If the two cross forms have global binary ranks r01, r10 and minimum allowed support ranks c01, c10, then `c01 + c10 ≥ min(8, r01, r10)` implies the exact minimum COPY cost **128** for every two-call root-code factorization. The new Schur-com" + }, + { + "number": 2372, + "title": "CLAIM: P112 arbitrary cross forms, Schur rank tradeoff and a formal COPY-floor interface (PR2294 open question 1)", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2372#discussioncomment-19143434", + "updated_at": "2026-10-23T10:50:08Z", + "matched_terms": [ + "schur rank" + ], + "score": 3, + "excerpt": "DONE / FINDING — [PR #5141](https://github.com/CrocSwap/integer-mult-bounds/pull/5141), exact published head `b75399c455aa24f21ec9c78c337c3c277efd177d`. 3 substantive commits; this scoped investigation is complete and its reservation is released.\n\nSharp COPY floor128 for every directed binary rank-(1,1) P112 cross-form pair, including both zero support minima, by a written equality-case proof and actual source rigidity. Source census, normal/optimized checks, official export and Git-free cold co" + }, + { + "kind": "local-task", + "title": "research/schur-intermediate-ranks/TASK.json", + "path": "research/schur-intermediate-ranks/TASK.json", + "sha256": "27abe9dc1e3485f83d59b5ffb307d1ee55e19014d76b6908fe62843f7eb4e348", + "matched_terms": [ + "schur-intermediate-ranks" + ], + "score": 3, + "excerpt": "{\n \"schema_version\": 1,\n \"task_id\": \"complex-rank-shape-decoder\",\n \"priority_revision\": 8,\n \"base_commit\": \"19fdb086ea96af9a9f87936a2b888e10af4ed810\",\n \"original_card\": {\n \"id\": \"complex-rank-shape-decoder\",\n \"question\": \"Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?\",\n \"starting_points\": [\n \"docs/research/current-priorities.md\",\n \"docs/research/research-family-status.md\",\n \"certificates/selected-result.json\"," + }, + { + "kind": "pr", + "number": 6053, + "title": "Prove the exact Schur rank–dimension law over every field (no new κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6053", + "head": "12385ca23315181e3d15eb23a2d9ffec65d9a909", + "base": "721c03822c421b7f7fcbb2598993b947c4d88419", + "updated_at": "2026-10-28T03:27:51Z", + "draft": false, + "state": "open", + "matched_terms": [ + "schur rank" + ], + "score": 3, + "excerpt": "with the formula checker. Literal witnesses recheck idempotence, commutation, prescribed blocks and Schur rank. Eight controls reject omitted/equated cross blocks, forced evenness, a wrong minimum, corrupted witness, wrong product block, slope-one-only law and reordered products. Coverage inventories and expected result digest are checked:\n\n`c38f9ced06db3ecf1bc4c7f8802df7f1b3228f3435946700e7340b115d3156db`\n\n**Known base CI issue:** the unchanged base fails two of six `test_research_current_statu" + }, + { + "number": 5121, + "title": "DONE: exact Schur minima for arbitrary invertible pivots (#5128)", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5121", + "updated_at": "2026-10-23T10:23:40Z", + "matched_terms": [ + "schur rank", + "nonmaximal schur" + ], + "score": 2, + "excerpt": "mission or new kappa. The selected frontier is unchanged.\n\nThe next useful mathematical question is nonmaximal Schur ranks at fixed A,B,H; a bounded d=2 binary rank-two classification is an initial test, not another replay of the maximal-rank theorem. Physical realization of the ternary witness requires an actual caller and a complete resource bill. Neither follow-up is claimed.\n\nNick Petalas #4774/#4785 supplies the open questions; #4771/#4746 the scalar/identity predecessors; #4597/#4278 the o" + }, + { + "kind": "pr", + "number": 5128, + "title": "Prove exact Schur minima for arbitrary invertible block pivots (no new κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5128", + "head": "2839d35e58b3285a1992a3ecbae2809ebef7661b", + "base": "20a1e31bc6009b9b3f4d084bbaadc6350e34fcba", + "updated_at": "2026-10-23T10:40:45Z", + "draft": false, + "state": "closed", + "matched_terms": [ + "schur rank", + "nonmaximal schur" + ], + "score": 2, + "excerpt": "a3ecbae2809ebef7661b/research/arbitrary-pivot-schur-minimum/README.md#open-next-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.\n" + }, + { + "number": 4653, + "title": "DONE: nilpotent Schur residual extension and weights", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4653#discussioncomment-19151335", + "updated_at": "2026-10-23T18:28:20Z", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "nd six controls. The checks construct full original projectors and headers, verify the actual sharp Schur rank, and compare every explicit basis with independent residual kernels and complete central invariants. Four actual code mutations fail in both modes. Committed bytes, all source-pin direct ancestry checks, official export integrity, both read-only Git-free replays and publication body/rendered HTML pass. All 18 exported files remain unchanged. Hosted [run 39999280092](https://github.com/C" + }, + { + "number": 1166, + "title": "Handoffs and requests for independent checks", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19230456", + "updated_at": "2026-10-28T00:14:51Z", + "matched_terms": [ + "nonmaximal schur" + ], + "score": 1, + "excerpt": "CLAIM / complex-rank-shape-decoder, changed scope: nonmaximal Schur-commutator ranks for prescribed arbitrary pivots\n\nQuestion: Krzysztof Wojt's merged [PR #5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128) (research/arbitrary-pivot-schur-minimum) gives the least dimension for commutator rank 2d with prescribed invertible A,B and product block H. Its Open next question 1 asks which smaller Schur-commutator ranks are feasible at each ambient dimension, starting with d=2 over F2. Th" + }, + { + "number": 1166, + "title": "Handoffs and requests for independent checks", + "kind": "discussion-comment", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19230733", + "updated_at": "2026-10-28T00:39:51Z", + "matched_terms": [ + "schur-intermediate-ranks" + ], + "score": 1, + "excerpt": "scussions/1166#discussioncomment-19230456). Both hosted checks passed, `plan` and `replay (research/schur-intermediate-ranks)`, in [run 40607943406](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40607943406).\n\nResult: for prescribed invertible pivots A,B and product block H (Open next question 1 of #5128), over every field the feasible Schur-commutator ranks at each n >= n0 form an interval [rho0, rhomax(n)], and n_min(rho) >= max(n0+rho-rho0, nmax-2(2d-rho)). The second term come" + }, + { + "number": 1267, + "title": "DONE: nine-root obstruction for a fixed P112 co-star decoder", + "kind": "discussion-reply", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1267#discussioncomment-18932969", + "updated_at": "2026-10-14T19:47:27Z", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "very block 4-clique and every frame meets enough groups. Closing these needs value-level algebra (a Schur rank-1 identity: M − ¼M[:,Q]M[Q,:] has rank ≤ 1 for a frame Q).\n- **Numerics (suggestive only).** Least-squares fits on the propagated supports of every survivor tried stall at a residual of 848–976, meaning at least 53 diagonal entries are unmet. The same solver reaches about 0 once the capacity is raised to 27. Nothing points to a cost-≤63 decoder.\n\nCertificates replay with the same indepe" + }, + { + "kind": "local-readme", + "title": "research/cex19-exact-pairing/README.md", + "path": "research/cex19-exact-pairing/README.md", + "sha256": "04bcde608f1510a6565a5766952bf70b4586e5eeafa82c32c2a5a64bf81d6d44", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "nd and a standalone relocation without Git;\n- the witness's ranks by separate column elimination;\n- Schur rank identities on 64 admissible pairings;\n- a complete satisfying assignment at cost 21 when the budget is raised;\n- rejection of the lower refutation when the essential budget clauses are removed;\n- all gate truth tables and propagation comparisons on 960 small cases;\n- the **entire 1,301-step proof again**, using an independent bit-mask,\n repeated-whole-clause-scan propagation implementa" + }, + { + "kind": "local-readme", + "title": "research/five-cube-three-totals/README.md", + "path": "research/five-cube-three-totals/README.md", + "sha256": "d1ed740cb7ffa96f776a5723438fb21f4e45ed638a15c208982ba1214b121b81", + "matched_terms": [ + "rank attainment" + ], + "score": 1, + "excerpt": "ges and different\ncopy/stage accounting remain outside scope. Neither mask construction nor\npairing-rank attainment proves an actual gather/COPY implementation.\nAll-size/compiler, common-label/mutable-source, whole-call hosting,\nprecision/tape, bit H1-H5 and analytic obligations remain inherited.\nThis is a written finite proof with executable evidence, not a formal\nmultiplication theorem or independent human review.\n\nExact base: `c0e3631dc24e3c24a861f7d3d79e0608481cccec`. Assignment seed 46,\nstr" + }, + { + "kind": "local-readme", + "title": "research/idempotent-factor-invariant/README.md", + "path": "research/idempotent-factor-invariant/README.md", + "sha256": "fae88ccbea3a16d041666f5956d0416b6a21ef57a21f1a0996c7c3a74f7fa3d1", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "ivot dimension theorem to arbitrary\nfields. It studies a prescribed product compression and maximal Schur rank;\nthis note classifies arbitrary ordered, possibly noncommuting residual pairs.\nNo dimension-minimum or header-count number from that proposal is claimed here.\n\n## Open next questions\n\n1. Can this complete descriptor yield a useful higher-rank transition table\n for one actual residual ensemble? The invariant controls state identity,\n which is needed to avoid merging states with diffe" + }, + { + "kind": "local-readme", + "title": "research/identity-pivot-sector-bound/README.md", + "path": "research/identity-pivot-sector-bound/README.md", + "sha256": "c997446a1fc4683694987feea5f2a8423b57d48d5513a27e178f84ecf56ffc12", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": " decomposition and enumerate complete invertible headers,\nchecking the six-map count against direct Schur ranks. Any density claim must\nspecify its ensemble and preserve dependencies among the six events; a product\nof marginal counts is not justified. No claim is held on that follow-up, and no\nphysical implementation should be inferred from such a count alone.\n" + }, + { + "kind": "local-readme", + "title": "research/p104-defect-output-channels/README.md", + "path": "research/p104-defect-output-channels/README.md", + "sha256": "65cd0ed43ce612475b0b034ceec1ea4891b8cee23fef614c07e39d5c113a355e", + "matched_terms": [ + "rank attainment" + ], + "score": 1, + "excerpt": "ions, not optimal widths or total live storage. No rank-seven\ndefect-image census is performed; all-rank attainment beyond rank 7 is unproved.\n\nThe source-authenticated primary checker uses prime 65537 and one source\nschedule. The separate internal checker imports no primary or predecessor\nexecutable, uses prime 65521 and a different source schedule, and independently\nchecks all seven dimensions and bounds. Nonzero modular minors give exact\ninteger/real independence. The universal upper proof pl" + }, + { + "kind": "local-readme", + "title": "research/p112-cross-form-rank-tradeoff/README.md", + "path": "research/p112-cross-form-rank-tradeoff/README.md", + "sha256": "3661d9edddb7abc82940ed053c85f3bd885e6af03461f1cebfdd66fa1b2b7e14", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "# P112 cross forms: a Schur rank tradeoff and formal COPY-floor interface\n\nTwo independent P112 root-code decoders still require **COPY cost 128**\nunder a broader class of arbitrary cross-call binary forms. If their global\nranks are r01,r10 and their minimum support-restricted ranks are c01,c10,\nthe sufficient condition is\n\n c01 + c10 >= min(8, r01, r10).\n\nThis follows by charging a term touching both calls at least\n`16-min(8,r01,r10)`, then using the exact coefficient identity to count\nterms" + }, + { + "kind": "local-readme", + "title": "research/p112-diagonal-rank-boundary/README.md", + "path": "research/p112-diagonal-rank-boundary/README.md", + "sha256": "77f3c0cbf3587c8ade05581d54cbba46330c1f0278ff2f73f1b815ff6805cf9b", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "l Pulikkan #620, icekylinx and the retained E8/Hamming lineage for their\npredecessor contributions. Schur rank inequalities and the difference-of-\nprojections identity are classical. The new application gives the sharp\ndiagonal-completion threshold. Predecessor files and credit are unchanged.\n\nIndependent human and formal proof-kernel review are unclaimed. The proof\nretains the cited geometric premises. No copied-information optimum,\narbitrary off-diagonal mask, rounded identity, physical source" + }, + { + "kind": "local-readme", + "title": "research/schur-header-count/README.md", + "path": "research/schur-header-count/README.md", + "sha256": "472295f32ebf3fcdc8daa4137af63db70d9943de7cbb97e47ed272823b2a227e", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "s, **all 496 scalar split pairs** are checked\n by constructing a header and directly computing the Schur rank for each\n identity-pivot pair. No six-map test is used to select the positive pairs.\n- All G4 completions of the resulting 3 and 9 positive split pairs are\n explicitly formed, inverted and checked by literal conjugation and Schur\n multiplication: **241,920 positive complete-header cases**, distinct for each fixed pair. This is\n not a raw enumeration of every GL5 header; completeness" + }, + { + "kind": "local-readme", + "title": "research/schur-nilpotent-extension/README.md", + "path": "research/schur-nilpotent-extension/README.md", + "sha256": "7e5e74f4e5ddc1793ac6e427a80492d8d978aa78f01f189e33d2831147c9639a", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "omplete headers.\nThe complete split inventory contains 19,602 splits; the verifier computes\nliteral Schur ranks on every identity-pivot H=0 candidate and constructs an\nactual ordered-pair intertwiner for every sharp one. Over F2 the count is\n3 splits / 60,480 headers, recovering the earlier ssafwann\n[PR4678](https://github.com/CrocSwap/integer-mult-bounds/pull/4678) fixture,\nnot claiming it as new. Binary padding in sectors 00,10,11 gives respectively\n18,18,21 splits; padding 11 to dimension 3 c" + }, + { + "kind": "local-task", + "title": "research/arbitrary-pivot-schur-minimum/TASK.json", + "path": "research/arbitrary-pivot-schur-minimum/TASK.json", + "sha256": "d18615b9ee1af54cc3e107c779edf9441572efa0a32432aad4ef19bdd4055413", + "matched_terms": [ + "nonmaximal schur" + ], + "score": 1, + "excerpt": " \"open_questions\": [\n {\n \"question\": \"For prescribed invertible A,B and arbitrary H, which nonmaximal Schur-commutator ranks are feasible at each ambient dimension?\",\n \"why_it_matters\": \"The six-map equivalence determines the maximal-rank boundary only; smaller ranks could have different dimension obstructions.\",\n \"first_step\": \"Classify rank-two residual commutators for d=2 over F_2 at fixed noncommuting A,B,H, with explicit finite scope before seeking a general theorem.\",\n " + }, + { + "kind": "local-task", + "title": "research/binary-schur-minimal-dimension/TASK.json", + "path": "research/binary-schur-minimal-dimension/TASK.json", + "sha256": "17d40d59f49eb45be0e9f085a051b1caf7b158c80dc2626cbc2a03811fb6e3f0", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "597,\n \"head\": \"dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb\",\n \"credit\": \"Nick Petalas: block-Schur rank bound and predecessor PR4278.\"\n },\n {\n \"pr\": 4609,\n \"head\": \"eb5ccf9288808d973551e6264300d30d2f6e48a0\",\n \"credit\": \"Ryanson Jonathan: binary witnesses and small minimal-dimension classification.\"\n },\n {\n \"pr\": 4617,\n \"head\": \"96c01a2124e234d798e9e97643c20fb5b430840d\",\n \"credit\": \"Ryanson Jonathan: uniform binary n=5d construction and minimal-dim" + }, + { + "kind": "local-task", + "title": "research/p112-cross-form-rank-tradeoff/TASK.json", + "path": "research/p112-cross-form-rank-tradeoff/TASK.json", + "sha256": "3a042ab09a0315efbb77d0ea5c0977f39e44f5debfadf400eabc84b55ab307a7", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "scope_status\": \"refined\",\n \"actual_scope\": \"PR2294 arbitrary two-call P112 cross forms: a stronger Schur rank price, the exact conditional COPY128 count interface in Lean, and its finite source binding.\",\n \"scope_change_reason\": \"Take the named open cross-form interface in PR2294 rather than repeat a selected-supplier arithmetic proof. The formalization covers the natural-number implication only; matrix premises remain explicit.\",\n \"bottleneck_link\": \"Eliminates additional two-call cross-form" + }, + { + "kind": "local-task", + "title": "research/schur-rank-attainment/TASK.json", + "path": "research/schur-rank-attainment/TASK.json", + "sha256": "47dfc3c95ec582cc879849a85071852229f53286202d3e1c3c6b7ccaae7dda83", + "matched_terms": [ + "defect pairing" + ], + "score": 1, + "excerpt": "d_at\": \"2026-10-28T03:02:42Z\",\n \"initial_hypothesis\": \"A maximal nonsingular minor of the baseline defect pairing gives efficient single deletions, followed by nested nonsingular minor deletions. Because these delete basis vectors within original sector blocks, the block constraints do not obstruct attainment.\",\n \"publication_status\": \"local-only; this new research is not part of PR6046\",\n \"predecessors\": [\n {\n \"pr\": 6031,\n \"author\": \"Nick Petalas\",\n \"head\": \"acc000f4edfa0b0" + }, + { + "kind": "pr", + "number": 5267, + "title": "Prove nilpotent Schur residual normal form and fixed-H weights (no κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5267", + "head": "8ab280c8a3ef0544f13ff23a1c69df4757cd4900", + "base": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "updated_at": "2026-10-23T18:37:53Z", + "draft": false, + "state": "closed", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "nt Jordan blocks.\n- **Five exhaustive split inventories** test the sector criterion against literal Schur ranks and transport every one of the **188 sharp outcomes** to its canonical ordered pair. The ternary scalar case has 128 passing splits and 3,105,423,360 complete headers.\n- **Six independent sector-factor censuses** check the stabilizer denominator; **nine rejection controls** cover the characteristic-two overclaim, omitted extended chain/exponents, nonsquare/nonnilpotent H, negative padd" + }, + { + "kind": "pr", + "number": 4634, + "title": "Prove optimal binary Schur sharpness dimension n = 3d for d >= 2", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4634", + "head": "9f053f7051e5fc3327d4337bb4bd8ac52cf5fcd0", + "base": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "updated_at": "2026-10-22T19:28:28Z", + "draft": false, + "state": "closed", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "ple in #4609; the new formula also realizes them. Nick Petalas's #4597 supplies the preceding block-Schur rank bound and #4278 the precursor setting; Ryanson's #4617 supplies the uniform n=5d construction and open question. Exact inspected heads are recorded in the README and TASK.json. The new theorem requires invertible pivots, not identity pivots; its equal pivots are generally nonidentity. The d=1 classification is credited to #4609 rather than re-proved here.\n\nOnly the five-file package [re" + }, + { + "kind": "pr", + "number": 4746, + "title": "Prove the exact identity-pivot Schur minimum over every field (no κ)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4746", + "head": "5f014560d6225cae17598ac479fb29d2947d8e6b", + "base": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "updated_at": "2026-10-22T19:31:50Z", + "draft": false, + "state": "closed", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": " over F2,F3,F4,F5: **18+84+260+630 = 992 cases**. Direct idempotence, commutation, pivots, product, Schur ranks, sector minima and ordered factors pass. It also checks 18 deficient-map controls, 12 nonbinary 4d witnesses, 12 nondiagonal size-three blocks, three invalid-input rejections and two unsigned-sector rejections.\n\nBoth registered commands passed locally in **0.67 s / 0.70 s**, including optimized Python with explicit checks. CPython 3.12.15, macOS arm64. Committed package replay, exact c" + }, + { + "kind": "pr", + "number": 4278, + "title": "Prove the exact one-step Schur commutator criterion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4278", + "head": "e38f8e9477a49689122ed11a83d163595b366460", + "base": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "updated_at": "2026-10-21T19:24:12Z", + "draft": false, + "state": "closed", + "matched_terms": [ + "schur rank" + ], + "score": 1, + "excerpt": "sting single-request Schur/rank framework and densities. The sharp F5 example has input ranks 2 and Schur ranks 1, agreeing numerically with its rank-drop lemma. No marginal density is computed here.\n- #4240, head `9f9c89ed75e9fdae6b6762925b080fb308824858`: classifies nonorthogonal rank-one header counts. This treats the Schur commutator of a previously commuting pair, without a shared count to compare.\n- #4246 / #4239: orthogonal full-chain and rank-one laws. Those preserved subclasses are cont" + } + ] + }, + "final_interpretation": "A direct same-theorem successor, PR6053, appeared during the session. No novelty claim is retained. Final scope is an independent audit at its exact head, using the coordinate-minor derivation and complete ternary d=2 coverage; this is additional corroboration, not a competing theorem submission." +} diff --git a/research/schur-rank-attainment/PROOF.md b/research/schur-rank-attainment/PROOF.md new file mode 100644 index 0000000000..7b233a1974 --- /dev/null +++ b/research/schur-rank-attainment/PROOF.md @@ -0,0 +1,203 @@ +# Every intermediate Schur rank attains the dimension lower bound + +Prepared for SHIN09-git with substantial OpenAI Codex assistance. +Apache-2.0. This is a scoped algebraic proof, not a physical supplier theorem. + +Final overlap refresh found apoursh's concurrent PR6053, opened during this +session, proving the same dimension law and a closed minimum-rank formula. +This coordinate-minor derivation is retained as a separate argument for the +source-bound audit in AUDIT.md. No novel-theorem or priority claim is retained. +The exact reviewed PR6053 proof is included as reference6053.md. + +## Statement and exact dependence + +Let K be any field, d >= 1, A,B invertible d by d matrices, and H arbitrary. +We seek commuting idempotents P,Q of dimension n, with leading blocks +P11=A, Q11=B, (PQ)11=H. Let S,Z be their Schur complements at those +invertible leading blocks, and let rho=rank(SZ-ZS). + +Put T00=I-A-B+H, T10=A-H, T01=B-H, T11=H and +nu=sum nullity(Tj), with j=10,01,11. Define + + n0 = rank(T00) + 3d - nu, + nmax = rank(T00) + 3d + nu. + +Let G,G' be the ordered maps below and T=diag(T10,T01,T11). +Put rho0=rank(T G G' T). Then for every integer rho in [rho0,2d], + + n_min(rho) = max(n0 + rho - rho0, nmax - 2(2d-rho)). (1) + +No smaller rank is feasible. At any fixed n >= n0 the feasible ranks are +exactly the integers from rho0 to + + min(2d, rho0+n-n0, floor((n-nmax+4d)/2)). (2) + +There is no pair at n K^d, +Yj:K^d -> Vj with Xj Yj=Tj. Concatenating the X maps as pi and the Y +maps as i gives pi i=I. The diagonal sector projections P0,Q0 commute +and are idempotent. In a basis [i,ker pi], their conjugates have the +prescribed leading blocks. Conversely the joint eigenspaces of any +commuting idempotents give exactly these factorizations; characteristic +two causes no difficulty since 0 and 1 remain distinct. + +In the three active sectors set Ij=im Xj and Nj=ker Yj. +They satisfy im Tj subset Ij and Nj subset ker Tj. For these subspaces, + + min dim Vj = dim Ij + d - dim Nj - rank Tj. (3) + +The rank inequality gives the lower bound. For attainment choose a +basis sigma of im Tj, write Tj=sigma phi, let psi read the coordinates +of a complement of Nj in ker Tj, and extend sigma to a basis of Ij +by tau. Then Xj=[sigma,0,tau], Yj=[phi;psi;0] give (3), the prescribed +image and kernel, and XjYj=Tj. The 00 sector is a rank factorization. + +Write a=sum codim Ij, b=sum dim Nj over active sectors. The exact +least total dimension for these choices is therefore + + n = nmax-a-b. (4) + +Padding only the 00 sector attains every larger n with the same rho. + +The ordered maps on U=K^d are + + G(x,y) = (A^-1 y, -B^-1(Hx+y), + (I-B^-1 H)x + (A^-1-B^-1)y), + G'(v10,v01,v11) = + (A^-1 v10 - B^-1 v01 + (A^-1-B^-1)v11, + H B^-1 v01 + (H B^-1-I)v11). + +With X=diag(X10,X01,X11), Y=diag(Y10,Y01,Y11), the +Schur-commutator rank equals rank(Y G G' X). These are the ordered +#5128/#6031 maps; H is not commuted with either inverse. + +## 2. Defect pairing + +For each active j fix a basis of the left kernel of Tj and a basis +of its right kernel. Lift a left-kernel row w to a covector on U^2 +and a right-kernel column z to a vector on U^2 as follows: + +| sector | left lift e(w) | right lift k(z) | +|---|---|---| +| 10 | (wA,w) | (-z,Az) | +| 01 | (0,w) | (-z,0) | +| 11 | (0,-w) | (z,0) | + +Direct multiplication gives e(w)G' equal to the pure j-sector +covector w, and Gk(z) equal to the pure j-sector vector z. +These identities use, respectively, wTj=0 and Tj z=0. +G is injective: G(x,y)=0 first forces y=0, then Hx=0, then x=0. +G' is onto: a row (u,v) annihilating it has u=0 from its first +component, then vHB^-1=0 and v(HB^-1-I)=0, hence v=0. +Thus all nu left lifts are independent, +as are all nu right lifts; in particular nu<=2d. + +Let E be the nu by 2d matrix of left lifts, K the 2d by nu matrix +of right lifts, and C=E K. Changing either within-sector basis +changes C by invertible block row/column factors, so its rank is +well defined. Let r=rank C. + +Choose any subset R of the original left basis indices and any subset +J of the original right basis indices. In each sector define Ij to be +the common annihilator of its retained left basis vectors, and Nj +to be the span of its retained right basis vectors. These choices +are admissible. No vector has been mixed across different sectors. + +For this choice a=|R| and b=|J|. The annihilator of im(G'X) is +exactly the span of the selected left lifts, and ker(YG) is exactly +the span of the selected right lifts. To see exactness, any row +annihilating G'X maps under the injective map e -> eG' into the +block annihilator of I; every such block covector already has its +unique listed lift. The analogous assertion uses the injectivity of +G and the pure-sector lifts of N. + +Consequently, using the restriction of E_R to span(K_J), + + rho = 2d-a-b+rank C[R,J]. (5) + +Indeed im(G'X)=ker E_R has dimension 2d-a and its intersection +with ker(YG)=im K_J has dimension b-rank C[R,J]. + +At R=J=all indices, the cost is n0 and the rank is forced to rho0, +so (5) also gives + + rho0 = 2d-2nu+r. (6) + +This agrees with rank(T G G' T): the latter uses the same images +im Tj and kernels ker Tj in the rank formula of #6031 Section 1. + +## 3. A coordinate-minor chain + +Every rank-r matrix C contains a nonsingular r by r coordinate +submatrix C[R*,J*]; the empty minor is used when r=0. +Begin with every row and column retained. + +First delete, one at a time, the nu-r rows outside R*, followed by +the nu-r columns outside J*. Each retained matrix contains the same +rank-r minor and is a submatrix of C, so its rank remains r. +After t deletions, 0<=t<=2(nu-r), equations (4)–(6) give + + rho=rho0+t, n=n0+t=n0+rho-rho0. + +At the end the retained matrix is a nonsingular r by r minor, +a=b=r and rho=2d-r. + +Now an invertible s by s matrix, s>=1, has a nonzero cofactor: +its adjugate is det(C) C^-1 and is nonzero. Delete the row and +column of one such cofactor. The retained (s-1) by (s-1) matrix is +nonsingular. Repeat until the empty minor. At retained size s, + + a=b=s, rho=2d-s, n=nmax-2s=nmax-2(2d-rho). + +Thus every integer rank from rho0 through 2d occurs. The construction +uses only deletion of original basis vectors. Even for a finite field, +it never asks for a generic vector, a nonempty Zariski-open set, or an +arbitrary transversal subject to a sector constraint. + +## 4. Match the lower bound + +The two branches of (1) are equal at rho=2d-r, by (6) and +nmax-n0=2nu. Below this crossover the slope-one branch is larger; +above it the slope-two branch is larger. Section 3 attains exactly +the larger branch in both phases. With #6031's lower bounds, (1) +follows. Padding the 00 sector and solving the two inequalities in +(1) for rho proves (2). + +The edge cases are included: r=0 has only the first phase; r=nu has +only the second phase; nu=0 gives the unique rank 2d already at n0. +The empty Schur complement at n=d has rank zero. + +## 5. What the evidence can and cannot establish + +For the complete d=2 ternary check, simultaneous conjugation by +W in GL_d(K) sends (A,B,H) to (WAW^-1,WBW^-1,WHW^-1). +Conjugate a witness P,Q by diag(W,I_(n-d)); this changes precisely +those leading blocks and leaves the two Schur complements unchanged. +The inverse transformation proves invariance of every feasible rank +and least dimension. The exact finite group partition therefore lets +8,136 representatives cover all 186,624 ternary input triples. +The action table, disjoint coverage and Burnside orbit count are +checked separately. Literal witnesses are built for representatives, +not separately for all 186,624 raw triples. + +The executable constructor uses exact prime-field arithmetic or rational +fractions. Independent finite subspace enumeration and literal full-matrix +checks corroborate the construction on declared finite domains. They do +not replace Sections 1–4, prove every field by testing, or certify a +physical header. The theorem inherits the common deletion, invertible +pivot and commuting-idempotent setting. Singular pivots, coefficient rings, +multiple deletions, native realization, ownership/restoration, precision, +stock and outer costs are outside its claim. No new kappa follows. + +Full independent human or formal-kernel review is not claimed. diff --git a/research/schur-rank-attainment/PUBLICATION.md b/research/schur-rank-attainment/PUBLICATION.md new file mode 100644 index 0000000000..831cf3af5a --- /dev/null +++ b/research/schur-rank-attainment/PUBLICATION.md @@ -0,0 +1,67 @@ +# Publication checkpoint: independent audit of PR6053 + +This note records the authorized publication of the completed research archive +at scientific commit **84b54b893ef0224aa5080abc1afd219222fa99a2**. +The bound README.md, TASK.json, AUDIT.md, VALIDATION.json and other research +files are retained byte-for-byte. Their local-only/publication fields describe +the completed research checkpoint; this note records its subsequent submission. + +## Exact target and overlap + +On 2026-10-28, canonical main was refreshed and still resolved to +721c03822c421b7f7fcbb2598993b947c4d88419. No entry-guidance or selected-result +change was present relative to the research base. PR6053 remained open at +12385ca23315181e3d15eb23a2d9ffec65d9a909, the exact source reviewed here. + +The full entry/end-of-session overlap snapshots are preserved in OVERLAP.json. +Publication-time all-state PR searches for 6053 and schur-rank-attainment +returned the target PR and no existing PR for this audit package. +Those targeted searches are not a novelty certificate. The contribution is an +independent audit with complete ternary d=2 coverage and an alternate +coordinate-minor construction, not a competing theorem claim. + +## Verification at the research checkpoint + +CPython 3.12.10 on Windows, standard library only: + +- Registered replay passed ordinary and optimized full checks, then all nine + actual source mutants. Ten malformed-fixture/false-formula controls passed. + This run completed at 2026-10-28T03:57:29Z in 346.585 seconds; the package + inventory and file hashes were unchanged by the run. +- The committed-byte check passed for all 22 original files. RESULT.json + line endings were normalized from CRLF to the committed LF bytes without + changing its parsed JSON value. +- Official export and declared-input coverage checks passed. +- An optimized full replay of the committed export passed with empty PATH, + no Git checkout, and read-only files. The exported file inventory and all + file hashes were unchanged. This completed at 2026-10-28T04:00:42Z; + scientific computation took 157.308 seconds. +- Original package ZIP bytes were compared against the committed export. + Container hashes identify that saved delivery, not a mathematical invariant. + +The scientific input hashes and result receipt remain unchanged by publication. +The publication adds only this note; no scientific code has changed since the +completed checks. The new publication commit receives a fresh committed-byte +and metadata/pin preflight before push. No selected supplier replay, original +PR6053 executable replay, full-history ancestry closure, formal proof-kernel +run or independent human review is claimed. + +## Shared CI status + +At this unchanged base, the shared onboarding job fails two navigation tests: +the current CI section still points to the earlier selected result, and the +current-status bold decimal does not match its existing test contract. +PR6050 separately repairs those references. Its current dependent historical +jobs also expose older source-pin drift. This archive changes no shared +documents, source pins of other packages or selected construction. + +These shared failures are distinct from the passing local research replays. +Hosted checks for this publication must be reported at their actual head. + +## Attribution and scope + +apoursh's PR6053 owns the concurrent all-field theorem and closed minimum-rank +formula reviewed here. Retain Nick Petalas #6031 and Krzysztof Wojt #5128 and +their credited lineage. Prepared for SHIN09-git with substantial OpenAI Codex +assistance. Separate verification algorithms were developed by the same +assistant. No new kappa, physical supplier or historical-priority claim. diff --git a/research/schur-rank-attainment/README.md b/research/schur-rank-attainment/README.md new file mode 100644 index 0000000000..1c333d45ed --- /dev/null +++ b/research/schur-rank-attainment/README.md @@ -0,0 +1,139 @@ +# Independent audit of the exact Schur rank/dimension law + +**Source-bound audit of PR6053 with a separate construction. No new kappa.** +Prepared for SHIN09-git with substantial OpenAI Codex assistance. Apache-2.0. + +This follows [Nick Petalas's PR6031](https://github.com/CrocSwap/integer-mult-bounds/pull/6031), +Open next question 1, and [Krzysztof Wojt's PR5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128). +Their sector reduction, ordered maps, deficiency lifts and lower bounds are +credited and retained unchanged. This package uses a coordinate-minor chain +that attains the bound while preserving the three sector constraints. +This package is a local research result, separate from publication PR6046. + +The final live overlap refresh found apoursh's [PR6053](https://github.com/CrocSwap/integer-mult-bounds/pull/6053), +opened at 03:27:51 UTC during this session. Its exact reviewed head is +12385ca23315181e3d15eb23a2d9ffec65d9a909. It proves the same dimension law +and an ordered closed formula for rho0. The final contribution is an +independent audit, including complete ternary d=2 corroboration and a +different attainment construction. It is not a competing new-theorem claim. +See AUDIT.md for the exact claim-to-evidence mapping and scope adjustment. + +## Result + +Let K be any field, d >= 1, A,B invertible d by d matrices, H arbitrary. +For commuting idempotents P,Q with leading blocks A,B and product leading +block H, let rho be the rank of the commutator of their Schur complements. +Use the quantities defined in PROOF.md: + + T00=I-A-B+H, T10=A-H, T01=B-H, T11=H, + nu=sum nullity(Tj) for j=10,01,11, + n0=rank(T00)+3d-nu, nmax=rank(T00)+3d+nu, + rho0=rank(T G G' T), T=diag(T10,T01,T11). + +For every integer rho from rho0 to 2d, the exact least ambient dimension is + + n_min(rho)=max(n0+rho-rho0, nmax-2(2d-rho)). + +No smaller rank occurs. At n >= n0 the feasible ranks are exactly + + rho0 ... min(2d, rho0+n-n0, floor((n-nmax+4d)/2)). + +The proof lifts sector kernels to a square defect pairing C. Retaining +coordinate rows R and columns J gives rank 2d-|R|-|J|+rank(C[R,J]). +First remove coordinates outside a maximal nonsingular minor. Then remove +row/column pairs at nonzero cofactors. These two phases meet the two lower +bounds exactly, without genericity assumptions over a finite field. + +## Declared computational coverage + +| Domain | Input cases actually constructed | Literal P,Q witnesses | Exhaustive admissible subspace pairs | +|---|---:|---:|---:| +| All A,B in GL2(F2), all H in M2(F2) | 576 | 2,496 | 21,690 | +| All GL2(F3) pairs and H, up to exact simultaneous conjugacy | 8,136 representatives | 26,148 | 113,768 | +| One fixed noncommuting d=3 binary pivot pair, all H | 512 | 2,546 | 35,801 | +| Structured inputs over Q,F2,F3,F5,F7,F11, d=1..4 | 165 | 861 | Not enumerated | +| Total | 9,389 labelled cases; **9,381 distinct triples** | **32,051** | **171,259** | + +The ternary representatives cover all **186,624** raw input triples. +The finite action table, orbit disjointness, complete coverage and Burnside +count are checked. Simultaneous conjugation preserves the prescribed-block +problem and literal Schur complements as proved in PROOF.md. Witnesses are +constructed for representatives, not separately for every raw triple. + +The d=3 binary pivots are A=((0,1,0),(0,0,1),(1,0,0)) and +B=((1,1,0),(0,1,1),(0,0,1)); this is not a census of all d=3 pivot pairs. +The structured rational/prime-field inputs are corroboration, not exhaustive +coverage of those fields or dimensions. + +The verifier also compares all 576 binary profiles to the unchanged PR6031 +program, checks every coordinate-subset pair for 609 small generic pairing +matrices (all 2x2 F2, 2x2 F3 and 3x3 F2 matrices), and rejects ten malformed +witness or false-formula controls. Nine actual source mutants test omitted +phases, principal-minor restriction, order/sign errors, sector mixing, a +wrong bound and a disabled independent rank check. +Two of these mutants additionally corrupt PR6053's ordered closed formula; +that formula is compared on all 9,389 labelled input cases. + +## Reproduce + +Python 3.12, standard library only. From this directory, including a Git-free +export: + + python -I -W error -B verify.py + python -I -O -W error -B verify.py + python -I -W error -B test_mutations.py + +From the repository: + + python -B scripts/research_package.py --package research/schur-rank-attainment + +A full replay takes about 2.5 minutes on the development machine; no timing +speedup is claimed. The registered commands allow 450 seconds per full replay +and 180 seconds for mutation checks. They read package-local files and create +no package output. The mutation harness uses temporary directories. + +RESULT.json binds the declared result and all mathematical/code/metadata +inputs by SHA-256. Ordinary replay recomputes and compares it; missing bound +files and changed frozen references fail explicitly, including under -O. +The authoring option --emit-receipt prints a candidate receipt and deliberately +does not compare RESULT.json. It is not the normal verification command. +The quick option is a smoke test and is not evidence for the complete domains. + +To inspect literal examples independently: + + python -I -B verify.py --emit-examples > examples.json + python -I -B check_witnesses.py < examples.json + +The second command imports no constructor code. This redirection syntax works +in a POSIX shell; on PowerShell pipe Get-Content -Raw examples.json to the +same checker. Fixture generation recomputes the full declared domains. + +## Files and boundaries + +- PROOF.md: field-independent argument and conjugacy coverage justification. +- AUDIT.md and reference6053.md: review map and exact concurrent-source proof. +- construct.py and linear.py: exact construction and arithmetic. +- oracle.py: separate finite subspace census, using explicit vector sets. +- check_witnesses.py: separate raw-matrix checker; no construction imports. +- ternary_orbits.py: complete finite group coverage. +- verify.py, test_mutations.py, RESULT.json: reproducible checks and fixed receipt. +- TASK.json, SOURCES.json, OVERLAP.json, VERIFY.json: scope, exact source pins, + overlap coverage and registered commands. +- reference6031.py, reference6031.md, reference5128.md: unchanged attributed + predecessor bytes. Source pins are checked before computation. +- VALIDATION.json: observed replay/export results; not a mathematical input. + +The all-field conclusion comes from PROOF.md, not from extrapolating the tests. +"Independent" checks here means separate algorithms/code paths, all developed +by the same assistant. No independent human or formal-kernel review is claimed. + +The hypotheses remain common deletion, invertible pivots, commuting idempotents +and coefficients in a field. No singular-pivot, coefficient-ring, physical +header, native delivery, restoration/ownership, precision, stock, outer-transfer +or selected-supplier claim is made. The selected frontier is unchanged. + +## Open next questions + +The next separate task would choose one concrete physical header and caller +contract, then translate and fully price a witness there. That contract is +not specified here; TASK.json records the blocker and first step. diff --git a/research/schur-rank-attainment/RESULT.json b/research/schur-rank-attainment/RESULT.json new file mode 100644 index 0000000000..e8485655d3 --- /dev/null +++ b/research/schur-rank-attainment/RESULT.json @@ -0,0 +1,122 @@ +{ + "PR6053_closed_formula_comparisons": 9389, + "binary_reference_comparisons": 576, + "complete_ternary_coverage": { + "burnside_orbit_count": 8136, + "coverage": "All A,B in GL_2(F3), all H in M_2(F3), by exact simultaneous conjugacy", + "distinct_actions": 24, + "group_elements": 48, + "invertible_pivots": 48, + "orbit_partition_sha256": "7a6ea3ee24fd992b7d5073c40ece8602fae4457adbaea0a789707640470a24c7", + "orbit_representatives": 8136, + "orbit_size_histogram": { + "1": 12, + "12": 66, + "24": 7620, + "6": 282, + "8": 156 + }, + "raw_triples": 186624 + }, + "controls_rejected": [ + "wrong_rank", + "wrong_dimension", + "wrong_product_block", + "changed_P_entry", + "singular_pivot", + "boolean_dimension", + "noncanonical_field_value", + "unsupported_composite_modulus", + "slope_one_only_formula", + "maximal_dimension_at_every_rank" + ], + "domains": { + "binary_complete": { + "literal_witnesses": 2496, + "noncommuting_pivot_triples": 288, + "rho0_counts": { + "0": 408, + "2": 144, + "4": 24 + }, + "subspace_pairs": 21690, + "triples": 576, + "two_phase_triples": 180 + }, + "binary_d3_all_H": { + "literal_witnesses": 2546, + "noncommuting_pivot_triples": 512, + "rho0_counts": { + "0": 108, + "1": 42, + "2": 231, + "3": 14, + "4": 105, + "6": 12 + }, + "subspace_pairs": 35801, + "triples": 512, + "two_phase_triples": 175 + }, + "structured_Q_and_prime_fields": { + "literal_witnesses": 861, + "noncommuting_pivot_triples": 147, + "rho0_counts": { + "0": 84, + "2": 65, + "4": 6, + "6": 6, + "8": 4 + }, + "subspace_pairs": 0, + "triples": 165, + "two_phase_triples": 44 + }, + "ternary_complete_up_to_conjugacy": { + "literal_witnesses": 26148, + "noncommuting_pivot_triples": 6480, + "rho0_counts": { + "0": 2350, + "1": 288, + "2": 3874, + "4": 1624 + }, + "subspace_pairs": 113768, + "triples": 8136, + "two_phase_triples": 816 + } + }, + "independent_minor_subset_census": { + "matrices": 609, + "sha256": "ceedd2d0d054ae3fcc6b252271b53a14c906d8610af519265d8771254d8f7692" + }, + "literal_witness_sha256": "146b692840920b901f9612f04b196e5c71478372fe6b5ef3c72dce45a1f8f1f4", + "literal_witnesses": 32051, + "mode": "complete declared domains", + "profile_sha256": "06e62eb259dfc4aa55b845ca2273670ec7ec8da35b98883f89f66ba8cbbbdaf8", + "schema_version": 1, + "scope": "finite corroboration of all-field proof; no kappa or supplier", + "source_sha256": { + "AUDIT.md": "48b5425d7d81d869fe0b6a4eed84494fce6b0d96c01a0724f30b20fe9661a395", + "LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "OVERLAP.json": "c97ed8d722911840930ff5e25f4f94d156b0e857c259b4d68bcf0eded12ca403", + "PROOF.md": "33b2b3a07f96e1004d7cccf2d356391dd5bcfa9ae38025221ebd9b106e02b46c", + "README.md": "17f6034302925805ce866ce10cbf7ce5b5a8abe2ba49c8ac585fcfc19c4578d7", + "SOURCES.json": "436c5badffd1192f7e7d2d7e570117a057d758b258cda8c3660fb7dbd81efae0", + "TASK.json": "26ce0f08ee56ed8e1b1fe43270ed83425ee45fb52189a514a6e1cc38609cd739", + "VERIFY.json": "c6aa7e14bc6288f666d67c0ca74aef452a9cbbc533ee20b78fabda9973f90323", + "check_witnesses.py": "f82ca005ef0f030dfd4284867f194d264a28e38da9590817ebe9c2784f330c3c", + "construct.py": "7d6d715a73215d13045093edeb2f3cfbdd81625c7982e245c8b0ff574a612f6e", + "linear.py": "1dcab54805638f35938c262387be7afb358039afc7b4b19f0a8e22e21d60d246", + "oracle.py": "2d3955aa38d5c175410e6faf08d17bc2ece4131e7bc9a00aedbd43392bff3292", + "reference5128.md": "77118415edf74aa4b6a49c94cb735913ad08377802ab44f3f51f66531b46593a", + "reference6031.md": "2c79b6beff2d2cce1f6d5c75230d63b4a980156ee32f8027c826a30b7f39030e", + "reference6031.py": "ad3cd5bc2fd712a4ac182946b4db0918f6f2fdb7795a6ef11e81ac1ee48d6748", + "reference6053.md": "43132f8def99b90f732fd4008f64bad74b71e0d3af035ed436169b54717d3c3a", + "ternary_orbits.py": "7de1f25879d089a8e7a72ad7227ea022c1624730d56a94aa4257d1121350fada", + "test_mutations.py": "c22e26f46959a50c40f45193f1484f8ad6851ecd7ba27e83ac4dba809ee99b9c", + "verify.py": "98bec2ad7f066622a3d1c852e497eca422c5931f6ec71d6afca95bfcbd554e30" + }, + "subspace_pairs": 171259, + "unique_triples": 9381 +} diff --git a/research/schur-rank-attainment/SOURCES.json b/research/schur-rank-attainment/SOURCES.json new file mode 100644 index 0000000000..3b0697496f --- /dev/null +++ b/research/schur-rank-attainment/SOURCES.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "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", + "vendored_as": "reference5128.md" + }, + { + "path": "research/schur-intermediate-ranks/PROOF.md", + "usage": "provenance", + "git_blob": "234a86b25f24e5fe85b64ebef0c24ca39fff278e", + "sha256": "2c79b6beff2d2cce1f6d5c75230d63b4a980156ee32f8027c826a30b7f39030e", + "vendored_as": "reference6031.md" + }, + { + "path": "research/schur-intermediate-ranks/verify.py", + "usage": "provenance", + "vendored_as": "reference6031.py", + "git_blob": "58a2bb02d28b0d9b7a8b683a7f9a2c8247ad6142", + "sha256": "ad3cd5bc2fd712a4ac182946b4db0918f6f2fdb7795a6ef11e81ac1ee48d6748" + }, + { + "path": "research/schur-ranks-all-fields/PROOF.md", + "usage": "provenance", + "pin": "head:12385ca23315181e3d15eb23a2d9ffec65d9a909:research/schur-ranks-all-fields/PROOF.md", + "git_blob": "698b34aba772375f85ae08cccfdc6e280b84218b", + "sha256": "43132f8def99b90f732fd4008f64bad74b71e0d3af035ed436169b54717d3c3a", + "vendored_as": "reference6053.md" + } + ] +} diff --git a/research/schur-rank-attainment/TASK.json b/research/schur-rank-attainment/TASK.json new file mode 100644 index 0000000000..ed7a3e2ae7 --- /dev/null +++ b/research/schur-rank-attainment/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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": "Independent audit of PR6053 at 12385ca23315181e3d15eb23a2d9ffec65d9a909: compare its all-field rank/dimension argument to a separately developed coordinate-minor construction, and corroborate its ordered closed rho0 formula with complete binary/ternary d=2 coverage, a fixed d=3 family and rational/prime-field fixtures.", + "scope_change_reason": "Handoff-first continuation of PR6031 Open next question 1. This is an algebraic side result in the Schur deletion family, not a paid decoder/coframe or signed-invoice optimization. Final live overlap refresh found apoursh's PR6053, opened 2026-10-28T03:27:51Z during this session. The task was narrowed to a source-bound independent computational/mathematical audit; the shared theorem is not claimed as a novel contribution.", + "bottleneck_link": "Resolve the exact algebraic dimension-versus-rank obligation before any physical header design is priced. No supplier or kappa gain is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at a proved attainment construction with bounded exact corroboration, or one explicit counterexample. No physical header, supplier replay, larger census or selected-frontier edit.", + "outcome": "completed", + "evidence": "PROOF.md retains the coordinate-minor derivation; AUDIT.md maps the exact reviewed claims to separate computations. RESULT.json records all 9,389 labelled formula comparisons, 9,381 distinct triples, 32,051 literal witnesses, 171,259 subspace pairs and exact coverage of all 186,624 ternary d=2 inputs via 8,136 conjugacy representatives. No discrepancy found within the audited scope; no independent human/formal-kernel acceptance.", + "author": "SHIN09-git", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, implementation, validation and writing; one assistant, no subagents, no independent human or formal-kernel review.", + "open_questions": [ + { + "question": "For a concrete physical header proposal, can these least-dimensional algebraic witnesses be realized with a complete paid/productive invoice?", + "why_it_matters": "The algebraic minimum alone does not specify a producer, consumer or actual multiplication cost.", + "first_step": "Choose one already specified physical header and caller contract, check live handoffs, and translate one exact A,B,H,rho witness into that contract before pricing all costs.", + "blocked_by": "No physical header, native layout, restoration/ownership contract or cost model is chosen in this package; this is a separate supplier task." + } + ], + "session_started_at": "2026-10-28T03:02:42Z", + "initial_hypothesis": "A maximal nonsingular minor of the baseline defect pairing gives efficient single deletions, followed by nested nonsingular minor deletions. Because these delete basis vectors within original sector blocks, the block constraints do not obstruct attainment.", + "publication_status": "local-only; this new research is not part of PR6046", + "predecessors": [ + { + "pr": 6031, + "author": "Nick Petalas", + "head": "acc000f4edfa0b0c4a90b505c6e02a4c3572f74c", + "role": "Lower bounds, sector-subspace reduction and explicit general-attainment question" + }, + { + "pr": 5128, + "author": "Krzysztof Wojt", + "role": "Arbitrary-pivot ordered factorization, sector construction and full-rank endpoint" + }, + { + "pr": 6053, + "author": "apoursh", + "head": "12385ca23315181e3d15eb23a2d9ffec65d9a909", + "role": "Concurrent all-field theorem and ordered closed minimum-rank formula; exact target of final audit, not a new theorem claimed here." + } + ], + "entry_note": "Selected result is PR6030 at this base. The canonical revision-8 task card retains historical PR5599 wording; original_card is preserved and the changed algebraic side scope is explicit. The initial research_selected_baseline.py attempt found a sparse-checkout input missing; no full selected supplier replay was run or claimed.", + "overlap_adjustment_at": "2026-10-28T03:43:00Z" +} diff --git a/research/schur-rank-attainment/VALIDATION.json b/research/schur-rank-attainment/VALIDATION.json new file mode 100644 index 0000000000..35e28e7542 --- /dev/null +++ b/research/schur-rank-attainment/VALIDATION.json @@ -0,0 +1,140 @@ +{ + "schema_version": 1, + "recorded_at": "2026-10-28T03:57:29.955186+00:00", + "research_started_at": "2026-10-28T03:02:42Z", + "scope": "Independent audit of apoursh PR6053 at 12385ca23315181e3d15eb23a2d9ffec65d9a909; no novelty or kappa claim.", + "registered_replay": { + "started_at": "2026-10-28T03:51:43.217824+00:00", + "finished_at": "2026-10-28T03:57:29.802727+00:00", + "command": [ + "{python}", + "-X", + "utf8", + "-B", + "scripts/research_package.py", + "--package", + "research/schur-rank-attainment" + ], + "seconds": 346.5848621999612, + "returncode": 0, + "package_unchanged": true, + "python": "3.12.10 (tags/v3.12.10:0cc8128, Apr 8 2025, 12:21:36) [MSC v.1943 64 bit (AMD64)]", + "log_sha256": "66994b561c270e4231aa23501337777f43a29d1e7e57b7dc1fd4b207e080612a" + }, + "source_mutations": { + "mode": "optimized fresh source-only subprocesses; exact receipt comparison disabled", + "positive_controls": 1, + "code_mutants_rejected": 9, + "results": [ + { + "name": "optimized_positive", + "status": "PASS", + "seconds": 15.747633099905215 + }, + { + "name": "reorder_closed_formula_inverse", + "status": "REJECTED", + "seconds": 0.2837741000112146, + "expected_check": "PR6053 ordered closed rho0", + "stderr_sha256": "a78a6192198b04894063e9f3acd223336ea870a206584edd6a3cd580bed11c52", + "last_error": "ValueError: PR6053 ordered closed rho0" + }, + { + "name": "omit_H_rank_closed_formula", + "status": "REJECTED", + "seconds": 0.37425830005668104, + "expected_check": "PR6053 ordered closed rho0", + "stderr_sha256": "7e807e88cfde1136e9237ef2065b4a952775e653886fbfc863237be77f930beb", + "last_error": "ValueError: PR6053 ordered closed rho0" + }, + { + "name": "omit_efficient_row_phase", + "status": "REJECTED", + "seconds": 0.26833619992248714, + "expected_check": "maximal rank minor", + "stderr_sha256": "c0575b1035e51f7467ef169a0744cfc73293124b53122bc2c62110525f45b984", + "last_error": "ValueError: maximal rank minor" + }, + { + "name": "use_principal_minors_only", + "status": "REJECTED", + "seconds": 0.42268980003427714, + "expected_check": "nonzero cofactor exists", + "stderr_sha256": "fc8169a7c4306317d683e3daafc948f39ede4f901ab4d8753205f8af962cf991", + "last_error": "ValueError: nonzero cofactor exists" + }, + { + "name": "reverse_H_Binverse_order", + "status": "REJECTED", + "seconds": 0.750686899991706, + "expected_check": "left lift identity", + "stderr_sha256": "33fd781d8d8ac1e16f761f7b5b76bebc34847a2b0a82ae9536010e6c36d065b7", + "last_error": "ValueError: left lift identity" + }, + { + "name": "lose_odd_characteristic_sign", + "status": "REJECTED", + "seconds": 1.0337002000305802, + "expected_check": "right lift identity", + "stderr_sha256": "f7cd3be1c84b63e48c9756f06e65398a0c67874607e9047d1e1fc7321a2ee488", + "last_error": "ValueError: right lift identity" + }, + { + "name": "mix_sector_annihilators", + "status": "REJECTED", + "seconds": 0.4241997000062838, + "expected_check": "sector factor", + "stderr_sha256": "9898ecb4d793e5ca22e51d78fd74bda17da53ef4bc2221bcc72606088604ef20", + "last_error": "ValueError: sector factor dimensions" + }, + { + "name": "wrong_slope_two_bound", + "status": "REJECTED", + "seconds": 0.448273399961181, + "expected_check": "sharp dimension law", + "stderr_sha256": "ffd3f041f67911f3fb2820c69699c7fa356b6be08a44938db90c447982add100", + "last_error": "ValueError: sharp dimension law" + }, + { + "name": "omit_independent_rank_check", + "status": "REJECTED", + "seconds": 16.31005179998465, + "expected_check": "independent checker accepted wrong_rank", + "stderr_sha256": "022888f2b38cc81b27aee0c29b581cc999eefb732a595932ab41ed3092a80abe", + "last_error": "ValueError: independent checker accepted wrong_rank" + } + ] + }, + "coverage": { + "unique_triples": 9381, + "labelled_closed_formula_comparisons": 9389, + "literal_witnesses": 32051, + "subspace_pairs": 171259, + "ternary": { + "burnside_orbit_count": 8136, + "coverage": "All A,B in GL_2(F3), all H in M_2(F3), by exact simultaneous conjugacy", + "distinct_actions": 24, + "group_elements": 48, + "invertible_pivots": 48, + "orbit_partition_sha256": "7a6ea3ee24fd992b7d5073c40ece8602fae4457adbaea0a789707640470a24c7", + "orbit_representatives": 8136, + "orbit_size_histogram": { + "1": 12, + "12": 66, + "24": 7620, + "6": 282, + "8": 156 + }, + "raw_triples": 186624 + } + }, + "written_review": "Reviewed all six lifts, the exact annihilator/kernel equalities, cost lower bounds, cofactor deletion, padding, simultaneous-conjugacy invariance, and PR6053's two disjoint cross blocks and ordered block elimination. No discrepancy found within the stated scope.", + "limitations": [ + "Same assistant authored the primary and separate verification paths; no independent human or proof-kernel acceptance.", + "No replay of the original PR6053 executable or its exact 886-case inventory is claimed.", + "No selected supplier replay or physical cost/pricing claim.", + "Repository is shallow; explicit fetched source pins resolve, but optional full source-history closure is not claimed." + ], + "delivery": "A subsequent official committed export and Git-free replay are recorded outside the package in export-validation.json, avoiding a self-referential committed receipt.", + "publication": "Local research only. PR6046 publishes the previous five-label study, not this audit." +} diff --git a/research/schur-rank-attainment/VERIFY.json b/research/schur-rank-attainment/VERIFY.json new file mode 100644 index 0000000000..d9d8751a63 --- /dev/null +++ b/research/schur-rank-attainment/VERIFY.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 450, + "checks": "All declared domains, source pins and exact receipt: independent complete subspace profiles, literal P/Q checks, ternary conjugacy coverage, 609 generic minor censuses and 10 negative controls. Also compare PR6053's ordered closed minimum-rank formula on every declared input." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 450, + "checks": "All declared domains, source pins and exact receipt: independent complete subspace profiles, literal P/Q checks, ternary conjugacy coverage, 609 generic minor censuses and 10 negative controls; assertions disabled. Also compare PR6053's ordered closed minimum-rank formula on every declared input." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/test_mutations.py" + ], + "timeout_seconds": 180, + "checks": "Optimized fresh-source positive control and nine actual code mutants; require the intended scientific rejection, with receipt comparison bypassed." + } + ] +} diff --git a/research/schur-rank-attainment/check_witnesses.py b/research/schur-rank-attainment/check_witnesses.py new file mode 100644 index 0000000000..11de6c7755 --- /dev/null +++ b/research/schur-rank-attainment/check_witnesses.py @@ -0,0 +1,107 @@ +"""Independent exact check of literal matrices. Imports no generation code. +SHIN09-git, substantial OpenAI Codex assistance. Apache-2.0. +Can read one fixture list on stdin; normal library use accepts the same records. +""" +from fractions import Fraction +import json +import sys + + +def require(ok,msg): + if not ok: + raise ValueError(msg) + + +def norm(x,p): + return x%p if p else Fraction(x) + + +def matrix(raw,p): + require(isinstance(raw,list) and raw and all(isinstance(row,list) for row in raw),"matrix list") + n=len(raw) + require(all(len(row)==n for row in raw),"square fixture") + require(all(type(x) is int if p else type(x) is str for row in raw for x in row),"exact scalar encoding") + if p: + require(all(0<=x

0 and all((X.r,X.c,X.p)==(d,d,p) for X in (A,B,H)),"pivot shapes") + A.inverse() + B.inverse() + return [eye(d,p)-A-B+H,A-H,B-H,H] + + +def ordered_maps(A,B,H): + d,p=A.r,A.p + ai,bi=A.inverse(),B.inverse() + O=zeros(d,d,p) + G=block([[O,ai],[-bi@H,-bi],[eye(d,p)-bi@H,ai-bi]]) + Gp=block([[ai,-bi,ai-bi],[O,H@bi,H@bi-eye(d,p)]]) + return G,Gp + + +def defect_pairing(A,B,H): + ts=compressed(A,B,H) + d,p=A.r,A.p + erows,kcols,emeta,kmeta=[],[],[],[] + for j,T in enumerate(ts[1:]): + for w in T.T.kernel(): + wa=(Mat([w],p,d)@A).a[0] + e=(tuple(wa)+tuple(w) if j==0 else + (0,)*d+tuple(w) if j==1 else + (0,)*d+tuple(-x for x in w)) + erows.append(e) + emeta.append((j,w)) + for z in T.kernel(): + az=(A@la.from_columns([z],d,p)).T.a[0] + k=(tuple(-x for x in z)+tuple(az) if j==0 else + tuple(-x for x in z)+(0,)*d if j==1 else + tuple(z)+(0,)*d) + kcols.append(k) + kmeta.append((j,z)) + E=Mat(erows,p,2*d) + K=la.from_columns(kcols,2*d,p) + nu=len(erows) + need(E.rank()==K.rank()==nu,"independent defect lifts") + G,Gp=ordered_maps(A,B,H) + # Verify every lifted row/vector against its pure-sector original. + for e,(j,w) in zip(E.a,emeta): + pure=[0]*(3*d) + pure[j*d:(j+1)*d]=w + need(Mat([e],p,2*d)@Gp==Mat([pure],p,3*d),"left lift identity") + for k,(j,z) in zip(K.T.a,kmeta): + pure=[0]*(3*d) + pure[j*d:(j+1)*d]=z + need(G@la.from_columns([k],2*d,p)==la.from_columns([pure],3*d,p),"right lift identity") + C=E@K + return ts,C,emeta,kmeta + + +def minor_chain(C): + """Pairs of retained coordinate rows/columns; never mixes sector bases.""" + need(C.r==C.c,"square defect pairing") + nu=C.r + rank=C.rank() + _,col_piv=la.eliminate(C.a,C.c,C.p) + small=C.take(list(range(nu)),col_piv) + _,row_piv=la.eliminate(small.T.a,small.T.c,C.p) + core_i=set(row_piv) + core_j=set(col_piv) + ii,jj=list(range(nu)),list(range(nu)) + chain=[(tuple(ii),tuple(jj),"start")] + for i in list(ii): + if i not in core_i: + ii.remove(i) + chain.append((tuple(ii),tuple(jj),"one row")) + for j in list(jj): + if j not in core_j: + jj.remove(j) + chain.append((tuple(ii),tuple(jj),"one column")) + need(len(ii)==len(jj)==rank and C.take(ii,jj).rank()==rank,"maximal rank minor") + while ii: + size=len(ii) + found=None + for i in ii: + for j in jj: + ni=[x for x in ii if x!=i] + nj=[x for x in jj if x!=j] + if C.take(ni,nj).rank()==size-1: + found=(ni,nj) + break + if found is not None: + break + need(found is not None,"nonzero cofactor exists") + ii,jj=found + chain.append((tuple(ii),tuple(jj),"paired row/column")) + return chain + + +def plan(A,B,H): + ts,C,emeta,kmeta=defect_pairing(A,B,H) + d,p=A.r,A.p + nu=C.r + n0=sum(T.rank() for T in ts) + nmax=ts[0].rank()+3*d+nu + rho0=2*d-2*nu+C.rank() + states={} + for ii,jj,kind in minor_chain(C): + rho=2*d-len(ii)-len(jj)+C.take(ii,jj).rank() + n=nmax-len(ii)-len(jj) + need(rho not in states,"rank must rise strictly along retained chain") + need(n==max(n0+rho-rho0,nmax-2*(2*d-rho)),"sharp dimension law") + ibases,nbases=[],[] + for j in range(3): + annihilators=[emeta[i][1] for i in ii if emeta[i][0]==j] + ibases.append(Mat(annihilators,p,d).kernel()) + nbases.append([kmeta[k][1] for k in jj if kmeta[k][0]==j]) + states[rho]={"n":n,"I":ibases,"N":nbases,"kind":kind, + "rows":list(ii),"columns":list(jj)} + need(sorted(states)==list(range(rho0,2*d+1)),"complete rank interval") + return {"n0":n0,"nmax":nmax,"rho0":rho0,"nu":nu,"pairing_rank":C.rank(), + "pairing":C,"states":states,"sectors":ts} + + +def sector_factors(T,ibasis,nbasis): + d,p=T.r,T.p + sigma=T.image() + standard=eye(d,p).a + full=sigma+la.extension(sigma,standard,d,p) + coordinates=la.from_columns(full,d,p).inverse() + phi=(coordinates@T).take(list(range(len(sigma))),list(range(d))) + kb=la.extension(nbasis,T.kernel(),d,p) + basis=list(nbasis)+kb + basis+=la.extension(basis,standard,d,p) + coords=la.from_columns(basis,d,p).inverse() + psi=coords.take(list(range(len(nbasis),len(nbasis)+len(kb))),list(range(d))) + tau=la.extension(sigma,ibasis,d,p) + X=la.from_columns(sigma+[(0,)*d]*len(kb)+tau,d,p) + Y=la.stack([phi,psi,zeros(len(tau),d,p)]) + need(X@Y==T,"sector factor product") + need(X.rank()==len(ibasis) and d-Y.rank()==len(nbasis),"sector factor dimensions") + need(all(all(not x for x in (Y@la.from_columns([v],d,p)).T.a[0]) for v in nbasis), + "sector kernel containment") + return X,Y + + +def build(A,B,H,state): + ts=compressed(A,B,H) + d,p=A.r,A.p + factors=[sector_factors(ts[0],ts[0].image(),ts[0].kernel())] + factors += [sector_factors(T,I,N) for T,I,N in zip(ts[1:],state["I"],state["N"])] + projection=la.join([X for X,Y in factors]) + inclusion=la.stack([Y for X,Y in factors]) + need(projection@inclusion==eye(d,p),"split boundary pi i") + n=inclusion.r + basis=inclusion.image()+projection.kernel() + change=la.from_columns(basis,n,p) + inv=change.inverse() + pd,qd=[],[] + for (X,Y),(pv,qv) in zip(factors,((0,0),(1,0),(0,1),(1,1))): + pd += [pv]*Y.r + qd += [qv]*Y.r + P0=Mat([[pd[i]*int(i==j) for j in range(n)] for i in range(n)],p,n) + Q0=Mat([[qd[i]*int(i==j) for j in range(n)] for i in range(n)],p,n) + P,Q=inv@P0@change,inv@Q0@change + need(n==state["n"],"realized dimension") + return P,Q + + +def literal_rank(A,B,H,P,Q): + d,n,p=A.r,P.r,A.p + need(n>=d and (P.r,P.c,P.p)==(Q.r,Q.c,Q.p)==(n,n,p),"literal shapes") + need(P@P==P and Q@Q==Q and P@Q==Q@P,"commuting idempotents") + top=list(range(d)); rest=list(range(d,n)) + need(P.take(top,top)==A and Q.take(top,top)==B and (P@Q).take(top,top)==H, + "prescribed blocks") + S=P.take(rest,rest)-P.take(rest,top)@A.inverse()@P.take(top,rest) + Z=Q.take(rest,rest)-Q.take(rest,top)@B.inverse()@Q.take(top,rest) + return (S@Z-Z@S).rank() diff --git a/research/schur-rank-attainment/linear.py b/research/schur-rank-attainment/linear.py new file mode 100644 index 0000000000..3e51ceef49 --- /dev/null +++ b/research/schur-rank-attainment/linear.py @@ -0,0 +1,143 @@ +"""Small exact matrix implementation over Q or a prime field. +SHIN09-git, substantial OpenAI Codex assistance. Apache-2.0. +No numerical tolerances, numpy, SymPy or predecessor executable imports. +""" +from fractions import Fraction + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def scalar(x, p): + if p: + if isinstance(x, Fraction): + return x.numerator * pow(x.denominator, -1, p) % p + return x % p + return Fraction(x) + + +def eliminate(rows, width, p): + a = [[scalar(x, p) for x in row] for row in rows] + need(all(len(row) == width for row in a), "ragged elimination input") + pivots = [] + for c in range(width): + i = len(pivots) + j = next((j for j in range(i, len(a)) if a[j][c]), None) + if j is None: + continue + a[i], a[j] = a[j], a[i] + inv = pow(a[i][c], -1, p) if p else 1 / a[i][c] + a[i] = [scalar(x * inv, p) for x in a[i]] + for j in range(len(a)): + if j != i and a[j][c]: + z = a[j][c] + a[j] = [scalar(x - z*y, p) for x,y in zip(a[j],a[i])] + pivots.append(c) + return a[:len(pivots)], pivots + + +class Mat: + def __init__(self, rows, p=0, width=None): + self.p = p + self.a = tuple(tuple(scalar(x,p) for x in row) for row in rows) + self.r = len(self.a) + self.c = len(self.a[0]) if self.r else (0 if width is None else width) + need(all(len(row)==self.c for row in self.a), "ragged matrix") + if width is not None: + need(self.c==width, "wrong explicit width") + + def __eq__(self, other): + return isinstance(other,Mat) and (self.p,self.r,self.c,self.a)==(other.p,other.r,other.c,other.a) + + def __matmul__(self, b): + need(self.p==b.p and self.c==b.r, "matrix product shape/field") + bt=list(zip(*b.a)) if b.r else [() for _ in range(b.c)] + return Mat([[sum(x*y for x,y in zip(row,col)) for col in bt] for row in self.a],self.p,b.c) + + def __add__(self,b): + need((self.r,self.c,self.p)==(b.r,b.c,b.p),"matrix sum shape/field") + return Mat([[x+y for x,y in zip(row,col)] for row,col in zip(self.a,b.a)],self.p,self.c) + + def __neg__(self): + return Mat([[-x for x in row] for row in self.a],self.p,self.c) + + def __sub__(self,b): + return self + (-b) + + @property + def T(self): + return Mat(list(zip(*self.a)) if self.r else [[] for _ in range(self.c)],self.p,self.r) + + def take(self,rows,cols): + return Mat([[self.a[i][j] for j in cols] for i in rows],self.p,len(cols)) + + def rank(self): + return len(eliminate(self.a,self.c,self.p)[1]) + + def inverse(self): + need(self.r==self.c,"inverse needs square matrix") + n=self.r + a,piv=eliminate([list(row)+list(e) for row,e in zip(self.a,eye(n,self.p).a)],2*n,self.p) + need(piv[:n]==list(range(n)) and len(piv)==n,"singular matrix") + return Mat([row[n:] for row in a],self.p,n) + + def kernel(self): + a,piv=eliminate(self.a,self.c,self.p) + result=[] + for c in range(self.c): + if c in piv: + continue + v=[scalar(0,self.p)]*self.c + v[c]=scalar(1,self.p) + for i,j in enumerate(piv): + v[j]=-a[i][c] + result.append(tuple(scalar(x,self.p) for x in v)) + return result + + def image(self): + _,piv=eliminate(self.a,self.c,self.p) + return [tuple(self.a[i][j] for i in range(self.r)) for j in piv] + + def json(self): + return [[x if self.p else str(x) for x in row] for row in self.a] + + +def zeros(r,c,p): + return Mat([[0]*c for _ in range(r)],p,c) + + +def eye(n,p): + return Mat([[int(i==j) for j in range(n)] for i in range(n)],p,n) + + +def from_columns(cols,height,p): + return Mat([[v[i] for v in cols] for i in range(height)],p,len(cols)) + + +def stack(blocks): + need(bool(blocks),"empty stack") + need(all(b.c==blocks[0].c and b.p==blocks[0].p for b in blocks),"stack shape/field") + return Mat([row for b in blocks for row in b.a],blocks[0].p,blocks[0].c) + + +def join(blocks): + need(bool(blocks),"empty join") + need(all(b.r==blocks[0].r and b.p==blocks[0].p for b in blocks),"join shape/field") + return Mat([sum((list(b.a[i]) for b in blocks),[]) for i in range(blocks[0].r)],blocks[0].p,sum(b.c for b in blocks)) + + +def block(rows): + return stack([join(row) for row in rows]) + + +def extension(start,candidates,width,p): + out=list(start) + need(Mat(out,p,width).rank()==len(out),"dependent starting basis") + extra=[] + for v in candidates: + if Mat(out+[v],p,width).rank()>len(out): + out.append(tuple(v)) + extra.append(tuple(v)) + return extra diff --git a/research/schur-rank-attainment/oracle.py b/research/schur-rank-attainment/oracle.py new file mode 100644 index 0000000000..391ffb2bb9 --- /dev/null +++ b/research/schur-rank-attainment/oracle.py @@ -0,0 +1,132 @@ +"""Independent finite subspace enumeration, with no constructor imports. +SHIN09-git, substantial OpenAI Codex assistance. Apache-2.0. +Exhausts the #6031 sector choices using literal finite vector sets. +""" +from itertools import product +from functools import lru_cache + + +def rank_vectors(vectors,p): + basis={} + for source in vectors: + v=[x%p for x in source] + for j in sorted(basis): + z=v[j] + if z: + v=[(x-z*y)%p for x,y in zip(v,basis[j])] + pivot=next((j for j,x in enumerate(v) if x),None) + if pivot is not None: + z=pow(v[pivot],-1,p) + basis[pivot]=tuple(x*z%p for x in v) + return len(basis) + + +def independent_basis(space,p): + out=[] + for v in sorted(space): + if rank_vectors(out+[v],p)>len(out): + out.append(v) + return tuple(out) + + +def mv(a,v,p): + return tuple(sum(x*y for x,y in zip(row,v))%p for row in a) + + +def mm(a,b,p): + return tuple(tuple(sum(a[i][k]*b[k][j] for k in range(len(b)))%p + for j in range(len(b[0]))) for i in range(len(a))) + + +def inverse(a,p): + n=len(a) + out=[list(row)+[int(i==j) for j in range(n)] for i,row in enumerate(a)] + for c in range(n): + j=next((j for j in range(c,n) if out[j][c]%p),None) + if j is None: + raise ValueError("singular oracle pivot") + out[c],out[j]=out[j],out[c] + scale=pow(out[c][c]%p,-1,p) + out[c]=[x*scale%p for x in out[c]] + for j in range(n): + if j!=c: + z=out[j][c] + out[j]=[(x-z*y)%p for x,y in zip(out[j],out[c])] + return tuple(tuple(row[n:]) for row in out) + + +@lru_cache(None) +def spaces(d,p): + vectors=tuple(product(range(p),repeat=d)) + initial=frozenset({(0,)*d}) + seen={initial} + todo=[initial] + while todo: + s=todo.pop() + for v in vectors: + if v in s: + continue + bigger=frozenset(tuple((x+t*y)%p for x,y in zip(w,v)) + for w in s for t in range(p)) + if bigger not in seen: + seen.add(bigger) + todo.append(bigger) + return tuple(sorted(seen,key=lambda s:(len(s),sorted(s)))) + + +@lru_cache(None) +def geometry(t,p): + d=len(t) + vectors=tuple(product(range(p),repeat=d)) + image=frozenset(mv(t,v,p) for v in vectors) + kernel=frozenset(v for v in vectors if mv(t,v,p)==(0,)*d) + all_s=spaces(d,p) + ims=[independent_basis(s,p) for s in all_s if image<=s] + kers=[independent_basis(s,p) for s in all_s if s<=kernel] + return ims,kers,rank_vectors(t,p) + + +def profile(A,B,H,p): + d=len(A) + ai,bi=inverse(A,p),inverse(B,p) + ts=[tuple(tuple((int(i==j)-A[i][j]-B[i][j]+H[i][j])%p for j in range(d)) for i in range(d)), + tuple(tuple((A[i][j]-H[i][j])%p for j in range(d)) for i in range(d)), + tuple(tuple((B[i][j]-H[i][j])%p for j in range(d)) for i in range(d)),H] + bih,hbi=mm(bi,H,p),mm(H,bi,p) + # Build the maps entrywise rather than importing the primary block code. + G=[]; Gp=[[0]*(3*d) for _ in range(2*d)] + for s in range(3): + for i in range(d): + if s==0: + G.append([0]*d+list(ai[i])) + elif s==1: + G.append([(-bih[i][j])%p for j in range(d)]+[(-bi[i][j])%p for j in range(d)]) + else: + G.append([(int(i==j)-bih[i][j])%p for j in range(d)]+[(ai[i][j]-bi[i][j])%p for j in range(d)]) + for i in range(d): + for j in range(d): + Gp[i][j]=ai[i][j] + Gp[i][d+j]=-bi[i][j]%p + Gp[i][2*d+j]=(ai[i][j]-bi[i][j])%p + Gp[d+i][d+j]=hbi[i][j] + Gp[d+i][2*d+j]=(hbi[i][j]-int(i==j))%p + M=mm(G,Gp,p) + choices=[geometry(t,p) for t in ts[1:]] + base=rank_vectors(ts[0],p)+sum(d-c[2] for c in choices) + best={} + examined=0 + def embedded(j,v): + return (0,)*(j*d)+tuple(v)+(0,)*((2-j)*d) + n_options=[] + for ns in product(*(c[1] for c in choices)): + nb=tuple(embedded(j,v) for j,basis in enumerate(ns) for v in basis) + n_options.append(nb) + for ims in product(*(c[0] for c in choices)): + ib=tuple(embedded(j,v) for j,basis in enumerate(ims) for v in basis) + mi=tuple(mv(M,v,p) for v in ib) + for nb in n_options: + rho=rank_vectors(mi+nb,p)-len(nb) + cost=base+len(ib)-len(nb) + best[rho]=min(best.get(rho,10**9),cost) + examined+=1 + return best,examined diff --git a/research/schur-rank-attainment/reference5128.md b/research/schur-rank-attainment/reference5128.md new file mode 100644 index 0000000000..c7d58883b4 --- /dev/null +++ b/research/schur-rank-attainment/reference5128.md @@ -0,0 +1,222 @@ +# Prescribed arbitrary pivots: the exact Schur dimension + +Krzysztof Wojt, with substantial OpenAI Codex assistance. Apache-2.0. + +This is a scoped all-field algebraic proof. The ordered Schur factorization +is Nick Petalas's #4597. The joint-sector and split-factor methods come from +ssafwann #4657/#4671 and Nick Petalas #4746/#4771/#4774/#4785. The new step is +the six-map criterion for arbitrary invertible, possibly noncommuting block +pivots, and its exact prescribed-boundary minimum. No historical priority +is claimed for the underlying linear algebra. + +## 1. Statement + +Let K be any field, d >= 1, and let A,B in GL_d(K) and H in M_d(K) be +prescribed. There is no commutation assumption on A,B,H. Among all commuting +idempotents P,Q in M_n(K) satisfying + +``` +P11=A, Q11=B, (PQ)11=H, +S=P22-P21 A^-1 P12, Z=Q22-Q21 B^-1 Q12, +rank(SZ-ZS)=2d, +``` + +the exact least dimension is + +``` +n_min = 3d + rank(I-A-B+H) + + nullity(A-H) + nullity(B-H) + nullity(H). (1) +``` + +For the simultaneous eigenspaces indexed by 00,10,01,11, every such pair +satisfies the componentwise bounds + +``` +r00 >= rank(I-A-B+H), +r10 >= d+nullity(A-H), +r01 >= d+nullity(B-H), +r11 >= d+nullity(H). (2) +``` + +All four equalities are attained together. The same construction attains +both least input ranks + +``` +rank P = 2d+nullity(A-H)+nullity(H), +rank Q = 2d+nullity(B-H)+nullity(H). (3) +``` + +Consequently it also minimizes both residual ranks, obtained by subtracting d. +One may add any number of unused 00-sector dimensions, so every n >= n_min +is feasible. Formula (1), not the finite verification, is the universal claim. + +## 2. Ordered ambient factors + +Let U=K^d, V=K^n, i:U -> V be inclusion of the first d coordinates and +pi:V -> U the corresponding projection. Thus pi i=I and +pi P i=A, pi Q i=B, pi PQ i=H. Define maps L:U^2 -> V and R:V -> U^2 by + +``` +L = [PQ i-Q i B^-1 H, P i A^-1-Q i B^-1], +R = [A^-1 pi P-B^-1 pi Q; + -pi PQ+H B^-1 pi Q]. (4) +``` + +The order of all factors is part of (4). Direct substitution gives +pi L=0 and R i=0. The operators + +``` +Ptilde=P-P i A^-1 pi P, Qtilde=Q-Q i B^-1 pi Q +``` + +have block forms diag(0,S), diag(0,Z). Multiplying (4) and cancelling the +two identical terms Q i B^-1 H B^-1 pi Q gives + +``` +L R = Ptilde Qtilde-Qtilde Ptilde = diag(0,SZ-ZS). (5) +``` + +This is the ambient form of #4597's ordered identity. It neither moves H +past B^-1 nor moves any pivot past another block. In particular +rank(SZ-ZS)<=2d. Equality holds exactly when L is injective and R is +surjective: a surjection onto U^2 followed by an injection from U^2 has +rank 2d, and rank 2d of the product forces both conditions. + +## 3. The six-map criterion without scalar pivots + +Commuting idempotents split V as the direct sum of their four simultaneous +eigenspaces, in every characteristic. Write + +``` +E00=(I-P)(I-Q), E10=P(I-Q), E01=(I-P)Q, E11=PQ, +Yj=Ej i:U -> Vj, Xj=pi|Vj:Vj -> U. +``` + +Their compressed products are + +``` +X00 Y00=I-A-B+H, X10 Y10=A-H, +X01 Y01=B-H, X11 Y11=H. (6) +``` + +In these coordinates the left factor is + +``` +L(x,y) = (0, + Y10 A^-1 y, + -Y01 B^-1(Hx+y), + Y11((I-B^-1 H)x+(A^-1-B^-1)y)). (7) +``` + +**Criterion.** rank(SZ-ZS)=2d if and only if each of Y10,Y01,Y11 is +injective and each of X10,X01,X11 is surjective. + +First prove that L is injective exactly when all three active Y maps are +injective. For necessity: + +* If 0!=z is in ker Y10, then (A-H)z=0 by (6). The nonzero pair + (x,y)=(-z,Az) is killed by (7): its first active component is Y10 z, + its second uses -Hz+Az=0, and its last argument is + -z+B^-1 Hz+z-B^-1 Az=0. +* If 0!=z is in ker Y01, then Hz=Bz. The pair (z,0) is killed by (7), + since B^-1 Hz=z and (I-B^-1 H)z=0. +* If 0!=z is in ker Y11, then Hz=0. Again (z,0) is killed by (7). + +Conversely, if all three Y maps are injective and L(x,y)=0, its 10 component +first gives y=0 because A is invertible. Its 01 component then gives Hx=0 +because B is invertible. Its 11 component finally gives x=0. + +Necessity of surjectivity of the X maps follows by applying this argument to +P^t,Q^t. Their leading blocks are A^t,B^t, their product block is H^t +(because PQ=QP), and their Schur commutator is -(SZ-ZS)^t. For each sector, +rank(Ej^t i)=rank(pi Ej)=rank Xj. Hence equality of commutator rank forces +all three X maps onto. This argument uses ranks, not an assumption that +the given coordinate splitting is orthogonal to the joint eigenspaces. + +For sufficiency, the preceding argument gives injectivity of L. If a pair +of row covectors (u,v) annihilates R, its restrictions to sectors 10,01,11 +are respectively + +``` +u A^-1 X10, +(-u+vH) B^-1 X01, +(u(A^-1-B^-1)-v+vH B^-1) X11. (8) +``` + +Surjectivity of X10 implies u=0. Surjectivity of X01 then implies vH=0. +The 11 expression reduces to -v X11, so v=0. Thus R is onto, proving the +criterion by (5). This also shows explicitly why noncommutation of A,B,H +does not obstruct the argument. + +## 4. Lower bound and simultaneous attainment + +If X:K^r -> K^d is onto and Y:K^d -> K^r is injective, the rank inequality +rank(XY)>=rank X+rank Y-r gives r>=d+nullity(XY). Apply it in each active +sector of (6). The 00 sector needs only r00>=rank(X00Y00). These are (2), +whose sum is (1). Adding the active sector dimensions of P and Q gives (3). + +Here is an explicit construction attaining them for every prescribed A,B,H. +For any T in M_d(K), choose a matrix N_T whose columns complement im T +in K^d and put + +``` +X_T=[T N_T], Y_T=[I;0]. +``` + +The middle space has dimension d+nullity(T); X_T is onto, Y_T is injective, +and X_T Y_T=T. Use these factors for T=A-H, B-H, H in sectors 10,01,11. +For T00=I-A-B+H choose an ordinary rank factorization X00Y00=T00 through +dimension rank T00. A zero-dimensional 00 sector is allowed. + +Let i be the vertical concatenation of the four Y maps and pi the horizontal +concatenation of the four X maps. By (6), pi i=I. On the sector direct sum, +define + +``` +P0=diag(0,I,0,I), Q0=diag(0,0,I,I). +``` + +They commute and are idempotent. Compression gives pi P0 i=A, +pi Q0 i=B, pi P0 Q0 i=H. Choose a basis N of ker pi. Since pi i=I, +M=[i N] is invertible. Set + +``` +P=M^-1 P0 M, Q=M^-1 Q0 M. +``` + +In the resulting coordinates, i is the first-block inclusion and pi its +projection. Thus P,Q have exactly the prescribed three leading blocks. +All six active maps have full rank, so their Schur commutator has rank 2d. +Their sector dimensions and input ranks attain (2) and (3) simultaneously. +This completes the proof; no diagonalization of H or compatibility condition +between A,B,H is needed. + +## 5. Specializations and a noncommuting sharp example + +If A=B=lambda I, (1) is precisely the common scalar-block formula of #4785. +If d=1 and A=p, B=q are distinct nonzero scalars, the three nullities sum +to [h in {0,p,q}], recovering #4774. A=B=I specializes to #4746/#4671. +These are consistency comparisons, not new results or predecessor audits. + +Over Q take + +``` +A=[[2,1],[0,2]], B=[[2,0],[1,2]], H=[[3,1],[1,3]]. +``` + +All three pairwise commutators of A,B,H are nonzero. Yet H=A+B-I, and +H, A-H=I-B, B-H=I-A are invertible. Formula (1) therefore gives n_min=6, +with sectors (0,2,2,2), rank P=rank Q=4 and Schur-commutator rank 4. +The same matrices reduced modulo three still give these ranks. These +examples lie outside the scalar-block predecessors. The verifier constructs +their complete matrices and checks their literal Schur products exactly. + +## 6. Boundary of the conclusion + +The theorem assumes both pivots invertible and P,Q commuting idempotents. +It concerns one common deletion over a field. It does not classify arbitrary +nonidempotent commuting inputs, singular-pivot generalized complements, +coefficient rings, nonmaximal commutator ranks or complete-header frequencies. +The attaining algebraic representation does not construct or price a physical +header producer/consumer, arbitrary dirty-owner restoration, precision, stock, +fixed tapes, recursive compilation or outer transfer. No new kappa follows. diff --git a/research/schur-rank-attainment/reference6031.md b/research/schur-rank-attainment/reference6031.md new file mode 100644 index 0000000000..234a86b25f --- /dev/null +++ b/research/schur-rank-attainment/reference6031.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. diff --git a/research/schur-rank-attainment/reference6031.py b/research/schur-rank-attainment/reference6031.py new file mode 100644 index 0000000000..58a2bb02d2 --- /dev/null +++ b/research/schur-rank-attainment/reference6031.py @@ -0,0 +1,365 @@ +#!/usr/bin/env python3 +"""Exact nonmaximal Schur-commutator rank profiles for d=2 over F2. + +Nick Petalas. Apache-2.0. Standard library only. + +For every A,B in GL_2(F2) and H in M_2(F2) this script +1. enumerates every sector choice I_j >= im T_j, N_j <= ker T_j and records + the least ambient dimension for each Schur-commutator rank; +2. checks the closed law n_min(rho)=max(n0+rho-rho0, nmax-2(2d-rho)) on the + feasible interval [rho0, 2d], and the rank identities rank R=2d-a, + rank L=2d-b on every enumerated choice; +3. builds a literal commuting idempotent pair for every (triple, rank) at the + claimed least dimension and recomputes its Schur commutator from scratch. +Seeded controls must be rejected. Exit status 0 means every check passed. +""" +from __future__ import annotations + +import hashlib +import itertools +import json +import sys + +D = 2 +SECTORS = ("10", "01", "11") + + +# ---- dense F2 matrices as lists of 0/1 rows ------------------------------- + +def mul(x, y): + cols = len(y[0]) + return [[sum(x[i][k] & y[k][j] for k in range(len(y))) & 1 + for j in range(cols)] for i in range(len(x))] + + +def add(x, y): + return [[(a ^ b) for a, b in zip(r, s)] for r, s in zip(x, y)] + + +def eye(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def zeros(r, c): + return [[0] * c for _ in range(r)] + + +def rows_to_masks(x): + return [sum(bit << j for j, bit in enumerate(row)) for row in x] + + +def mask_rank(masks): + basis = [] + for v in masks: + for b in basis: + v = min(v, v ^ b) + if v: + basis.append(v) + return len(basis) + + +def rank(x): + return mask_rank(rows_to_masks(x)) if x and x[0] else 0 + + +def transpose(x): + return [list(c) for c in zip(*x)] + + +def inverse(x): + n = len(x) + a = [row[:] + e for row, e in zip(x, eye(n))] + for c in range(n): + piv = next((r for r in range(c, n) if a[r][c]), None) + if piv is None: + raise ValueError("singular") + a[c], a[piv] = a[piv], a[c] + for r in range(n): + if r != c and a[r][c]: + a[r] = [u ^ v for u, v in zip(a[r], a[c])] + return [row[n:] for row in a] + + +def block(rows): + out = [] + for brow in rows: + for i in range(len(brow[0])): + out.append(sum((b[i] for b in brow), [])) + return out + + +def sub_block(x, r0, r1, c0, c1): + return [row[c0:c1] for row in x[r0:r1]] + + +# ---- subspaces of F2^2 as frozensets of vector tuples ----------------------- + +VECS = [tuple(v) for v in itertools.product((0, 1), repeat=D)] + + +def span(vs): + out = {tuple([0] * D)} + for v in vs: + out |= {tuple(a ^ b for a, b in zip(s, v)) for s in out} + return frozenset(out) + + +SUBSPACES = sorted({span(c) for k in range(D + 1) + for c in itertools.combinations(VECS, k)}, + key=lambda s: (len(s), sorted(s))) + + +def dim(s): + return len(s).bit_length() - 1 + + +def basis(s, start=()): + """Basis of s extending the independent list start (vectors in s).""" + out = list(start) + for v in sorted(s): + if span(out) != span(out + [v]): + out.append(v) + return out[len(start):] + + +def image(t): + return span([tuple(c) for c in transpose(t)]) + + +def kernel(t): + return frozenset(v for v in VECS + if all(sum(a & b for a, b in zip(row, v)) & 1 == 0 for row in t)) + + +# ---- the reduction ---------------------------------------------------------- + +def compressed(a, b, h): + i2 = eye(D) + return {"00": add(add(add(i2, a), b), h), "10": add(a, h), + "01": add(b, h), "11": h} + + +def factor_maps(a, b, h): + """G: U^2 -> U^3 and G': U^3 -> U^2 with L=Y G and R=G' X (PROOF.md).""" + ai, bi = inverse(a), inverse(b) + z = zeros(D, D) + bih, hbi = mul(bi, h), mul(h, bi) + g = block([[z, ai], [bih, bi], [add(eye(D), bih), add(ai, bi)]]) + gp = block([[ai, bi, add(ai, bi)], [z, hbi, add(hbi, eye(D))]]) + return g, gp + + +def embed(j, v): + out = [0] * (3 * D) + out[D * j:D * j + D] = v + return out + + +def profile(a, b, h, check_identities=True): + t = compressed(a, b, h) + g, gp = factor_maps(a, b, h) + m = mul(g, gp) + im = {s: image(t[s]) for s in SECTORS} + ker = {s: kernel(t[s]) for s in SECTORS} + ich = [[s for s in SUBSPACES if im[j] <= s] for j in SECTORS] + nch = [[s for s in SUBSPACES if s <= ker[j]] for j in SECTORS] + gt = transpose(g) + best = {} + witness = {} + for ichoice in itertools.product(*ich): + cols = [embed(k, list(v)) for k, s in enumerate(ichoice) for v in basis(s)] + mi = rows_to_masks([[sum(row[q] & c[q] for q in range(3 * D)) & 1 + for row in m] for c in cols]) + a_def = sum(D - dim(s) for s in ichoice) + rank_r = mask_rank(rows_to_masks([[sum(row[q] & c[q] for q in range(3 * D)) & 1 + for row in gp] for c in cols])) + for nchoice in itertools.product(*nch): + nb = rows_to_masks([embed(k, list(v)) for k, s in enumerate(nchoice) + for v in basis(s)]) + f = mask_rank(mi + nb) - len(nb) + b_def = len(nb) + if check_identities: + # rank L = 2d - b: rank of U^2 -> U^3/N, i.e. rank[G | N] - dim N. + rank_l = mask_rank(rows_to_masks(gt) + nb) - len(nb) + if rank_r != 2 * D - a_def or rank_l != 2 * D - b_def: + raise AssertionError("rank R/L identity fails") + if not (2 * D - a_def - b_def <= f <= 2 * D - max(a_def, b_def)): + raise AssertionError("Sylvester sandwich fails") + cost = sum(dim(s) for s in ichoice) - b_def + if cost < best.get(f, 10 ** 9): + best[f] = cost + witness[f] = (ichoice, nchoice) + base = rank(t["00"]) + sum(D - rank(t[j]) for j in SECTORS) + nmin = {f: base + c for f, c in best.items()} + tt = block([[t[s] if s == r else zeros(D, D) for s in SECTORS] for r in SECTORS]) + rho0 = rank(mul(mul(tt, m), tt)) + return t, nmin, witness, rho0 + + +def law(t, rho0): + n0 = rank(t["00"]) + sum(rank(t[j]) for j in SECTORS) + nmax = 3 * D + rank(t["00"]) + sum(D - rank(t[j]) for j in SECTORS) + return {r: max(n0 + r - rho0, nmax - 2 * (2 * D - r)) + for r in range(rho0, 2 * D + 1)}, n0, nmax + + +# ---- literal witness --------------------------------------------------------- + +def sector_factors(tj, ij, nj): + """X (d x r), Y (r x d) with XY=tj, im X=ij, ker Y=nj, r minimal.""" + imt = image(tj) + sigma = basis(imt) + phi_cols = [] + for col in transpose(tj): # coordinates of each column in basis sigma + for coeffs in itertools.product((0, 1), repeat=len(sigma)): + vec = tuple(sum(c & s[q] for c, s in zip(coeffs, sigma)) & 1 for q in range(D)) + if vec == tuple(col): + phi_cols.append(list(coeffs)) + break + phi = transpose(phi_cols) if sigma else [] + nbas = basis(nj) + kbas = basis(kernel(tj), nbas) + wbas = basis(frozenset(VECS), nbas + kbas) + full = nbas + kbas + wbas # basis of U; psi reads the kbas coordinates + coords = inverse(transpose([list(v) for v in full])) + psi = [coords[len(nbas) + q] for q in range(len(kbas))] + tau = basis(ij, sigma) + y = [row[:] for row in phi] + psi + [[0] * D for _ in tau] + x_cols = [list(s) for s in sigma] + [[0] * D for _ in psi] + [list(v) for v in tau] + x = transpose(x_cols) if x_cols else [[] for _ in range(D)] + return x, y + + +def build_pair(a, b, h, ichoice, nchoice): + t = compressed(a, b, h) + sel = {"00": (image(t["00"]), kernel(t["00"]))} + for k, j in enumerate(SECTORS): + sel[j] = (ichoice[k], nchoice[k]) + xs, ys, p0d, q0d = [], [], [], [] + for j in ("00",) + SECTORS: + x, y = sector_factors(t[j], *sel[j]) + xs.append(x) + ys += y + p0d += [int(j[0] == "1")] * len(y) + q0d += [int(j[1] == "1")] * len(y) + n = len(ys) + pi = [sum((x[r] for x in xs), []) for r in range(D)] + inc = ys + if mul(pi, inc) != eye(D): + raise AssertionError("pi i != I") + # basis of ker pi + kerpi = [] + for v in itertools.product((0, 1), repeat=n): + if len(kerpi) == n - D: + break + if any(sum(pi[r][q] & v[q] for q in range(n)) & 1 for r in range(D)): + continue + if mask_rank(rows_to_masks(kerpi + [list(v)])) == len(kerpi) + 1: + kerpi.append(list(v)) + mm = transpose(transpose(inc) + kerpi) + mi = inverse(mm) + p0 = [[int(i == j) * p0d[i] for j in range(n)] for i in range(n)] + q0 = [[int(i == j) * q0d[i] for j in range(n)] for i in range(n)] + return mul(mul(mi, p0), mm), mul(mul(mi, q0), mm) + + +def literal_rank(a, b, h, p, q): + n = len(p) + if mul(p, p) != p or mul(q, q) != q or mul(p, q) != mul(q, p): + raise AssertionError("not commuting idempotents") + if sub_block(p, 0, D, 0, D) != a or sub_block(q, 0, D, 0, D) != b \ + or sub_block(mul(p, q), 0, D, 0, D) != h: + raise AssertionError("prescribed blocks fail") + if n == D: + return 0 + ai, bi = inverse(a), inverse(b) + s = add(sub_block(p, D, n, D, n), + mul(mul(sub_block(p, D, n, 0, D), ai), sub_block(p, 0, D, D, n))) + z = add(sub_block(q, D, n, D, n), + mul(mul(sub_block(q, D, n, 0, D), bi), sub_block(q, 0, D, D, n))) + return rank(add(mul(s, z), mul(z, s))) + + +# ---- driver ------------------------------------------------------------------- + +def triples(): + mats = [[[w, x], [y, z]] for w, x, y, z in itertools.product((0, 1), repeat=4)] + gl = [m for m in mats if (m[0][0] & m[1][1]) ^ (m[0][1] & m[1][0])] + return [(a, b, h) for a in gl for b in gl for h in mats] + + +def run(): + rows = [] + witnesses = 0 + for a, b, h in triples(): + t, nmin, wit, rho0 = profile(a, b, h) + predicted, n0, nmax = law(t, rho0) + if nmin != predicted: + raise AssertionError(f"law fails at {a},{b},{h}: {nmin} vs {predicted}") + for r, (ich, nch) in wit.items(): + p, q = build_pair(a, b, h, ich, nch) + if len(p) != nmin[r] or literal_rank(a, b, h, p, q) != r: + raise AssertionError("literal witness fails") + witnesses += 1 + rows.append({"A": a, "B": b, "H": h, "noncommuting": mul(a, b) != mul(b, a), + "n0": n0, "rho0": rho0, "nmax": nmax, + "n_min": [nmin[r] for r in range(rho0, 2 * D + 1)]}) + return rows, witnesses + + +def controls(): + """Each seeded mutation must be rejected by the same checks.""" + a, b, h = eye(D), eye(D), eye(D) # A=B=H=I: slope-two profile 2,4,6,8,10 + t, nmin, wit, rho0 = profile(a, b, h) + predicted, _, _ = law(t, rho0) + rejected = 0 + # 1. slope-one-only law (drop the 2(2d-rho) branch) + n0 = rank(t["00"]) + sum(rank(t[j]) for j in SECTORS) + rejected += {r: n0 + r - rho0 for r in predicted} != nmin + # 2. #5128 formula alone for every rank + rejected += any(nmin[r] != predicted[2 * D] for r in nmin) is True + # 3. corrupted witness: flip one entry of P + ich, nch = wit[2] + p, q = build_pair(a, b, h, ich, nch) + p[-1][-1] ^= 1 + try: + literal_rank(a, b, h, p, q) + except AssertionError: + rejected += 1 + # 4. wrong prescribed H + p, q = build_pair(a, b, h, ich, nch) + try: + literal_rank(a, b, zeros(D, D), p, q) + except AssertionError: + rejected += 1 + return rejected + + +def main(): + rows, witnesses = run() + rejected = controls() + profiles = {} + for r in rows: + key = (r["rho0"], tuple(r["n_min"])) + profiles[key] = profiles.get(key, 0) + 1 + summary = { + "triples": len(rows), + "noncommuting_triples": sum(r["noncommuting"] for r in rows), + "literal_witnesses": witnesses, + "distinct_profiles": len(profiles), + "rho0_counts": {str(k): sum(1 for r in rows if r["rho0"] == k) for k in range(5)}, + "controls_rejected": rejected, + "rows_sha256": hashlib.sha256(json.dumps(rows, sort_keys=True).encode()).hexdigest(), + } + expected = {"triples": 576, "noncommuting_triples": 288, "controls_rejected": 4} + ok = all(summary[k] == v for k, v in expected.items()) + print(json.dumps(summary, indent=1, sort_keys=True)) + if not ok: + print("FAIL", file=sys.stderr) + return 1 + print("PASS_SCHUR_INTERMEDIATE_RANKS_D2_F2") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/research/schur-rank-attainment/reference6053.md b/research/schur-rank-attainment/reference6053.md new file mode 100644 index 0000000000..698b34aba7 --- /dev/null +++ b/research/schur-rank-attainment/reference6053.md @@ -0,0 +1,317 @@ +# Exact intermediate Schur ranks over every field + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. + +This resolves both open next questions in Nick Petalas's +[PR #6031](https://github.com/CrocSwap/integer-mult-bounds/pull/6031), +`research/schur-intermediate-ranks`, scientific head +`acc000f4edfa0b0c4a90b505c6e02a4c3572f74c`. We use its sector-subspace reduction +and minimum realization cost, and Krzysztof Wojt's +[PR #5128](https://github.com/CrocSwap/integer-mult-bounds/pull/5128), +`research/arbitrary-pivot-schur-minimum`, scientific head +`2839d35e58b3285a1992a3ecbae2809ebef7661b`, for the Schur factorization and +commuting-idempotent realization. Those predecessor reductions are cited, +not claimed as new or independently re-proved here. The added argument is a +sector-preserving decomposition into two bilinear pairings. Reducing a +bilinear pairing to a rank core and its radicals is classical linear algebra; +no historical priority is claimed for that operation. + +## 1. Statement and setting + +Let K be any field, let d >= 1, and fix A,B in GL_d(K) and H in M_d(K). +No commutation among A,B,H is assumed. Define + +``` +F = A-H, J = B-H, T00 = I-A-B+H, +s = nullity F + nullity J + nullity H, +n0 = rank T00 + rank F + rank J + rank H, +nmax = 3d + rank T00 + s. +``` + +Here `nmax` denotes the least dimension attaining the maximum commutator +rank 2d, as in #5128; it is not an upper bound on the ambient dimension. +Consider all commuting idempotents P,Q in M_n(K) satisfying + +``` +P11 = A, Q11 = B, (PQ)11 = H, +``` + +where the leading block has size d. Their Schur complements are + +``` +S = P22 - P21 A^-1 P12, Z = Q22 - Q21 B^-1 Q12. +``` + +Put rho = rank(SZ-ZS), and let n_min(rho) be the least ambient dimension +for that rank with the prescribed A,B,H. + +**Theorem.** The minimum possible rank is + +``` +rho0 = rank(J A^-1 F) + rank(F B^-1 J) + 2 rank H - 2d. (1) +``` + +For every integer rho with rho0 <= rho <= 2d, + +``` +n_min(rho) = max(n0 + rho - rho0, nmax - 2(2d-rho)). (2) +``` + +There are no other possible ranks. A rank rho in this interval is feasible +at dimension n exactly when n >= n_min(rho). Thus the theorem also decides +the complete rank set at every ambient dimension. Both formulas hold in +arbitrary characteristic and over finite or infinite fields. + +## 2. Cited reduction and the deficiency pairing + +Write U = K^d and E = U direct-sum U. In the 10,01,11 sectors put +`T10=F`, `T01=J`, `T11=H`. The reduction in #6031, Sections 1--3, permits +arbitrary sectorwise subspaces + +``` +im Tj <= Ij <= U, Nj <= ker Tj. (3) +``` + +They are realized by maps Xj,Yj with XjYj=Tj, im Xj=Ij and ker Yj=Nj. +Their least sector dimension is +`dim Ij + d - dim Nj - rank Tj`; the 00 sector can have dimension +rank T00. In particular, with + +``` +a = sum_j (d - dim Ij), b = sum_j dim Nj, +``` + +the least ambient dimension realizing these choices is + +``` +n = nmax - a - b. (4) +``` + +The same predecessor supplies the maps + +``` +G(x,y) = (A^-1 y, -B^-1(Hx+y), (I-B^-1 H)x + (A^-1-B^-1)y), +G'(u,v,w) = (A^-1 u - B^-1 v + (A^-1-B^-1)w, + H B^-1 v + (H B^-1-I)w). +``` + +Here G:E -> U^3 is injective and G':U^3 -> E is surjective. If +`I = I10 direct-sum I01 direct-sum I11` and similarly N, the Schur +commutator rank equals the rank of `L R`, with `L=Y G`, `R=G' X`. +Let + +``` +C = G'I <= E, D' = annihilator(C) <= E*, +K' = G^-1 N <= E. +``` + +The deficiency identities in #6031 give dim D'=a and dim K'=b. Restrict +the natural bilinear evaluation pairing `E* x E -> K` to D' x K', +and call its rank q. Its right kernel is K' intersect C. Therefore + +``` +rho = dim C - dim(C intersect K') + = 2d - a - b + q. (5) +``` + +All annihilators here are algebraic dual annihilators, not Hermitian +orthogonal complements. + +For the largest possible deficiencies, take Ij=im Tj and Nj=ker Tj. +Their spaces D,K have the following direct-sum decompositions; w is a +row covector and z is a column vector: + +``` +D10 = {(wA,w) : wF=0}, K10 = {(-z,Az) : Fz=0}, +D01 = {(0,w) : wJ=0}, K01 = {(z,0) : Jz=0}, +D11 = {(0,-w) : wH=0}, K11 = {(z,0) : Hz=0}, +D = D10 + D01 + D11, K = K10 + K01 + K11. (6) +``` + +These are precisely the pure-sector lifts in #6031's deficiency proof. +For example G(-z,Az)=(z,0,0) when Fz=0, whereas G(z,0)=(0,-z,0) +when Jz=0 and G(z,0)=(0,0,z) when Hz=0. The minus sign in the 01 lift +does not change its subspace. The covector lifts follow by composing +with G'. Injectivity of G and of the dual map of G' proves that the +sums in (6) are direct. Each of D and K has dimension s. + +More generally D' is an arbitrary direct sum of subspaces of the three +Dj, and K' an arbitrary direct sum of subspaces of the three Kj. +Indeed, a choice of covectors Wj <= left ker Tj corresponds exactly +to Ij=annihilator(Wj), and a subspace of Kj corresponds exactly to Nj. +Thus every sectorwise subspace choice made below is allowed by (3), +not merely a choice in the unrestricted spaces E or E*. + +## 3. Only two pairing blocks survive + +Compute the evaluation pairing of (6). The entry in each cell is the +value on the corresponding w,z, with their row and column constraints: + +| | K10 | K01 | K11 | +|---|---|---|---| +| D10 | 0 | w H z | 0 | +| D01 | w H z | 0 | 0 | +| D11 | 0 | 0 | 0 | + +For example the D10,K10 entry is `-wAz+wAz=0`. The D10,K01 entry +is wAz=wHz because wF=0; the D01,K10 entry is wAz=wHz because Fz=0. +The D10,K11 entry vanishes since wA=wH and Hz=0. The D11,K10 entry +vanishes since Az=Hz and wH=0. All remaining entries vanish directly. +These identities also hold in characteristic two. + +Let + +``` +r1 = rank of (left ker F) x (ker J) -> K, (w,z) |-> wHz, +r2 = rank of (left ker J) x (ker F) -> K, (w,z) |-> wHz, +r = r1 + r2. (7) +``` + +The two nonzero blocks have separate domain and codomain sectors, so +the full D x K pairing has rank r. The two ranks need not be equal. +At the largest deficiencies a=b=s, equation (5) gives + +``` +rho0 = 2d - 2s + r. (8) +``` + +Every restriction has q <= r and a,b <= s. More precisely, the +rank lower bound rho >= rho0 follows either from the unit-step +argument in #6031 or by deleting one basis direction at a time +from the full pairing: such a deletion lowers a+b by one and q by +zero or one, so (5) cannot decrease. Thus (8) is the minimum rank. +Its least dimension is `nmax-2s=n0` by (4). + +## 4. Sharp dimension for every intermediate rank + +Put delta=2d-rho. For any admissible pair D',K', equation (5) says +`delta=a+b-q`. Since q <= min(a,b,r), + +``` +a+b <= 2 delta, a+b <= delta+r. +``` + +Equation (4), or the corresponding lower bound for a nonminimal +realization of the same subspaces, therefore implies + +``` +n >= nmax - delta - min(delta,r). (9) +``` + +We now attain (9), for every integer +`0 <= delta <= 2s-r = 2d-rho0`, while respecting all three sectors. + +Reduce each of the two nonzero bilinear blocks in the table to rank +normal form by choosing bases within its row and column sectors. +Each block is a direct sum of paired one-dimensional coordinates +with evaluation matrix I, and zero left/right radical coordinates. +Because the blocks use disjoint sectors, these two basis changes +can be performed independently. There are r paired coordinates on +each side in total, and `2s-2r` unpaired radical coordinates across +the two sides, including both 11 sectors. + +* If `0 <= delta <= r`, choose any delta of the paired coordinates, + retaining each on both sides. This gives a=b=delta and q=delta. + Hence the resulting rank is `2d-delta`, with cost `nmax-2delta`. +* If `r <= delta <= 2s-r`, retain all r paired coordinates on both + sides and add any `delta-r` radical coordinates. There are enough + because `delta-r <= 2s-2r`. Then a+b=delta+r and q=r, giving rank + `2d-delta` with cost `nmax-delta-r`. + +The normal forms and all the selections are within individual sectors. +Section 2 therefore realizes them by actual commuting idempotents +with the prescribed three leading blocks. No field-size condition +or generic choice of a vector is needed. + +Consequently equality holds in (9). Since + +``` +n0 = nmax-2s, rho0 = 2d-2s+r, +n0+rho-rho0 = nmax-delta-r, +``` + +this equality is exactly (2). It also establishes every integer rank +in the stated interval; the factorization through E excludes ranks +above 2d. Padding the 00 sector with any number of coordinates on +which both X00 and Y00 are zero preserves A,B,H and the commutator +rank. It attains every larger ambient dimension. This proves the +claimed feasibility statement for each n, including zero-size Schur +complements when n=d. + +## 5. Eliminating nullspace bases from rho0 + +For arbitrary square F,J,H of size d, the rank of the pairing +`(left ker F) x (ker J) -> K`, `(w,z) |-> wHz`, is + +``` +r1 = rank [[F,H],[0,J]] - rank F - rank J. (10) +``` + +One way to see (10) is to project the image of the block matrix to +its bottom component. That projection has image im J; its kernel +inside the block-matrix image is the top-component subspace +`im F + H ker J`. Subtracting rank F leaves the rank of the induced +map `ker J -> U/im F`, which is also the rank of the displayed +pairing against left ker F. + +In our setting F+H=A is invertible. Adding the second block column +to the first changes the block matrix to `[[A,H],[J,J]]`. Eliminating +the bottom-left block gives the Schur complement + +``` +J - J A^-1 H = J A^-1 F. +``` + +Therefore + +``` +r1 = d + rank(J A^-1 F) - rank F - rank J, +r2 = d + rank(F B^-1 J) - rank F - rank J. (11) +``` + +The second identity uses J+H=B and the swapped pairing. Substitute +(11) and `s=3d-rank F-rank J-rank H` into (8) to obtain (1). +The order of factors is essential; A,B,H need not commute. + +## 6. An odd minimum-rank fixture over F3 + +Take d=2 over F3 and + +``` +H = [[1,0],[0,1]], +A = [[1,0],[0,2]], B = [[1,1],[0,1]], +F = [[0,0],[0,1]], J = [[0,1],[0,0]], +T00 = [[0,2],[0,2]]. +``` + +Then s=2, n0=5 and nmax=9. In this field + +``` +J A^-1 F = [[0,2],[0,0]], F B^-1 J = [[0,0],[0,0]], +r1=1, r2=0, rho0=1. +``` + +Formula (2) gives the exact minimum dimensions + +| rho | 1 | 2 | 3 | 4 | +|---|---|---|---|---| +| n_min(rho) | 5 | 6 | 7 | 9 | + +In particular, neither equality of the two pairing ranks nor evenness +of rho0 can be imported from the binary d=2 census in #6031. +That census remains valid; this fixture is over a different field. + +## 7. Scope and verification boundary + +This is a written algebraic proof for one common deletion with invertible +pivots. The independent finite checks accompanying the package corroborate +its identities and constructions; they do not prove its universal +quantifiers or constitute proof-kernel verification. The theorem depends +on the cited predecessor factorization and sector realization. + +It supplies no physical header producer or consumer, header count, +dirty-owner restoration protocol, precision bound, stock estimate, +recursive compilation or outer transfer. Those costs are unpriced here, +not zero. It changes neither the selected multiplication construction nor +kappa, and it makes no claim that archival publication is scientific +acceptance of the theorem. diff --git a/research/schur-rank-attainment/ternary_orbits.py b/research/schur-rank-attainment/ternary_orbits.py new file mode 100644 index 0000000000..56c4c3fd10 --- /dev/null +++ b/research/schur-rank-attainment/ternary_orbits.py @@ -0,0 +1,71 @@ +"""Complete simultaneous-conjugacy partition of 2x2 ternary triples. +SHIN09-git, substantial OpenAI Codex assistance. Apache-2.0. +Independent of the Schur constructor; arithmetic is the subspace oracle. +""" +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +from types import ModuleType + +path=Path(__file__).with_name("oracle.py") +o=ModuleType("orbit_oracle") +o.__file__=str(path) +exec(compile(path.read_bytes(),str(path),"exec"),o.__dict__) + +def partition(): + matrices=[tuple(tuple(v[i*2:(i+1)*2]) for i in range(2)) + for v in product(range(3),repeat=4)] + index={a:i for i,a in enumerate(matrices)} + gl=[i for i,a in enumerate(matrices) if o.rank_vectors(a,3)==2] + if len(gl)!=48: + raise ValueError("GL2 F3 census") + actions=[] + for g in gl: + inverse=o.inverse(matrices[g],3) + row=[index[o.mm(o.mm(matrices[g],a,3),inverse,3)] for a in matrices] + if sorted(row)!=list(range(81)) or {row[x] for x in gl}!=set(gl): + raise ValueError("conjugation not a permutation") + actions.append(row) + # Independently verify composition of the full finite action table. + position={g:i for i,g in enumerate(gl)} + for gi,g in enumerate(gl): + for hi,h in enumerate(gl): + gh=index[o.mm(matrices[g],matrices[h],3)] + if actions[position[gh]]!=[actions[gi][actions[hi][m]] for m in range(81)]: + raise ValueError("conjugation action composition") + def encode(a,b,h): + return (a*81+b)*81+h + seen=set() + representatives=[] + digest=sha256() + sizes={} + for a in gl: + for b in gl: + for h in range(81): + key=encode(a,b,h) + if key in seen: + continue + orbit=sorted({encode(row[a],row[b],row[h]) for row in actions}) + if key!=min(orbit) or seen.intersection(orbit): + raise ValueError("orbit partition overlap or ordering") + seen.update(orbit) + representatives.append((a,b,h)) + sizes[str(len(orbit))]=sizes.get(str(len(orbit)),0)+1 + digest.update(json.dumps(orbit,separators=(",",":")).encode()+b"\n") + expected={encode(a,b,h) for a in gl for b in gl for h in range(81)} + fixed_sum=sum(sum(row[a]==a for a in gl)**2 * sum(row[m]==m for m in range(81)) + for row in actions) + if fixed_sum%48 or seen!=expected or len(representatives)!=fixed_sum//48: + raise ValueError("complete ternary triple coverage") + metadata={"raw_triples":len(expected),"orbit_representatives":len(representatives), + "invertible_pivots":len(gl),"group_elements":len(actions), + "distinct_actions":len({tuple(a) for a in actions}), + "burnside_orbit_count":fixed_sum//48, + "orbit_size_histogram":sizes,"orbit_partition_sha256":digest.hexdigest(), + "coverage":"All A,B in GL_2(F3), all H in M_2(F3), by exact simultaneous conjugacy"} + return [(matrices[a],matrices[b],matrices[h]) for a,b,h in representatives],metadata + +if __name__=="__main__": + _,metadata=partition() + print(json.dumps(metadata,indent=2,sort_keys=True)) diff --git a/research/schur-rank-attainment/test_mutations.py b/research/schur-rank-attainment/test_mutations.py new file mode 100644 index 0000000000..b314256559 --- /dev/null +++ b/research/schur-rank-attainment/test_mutations.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +"""Real source mutants; receipt comparison deliberately bypassed. +SHIN09-git, substantial OpenAI Codex assistance. Apache-2.0. +""" +from hashlib import sha256 +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import time + +HERE=Path(__file__).resolve().parent + +MUTANTS=( + ("reorder_closed_formula_inverse","verify.py", + "(J@A.inverse()@F).rank()","(A.inverse()@J@F).rank()","PR6053 ordered closed rho0"), + ("omit_H_rank_closed_formula","verify.py", + "+2*H.rank()-2*A.r","+0*H.rank()-2*A.r","PR6053 ordered closed rho0"), + ("omit_efficient_row_phase","construct.py", + "if i not in core_i:","if False and i not in core_i:","maximal rank minor"), + ("use_principal_minors_only","construct.py", + "if C.take(ni,nj).rank()==size-1:","if i == j and C.take(ni,nj).rank()==size-1:","nonzero cofactor exists"), + ("reverse_H_Binverse_order","construct.py", + "Gp=block([[ai,-bi,ai-bi],[O,H@bi,H@bi-eye(d,p)]])", + "Gp=block([[ai,-bi,ai-bi],[O,bi@H,bi@H-eye(d,p)]])","left lift identity"), + ("lose_odd_characteristic_sign","construct.py", + "tuple(-x for x in z)+(0,)*d if j==1", + "tuple(z)+(0,)*d if j==1","right lift identity"), + ("mix_sector_annihilators","construct.py", + "if emeta[i][0]==j]","if emeta[i][0]!=j]","sector factor"), + ("wrong_slope_two_bound","construct.py", + "nmax-2*(2*d-rho)","nmax-(2*d-rho)","sharp dimension law"), + ("omit_independent_rank_check","check_witnesses.py", + 'require(actual==rho,"literal Schur commutator rank")', + 'require(True,"literal Schur commutator rank")',"independent checker accepted wrong_rank"), +) + +def run(): + results=[] + with tempfile.TemporaryDirectory(prefix="schur-rank-mutants-") as tmp: + root=Path(tmp) + pristine=root/"positive" + pristine.mkdir() + for src in HERE.iterdir(): + if src.is_file(): + shutil.copyfile(src,pristine/src.name) + command=[sys.executable,"-I","-O","-B","verify.py","--quick","--emit-receipt"] + t=time.perf_counter() + positive=subprocess.run(command,cwd=pristine,capture_output=True,text=True,encoding="utf-8",timeout=90) + if positive.returncode: + raise ValueError("optimized source-only positive control failed: "+positive.stderr) + payload=json.loads(positive.stdout) + if payload["unique_triples"]!=219 or payload["literal_witnesses"]!=1093: + raise ValueError("positive coverage changed") + results.append({"name":"optimized_positive","status":"PASS","seconds":time.perf_counter()-t}) + for name,filename,old,new,message in MUTANTS: + dest=root/name + shutil.copytree(pristine,dest) + target=dest/filename + source=target.read_text(encoding="utf-8") + if source.count(old)!=1: + raise ValueError("mutant target must match exactly once: "+name) + mutated=source.replace(old,new,1) + compile(mutated,str(target),"exec") + target.write_text(mutated,encoding="utf-8",newline="\n") + t=time.perf_counter() + run=subprocess.run(command,cwd=dest,capture_output=True,text=True,encoding="utf-8",timeout=90) + if run.returncode==0 or message not in run.stderr or "SyntaxError" in run.stderr: + raise ValueError("mutant not rejected by intended scientific check "+name+"\n"+run.stderr[-1800:]) + results.append({"name":name,"status":"REJECTED","seconds":time.perf_counter()-t, + "expected_check":message,"stderr_sha256":sha256(run.stderr.encode()).hexdigest(), + "last_error":run.stderr.strip().splitlines()[-1]}) + return {"mode":"optimized fresh source-only subprocesses; exact receipt comparison disabled", + "positive_controls":1,"code_mutants_rejected":len(MUTANTS),"results":results} + +if __name__=="__main__": + print(json.dumps(run(),indent=2)) diff --git a/research/schur-rank-attainment/verify.py b/research/schur-rank-attainment/verify.py new file mode 100644 index 0000000000..52046e50ce --- /dev/null +++ b/research/schur-rank-attainment/verify.py @@ -0,0 +1,245 @@ +#!/usr/bin/env python3 +"""Bounded exact corroboration and literal checks for PROOF.md. +SHIN09-git, substantial OpenAI Codex assistance. Apache-2.0. +Finite checks corroborate; the all-field assertion is the written proof. +""" +import argparse +from copy import deepcopy +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations, product +import json +from pathlib import Path +import sys +import time +from types import ModuleType + +HERE=Path(__file__).resolve().parent +BOUND_FILES=("linear.py","construct.py","oracle.py","check_witnesses.py","verify.py", + "PROOF.md","README.md","TASK.json","SOURCES.json","VERIFY.json", + "OVERLAP.json","reference6031.py","reference6031.md","reference5128.md","LICENSE", + "ternary_orbits.py","test_mutations.py","reference6053.md","AUDIT.md") + +def load(name): + path=HERE/(name+".py") + mod=ModuleType(name) + mod.__file__=str(path) + exec(compile(path.read_bytes(),str(path),"exec"),mod.__dict__) + return mod + +c=load("construct") +o=load("oracle") +ind=load("check_witnesses") +ref=load("reference6031") +need=c.need + +def canonical(x): + return json.dumps(x,sort_keys=True,separators=(",",":"),ensure_ascii=True).encode() + +def reviewed_closed_rank(A,B,H): + # apoursh PR6053, equation (1), independently evaluated here. + F,J=A-H,B-H + return (J@A.inverse()@F).rank()+(F@B.inverse()@J).rank()+2*H.rank()-2*A.r + +def all_matrices(d,p): + for flat in product(range(p),repeat=d*d): + yield tuple(tuple(flat[i*d:(i+1)*d]) for i in range(d)) + +def domains(quick=False,ternary_representatives=None): + m2=list(all_matrices(2,2)) + gl2=[a for a in m2 if o.rank_vectors(a,2)==2] + binary=list(product(gl2,gl2,m2)) + for A,B,H in (binary[::71] if quick else binary): + yield "binary_quick" if quick else "binary_complete",2,A,B,H,True + m3=list(all_matrices(2,3)) + gl3=[a for a in m3 if o.rank_vectors(a,3)==2] + pairs=[(a,b) for a in gl3 for b in gl3 if o.mm(a,b,3)!=o.mm(b,a,3)] + pairs=[pairs[i*len(pairs)//8] for i in range(8)] + if quick: + for A,B in pairs: + for H in m3[::20]: + yield "ternary_eight_pairs",3,A,B,H,True + else: + need(ternary_representatives is not None,"complete ternary partition required") + for A,B,H in ternary_representatives: + yield "ternary_complete_up_to_conjugacy",3,A,B,H,True + A=((0,1,0),(0,0,1),(1,0,0)) + B=((1,1,0),(0,1,1),(0,0,1)) + m32=list(all_matrices(3,2)) + for H in (m32[::127] if quick else m32): + yield "binary_d3_all_H",2,A,B,H,True + for p in (0,2,3,5,7,11): + for d in range(1,5): + A=[list(row) for row in c.eye(d,p).a] + B=[list(row) for row in c.eye(d,p).a] + if d>1: + A[0][1]=Fraction(1,2) if not p else 1 + B[1][0]=Fraction(1,3) if not p else 1 + A,B=c.Mat(A,p),c.Mat(B,p) + candidates=[c.zeros(d,d,p),c.eye(d,p),A,B,A+B-c.eye(d,p),A@B,B@A, + c.Mat([[i+2 if i==j else 0 for j in range(d)] for i in range(d)],p)] + if p==0: + candidates.append(c.Mat([[Fraction(i+1,i+2) if i==j else 0 for j in range(d)] for i in range(d)],0)) + for H in {H.a:H for H in candidates}.values(): + yield "structured_Q_and_prime_fields",p,A.a,B.a,H.a,False + +def fixture(A,B,H,rho,state): + P,Q=c.build(A,B,H,state) + need(c.literal_rank(A,B,H,P,Q)==rho,"primary literal rank") + rec={"field":A.p,"d":A.r,"n":P.r,"rho":rho, + "A":A.json(),"B":B.json(),"H":H.json(),"P":P.json(),"Q":Q.json()} + ind.check(rec) + return rec + +def core_minor_census(quick=False): + total=0 + digest=sha256() + for p,d in ((2,2),(3,2),(2,3)): + matrices=list(all_matrices(d,p)) + if quick: + matrices=matrices[::max(1,len(matrices)//8)] + subsets=[s for n in range(d+1) for s in combinations(range(d),n)] + for raw in matrices: + C=c.Mat(raw,p) + r=o.rank_vectors(raw,p) + best={} + for ii in subsets: + for jj in subsets: + entries=tuple(tuple(raw[i][j] for j in jj) for i in ii) + rr=o.rank_vectors(entries,p) + rho=2*d-len(ii)-len(jj)+rr + cost=2*d-len(ii)-len(jj) + best[rho]=min(best.get(rho,10**9),cost) + actual={} + for ii,jj,kind in c.minor_chain(C): + rr=o.rank_vectors(tuple(tuple(raw[i][j] for j in jj) for i in ii),p) + rho=2*d-len(ii)-len(jj)+rr + actual[rho]=2*d-len(ii)-len(jj) + need(actual==best,"minor-chain vs complete independent subset census") + need(actual=={rho:max(rho-r,2*rho-2*d) for rho in range(r,2*d+1)},"pure minor cost law") + digest.update(canonical([p,raw,sorted(actual.items())])+b"\n") + total+=1 + return {"matrices":total,"sha256":digest.hexdigest()} + +def controls(examples): + rejected=[] + def rejects(name,rec): + try: + ind.check(rec) + except (ValueError,ZeroDivisionError): + rejected.append(name) + else: + raise ValueError("independent checker accepted "+name) + ordinary=next(x for x in examples if x["field"]==3 and x["rho"]>0) + bad=deepcopy(ordinary); bad["rho"]-=1; rejects("wrong_rank",bad) + bad=deepcopy(ordinary); bad["n"]+=1; rejects("wrong_dimension",bad) + bad=deepcopy(ordinary); bad["H"][0][0]=(bad["H"][0][0]+1)%3; rejects("wrong_product_block",bad) + bad=deepcopy(ordinary); bad["P"][0][0]=(bad["P"][0][0]+1)%3; rejects("changed_P_entry",bad) + bad=deepcopy(ordinary); bad["A"]=[[0]*bad["d"] for _ in range(bad["d"])]; rejects("singular_pivot",bad) + bad=deepcopy(ordinary); bad["d"]=True; rejects("boolean_dimension",bad) + bad=deepcopy(ordinary); bad["P"][0][0]+=3; rejects("noncanonical_field_value",bad) + bad=deepcopy(ordinary); bad["field"]=4; rejects("unsupported_composite_modulus",bad) + A=c.eye(2,3) + states=c.plan(A,A,A)["states"] + need(states[1]["n"]==4 and states[1]["n"]!=3,"slope-one-only control") + rejected.append("slope_one_only_formula") + need(states[0]["n"]!=states[4]["n"],"maximal-only control") + rejected.append("maximal_dimension_at_every_rank") + return rejected + +def run(quick=False,all_fixtures=False): + start=time.perf_counter() + sources=json.loads((HERE/"SOURCES.json").read_bytes()) + for row in sources["files"]: + if "vendored_as" in row: + need(sha256((HERE/row["vendored_as"]).read_bytes()).hexdigest()==row["sha256"], + "frozen reference changed") + summaries={} + digest=sha256() + profile_digest=sha256() + examples=[] + kept=set() + all_records=[] + binary_ref_comparisons=0 + unique=set() + ternary,coverage=(None,None) if quick else load("ternary_orbits").partition() + for group,p,a,b,h,enumerate_spaces in domains(quick,ternary): + A,B,H=(c.Mat(x,p) for x in (a,b,h)) + unique.add(canonical([p,A.json(),B.json(),H.json()])) + plan=c.plan(A,B,H) + need(reviewed_closed_rank(A,B,H)==plan["rho0"],"PR6053 ordered closed rho0") + actual={rho:state["n"] for rho,state in plan["states"].items()} + if enumerate_spaces: + exact,count=o.profile(a,b,h,p) + need(actual==exact,"complete subspace oracle disagrees") + else: + count=0 + if p==2 and len(a)==2 and group.startswith("binary"): + _,original,_,r0=ref.profile(*[[list(row) for row in X] for X in (a,b,h)]) + need(actual==original and plan["rho0"]==r0,"frozen PR6031 comparison") + binary_ref_comparisons+=1 + d=A.r + G,Gp=c.ordered_maps(A,B,H) + active=plan["sectors"][1:] + T=c.block([[active[i] if i==j else c.zeros(d,d,p) for j in range(3)] for i in range(3)]) + need((T@G@Gp@T).rank()==plan["rho0"],"baseline T G G' T identity") + row=summaries.setdefault(group,{"triples":0,"literal_witnesses":0,"subspace_pairs":0, + "noncommuting_pivot_triples":0,"rho0_counts":{}, + "two_phase_triples":0}) + row["triples"]+=1 + row["subspace_pairs"]+=count + row["noncommuting_pivot_triples"]+=int(A@B!=B@A) + row["rho0_counts"][str(plan["rho0"])]=row["rho0_counts"].get(str(plan["rho0"]),0)+1 + row["two_phase_triples"]+=int(00 and not any(x["field"]==3 and x["rho"]>0 for x in examples): + examples.append(rec) + if all_fixtures: + all_records.append(rec) + minor=core_minor_census(quick) + summary={"schema_version":1,"scope":"finite corroboration of all-field proof; no kappa or supplier", + "mode":"quick" if quick else "complete declared domains", + "domains":summaries,"unique_triples":len(unique), + "binary_reference_comparisons":binary_ref_comparisons, + "PR6053_closed_formula_comparisons":sum(x["triples"] for x in summaries.values()), + "complete_ternary_coverage":coverage, + "literal_witnesses":sum(x["literal_witnesses"] for x in summaries.values()), + "subspace_pairs":sum(x["subspace_pairs"] for x in summaries.values()), + "profile_sha256":profile_digest.hexdigest(),"literal_witness_sha256":digest.hexdigest(), + "independent_minor_subset_census":minor,"controls_rejected":controls(examples), + "source_sha256":{name:sha256((HERE/name).read_bytes()).hexdigest() for name in BOUND_FILES}} + print("computed",summary["unique_triples"],"unique triples;",summary["literal_witnesses"], + "literal witnesses; seconds",round(time.perf_counter()-start,3),file=sys.stderr,flush=True) + return summary,examples,all_records + +def main(): + ap=argparse.ArgumentParser() + ap.add_argument("--quick",action="store_true") + ap.add_argument("--emit-receipt",action="store_true") + ap.add_argument("--emit-examples",action="store_true") + ap.add_argument("--emit-fixtures",action="store_true") + args=ap.parse_args() + summary,examples,fixtures=run(args.quick,args.emit_fixtures) + if args.emit_receipt: + print(json.dumps(summary,indent=2,sort_keys=True)) + elif args.emit_examples: + print(json.dumps(examples,indent=2)) + elif args.emit_fixtures: + print(json.dumps(fixtures,separators=(",",":"))) + elif args.quick: + print("PASS_SCHUR_RANK_ATTAINMENT_QUICK") + else: + expected=json.loads((HERE/"RESULT.json").read_bytes()) + need(canonical(summary)==canonical(expected),"source-bound exact receipt mismatch") + print("PASS_SCHUR_RANK_ATTAINMENT",summary["unique_triples"],summary["literal_witnesses"]) + +if __name__=="__main__": + main()