From 5f014560d6225cae17598ac479fb29d2947d8e6b Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:01:45 +0100 Subject: [PATCH] feat(research): extend fixed-H Schur minima to every field --- research/all-field-identity-schur/README.md | 228 ++++++++++++++ .../all-field-identity-schur/SOURCES.json | 24 ++ research/all-field-identity-schur/TASK.json | 169 ++++++++++ research/all-field-identity-schur/VERIFY.json | 34 ++ research/all-field-identity-schur/verify.py | 291 ++++++++++++++++++ 5 files changed, 746 insertions(+) create mode 100644 research/all-field-identity-schur/README.md create mode 100644 research/all-field-identity-schur/SOURCES.json create mode 100644 research/all-field-identity-schur/TASK.json create mode 100644 research/all-field-identity-schur/VERIFY.json create mode 100644 research/all-field-identity-schur/verify.py diff --git a/research/all-field-identity-schur/README.md b/research/all-field-identity-schur/README.md new file mode 100644 index 0000000000..c3a64475cc --- /dev/null +++ b/research/all-field-identity-schur/README.md @@ -0,0 +1,228 @@ +# Exact identity-pivot Schur dimension over every field + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof with finite corroboration. For every field K +and every prescribed H in M_d(K), d >= 1, the minimum ambient dimension for +commuting idempotents P,Q with common leading blocks I_d, leading product block +H, and Schur-commutator rank 2d is + +```text +n_min(H) = 4d + nullity(H(I-H)). +``` + +This extends ssafwann's binary fixed-H theorem in +[PR #4671](https://github.com/CrocSwap/integer-mult-bounds/pull/4671), at +`8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9`, to arbitrary characteristic. +The new part is the signed sector formulation and construction outside F2. +The binary conclusion and its six-map argument retain predecessor credit. +No predecessor result is being audited. No kappa is claimed. + +In particular, over every field with more than two elements, the unrestricted +identity-pivot minimum is **4d for every d >= 1**. The common identity-pivot +restriction matters. Ryanson Jonathan's #4609 already supplies the unrestricted +ternary scalar minimum four; the general prescribed-H and identity-pivot +statements here are stronger restrictions, not a claim to discover that value. + +## Statement + +All ranks and nullities are over K. Matrices need not be symmetric. Write + +```text +P = [[I,R],[C,D]], Q = [[I,L],[E,F]], P²=P, Q²=Q, PQ=QP, +S = D-CR, Z = F-EL, K0 = SZ-ZS. +``` + +Let U=K^d, i:U -> V=K^n be coordinate inclusion, and pi:V -> U be coordinate +projection. The prescribed matrix is H=pi PQ i. Put W=I-H, +a=nullity(H), and b=nullity(W). Then + +```text +n_min(H) = 4d+a+b, +(r00,r10,r01,r11) >= (d-b,d+b,d+b,d+a), +rank(P), rank(Q) >= 2d+a+b. +``` + +Here r_ab is the dimension of the simultaneous (a,b) eigenspace of P,Q. +Every sharp pair obeys the componentwise bounds. All equalities, including +both input-rank bounds, are simultaneously attained for every prescribed H. + +The identity nullity(HW)=a+b holds without semisimplicity. Indeed, if HWx=0, +then x=Wx+Hx with Wx in ker H and Hx in ker W. These kernels have zero +intersection because H+W=I. The reverse inclusion is immediate. + +## Signed sector criterion + +Commuting idempotents give a direct decomposition into four joint eigenspaces, +over every field, using the mutually annihilating projectors + +```text +E00=(I-P)(I-Q), E10=P(I-Q), E01=(I-P)Q, E11=PQ. +``` + +Let Y_j=E_j i:U -> V_j and X_j=pi|V_j:V_j -> U. Compression gives + +```text +X00 Y00 = -W, X10 Y10 = W, X01 Y01 = W, X11 Y11 = H. (1) +``` + +The minus sign in the 00 sector is essential outside characteristic two. +In particular, the four products sum to I. + +Nick Petalas's ordered block factorization from +[PR #4597](https://github.com/CrocSwap/integer-mult-bounds/pull/4597), at +`dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb`, specializes to + +```text +K0 = [G-EH, C-E] [R-L; -T+HL], (2) +G=(PQ)21, T=(PQ)12. +``` + +For clarity, define its ambient factors + +```text +A = [PQ i-Q i H, (P-Q)i] : U² -> V, +B = [pi(P-Q); -pi PQ+H pi Q] : V -> U². +``` + +They satisfy pi A=0 and Bi=0. Their nonzero coordinate blocks are exactly +the two factors in (2). In joint-sector coordinates they act as + +```text +A(x,y) = (0, Y10 y, -Y01(Hx+y), Y11 W x), +B(v00,v10,v01,v11) = (X10 v10-X01 v01, + H X01 v01-W X11 v11). (3) +``` + +**Criterion.** rank K0=2d exactly when Y10,Y01,Y11 are injective and +X10,X01,X11 are surjective. + +For necessity, rank K0=2d forces A injective and B onto by (2). +If Y10 z=0 for z != 0, (1) gives Hz=z, and A(z,-z)=0. +If Y01 z=0, again Hz=z, and A(z,0)=0. +If Y11 z=0, then Hz=0, and A(z,0)=0. +Each contradicts injectivity. Applying this argument to P transpose and +Q transpose proves surjectivity of the three X maps. Their sector inclusion +ranks are the ranks of E_j transpose i, equal to rank(pi E_j)=rank X_j. +The transpose commutator is minus K0 transpose, so its rank is unchanged. + +For sufficiency, injectivity of Y10 first gives y=0 when A(x,y)=0. +The other two sectors give Hx=Wx=0, hence x=0. If a covector (u,v) +annihilates B, evaluating on sectors 10,01,11 and using surjectivity gives +u=0, -u+vH=0, and vW=0. Thus vH=vW=0, so v=0. Therefore B is onto. +Since Bi=0, B restricted to ker pi is onto as well. The product of the +coordinate factors in (2) consequently has rank 2d. This proves the criterion. + +## Lower bound and attaining construction + +For each active sector j=10,01,11, the criterion and the rank inequality for +a product give rank(X_j Y_j) >= 2d-r_j. Equation (1) therefore gives +r10,r01 >= d+b and r11 >= d+a. The 00 sector only needs +r00 >= rank(-W)=d-b. Their sum is 4d+a+b. Also +rank P=r10+r11 and rank Q=r01+r11, proving the input-rank bounds. + +To attain all bounds, factor each active compressed product T through a space +of dimension d+nullity(T). Choose columns N_T complementing im T and set + +```text +X_T = [T N_T], Y_T = [I;0]. +``` + +Then X_T is onto, Y_T is injective and X_T Y_T=T. Use this for W in sectors +10 and 01, and H in sector 11. In sector 00 use a rank factorization of +**-W** through dimension rank W, allowing a zero-dimensional sector. +Stack the four Y maps to make i and concatenate the X maps to make pi. +Equation (1) gives pi i=-W+W+W+H=I. + +On this direct sum use P0=diag(0,I,0,I), Q0=diag(0,0,I,I). +Then pi P0 i=pi Q0 i=W+H=I and pi P0 Q0 i=H. Complete i by a basis N of +ker pi. The square matrix M=[i N] is invertible since pi i=I. Thus + +```text +P=M^-1 P0 M, Q=M^-1 Q0 M +``` + +have the prescribed coordinate pivots and product. All six active maps have +the required full ranks, so the criterion attains commutator rank 2d. +The dimension is exactly (d-b)+2(d+b)+(d+a)=4d+a+b. + +For |K|>2 choose any lambda outside {0,1} and H=lambda I. Then a=b=0, +so n=4d is attainable and minimal for every d. The exceptional binary scalar +case has minimum five, already proved in #4671. The binary d>=2 minimum +4d also remains that predecessor's result. + +## Evidence and reproduction + +The standard-library verifier imports no predecessor executable. It constructs +the full P,Q matrices, directly checks idempotence, commutation, pivots, +prescribed product, Schur complements, input ranks, sector dimensions and the +ordered factorization. Its exhaustive fixed-H domains are d=1,2 over +F2,F3,F4,F5, with respectively **18,84,260,630** constructions, totaling 992. +F4 uses x²+x+1, not arithmetic modulo four. + +It also checks 12 nonbinary 4d witnesses at d=1,...,4, 12 nondiagonal +size-three product blocks, and 18 premise-preserving controls deleting one +active injection or surjection. Three malformed/singular/capacity inputs are +rejected. An odd-characteristic control distinguishes subtraction from the +binary plus formula. Counts are generated by the executed loops, not estimates. +The universal theorem rests on the written proof, not finite extrapolation. + +From the repository root, using CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/all-field-identity-schur/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/all-field-identity-schur/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/all-field-identity-schur +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/all-field-identity-schur --check-source-history +``` + +The marker is `PASS_ALL_FIELD_IDENTITY_SCHUR`. The generated stdout receipt +binds all package files by SHA256. It writes no files. No handwritten receipt +is committed. A different CPython 3.12 path may replace the local path. + +## Scope and code constraints + +This is one common identity-pivot deletion over a field. Nonidentity pivots, +coefficient rings, later orbit distributions and header counts are outside the +claim. Header selection/emission, reads, restoration, stock, precision and the +complete consumer costs remain unknown. No selected scientific cold replay, +Lean, Docker, independent human or proof-kernel review is claimed. + +All verifier calls are direct, with no recursion, subprocesses or generated +code. The fixed main program uses only q=2,3,4,5 and d<=4. Mathematical matrices +have at most 18 rows. Elimination enforces a capacity of 24 rows and +48 augmented columns. Every exhaustive scan has at most 625 matrices; +only the current construction and counters persist. Functions stay below +60 lines. Explicit exceptions keep checks active under -O. Warnings are errors. +CPython's dynamic arithmetic and collection allocation is a managed-runtime +deviation from Power of Ten rule 3, with live state bounded by these domains. +No external static analyzer is required or claimed. + +The formal-interface-lemma card is explicitly changed to this algebraic side +theorem. It transfers an existing binary structural result to the odd-field +domain relevant to the retained normalizer, without claiming physical admission +or expanding a supplier family. The historical card baseline was attempted +and stopped at omitted sparse-checkout input +`research/fresh-helper-boundary/ARITHMETIC-RESULT.json`; no baseline pass is claimed. + +## Open next questions + +1. Determine the prescribed-product minimum for common nonidentity scalar + pivots. First derive the four compressed sector products and the exact + full-rank criterion. The identity-pivot six-map argument does not supply it. +2. Extend the binary one-block header count of #4678 to odd fields with the + shared-H dependence retained. First count one fixed scalar sector profile. + An actual header cover and its physical bill remain separate obligations. + +## Credit + +ssafwann's #4671 supplies the binary fixed-H theorem, six-map criterion and +split-factor construction; #4657 supplies the identity-pivot precursor. +Nick Petalas's #4597 supplies the ordered block identity, and #4278/#4259/#4228 +retain the scalar Schur, laminar-header and single-request lineage. +Ryanson Jonathan's #4609/#4617 and lee-phys's #4634 supply the earlier field +sharpness and dimension constructions. Cinna Davis's #4100 supplies the BIT +request context and retains the normalizer lineage of source527, +commdata2338 and Jose Manuel. No predecessor files or credit lines are changed. +Exact pending-head citations are recorded in TASK.json; they are citations, +not runtime inputs or claims of Git ancestry. diff --git a/research/all-field-identity-schur/SOURCES.json b/research/all-field-identity-schur/SOURCES.json new file mode 100644 index 0000000000..c6dc425e7d --- /dev/null +++ b/research/all-field-identity-schur/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/schur-commutator-criterion/README.md", + "usage": "provenance", + "git_blob": "6b37342de04f5c42c198dd6ba14cea9845be6f05", + "sha256": "5616da2e708a8425f1bf0bf5c89c236ef8ed0a23d0544d30ae2142ffe167dc01" + } + ] +} diff --git a/research/all-field-identity-schur/TASK.json b/research/all-field-identity-schur/TASK.json new file mode 100644 index 0000000000..0e12b3fea4 --- /dev/null +++ b/research/all-field-identity-schur/TASK.json @@ -0,0 +1,169 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Extend the binary fixed-H identity-pivot Schur minimum to every field: n_min(H)=4d+nullity(H(I-H)).", + "scope_change_reason": "A written algebraic side theorem extends a binary structural result to arbitrary characteristic; no formalization or selected-caller audit is claimed.", + "bottleneck_link": "A structural bound for shared Schur deletion in odd fields; header production and full physical costs remain open.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved and directly corroborated all-field extension.", + "outcome": "completed", + "evidence": "README proof; verify.py constructs and checks all 992 fixed-H cases for d=1,2 over F2,F3,F4,F5.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Minimum for common nonidentity scalar pivots with prescribed H", + "why_it_matters": "Separates the identity restriction from general admitted pivots.", + "first_step": "Derive signed sector products and the replacement full-rank criterion.", + "blocked_by": "The current six-map theorem assumes identity pivots." + }, + { + "question": "Odd-field complete-header frequency for a fixed sector profile", + "why_it_matters": "Dimension feasibility does not give a passing header probability.", + "first_step": "Extend the shared-H factor count of #4678 for one scalar profile.", + "blocked_by": "No odd-field header count or physical cover is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19130812", + "preserved_checkout": { + "branch": null, + "detached_head": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "prior_commits": [ + "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "6044f37b1f75a57f5fea6d17077b6985893062c1", + "4f19cedcd8d81e4a2359449309fa6e9f17dfd22e", + "f626db5c3a3d781d8f7695038776c621651f75e1" + ] + }, + "citations": [ + { + "pr": 4671, + "author": "ssafwann", + "head": "8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9", + "path": "research/identity-pivot-sector-bound/README.md", + "sha256": "c997446a1fc4683694987feea5f2a8423b57d48d5513a27e178f84ecf56ffc12", + "contribution": "Binary fixed-H theorem, six-map proof and split-factor construction." + }, + { + "pr": 4597, + "author": "Nick Petalas", + "head": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb", + "path": "research/block-schur-commutator/README.md", + "contribution": "Ordered all-field block Schur factorization." + } + ], + "overlap": { + "canonical_main": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "priority_revision": 7, + "open_pr_records": 506, + "open_pr_fetched_at": "2026-10-22T18:54:20.523162+00:00", + "discussion_records": 3661, + "discussion_fetched_at": "2026-10-22T18:55:05.284987+00:00", + "coverage_limit": "Overlap helper omits sparse local notes; separate git grep searches all origin/main research READMEs. Remote arbitrary diffs and unpublished work are not exhaustively searched. Own earlier PRs are excluded as targets.", + "searched_terms": [ + "identity-pivot", + "prescribed H", + "Schur dimension", + "H-H^2", + "4d field" + ], + "final_origin_main": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "related_heads": { + "4597": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb", + "4634": "9f053f7051e5fc3327d4337bb4bd8ac52cf5fcd0", + "4657": "b79f90bc8d839a4998a40b10bcb437e87baa8397", + "4678": "af9cf805c501e4e9e947c98c0b97b2281b6b6e97", + "4617": "96c01a2124e234d798e9e97643c20fb5b430840d", + "4735": "4afbea22e79e19d1d65702eb4090d454ee39d967", + "4671": "8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9", + "4689": "3a72fbad148294aa9ca7f900a48dbb10e64232be", + "4608": "aae3cddad698f9c8fb293304eb7260a96ce6190a", + "4609": "eb5ccf9288808d973551e6264300d30d2f6e48a0" + }, + "final_checkpoint_utc": "2026-10-22T19:01:06.107499+00:00" + }, + "verification": { + "python": "CPython 3.12", + "fixed_h_cases": 992, + "registered_check_seconds": [ + 0.6710027909139171, + 0.6981331249698997 + ], + "normal_and_optimized": "pass", + "independent_human_or_kernel_review": "unclaimed" + } +} diff --git a/research/all-field-identity-schur/VERIFY.json b/research/all-field-identity-schur/VERIFY.json new file mode 100644 index 0000000000..122836a2cf --- /dev/null +++ b/research/all-field-identity-schur/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All 992 fixed-H constructions, direct full matrices, signed factors, 18 deficient-map controls, F4 arithmetic and input rejection." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All 992 fixed-H constructions, direct full matrices, signed factors, 18 deficient-map controls, F4 arithmetic and input rejection." + } + ] +} diff --git a/research/all-field-identity-schur/verify.py b/research/all-field-identity-schur/verify.py new file mode 100644 index 0000000000..8e2e0f2ca5 --- /dev/null +++ b/research/all-field-identity-schur/verify.py @@ -0,0 +1,291 @@ +#!/usr/bin/env python3 +"""Exact, read-only corroboration of the all-field fixed-H Schur theorem.""" + +import hashlib +import itertools +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(x, y, q): + return x ^ y if q == 4 else (x + y) % q + + +def neg(x, q): + return x if q == 4 else (-x) % q + + +def mul(x, y, q): + if q != 4: + return x * y % q + value = (x if y & 1 else 0) ^ ((x << 1) if y & 2 else 0) + return value ^ 7 if value & 4 else value + + +def inv(x, q): + require(x != 0, "zero inverse") + for y in range(1, q): + if mul(x, y, q) == 1: + return y + raise ValueError("nonfield arithmetic") + + +def eye(n): + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def plus(a, b, q, sign=1): + require(len(a) == len(b), "matrix row mismatch") + require(all(len(x) == len(y) for x, y in zip(a, b)), "matrix column mismatch") + return tuple(tuple(add(x, y if sign == 1 else neg(y, q), q) + for x, y in zip(row, other)) for row, other in zip(a, b)) + + +def product(a, b, q): + require(bool(a) and bool(b), "empty matrix multiplication") + require(len(a[0]) == len(b), "product shape mismatch") + result = [] + for row in a: + output = [] + for j in range(len(b[0])): + value = 0 + for k in range(len(b)): + value = add(value, mul(row[k], b[k][j], q), q) + output.append(value) + result.append(tuple(output)) + return tuple(result) + + +def reduced(a, q): + if not a: + return (), () + require(len(a) <= 24 and len(a[0]) <= 48, "matrix capacity") + require(all(len(row) == len(a[0]) for row in a), "ragged matrix") + require(all(0 <= x < q for row in a for x in row), "field element") + rows = [list(row) for row in a] + pivots = [] + for j in range(len(rows[0])): + r = len(pivots) + if r == len(rows): + break + pivot = next((i for i in range(r, len(rows)) if rows[i][j]), None) + if pivot is None: + continue + rows[r], rows[pivot] = rows[pivot], rows[r] + scale = inv(rows[r][j], q) + rows[r] = [mul(x, scale, q) for x in rows[r]] + for i in range(len(rows)): + if i != r and rows[i][j]: + factor = rows[i][j] + rows[i] = [add(x, neg(mul(factor, y, q), q), q) + for x, y in zip(rows[i], rows[r])] + pivots.append(j) + return tuple(tuple(row) for row in rows), tuple(pivots) + + +def rank(a, q): + return len(reduced(a, q)[1]) + + +def inverse(a, q): + n = len(a) + require(n > 0 and all(len(row) == n for row in a), "inverse shape") + r, pivots = reduced(tuple(row + unit for row, unit in zip(a, eye(n))), q) + require(pivots == tuple(range(n)), "singular matrix") + return tuple(row[n:] for row in r) + + +def transpose(a): + return tuple(zip(*a)) + + +def active_factor(t, q): + """XY=t, X onto and Y injective, through d+nullity(t).""" + d = len(t) + columns = [tuple(row[j] for row in t) for j in range(d)] + current = rank(t, q) + extra = [] + for unit in eye(d): + candidate = transpose(columns + extra + [unit]) + if rank(candidate, q) > current: + extra.append(unit) + current += 1 + x = transpose(columns + extra) + y = eye(d) + tuple((0,) * d for _ in extra) + require(rank(x, q) == d and rank(y, q) == d, "active ranks") + require(product(x, y, q) == t, "active product") + return x, y + + +def rank_factor(t, q): + """Rank factorization through rank(t), including the zero sector.""" + d = len(t) + _, pivots = reduced(t, q) + r = len(pivots) + x = tuple(tuple(row[j] for j in pivots) for row in t) + if r == 0: + return x, () + _, rows = reduced(transpose(x), q) + square = tuple(x[j] for j in rows) + y = product(inverse(square, q), tuple(t[j] for j in rows), q) + require(product(x, y, q) == t, "rank factor product") + require(len(y) == rank(t, q), "minimal rank factor") + return x, y + + +def assemble(h, q, defect=None): + d = len(h) + w = plus(eye(d), h, q, -1) + factors = [rank_factor(tuple(tuple(neg(x, q) for x in row) for row in w), q), + active_factor(w, q), active_factor(w, q), active_factor(h, q)] + if defect is not None: + sector, side = defect + x, y = factors[sector] + require(all(v == 0 for row in (h if sector == 3 else w) for v in row), + "defect requires zero compressed product") + if side == "x": + x = tuple((0,) * len(x[0]) for _ in x) + else: + y = tuple((0,) * d for _ in y) + factors[sector] = x, y + sizes = tuple(len(y) for _, y in factors) + inclusion = tuple(row for _, y in factors for row in y) + projection = tuple(tuple(v for x, _ in factors for v in x[j]) for j in range(d)) + require(product(projection, inclusion, q) == eye(d), "split maps") + r, pivots = reduced(projection, q) + n = len(inclusion) + null_columns = [] + for j in range(n): + if j not in pivots: + column = [0] * n + column[j] = 1 + for i, pivot in enumerate(pivots): + column[pivot] = neg(r[i][j], q) + null_columns.append(tuple(column)) + basis = tuple(inclusion[j] + tuple(c[j] for c in null_columns) for j in range(n)) + basis_inverse = inverse(basis, q) + p_mask = (0,) * sizes[0] + (1,) * sizes[1] + (0,) * sizes[2] + (1,) * sizes[3] + q_mask = (0,) * sizes[0] + (0,) * sizes[1] + (1,) * (sizes[2] + sizes[3]) + p = product(basis_inverse, tuple(tuple(mul(v, p_mask[j], q) for v in row) + for j, row in enumerate(basis)), q) + z = product(basis_inverse, tuple(tuple(mul(v, q_mask[j], q) for v in row) + for j, row in enumerate(basis)), q) + return p, z, sizes + + +def block(a, row, height, col, width): + return tuple(tuple(line[col:col + width]) for line in a[row:row + height]) + + +def inspect(p, z, h, q, sharp=True): + d, n = len(h), len(p) + require(product(p, p, q) == p and product(z, z, q) == z, "idempotence") + pq = product(p, z, q) + require(pq == product(z, p, q), "commutation") + require(block(p, 0, d, 0, d) == eye(d), "P identity pivot") + require(block(z, 0, d, 0, d) == eye(d), "Q identity pivot") + require(block(pq, 0, d, 0, d) == h, "prescribed product") + c, e = block(p, d, n-d, 0, d), block(z, d, n-d, 0, d) + r, l = block(p, 0, d, d, n-d), block(z, 0, d, d, n-d) + s = plus(block(p, d, n-d, d, n-d), product(c, r, q), q, -1) + t = plus(block(z, d, n-d, d, n-d), product(e, l, q), q, -1) + k = plus(product(s, t, q), product(t, s, q), q, -1) + x = plus(block(pq, d, n-d, 0, d), product(e, h, q), q, -1) + u, v = plus(c, e, q, -1), plus(r, l, q, -1) + y = plus(block(pq, 0, d, d, n-d), product(h, l, q), q, -1) + require(k == plus(product(x, v, q), product(u, y, q), q, -1), "ordered factors") + kr = rank(k, q) + require((kr == 2*d) == sharp, "sharpness criterion") + require(rank(s, q) == rank(p, q)-d and rank(t, q) == rank(z, q)-d, + "Schur rank drop") + return k, product(x, v, q), product(u, y, q) + + +def verify_constructions(): + counts = {} + sign_witness = None + for q in (2, 3, 4, 5): + count = 0 + for d in (1, 2): + for values in itertools.product(range(q), repeat=d*d): + h = tuple(tuple(values[i*d:(i+1)*d]) for i in range(d)) + p, z, sizes = assemble(h, q) + k, xv, uy = inspect(p, z, h, q) + a, b = d-rank(h, q), d-rank(plus(eye(d), h, q, -1), q) + require(sizes == (d-b, d+b, d+b, d+a), "sector minima") + require(len(p) == 4*d+a+b, "ambient minimum") + require(rank(p, q) == rank(z, q) == 2*d+a+b, "input minima") + j = product(h, plus(eye(d), h, q, -1), q) + require(d-rank(j, q) == a+b, "coprime nullity identity") + if q in (3, 5) and plus(xv, uy, q) != k: + sign_witness = (q, h) + count += 1 + counts[str(q)] = count + require(sign_witness is not None, "odd-characteristic sign control") + return counts, sign_witness + + +def verify_controls(): + defects = 0 + for q in (3, 4, 5): + for sector in (1, 2, 3): + h = ((0 if sector == 3 else 1,),) + for side in ("x", "y"): + p, z, _ = assemble(h, q, (sector, side)) + inspect(p, z, h, q, sharp=False) + defects += 1 + require(mul(2, 2, 4) == 3 and add(1, 1, 4) == 0, "F4, not Z/4") + rejected = 0 + for bad in (((0,),), ((1, 0),)): + try: + inverse(bad, 3) + except ValueError: + rejected += 1 + try: + reduced(((0,) * 49,) * 2, 3) + except ValueError: + rejected += 1 + require(rejected == 3, "singular/shape/capacity rejection") + for q in (3, 5): + w = neg(1, q) + require(add(add(add(w, w, q), w, q), 2, q) != 1, + "unsigned 00 sector must fail outside characteristic two") + for q in (3, 4, 5): + for d in range(1, 5): + h = tuple(tuple(2 if i == j else 0 for j in range(d)) for i in range(d)) + p, z, _ = assemble(h, q) + inspect(p, z, h, q) + require(len(p) == 4*d, "nonbinary unrestricted minimum") + for q in (2, 3, 4, 5): + for diagonal in ((0, 0, 1), (1, 1, 0), (0, 1, 2 if q > 2 else 1)): + h = tuple(tuple(diagonal[i] if i == j else int(j == i+1) + for j in range(3)) for i in range(3)) + p, z, _ = assemble(h, q) + inspect(p, z, h, q) + return {"missing_active_maps": defects, "rejected_inputs": rejected, + "unrestricted_witnesses": 12, "nondiagonal_size_three": 12, + "unsigned_sector_rejections": 2} + + +def main(): + counts, sign_witness = verify_constructions() + controls = verify_controls() + root = Path(__file__).resolve().parent + files = tuple(sorted(path for path in root.iterdir() if path.is_file())) + require(5 <= len(files) <= 8, "receipt file capacity") + receipt = {"claim_type": "scoped algebraic proof with finite corroboration", + "fixed_h_constructions": counts, "controls": controls, + "odd_sign_witness": sign_witness, + "files_sha256": {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in files}} + print(json.dumps(receipt, sort_keys=True)) + print("PASS_ALL_FIELD_IDENTITY_SCHUR") + + +if __name__ == "__main__": + main()