From 1c9996b87d497a1690630302a0ac65748affbf16 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:55:15 +0100 Subject: [PATCH] feat(research): prove the scalar-block Schur dimension formula --- .../scalar-block-schur-dimension/PROOF.md | 159 +++++++ .../scalar-block-schur-dimension/README.md | 143 ++++++ .../scalar-block-schur-dimension/SOURCES.json | 42 ++ .../scalar-block-schur-dimension/TASK.json | 209 +++++++++ .../scalar-block-schur-dimension/VERIFY.json | 34 ++ .../scalar-block-schur-dimension/verify.py | 438 ++++++++++++++++++ 6 files changed, 1025 insertions(+) create mode 100644 research/scalar-block-schur-dimension/PROOF.md create mode 100644 research/scalar-block-schur-dimension/README.md create mode 100644 research/scalar-block-schur-dimension/SOURCES.json create mode 100644 research/scalar-block-schur-dimension/TASK.json create mode 100644 research/scalar-block-schur-dimension/VERIFY.json create mode 100644 research/scalar-block-schur-dimension/verify.py diff --git a/research/scalar-block-schur-dimension/PROOF.md b/research/scalar-block-schur-dimension/PROOF.md new file mode 100644 index 0000000000..0c4eb58ed9 --- /dev/null +++ b/research/scalar-block-schur-dimension/PROOF.md @@ -0,0 +1,159 @@ +# Exact dimension for a common scalar block + +This proof was produced by Nick Petalas. Apache-2.0. + +Let K be any field, d >= 1, lambda in K nonzero and H in M_d(K). +Consider commuting idempotents P,Q on K^n whose first d-by-d blocks are +both lambda I_d and whose product PQ has first block H. Let S,Z be the +two Schur complements after deleting those first d coordinates. Then the +least n permitting rank(SZ-ZS)=2d is exactly + +```text +n_min(lambda,H) = 3d + rank((1-2lambda)I+H) + + 2 nullity(lambda I-H) + nullity(H). (1) +``` + +Every minimum is attained over K, without diagonalizability assumptions +on H. This answers Open next question 2 of Nick Petalas's #4771. The +identity-block result of #4746 and ssafwann's #4671, and the scalar-block-size +one result of #4771, are cited predecessors. The new part is the common +nonidentity scalar block with an arbitrary prescribed matrix product. + +## Compression and the full-rank criterion + +Put U=K^d, V=K^n. Let i:U -> V be coordinate inclusion and pi:V -> U +coordinate projection, so pi i=I. The joint eigenspace projectors are + +```text +E00=(I-P)(I-Q), E10=P(I-Q), E01=(I-P)Q, E11=PQ. +``` + +They give a direct sum V=V00+V10+V01+V11 in every characteristic. Set +Y_j=E_j i:U -> V_j and X_j=pi restricted to V_j:V_j -> U. Write + +```text +D=lambda I-H, T0=(1-2lambda)I+H, +a=nullity(H), b=nullity(D), c=rank(T0). +``` + +Compression gives + +```text +X00 Y00=T0, X10 Y10=D, X01 Y01=D, X11 Y11=H. (2) +``` + +In particular, their sum T0+2D+H is I. The signed joint-sector method +comes from ssafwann's #4671 and Nick Petalas's #4746. Here the products +and the rank argument retain lambda throughout. + +Use Nick Petalas's ordered block Schur identity from #4597, with equal +pivot blocks lambda I. Its ambient factors are + +```text +A=[PQ i-Q i H/lambda, (P-Q)i/lambda] : U^2 -> V, +B=[pi(P-Q)/lambda; -pi PQ+H pi Q/lambda] : V -> U^2. +``` + +We have pi A=0 and Bi=0. Since V=i(U) direct-sum ker pi, the Schur +commutator is the product of A in ker pi coordinates and B restricted to +ker pi. Thus its rank is 2d exactly when A is injective and B is onto. +In joint-sector coordinates, + +```text +A(x,y) = (1/lambda)(0, Y10 y, -Y01(Hx+y), Y11 D x), +B(v00,v10,v01,v11) + = (1/lambda)(X10 v10-X01 v01, + H X01 v01-D X11 v11). (3) +``` + +**Criterion.** Rank(SZ-ZS)=2d if and only if Y10,Y01,Y11 are injective +and X10,X01,X11 are onto. + +For necessity, rank 2d forces A injective. If Y10 z=0, (2) implies +Dz=0, hence Hz=lambda z. Equation (3) then gives A(z,-lambda z)=0, +so z=0. If Y01 z=0, the same product equation gives Dz=0 and +A(z,0)=0, hence z=0. If Y11 z=0, (2) gives Hz=0. Thus +Dz=lambda z and again A(z,0)=0, hence z=0. This proves all three +injections. Apply the same necessity argument to the dual commuting +projectors with inclusion pi* and projection i*. Their commutator has +the same rank, and their sector inclusion ranks are the ranks of X_j*. +Consequently the three X_j are onto. + +For sufficiency, A(x,y)=0 first gives y=0 by injectivity of Y10. +The other two sectors give Hx=Dx=0. Since H+D=lambda I and lambda +is nonzero, x=0. Thus A is injective. If a covector (u,v) annihilates B, +surjectivity of X10 gives u=0. Surjectivity of X01 and X11 then gives +vH=vD=0, hence lambda v=0 and v=0. Thus B is onto. As Bi=0, +its restriction to ker pi is onto too. Their product has rank 2d, +proving the criterion. + +## Lower bound and attaining construction + +Let r_j=dim V_j. For every active sector 10,01,11, the criterion and +the rank inequality for a product imply + +```text +rank(X_j Y_j) >= rank X_j + rank Y_j - r_j = 2d-r_j. +``` + +Equation (2) therefore gives the componentwise necessary bounds + +```text +(r00,r10,r01,r11) >= (c,d+b,d+b,d+a). (4) +``` + +Their sum is (1). Also rank P=r10+r11 and rank Q=r01+r11 are +each at least 2d+a+b. These input-rank bounds can be attained together +with all four sector bounds. + +For an arbitrary d-by-d matrix T, let N_T have columns forming a +complement to im T in U. On a space of dimension d+nullity(T) put + +```text +X_T=[T N_T], Y_T=[I;0]. +``` + +Then X_T Y_T=T, X_T is onto and Y_T is injective. Use this for T=D +in sectors 10 and 01 and for T=H in sector 11. In sector 00 take any +rank factorization T0=X00 Y00 through dimension c, including dimension +zero if T0=0. Stack the Y maps to form i and concatenate the X maps to +form pi. By (2), pi i=T0+2D+H=I. + +On this direct sum let P0 and Q0 act by their sector eigenvalues 00, +10,01,11. Complete i to a coordinate basis M=[i N], where N is a basis +of ker pi. This is invertible because pi i=I. Then + +```text +P=M^-1 P0 M, Q=M^-1 Q0 M +``` + +are commuting idempotents with the prescribed leading blocks and product. +All six active maps have full rank, so (3) proves sharpness. The dimension +is exactly c+2(d+b)+(d+a). This proves (1) and simultaneous attainment +of (4) and both input-rank bounds over every field. + +## Specializations and a nondiagonal example + +At lambda=1, c=rank(H-I)=d-b, so (1) reduces to the predecessor +identity-pivot formula 4d+a+b. At d=1 it reduces to all three cases +of the predecessor scalar formula in #4771. These are calibration +specializations, not new results. + +For a new nondiagonal instance, over F5 take + +```text +lambda=2, d=2, H=[[3,1],[0,3]]. +``` + +Here T0=[[0,1],[0,0]] has rank one, while H and D=2I-H are +invertible. Thus the exact minimum is seven, with sectors (1,2,2,2), +input ranks four and Schur-commutator rank four. Replacing this Jordan +block by 3I gives minimum six. A nondiagonal nilpotent part can therefore +change the minimum even when H and lambda I-H have the same nullities. +The construction above realizes both cases directly. + +This is a scoped algebraic proof, not a complete multiplication theorem. +It supplies neither header frequencies nor a paid header producer or +consumer. Unequal block pivots, general coefficient rings, subsequent +Schur-state transitions, precision, restoration and stock remain separate +obligations. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/scalar-block-schur-dimension/README.md b/research/scalar-block-schur-dimension/README.md new file mode 100644 index 0000000000..cbed8b8dd7 --- /dev/null +++ b/research/scalar-block-schur-dimension/README.md @@ -0,0 +1,143 @@ +# Exact Schur dimension for a common scalar block + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof with finite corroboration. For every field K, +every nonzero lambda in K and every prescribed H in M_d(K), d >= 1, the least +ambient dimension of commuting idempotents P,Q with common leading blocks +lambda I_d, leading product block H and Schur-commutator rank 2d is + +```text +n_min(lambda,H) = 3d + rank((1-2lambda)I+H) + + 2 nullity(lambda I-H) + nullity(H). +``` + +Every minimum is attained by the construction in [PROOF.md](PROOF.md), including +nondiagonal and nondiagonalizable H. The four minimal joint-sector dimensions +are `(rank((1-2lambda)I+H), d+b, d+b, d+a)`, where `a=nullity(H)` and +`b=nullity(lambda I-H)`. Both input projectors simultaneously have minimum +rank `2d+a+b`. + +This answers Open next question 2 of +[PR #4771](https://github.com/CrocSwap/integer-mult-bounds/pull/4771), pinned at +`22cb0bda57237d39d0e6944b232447d3a2809311`. That package treats scalar block +size one. Nick Petalas's #4746 and ssafwann's #4671 treat identity blocks. +Their results are cited inputs and specializations, not audit targets. The new +result allows a nonidentity scalar block and an arbitrary matrix product H. +No new kappa or selected-frontier change is claimed. + +For example, over F5 with lambda=2 and `H=[[3,1],[0,3]]`, the exact minimum +is seven, with sectors `(1,2,2,2)`, input ranks four and Schur-commutator +rank four. For the diagonal product `H=3I_2` the minimum is six. Both H and +`2I-H` are invertible in both examples. The nilpotent part changes the +00-sector rank, which the identity-pivot formula does not capture. + +## Evidence and reproduction + +The proof specializes the ordered block identity of #4597 and proves that +sharpness is equivalent to injectivity and surjectivity of all six active +sector maps. The rank inequality bounds each sector separately. A split +factorization attains all four bounds and both input ranks simultaneously. +The proof holds over every field; the finite checks are corroboration. + +The independently written standard-library verifier imports no predecessor +executable. It constructs full P,Q and directly checks idempotence, +commutation, both scalar block pivots, the prescribed product block, Schur +idempotence, rank drops, the ordered commutator factorization, the six-map +criterion, the ambient minimum and both input ranks. Its executed domains are: + +- All 3,446 pairs `(lambda,H)` with nonzero lambda and every two-by-two H over + F2,F3,F4,F5, respectively 16, 162, 768 and 2,500 constructions. +- All 210 scalar pairs over F2,F3,F4,F5,F7,F8,F9, including direct numerical + comparison with #4771's piecewise scalar specialization. +- 482 additional Jordan and companion-style constructions at d=2,3 over + those seven fields. These overlap the exhaustive domains where applicable. +- An independent enumeration of 45,900 full-rank factor pairs over F2, + finding the exact minimum middle dimension for each of the 16 two-by-two + compressed products. This corroborates the sector cost, rather than + enumerating all ambient commuting projector pairs. +- Six premise-preserving missing-map controls and five malformed-input + controls. The former retain commuting idempotents and the prescribed + compressed products while lowering one necessary injection or surjection. +- All 1,808 field triples test associativity and distributivity; every nonzero + element has its inverse checked. F4,F8,F9 use irreducible polynomial + quotients, rather than arithmetic modulo their orders. + +Two explicit checks compare the nondiagonal seven-dimensional F5 example +with its six-dimensional diagonal control. The generated stdout receipt binds +all six package files by SHA256. The verifier writes nothing into the checkout. + +From the repository root, with CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/scalar-block-schur-dimension/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/scalar-block-schur-dimension/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/scalar-block-schur-dimension +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/scalar-block-schur-dimension --check-source-history +``` + +The scientific marker is `PASS_SCALAR_BLOCK_SCHUR_DIMENSION`. A different +CPython 3.12 path may replace the local path. All checks use explicit exceptions +and remain active under optimized Python. Metadata and source-history checks +are separate from mathematical verification. The selected source-binding +orientation passed; no selected scientific replay was run. + +## Scope and code constraints + +This is one deletion with equal nonzero scalar block pivots, field coefficients +and commuting idempotents. It gives no complete-header count, later-state law, +coefficient-ring theorem or arbitrary-block-pivot dimension minimum. Header +production, selection/emission, dispatch, dirty restoration, precision, stock +and the complete physical consumer costs remain unknown. No physical supplier +admission or complete multiplication theorem follows. Independent human and +formal proof-kernel review are unclaimed. Lean, Docker and selected cold replay +were not run. + +The verifier has fixed domains, fields of order at most nine, deleted blocks +of size at most three and constructed matrices of size at most 18. Matrix +operations enforce a 24-row, 48-column capacity, including augmented elimination. +The largest exhaustive target scan has 625 matrices per pivot, and the factor +census retains at most 210 full-rank maps and 16 minima. Only the current full +construction and counters persist across target scans. All calls are direct; +there is no recursion, subprocess, callback chain or generated code. Functions +stay below 60 physical lines. Warnings are errors in both registered commands; +syntax, function lengths and dynamic-code calls are inspected locally. No +external static analyzer is installed or claimed. + +Power of Ten rule 3 deviation: CPython arithmetic and tuples allocate during +execution, so this standalone verifier cannot prohibit dynamic allocation. +The fixed field, matrix, census and six-file receipt capacities bound its live +data. Both registered modes exercise these bounds, and explicit controls reject +an oversized matrix and invalid target shapes. The deviation is confined to +this verifier; reassess storage and input validation before adding larger +domains or an external parameter interface. It owns no external mutable resource. + +## Open next questions + +1. Determine the prescribed-H minimum for unequal scalar block pivots pI_d + and qI_d at d>=2. This would separate equality of the pivots from their + scalarity. Start with the two ambient factors and an H with an eigenvalue + at one pivot but not the other. The scalar unequal-pivot question is + separately claimed and is not delivered here. +2. Count complete headers attaining one nonidentity scalar-block profile. + Feasibility alone gives no frequency or paid header cover. Start with the + F5 profile `(1,2,2,2)`, d=2, lambda=2 and the fixed Jordan product above. + A joint factorization count and the producer/consumer bill remain open. + +## Credit and task scope + +Nick Petalas's #4771 supplies the explicit open matrix-product question and +scalar predecessor; #4746 supplies the all-field identity-pivot predecessor. +ssafwann's #4671/#4657 supplies the binary fixed-H theorem, six-map method +and split-sector construction. Nick Petalas's #4597/#4278 supplies the ordered +block and scalar Schur factorizations. Ryanson Jonathan's #4609/#4617 and +lee-phys's #4634 supply earlier small-field and unrestricted-block sharpness +constructions. Nick Petalas's #4259/#4228 retains the laminar-header and +single-request context. Cinna Davis supplies the BIT request setting; +source527, commdata2338 and Jose Manuel retain the normalizer lineage credit. + +The formal-interface-lemma card is explicitly changed to this algebraic side +question. It resolves a prescribed-boundary dimension question without auditing +another contributor or expanding a physical construction. Exact source pins, +overlap coverage, the advance claim and preserved checkout state are recorded +in TASK.json and SOURCES.json. No predecessor file or credit line is changed. diff --git a/research/scalar-block-schur-dimension/SOURCES.json b/research/scalar-block-schur-dimension/SOURCES.json new file mode 100644 index 0000000000..6306721133 --- /dev/null +++ b/research/scalar-block-schur-dimension/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/scalar-pivot-schur-dimension/README.md", + "usage": "provenance", + "git_blob": "7ccd8ef743a665e4177cbc712da78ec58da0e83a", + "sha256": "326fbbab0d25a94113e4ede541873025209a26ac3d3171b2c4ea48189982dad0" + }, + { + "path": "research/scalar-pivot-schur-dimension/PROOF.md", + "usage": "provenance", + "git_blob": "ebfb0d1b1c57651a0a34434ca42aec05e4ddc6b6", + "sha256": "c3573842b497de3b41d4cd5b6ef72edfee8e4cc968acfdfc27bfcbb5b3ca09d2" + }, + { + "path": "research/all-field-identity-schur/README.md", + "usage": "provenance", + "git_blob": "c3a64475cc52ba7025d57d2c1a810a35c563ca40", + "sha256": "e702c6e05e3283363294ed10a1b9bc4b589c46cc2fb7df198ec9c6841ec78f78" + }, + { + "path": "research/block-schur-commutator/README.md", + "usage": "provenance", + "git_blob": "79790ccea54cfea1aab611768927651a81f2fb18", + "sha256": "945c1420fe9fb5c26dec49e7d6005d77382ca9dc6ca0f424d8baa1500bfc092c" + } + ] +} diff --git a/research/scalar-block-schur-dimension/TASK.json b/research/scalar-block-schur-dimension/TASK.json new file mode 100644 index 0000000000..63d27a47e6 --- /dev/null +++ b/research/scalar-block-schur-dimension/TASK.json @@ -0,0 +1,209 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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": "Exact minimum ambient dimension for commuting field idempotents with common leading block lambda I_d, arbitrary prescribed leading product H, and Schur-commutator rank 2d.", + "scope_change_reason": "Answer Open next question 2 of PR4771 with an original algebraic block theorem; this is neither a predecessor audit nor a formalization.", + "bottleneck_link": "A changed shared-header boundary has a different exact sharpness dimension. Header production and full physical costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original dimension formula; package it without extending to unequal block pivots or header counts.", + "outcome": "completed", + "evidence": "PROOF.md establishes the formula and simultaneous attainment. verify.py checks 3446 exhaustive size-two pairs, 210 scalar pairs, 482 additional block samples, 45900 full-rank factor pairs and eleven controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Unequal nonzero scalar block pivots at d>=2", + "why_it_matters": "Separates equality of pivots from scalarity.", + "first_step": "Derive the two ambient factors for pI_d,qI_d and a product H singular at one pivot.", + "blocked_by": "The proof fixes equal pivots; the scalar unequal-pivot question is separately claimed." + }, + { + "question": "Complete-header count for a nonidentity scalar-block profile", + "why_it_matters": "Dimension feasibility does not determine frequency or a paid header cover.", + "first_step": "Count joint sector factorizations for the F5 profile (1,2,2,2), d=2, lambda=2, H=[[3,1],[0,3]].", + "blocked_by": "No joint counting law or physical header-producer/consumer bill is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131555", + "playbook": "Autonomous local run", + "preserved_checkout": { + "branch": "research/w8-1022f-scalar-pivot-schur", + "head": "22cb0bda57237d39d0e6944b232447d3a2809311", + "prior_commits": [ + "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b", + "20bb93cd990d2ff683e4d0fc56b87a42cd5d3296", + "dc6226289576ab7631e43918c0071558cb0d13f7", + "9fd59d9b08ecd1ebf43fdf41d0fdcdb2bb4bb8e3" + ], + "initial_status": "clean including ignored files" + }, + "overlap": { + "canonical_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "initial_open_limit": 100, + "account_pr_limit": 60, + "live_open_prs": 299, + "latest_handoff_comments": 30, + "active_discussions": 15, + "cache_open_prs": { + "records": 299, + "complete_pagination": true, + "fetched_at": "2026-10-22T19:45:13.565143+00:00" + }, + "cache_discussions": { + "records": 3712, + "complete_pagination": true, + "fetched_at": "2026-10-22T19:46:08.245656+00:00" + }, + "main_search_terms": [ + "common scalar block", + "nonidentity pivot", + "prescribed matrix product", + "3d.*null", + "rank.*1-2" + ], + "merged_search_terms": [ + "Schur", + "scalar block", + "prescribed product" + ], + "local_coverage": "Sparse helper searched 94 records and omitted 6225 tracked notes; separate git grep searched every main research README. No code-diff or unpublished-result coverage is claimed.", + "reservation": "formal-interface-lemma-common-scalar-block-prescribed-product-schur-dimension.lock", + "related_open_prs": [ + 4774 + ], + "final_checkpoint_utc": "2026-10-22T19:55:15.280703+00:00", + "final_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "related_open_work": { + "4774": "Distinct nonzero scalar pivots p!=q, whereas this theorem fixes equal scalar blocks. No common parameter tuple and no overlapping numerical minimum. Its title and full body were read." + }, + "final_open_snapshot_records": 305 + }, + "citations": [ + { + "pr": 4771, + "head": "22cb0bda57237d39d0e6944b232447d3a2809311", + "author": "Nick Petalas", + "contribution": "Open matrix-product question and scalar-pivot predecessor.", + "usage": "Cited theorem/context only; no imported executable.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4771" + }, + { + "pr": 4746, + "head": "5f014560d6225cae17598ac479fb29d2947d8e6b", + "author": "Nick Petalas", + "contribution": "All-field identity-block predecessor.", + "usage": "Cited theorem/context only; no imported executable.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4746" + }, + { + "pr": 4671, + "head": "8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9", + "author": "ssafwann", + "contribution": "Binary prescribed-H theorem, six-map criterion and sector construction.", + "usage": "Cited theorem/context only; no imported executable.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4671" + }, + { + "pr": 4597, + "head": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb", + "author": "Nick Petalas", + "contribution": "Ordered block Schur factorization.", + "usage": "Cited theorem/context only; no imported executable.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4597" + } + ], + "verification": { + "python": "CPython 3.12.15 / arm64", + "direct_timings": [ + { + "mode": "normal", + "seconds": 1.8326071250485256, + "returncode": 0 + }, + { + "mode": "optimized", + "seconds": 1.8071279999567196, + "returncode": 0 + } + ], + "normal_and_optimized": "pass", + "selected_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "static_inspection": "AST syntax, direct call graph, fixed bounds, no recursion or dynamic-code calls; all functions below 60 physical lines.", + "external_static_analyzer": "not installed; no external analysis claimed" + } +} diff --git a/research/scalar-block-schur-dimension/VERIFY.json b/research/scalar-block-schur-dimension/VERIFY.json new file mode 100644 index 0000000000..fef5c37b8a --- /dev/null +++ b/research/scalar-block-schur-dimension/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": 120, + "checks": "3446 exhaustive d=2 pairs; 210 scalar pairs; 482 block samples; 45900 factor pairs; direct Schur products, six-map ranks, six missing-map and five malformed-input controls; generated six-file hash receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "3446 exhaustive d=2 pairs; 210 scalar pairs; 482 block samples; 45900 factor pairs; direct Schur products, six-map ranks, six missing-map and five malformed-input controls; generated six-file hash receipt." + } + ] +} diff --git a/research/scalar-block-schur-dimension/verify.py b/research/scalar-block-schur-dimension/verify.py new file mode 100644 index 0000000000..b0e5f42c2a --- /dev/null +++ b/research/scalar-block-schur-dimension/verify.py @@ -0,0 +1,438 @@ +#!/usr/bin/env python3 +"""Direct finite-field witnesses for the common scalar-block dimension theorem. + +Produced by Nick Petalas. Apache-2.0. +No predecessor executable or external input is imported. +""" +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import platform + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digits(value, prime, degree): + result = [] + for _ in range(degree): + result.append(value % prime) + value //= prime + return result + + +def polynomial_product(a, b, prime, modulus): + degree = len(modulus) - 1 + left, right = digits(a, prime, degree), digits(b, prime, degree) + work = [0] * (2 * degree - 1) + for i in range(degree): + for j in range(degree): + work[i + j] = (work[i + j] + left[i] * right[j]) % prime + for k in range(2 * degree - 2, degree - 1, -1): + coefficient = work[k] + for j in range(degree + 1): + work[k - degree + j] -= coefficient * modulus[j] + work[k - degree + j] %= prime + return sum(work[j] * prime ** j for j in range(degree)) + + +class Field: + def __init__(self, order): + definitions = {2: (2, (0, 1)), 3: (3, (0, 1)), + 4: (2, (1, 1, 1)), 5: (5, (0, 1)), + 7: (7, (0, 1)), 8: (2, (1, 1, 0, 1)), + 9: (3, (1, 0, 1))} + require(order in definitions, "unsupported field order") + prime, modulus = definitions[order] + degree = len(modulus) - 1 + self.q = order + self.add = [[sum(((x + y) % prime) * prime ** k + for k, (x, y) in enumerate(zip(digits(a, prime, degree), + digits(b, prime, degree)))) + for b in range(order)] for a in range(order)] + self.mul = [[polynomial_product(a, b, prime, modulus) + for b in range(order)] for a in range(order)] + self.neg = [next(b for b in range(order) if self.add[a][b] == 0) + for a in range(order)] + self.inv = [0] + [next(b for b in range(1, order) if self.mul[a][b] == 1) + for a in range(1, order)] + + +class Matrix: + __slots__ = ("rows", "cols") + + def __init__(self, rows, cols): + self.rows = rows + self.cols = cols + + def __eq__(self, other): + return isinstance(other, Matrix) and self.cols == other.cols and self.rows == other.rows + + +def matrix(rows, cols=None): + values = tuple(tuple(row) for row in rows) + width = len(values[0]) if values and cols is None else (cols or 0) + require(len(values) <= 24 and 0 <= width <= 48, "matrix capacity") + require(all(len(row) == width for row in values), "ragged matrix") + return Matrix(values, width) + + +def zero(rows, cols): + require(0 <= rows <= 24 and 0 <= cols <= 48, "zero capacity") + return matrix([[0] * cols for _ in range(rows)], cols) + + +def identity(size): + require(0 <= size <= 24, "identity capacity") + return matrix([[int(i == j) for j in range(size)] for i in range(size)], size) + + +def transpose(a): + return matrix([[a.rows[i][j] for i in range(len(a.rows))] + for j in range(a.cols)], len(a.rows)) + + +def scale(a, coefficient, field): + require(0 <= coefficient < field.q, "invalid scalar") + return matrix([[field.mul[coefficient][v] for v in row] for row in a.rows], a.cols) + + +def add(a, b, field): + require((len(a.rows), a.cols) == (len(b.rows), b.cols), "sum shape") + return matrix([[field.add[x][y] for x, y in zip(row_a, row_b)] + for row_a, row_b in zip(a.rows, b.rows)], a.cols) + + +def subtract(a, b, field): + return add(a, scale(b, field.neg[1], field), field) + + +def multiply(a, b, field): + require(a.cols == len(b.rows), "product shape") + output = [[0] * b.cols for _ in a.rows] + for i, row in enumerate(a.rows): + for k, value in enumerate(row): + if value: + for j in range(b.cols): + output[i][j] = field.add[output[i][j]][field.mul[value][b.rows[k][j]]] + return matrix(output, b.cols) + + +def join_horizontal(a, b): + require(len(a.rows) == len(b.rows), "horizontal shape") + return matrix([x + y for x, y in zip(a.rows, b.rows)], a.cols + b.cols) + + +def join_vertical(a, b): + require(a.cols == b.cols, "vertical shape") + return matrix(a.rows + b.rows, a.cols) + + +def select(a, row_indices, column_indices): + require(len(row_indices) <= 24 and len(column_indices) <= 48, "selection capacity") + require(all(0 <= i < len(a.rows) for i in row_indices), "invalid row") + require(all(0 <= j < a.cols for j in column_indices), "invalid column") + return matrix([[a.rows[i][j] for j in column_indices] for i in row_indices], + len(column_indices)) + + +def reduce_rows(a, field): + work = [list(row) for row in a.rows] + pivots = [] + for column in range(a.cols): + pivot = next((i for i in range(len(pivots), len(work)) if work[i][column]), None) + if pivot is None: + continue + target = len(pivots) + work[target], work[pivot] = work[pivot], work[target] + inverse_value = field.inv[work[target][column]] + work[target] = [field.mul[inverse_value][v] for v in work[target]] + for i in range(len(work)): + if i != target and work[i][column]: + coefficient = work[i][column] + work[i] = [field.add[x][field.neg[field.mul[coefficient][y]]] + for x, y in zip(work[i], work[target])] + pivots.append(column) + if len(pivots) == len(work): + break + return matrix(work, a.cols), tuple(pivots) + + +def rank(a, field): + return len(reduce_rows(a, field)[1]) + + +def inverse(a, field): + size = len(a.rows) + require(size == a.cols and size > 0, "inverse shape") + reduced, pivots = reduce_rows(join_horizontal(a, identity(size)), field) + require(pivots == tuple(range(size)), "singular matrix") + return select(reduced, tuple(range(size)), tuple(range(size, 2 * size))) + + +def kernel(a, field): + reduced, pivots = reduce_rows(a, field) + free = tuple(j for j in range(a.cols) if j not in pivots) + columns = [] + for j in free: + vector = [0] * a.cols + vector[j] = 1 + for i, pivot in enumerate(pivots): + vector[pivot] = field.neg[reduced.rows[i][j]] + columns.append(vector) + return transpose(matrix(columns, a.cols)) + + +def factor_product(target, active, field): + size = len(target.rows) + require(size == target.cols and 1 <= size <= 3, "target shape") + if active: + extended = join_horizontal(target, identity(size)) + pivots = reduce_rows(extended, field)[1] + complement = select(extended, tuple(range(size)), tuple(j for j in pivots if j >= size)) + x = join_horizontal(target, complement) + y = join_vertical(identity(size), zero(complement.cols, size)) + else: + columns = reduce_rows(target, field)[1] + x = select(target, tuple(range(size)), columns) + rows = reduce_rows(transpose(x), field)[1] + if columns: + square = select(x, rows, tuple(range(len(columns)))) + y = multiply(inverse(square, field), select(target, rows, tuple(range(size))), field) + else: + y = zero(0, size) + require(multiply(x, y, field) == target, "factor product") + return x, y + + +def sector_products(size, pivot, h, field): + require(1 <= size <= 3 and len(h.rows) == size and h.cols == size, "product-block shape") + require(0 < pivot < field.q, "zero or invalid pivot") + scalar_i = scale(identity(size), pivot, field) + t0 = add(subtract(identity(size), add(scalar_i, scalar_i, field), field), h, field) + difference = subtract(scalar_i, h, field) + return t0, difference, difference, h + + +def build_pair(size, pivot, h, field, defect=None): + targets = sector_products(size, pivot, h, field) + factors = [factor_product(t, j > 0, field) for j, t in enumerate(targets)] + if defect is not None: + sector, side = defect + x, y = factors[sector] + require(targets[sector] == zero(size, size), "defect needs a zero product") + if side == "Y": + rows = [list(row) for row in y.rows] + rows[0][0] = 0 + y = matrix(rows, size) + else: + require(side == "X", "unknown defect side") + rows = [list(row) for row in x.rows] + rows[0][size] = 0 + x = matrix(rows) + require(multiply(x, y, field) == targets[sector], "defect changed compressed product") + factors[sector] = x, y + include, project = zero(0, size), zero(size, 0) + masks_p, masks_q, dimensions = [], [], [] + for j, (x, y) in enumerate(factors): + include, project = join_vertical(include, y), join_horizontal(project, x) + dimensions.append(len(y.rows)) + masks_p.extend([int(j in (1, 3))] * len(y.rows)) + masks_q.extend([int(j in (2, 3))] * len(y.rows)) + require(multiply(project, include, field) == identity(size), "coordinate splitting") + basis = join_horizontal(include, kernel(project, field)) + back = inverse(basis, field) + p_basis = matrix([[field.mul[masks_p[i]][v] for v in row] for i, row in enumerate(basis.rows)]) + q_basis = matrix([[field.mul[masks_q[i]][v] for v in row] for i, row in enumerate(basis.rows)]) + return multiply(back, p_basis, field), multiply(back, q_basis, field), tuple(dimensions) + + +def inspect_pair(p, q, size, pivot, h, field): + count = len(p.rows) + require(p.cols == count and q.cols == count and len(q.rows) == count, "pair shape") + require(multiply(p, p, field) == p and multiply(q, q, field) == q, "idempotence") + pq = multiply(p, q, field) + require(pq == multiply(q, p, field), "commutation") + top, tail = tuple(range(size)), tuple(range(size, count)) + expected = scale(identity(size), pivot, field) + require(select(p, top, top) == expected and select(q, top, top) == expected, "pivot blocks") + require(select(pq, top, top) == h, "prescribed product") + r, c = select(p, top, tail), select(p, tail, top) + l, e = select(q, top, tail), select(q, tail, top) + s = subtract(select(p, tail, tail), scale(multiply(c, r, field), field.inv[pivot], field), field) + z = subtract(select(q, tail, tail), scale(multiply(e, l, field), field.inv[pivot], field), field) + commutator = subtract(multiply(s, z, field), multiply(z, s, field), field) + require(multiply(s, s, field) == s and multiply(z, z, field) == z, "Schur idempotence") + require(rank(s, field) == rank(p, field) - size, "P rank drop") + require(rank(z, field) == rank(q, field) - size, "Q rank drop") + u = scale(subtract(c, e, field), field.inv[pivot], field) + v = scale(subtract(r, l, field), field.inv[pivot], field) + x = subtract(select(pq, tail, top), scale(multiply(e, h, field), field.inv[pivot], field), field) + y = subtract(select(pq, top, tail), scale(multiply(h, l, field), field.inv[pivot], field), field) + require(commutator == subtract(multiply(x, v, field), multiply(u, y, field), field), + "ordered Schur factorization") + sectors = (add(subtract(subtract(identity(count), p, field), q, field), pq, field), + subtract(p, pq, field), subtract(q, pq, field), pq) + active_ranks = tuple((rank(select(t, top, tuple(range(count))), field), + rank(select(t, tuple(range(count)), top), field)) for t in sectors[1:]) + require((rank(commutator, field) == 2 * size) == + all(a == size and b == size for a, b in active_ranks), "six-map criterion") + return rank(commutator, field), tuple(rank(t, field) for t in sectors), rank(p, field), active_ranks + + +def check_case(size, pivot, h, field): + p, q, dimensions = build_pair(size, pivot, h, field) + sharp_rank, measured_dims, input_rank, _ = inspect_pair(p, q, size, pivot, h, field) + products = sector_products(size, pivot, h, field) + a = size - rank(h, field) + b = size - rank(products[1], field) + predicted_dims = (rank(products[0], field), size + b, size + b, size + a) + require(dimensions == measured_dims == predicted_dims, "sector minima") + require(len(p.rows) == 3 * size + rank(products[0], field) + 2 * b + a, "dimension formula") + require(sharp_rank == 2 * size and input_rank == 2 * size + a + b, "attained ranks") + require(rank(q, field) == input_rank, "second input rank") + return len(p.rows), dimensions + + +def all_blocks(size, order): + require(1 <= size <= 2 and 2 <= order <= 5, "exhaustive domain") + for entries in product(range(order), repeat=size * size): + yield matrix([entries[i * size:(i + 1) * size] for i in range(size)]) + + +def field_controls(field): + count = 0 + for a, b, c in product(range(field.q), repeat=3): + require(field.mul[a][field.add[b][c]] == + field.add[field.mul[a][b]][field.mul[a][c]], "distributivity") + require(field.mul[a][field.mul[b][c]] == field.mul[field.mul[a][b]][c], "associativity") + require(field.add[a][b] == field.add[b][a], "commutative addition") + count += 1 + for a in range(1, field.q): + require(field.mul[a][field.inv[a]] == 1, "field inverse") + return count + + +def independent_factor_census(): + field = Field(2) + minima = {} + pairs = 0 + for middle in (2, 3, 4): + onto = [] + for entries in product(range(2), repeat=2 * middle): + x = matrix([entries[:middle], entries[middle:]]) + if rank(x, field) == 2: + onto.append(x) + for x, yt in product(onto, repeat=2): + target = multiply(x, transpose(yt), field) + key = target.rows + minima[key] = min(middle, minima.get(key, 5)) + pairs += 1 + require(len(minima) == 16, "factor census coverage") + for h in all_blocks(2, 2): + require(minima[h.rows] == 4 - rank(h, field), "independent middle-space minimum") + return pairs, len(minima) + + +def rejection_controls(): + field = Field(3) + defects = 0 + for sector, side in product((1, 2, 3), ("X", "Y")): + h = zero(2, 2) if sector == 3 else scale(identity(2), 2, field) + p, q, _ = build_pair(2, 2, h, field, (sector, side)) + result = inspect_pair(p, q, 2, 2, h, field) + require(result[0] < 4 and result[3][sector - 1] != (2, 2), "missing-map control") + defects += 1 + rejected = 0 + for mode in range(5): + try: + if mode == 0: + sector_products(2, 0, identity(2), field) + elif mode == 1: + sector_products(2, 2, identity(1), field) + elif mode == 2: + matrix([[0] * 49]) + elif mode == 3: + inverse(matrix([[1, 0], [1, 0]]), field) + else: + Field(6) + except ValueError: + rejected += 1 + else: + raise ValueError("malformed control accepted") + return defects, rejected + + +def sampled_cases(field): + count = 0 + for size, pivot in product((2, 3), range(1, field.q)): + for diagonal in range(field.q): + rows = [list(row) for row in scale(identity(size), diagonal, field).rows] + for i in range(size - 1): + rows[i][i + 1] = 1 + check_case(size, pivot, matrix(rows), field) + count += 1 + rows = [[0] * size for _ in range(size)] + for i in range(size - 1): + rows[i + 1][i] = 1 + rows[0][-1] = 1 + rows[1][-1] = 1 + check_case(size, pivot, matrix(rows), field) + count += 1 + return count + + +def receipt(): + directory = Path(__file__).resolve().parent + expected = {"README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"} + files = sorted(p.name for p in directory.iterdir() if p.is_file()) + require(set(files) == expected, "unexpected package files") + return {name: sha256((directory / name).read_bytes()).hexdigest() for name in files} + + +def main(): + exhaustive, sampled, scalar, field_checks = 0, 0, 0, 0 + by_field = {} + for order in (2, 3, 4, 5, 7, 8, 9): + field = Field(order) + field_checks += field_controls(field) + for pivot, h in product(range(1, order), range(order)): + dimension, _ = check_case(1, pivot, matrix([[h]]), field) + if h == 0: + expected = 4 + int(field.add[pivot][pivot] != 1) + elif h == pivot: + expected = 5 + int(pivot != 1) + else: + t0 = field.add[field.add[1][field.neg[field.add[pivot][pivot]]]][h] + expected = 3 + int(t0 != 0) + require(dimension == expected, "scalar predecessor specialization") + scalar += 1 + local_count = 0 + if order <= 5: + for pivot in range(1, order): + for h in all_blocks(2, order): + check_case(2, pivot, h, field) + local_count += 1 + exhaustive += local_count + by_field[str(order)] = local_count + sampled += sampled_cases(field) + pairs, targets = independent_factor_census() + defects, rejected = rejection_controls() + example = check_case(2, 2, matrix([[3, 1], [0, 3]]), Field(5)) + require(example == (7, (1, 2, 2, 2)), "nondiagonal example") + diagonal = check_case(2, 2, scale(identity(2), 3, Field(5)), Field(5)) + require(diagonal[0] == 6, "diagonal control") + print("PASS_SCALAR_BLOCK_SCHUR_DIMENSION") + print(json.dumps({"scalar_cases": scalar, "exhaustive_d2": exhaustive, + "d2_by_field": by_field, "sampled_d2_d3": sampled, + "field_triples": field_checks, "factor_pairs": pairs, + "factor_targets": targets, "missing_map_controls": defects, + "malformed_controls": rejected, "nondiagonal_example": example, + "python": platform.python_version(), "sha256": receipt()}, sort_keys=True)) + + +if __name__ == "__main__": + main()