diff --git a/research/unequal-pivot-schur-dimension/PROOF.md b/research/unequal-pivot-schur-dimension/PROOF.md new file mode 100644 index 0000000000..546fdc24fd --- /dev/null +++ b/research/unequal-pivot-schur-dimension/PROOF.md @@ -0,0 +1,112 @@ +# Unequal scalar pivots and a prescribed product + +This proof was produced by Nick Petalas. Apache-2.0. + +Let K be any field and prescribe distinct nonzero p,q in K and h in K. +For commuting idempotents P,Q with P11=p, Q11=q and (PQ)11=h, the least +ambient dimension for Schur-commutator rank two is + +```text +N(p,q,h) = 3 + [h in {0,p,q}] + [1-p-q+h != 0]. (1) +``` + +Brackets denote indicators of field equalities or inequalities. Every minimum +is attained. The hypothesis p!=q is essential. This answers Open next question +1 of Nick Petalas's #4771, whose equal-pivot theorem is a predecessor, not +part of the new claim. The sector construction follows ssafwann's #4671 and +Nick Petalas's #4746/#4771; the scalar factorization follows #4278. + +## Four sectors + +Let i:K -> V be coordinate inclusion and pi:V -> K coordinate projection. +Write E00=(I-P)(I-Q), E10=P(I-Q), E01=(I-P)Q and E11=PQ. +Their images Vj form a direct sum. Put Yj=Ej i and Xj=pi restricted to Vj. +The four scalar products are + +```text +t00=1-p-q+h, t10=p-h, t01=q-h, t11=h. (2) +``` + +Conversely, any four pairs of maps Xj,Yj with these products give pi i=1, +since the products sum to 1. On their direct sum, take the diagonal +projectors with sector eigenvalues 00,10,01,11. Choosing the first basis +vector to be i(1) and the remaining vectors in ker pi realizes the prescribed +coordinate entries. Thus sector constructions give actual full matrices. + +## Exact independence criterion + +The cited scalar factorization, valid for arbitrary nonzero p,q, uses + +```text +A = [PQ i - (h/q)Q i, P i/p - Q i/q], +B = [pi P/p - pi Q/q; -pi PQ + (h/q)pi Q]. +``` + +Here pi A=0 and Bi=0. In coordinates V=i(K) direct-sum ker pi, AB induces +the Schur commutator on ker pi. Its rank is two exactly when A and B both +have rank two. A rank-two A is injective and a rank-two B is surjective; +Bi=0 means B restricted to ker pi remains surjective. + +On each sector, A equals Yj times a row aj, and B equals a column bj times +Xj, as follows: + +```text +sector aj bj +00 (0,0) (0,0)^T +10 (0,1/p) (1/p,0)^T +01 (-h/q,-1/q) (-1/q,h/q)^T +11 ((q-h)/q,(q-p)/(pq)) ((q-p)/(pq),-(q-h)/q)^T +``` + +Each bj is the same invertible rotation of aj, namely (a2,-a1)^T. +Therefore the independence relations for A and B are identical, with Yj +and Xj respectively deciding whether a direction occurs. The determinants +of the pairs of rows are + +```text +det(a10,a01)=h/(pq), +det(a10,a11)=-(q-h)/(pq), +det(a01,a11)=(p-h)/(pq). (3) +``` + +All three rows are nonzero because p,q are nonzero and distinct. + +If h is outside {0,p,q}, all three active products t10,t01,t11 are nonzero. +Both maps in each sector are nonzero, and (3) guarantees independent +directions. These three sectors each require one dimension. + +If h=0, sectors 10 and 01 have nonzero products but parallel directions. +Sector 11 has zero product and its direction is independent of both. +Consequently rank two for both factors is equivalent to X11 and Y11 both +being nonzero. This sector requires two dimensions, in addition to the +one-dimensional sectors 10 and 01. + +If h=p, sectors 01 and 11 have nonzero products but parallel directions. +The independent direction is sector 10, whose product vanishes. Both +X10 and Y10 must be nonzero. The required dimensions are again 1+1+2. + +If h=q, the same argument uses nonzero-product sectors 10 and 11 and +zero-product sector 01. Both X01 and Y01 must be nonzero. These cases +are disjoint because p and q are nonzero and distinct. + +Sector 00 has no effect on either rank. Its product t00 requires exactly +one dimension when nonzero and can be omitted otherwise. Adding its +contribution gives the lower bound (1). + +## Attainment + +A nonzero scalar product t is realized in dimension one by Y=(1), X=(t). +A zero product for which both maps must be nonzero is realized in dimension +two by Y=(1,0)^T, X=(0,1). Omit every other zero-product sector. +These choices attain every sector lower bound above. Their products sum to +1, so the coordinate construction following (2) applies. The independence +conditions hold, hence the Schur commutator has rank two. This proves (1) +over every field. + +For example, over F3, p=1,q=2 gives dimensions five, five and four at +h=0,1,2 respectively. Over F5, p=2,q=3,h=4 gives dimension three. +The equal-pivot rule cannot be reused: at h=p with p!=q it is just one +zero-product sector, rather than the two required when p=q=h. + +This is a scoped algebraic theorem about one-coordinate Schur complements. +It gives neither a header frequency nor a paid physical implementation. diff --git a/research/unequal-pivot-schur-dimension/README.md b/research/unequal-pivot-schur-dimension/README.md new file mode 100644 index 0000000000..c34e329315 --- /dev/null +++ b/research/unequal-pivot-schur-dimension/README.md @@ -0,0 +1,132 @@ +# Exact Schur dimension for unequal scalar pivots + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof with finite corroboration. Over every field, +let P,Q be commuting idempotents with distinct nonzero scalar leading entries +p,q and prescribed leading product entry h. The exact least ambient dimension +attaining Schur-commutator rank two is + +```text +N(p,q,h) = 3 + [h in {0,p,q}] + [1-p-q+h != 0]. +``` + +Brackets denote indicators. Every minimum is attained by explicit matrices. +Over F3, p=1,q=2 gives minima five, five and four at h=0,1,2 respectively. +Over F5, p=2,q=3,h=4 gives dimension three. + +This answers Open next question 1 of +[PR #4771](https://github.com/CrocSwap/integer-mult-bounds/pull/4771), head +`22cb0bda57237d39d0e6944b232447d3a2809311`. That equal-pivot classification +is cited, not audited. Equality of pivots is a real boundary: at h=p with +p!=q, just one zero-product sector requires two dimensions; at p=q=h, +the predecessor requires two such sectors. No new kappa is claimed. + +## Proof and evidence + +[PROOF.md](PROOF.md) decomposes the commuting idempotents into four joint +eigenspaces, with compressed products `(1-p-q+h,p-h,q-h,h)`. The three +active directions have pair determinants `h/(pq)`, `-(q-h)/(pq)` and +`(p-h)/(pq)`. Away from the three endpoints, their nonzero products force +rank two. At each endpoint, the missing independent direction requires a +two-dimensional zero-product sector. This proves the lower bound and gives +an attaining construction over every field. + +The standalone verifier constructs full matrices for all **1,140** distinct +nonzero pivot/product triples over F3,F4,F5,F7,F8,F9. It checks idempotence, +commutation, both pivots, the product entry, literal Schur multiplication, +commutator rank and the scalar factorization. F4,F8,F9 use polynomial +quotient fields, not arithmetic modulo their orders. + +A separate optimization enumerates **14,270** scalar vector pairs and +**3,528** sector-map patterns. Every minimum agrees. Dimensions zero, one +and two realize every possible zero/nonzero scalar-map type, so this covers +the sector optimization rather than truncating an ambient-matrix search. +Eight rejection controls cover all three missing required endpoint sectors, +zero/equal pivots, an out-of-field product, a nonfield order and a mutated +projector. Explicit exceptions keep checks active under optimized Python. + +The finite-field and matrix helpers are adapted from Nick Petalas's #4771 +verifier, with exact provenance in SOURCES.json. The new constructions, +parameter domain and optimization implement the unequal-pivot theorem. +No predecessor executable is imported or invoked at runtime. + +## Reproduction + +From the repository root, using CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/unequal-pivot-schur-dimension/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/unequal-pivot-schur-dimension/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/unequal-pivot-schur-dimension +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/unequal-pivot-schur-dimension --check-source-history +``` + +Any CPython 3.12 interpreter can replace the local interpreter path. The direct +verifier writes nothing and prints `PASS_UNEQUAL_PIVOT_SCHUR_DIMENSION`, the +counts above and a generated SHA256 receipt for all six package files. +Metadata and source-history checks are separate from mathematical acceptance. +Each registered command has a 60-second timeout. Local measured durations were +0.113 seconds ordinary and 0.115 seconds optimized on CPython 3.12.15. +These are check durations, not performance comparisons. + +The selected source-binding orientation passed after its inputs were +materialized. Current guidance replaces the card's historical first command +with `scripts/research_selected_baseline.py`. This checks metadata only. + +## Scope and implementation bounds + +The proof covers one-coordinate deletion, distinct nonzero scalar pivots and +commuting field idempotents. Equal pivots are credited predecessor work. +Larger prescribed product blocks, nonfield rings and later elimination +states remain outside scope. Header production/frequency, physical caller, +restoration, stock, precision and the complete consumer bill are unknown. +No supplier admission, selected-frontier change or complete multiplication +theorem is supplied. Independent human and formal proof-kernel review are +unclaimed. No Lean, Docker or selected operator replay was run. + +The verifier has no recursion, subprocess, callback or generated code. Its +six fixed field domains have order at most nine; matrices have at most five +rows, helper capacities permit six rows, and elimination has at most twelve +columns. Scalar vector scans total at most 1+9^2+9^4 iterations per field; each pattern product +has four factors of at most four types, and receipts read six files of at +most 100,000 bytes each. No result matrices accumulate across triples. +Functions stay below 60 physical lines. Both registered modes use warnings +as errors. No external static analyzer is installed or claimed. + +Power of Ten rule 3 deviation: CPython and its standard library allocate +dynamically. The fixed domains and stated collection limits bound live data, +but do not prohibit allocation after initialization. The verifier owns no +external mutable resources. Reassess capacities before exposing search sizes +as external inputs. + +## Open next questions + +1. Determine the least dimension for unequal scalar block pivots pI_d,qI_d + and prescribed leading product H. Begin with a nondiagonal 2-by-2 H. + Scalar nonvanishing no longer determines sector-map ranks; no block theorem + is provided here. +2. Count complete headers realizing one prescribed unequal-pivot profile. + Begin with the F3 p=1,q=2,h=2 construction and specify the weighted header + ensemble. Existence alone does not give frequency or paid production cost. + +Structured questions, first steps and blockers are in [TASK.json](TASK.json). + +## Credit and task scope + +Nick Petalas's #4771 supplies the explicit open question, equal-pivot theorem +and finite-field/matrix helpers. Nick Petalas's #4746 and ssafwann's +#4671/#4657 supply earlier identity-pivot sector constructions. Nick +Petalas's #4278/#4597 supplies scalar and ordered block factorizations. +Ryanson Jonathan's #4609/#4617 and lee-phys's #4634 supply preceding +small-field and block sharpness examples. 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 settles a new prescribed-boundary minimum without extending a +physical construction. Canonical main, source pins and overlap limitations +are recorded in TASK.json and SOURCES.json. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131498). diff --git a/research/unequal-pivot-schur-dimension/SOURCES.json b/research/unequal-pivot-schur-dimension/SOURCES.json new file mode 100644 index 0000000000..33494c0da3 --- /dev/null +++ b/research/unequal-pivot-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/scalar-pivot-schur-dimension/verify.py", + "usage": "provenance", + "git_blob": "dcaacaee1b8b36bc1afcac1f192d1d7d3aba00ca", + "sha256": "136cf14c409556a76b344aa99ba3ef58c8612d7cd87f7ea456ecd97181cfb76a" + }, + { + "path": "research/schur-commutator-criterion/README.md", + "usage": "provenance", + "git_blob": "6b37342de04f5c42c198dd6ba14cea9845be6f05", + "sha256": "5616da2e708a8425f1bf0bf5c89c236ef8ed0a23d0544d30ae2142ffe167dc01" + } + ] +} diff --git a/research/unequal-pivot-schur-dimension/TASK.json b/research/unequal-pivot-schur-dimension/TASK.json new file mode 100644 index 0000000000..ac688e2550 --- /dev/null +++ b/research/unequal-pivot-schur-dimension/TASK.json @@ -0,0 +1,210 @@ +{ + "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 least ambient dimension for commuting field idempotents with distinct nonzero scalar pivots p,q, prescribed leading product h, and Schur-commutator rank two.", + "scope_change_reason": "Answer Open next question 1 of PR4771 by removing equality of scalar pivots. This is an original written algebraic side proof, not formalization or an audit.", + "bottleneck_link": "Separates scalarity from equality in a common-header Schur boundary. Physical header production and complete consumer costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified exact dimension law; leave block-pivot and header-frequency extensions open.", + "outcome": "completed", + "evidence": "PROOF.md proves N=3+[h in {0,p,q}]+[1-p-q+h!=0] with attainment. verify.py constructs 1140 parameter triples, enumerates 14270 scalar vector pairs and 3528 sector patterns, and exercises eight rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Unequal scalar block pivots pI_d,qI_d with prescribed product H", + "why_it_matters": "Matrix products couple sector-map ranks, so scalar nonvanishing does not decide the attainable boundary.", + "first_step": "Start with one nondiagonal 2-by-2 product H and derive the sector rank constraints.", + "blocked_by": "Only one-coordinate scalar deletion is proved here." + }, + { + "question": "Complete-header frequency for a prescribed unequal-pivot profile", + "why_it_matters": "Dimension feasibility alone does not provide header frequency or a paid header producer.", + "first_step": "Specify a weighted complete-header ensemble for the F3 p=1,q=2,h=2 construction.", + "blocked_by": "No header-counting or physical producer model is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131498", + "playbook": "Investigation", + "preserved_checkout": { + "branch": "research/w1-1022f-binary-chain-distance", + "head": "ecd0e3512ea3f108112ea4c127dd4ced2369b7a0", + "prior_commits": [ + "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "6044f37b1f75a57f5fea6d17077b6985893062c1", + "4f19cedcd8d81e4a2359449309fa6e9f17dfd22e" + ] + }, + "overlap": { + "checked_at": "2026-10-22T19:47:23.004652+00:00", + "main": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "coverage": { + "open_prs": { + "fetched_at": "2026-10-22T19:43:18.142903+00:00", + "complete_pagination": true, + "records": 299 + }, + "discussions": { + "fetched_at": "2026-10-22T19:44:03.572364+00:00", + "complete_pagination": true, + "records": 3709 + } + }, + "local_coverage": "Helper searched 46 of 6319 tracked notes. Separate git grep searches all origin/main research READMEs. Sparse coverage is not proof of novelty.", + "terms": [ + "unequal pivots", + "distinct scalar pivot", + "N(p,q,h)", + "1-p-q+h" + ], + "related_open_same_object": [], + "limitations": "No exhaustive code-diff or unpublished-result search. Full open PR/discussion snapshot coverage does not imply exhaustive novelty.", + "final_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "final_checkpoint_utc": "2026-10-22T19:48:16.975149+00:00", + "final_result": "No open Schur PR returned by title/body search. Main searches found only the credited PR4771 open question. Later claims explicitly separate unequal scalar pivots from the common scalar block question." + }, + "checkpoint": { + "main": "624de9dc66858af0945e5f8a0942488d62280d43", + "selected_kappa": "60403/20000000", + "selected_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "orientation_note": "Initial baseline attempts found sparse missing inputs. After git sparse-checkout add materialized the selected closure, the metadata-only baseline passed." + }, + "citations": [ + { + "pr": 4771, + "author": "Nick Petalas", + "head": "22cb0bda57237d39d0e6944b232447d3a2809311", + "contribution": "Explicit unequal-pivot open question, equal-pivot theorem, finite-field and matrix helper code.", + "usage": "The actual retained source bytes at base_commit are pinned in SOURCES.json; no pending head object is required." + }, + { + "pr": 4278, + "author": "Nick Petalas", + "contribution": "Scalar Schur commutator factorization for arbitrary nonzero pivots.", + "usage": "Cited theorem; retained README is pinned as provenance." + }, + { + "pr": 4746, + "author": "Nick Petalas", + "contribution": "All-field identity-pivot predecessor." + }, + { + "pr": 4671, + "author": "ssafwann", + "contribution": "Binary dimension theorem and four-sector method." + }, + { + "pr": 4657, + "author": "ssafwann", + "contribution": "Identity-pivot precursor." + }, + { + "pr": 4597, + "author": "Nick Petalas", + "contribution": "Ordered block factorization." + }, + { + "pr": 4609, + "author": "Ryanson Jonathan", + "contribution": "Preceding small-field sharpness examples." + }, + { + "pr": 4617, + "author": "Ryanson Jonathan", + "contribution": "Preceding binary block construction." + }, + { + "pr": 4634, + "author": "lee-phys", + "contribution": "Unrestricted block sharpness examples." + } + ], + "verification": { + "python": "3.12.15", + "direct_seconds": [ + 0.11342070798855275, + 0.11543416697531939 + ], + "normal_and_optimized": "pass", + "largest_function_lines": 33, + "syntax": "pass", + "static_analyzer": "not installed", + "selected_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY" + } +} diff --git a/research/unequal-pivot-schur-dimension/VERIFY.json b/research/unequal-pivot-schur-dimension/VERIFY.json new file mode 100644 index 0000000000..79fd1cf3af --- /dev/null +++ b/research/unequal-pivot-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": 60, + "checks": "1140 attaining unequal-pivot triples over six fields, 14270 vector pairs, 3528 sector-map patterns, literal Schur products and eight rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "1140 attaining unequal-pivot triples over six fields, 14270 vector pairs, 3528 sector-map patterns, literal Schur products and eight rejection controls." + } + ] +} diff --git a/research/unequal-pivot-schur-dimension/verify.py b/research/unequal-pivot-schur-dimension/verify.py new file mode 100644 index 0000000000..58e2e1cd5f --- /dev/null +++ b/research/unequal-pivot-schur-dimension/verify.py @@ -0,0 +1,300 @@ +#!/usr/bin/env python3 +"""Unequal-pivot Schur minima, produced by Nick Petalas. Apache-2.0. + +Finite-field/matrix helpers adapted from Nick Petalas, PR4771 verify.py. +""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digits(value, prime, degree): + return [(value // prime**i) % prime for i in range(degree)] + + +def field_product(a, b, prime, modulus): + degree = len(modulus) - 1 + left, right = digits(a, prime, degree), digits(b, prime, degree) + coefficients = [0] * (2 * degree - 1) + for i in range(degree): + for j in range(degree): + coefficients[i + j] += left[i] * right[j] + for i in range(2 * degree - 2, degree - 1, -1): + for j in range(degree): + coefficients[i - degree + j] -= coefficients[i] * modulus[j] + return sum((coefficients[i] % prime) * prime**i for i 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") + prime, modulus = definitions[order] + self.q = order + degree = len(modulus) - 1 + self.add = [[sum(((a // prime**i + b // prime**i) % prime) + * prime**i for i in range(degree)) + for b in range(order)] for a in range(order)] + self.mul = [[field_product(a, b, prime, modulus) + for b in range(order)] for a in range(order)] + self.neg = [self.add[a].index(0) for a in range(order)] + self.inv = [0] + [self.mul[a].index(1) for a in range(1, order)] + require(all(self.mul[a][self.inv[a]] == 1 for a in range(1, order)), + "field inverses") + + def sub(self, a, b): + return self.add[a][self.neg[b]] + + def dot(self, left, right): + require(len(left) == len(right) <= 12, "dot capacity") + value = 0 + for a, b in zip(left, right, strict=True): + value = self.add[value][self.mul[a][b]] + return value + + +def identity(size): + require(0 <= size <= 6, "identity capacity") + return [[int(i == j) for j in range(size)] for i in range(size)] + + +def mm(field, left, right): + require(1 <= len(left) <= 6 and 1 <= len(right) <= 6, "matrix capacity") + require(all(len(row) == len(right) for row in left), "matrix shape") + columns = list(zip(*right, strict=True)) + return [[field.dot(row, column) for column in columns] for row in left] + + +def subtract(field, left, right): + return [[field.sub(a, b) for a, b in zip(x, y, strict=True)] + for x, y in zip(left, right, strict=True)] + + +def eliminate(field, matrix): + require(1 <= len(matrix) <= 6 and 1 <= len(matrix[0]) <= 12, + "elimination capacity") + width = len(matrix[0]) + require(all(len(row) == width for row in matrix), "ragged matrix") + result = [row[:] for row in matrix] + pivot_row = 0 + for column in range(width): + candidates = [i for i in range(pivot_row, len(result)) if result[i][column]] + if not candidates: + continue + index = candidates[0] + result[pivot_row], result[index] = result[index], result[pivot_row] + scale = field.inv[result[pivot_row][column]] + result[pivot_row] = [field.mul[scale][a] for a in result[pivot_row]] + for i in range(len(result)): + if i != pivot_row: + scale = result[i][column] + result[i] = [field.sub(a, field.mul[scale][b]) + for a, b in zip(result[i], result[pivot_row], strict=True)] + pivot_row += 1 + if pivot_row == len(result): + break + return result, pivot_row + + +def inverse(field, matrix): + size = len(matrix) + unit = identity(size) + augmented = [row + unit[i] for i, row in enumerate(matrix)] + reduced, rank = eliminate(field, augmented) + require(rank == size and [row[:size] for row in reduced] == unit, + "singular basis") + result = [row[size:] for row in reduced] + require(mm(field, matrix, result) == unit, "inverse product") + return result + + +def pair_types(field): + """Enumerate every scalar X,Y type through dimensions zero, one and two.""" + options = [{} for _ in range(field.q)] + count = 0 + for size in range(3): + for vector in product(range(field.q), repeat=2 * size): + x, y = vector[:size], vector[size:] + target = field.dot(x, y) + flags = (any(x), any(y)) + options[target].setdefault(flags, size) + count += 1 + return options, count + + +def products(field, p, q, h): + require(0 < p < field.q and 0 < q < field.q and p != q, + "distinct nonzero pivots required") + require(0 <= h < field.q, "invalid product") + return [field.add[field.sub(field.sub(1, p), q)][h], + field.sub(p, h), field.sub(q, h), h] + + +def minimum(field, p, q, h): + return 3 + int(h in (0, p, q)) + int(products(field, p, q, h)[0] != 0) + + +def directions(field, p, q, h): + ip, iq = field.inv[p], field.inv[q] + hq = field.mul[h][iq] + return [[0, 0], [0, ip], [field.neg[hq], field.neg[iq]], + [field.sub(1, hq), field.sub(ip, iq)]] + + +def construct(field, p, q, h, omit_required=False): + targets = products(field, p, q, h) + required = 3 if h == 0 else 1 if h == p else 2 if h == q else -1 + inclusion, projection, p_mask, q_mask, sizes = [], [], [], [], [] + for sector, target in enumerate(targets): + size = 1 if target else 2 if sector == required and not omit_required else 0 + sizes.append(size) + if size: + inclusion.extend([1] + [0] * (size - 1)) + projection.extend([target] if size == 1 else [0, 1]) + p_mask.extend([int(sector in (1, 3))] * size) + q_mask.extend([int(sector in (2, 3))] * size) + require(field.dot(projection, inclusion) == 1, "compression sum") + size = len(inclusion) + anchor = next(i for i in range(size) if projection[i]) + columns = [inclusion] + for j in range(size): + if j != anchor: + vector = [int(i == j) for i in range(size)] + vector[anchor] = field.neg[field.mul[projection[j]][field.inv[projection[anchor]]]] + columns.append(vector) + basis = [list(row) for row in zip(*columns, strict=True)] + back = inverse(field, basis) + left = mm(field, back, [[field.mul[p_mask[i]][a] for a in row] + for i, row in enumerate(basis)]) + right = mm(field, back, [[field.mul[q_mask[i]][a] for a in row] + for i, row in enumerate(basis)]) + return left, right, sizes + + +def schur(field, matrix): + require(matrix[0][0] != 0, "zero Schur pivot") + scale = field.inv[matrix[0][0]] + return [[field.sub(matrix[i][j], field.mul[field.mul[matrix[i][0]][scale]][matrix[0][j]]) + for j in range(1, len(matrix))] for i in range(1, len(matrix))] + + +def verify_pair(field, p, q, h, left, right): + pq = mm(field, left, right) + require(mm(field, left, left) == left and mm(field, right, right) == right, + "idempotence") + require(pq == mm(field, right, left), "commutation") + require(left[0][0] == p and right[0][0] == q and pq[0][0] == h, + "prescribed compression") + s, t = schur(field, left), schur(field, right) + commutator = subtract(field, mm(field, s, t), mm(field, t, s)) + ip, iq = field.inv[p], field.inv[q] + hq = field.mul[h][iq] + a = [[field.sub(pq[i][0], field.mul[hq][right[i][0]]), + field.sub(field.mul[ip][left[i][0]], field.mul[iq][right[i][0]])] + for i in range(1, len(left))] + b = [[field.sub(field.mul[ip][left[0][j]], field.mul[iq][right[0][j]]) + for j in range(1, len(left))], + [field.sub(field.mul[hq][right[0][j]], pq[0][j]) + for j in range(1, len(left))]] + require(mm(field, a, b) == commutator, "ordered scalar factorization") + return eliminate(field, commutator)[1] + + +def enumerated_minimum(field, p, q, h, options): + rows = directions(field, p, q, h) + choices = [list(options[t].items()) for t in products(field, p, q, h)] + best, patterns = 99, 0 + for combination in product(*choices): + x_rows = [row if flags[0] else [0, 0] + for row, (flags, _) in zip(rows, combination, strict=True)] + y_rows = [row if flags[1] else [0, 0] + for row, (flags, _) in zip(rows, combination, strict=True)] + if eliminate(field, x_rows)[1] == eliminate(field, y_rows)[1] == 2: + best = min(best, sum(size for _, size in combination)) + patterns += 1 + require(best != 99, "no attaining pattern") + return best, patterns + + +def controls(): + field = Field(5) + count = 0 + for h in (0, 2, 3): + left, right, _ = construct(field, 2, 3, h, omit_required=True) + require(verify_pair(field, 2, 3, h, left, right) < 2, + "necessary zero-product sector omitted undetected") + count += 1 + for p, q, h in ((0, 2, 1), (2, 2, 1), (2, 3, 5)): + try: + products(field, p, q, h) + except ValueError: + count += 1 + else: + raise ValueError("invalid parameters accepted") + try: + Field(6) + except ValueError: + count += 1 + else: + raise ValueError("nonfield order accepted") + left, right, _ = construct(field, 2, 3, 4) + require(minimum(field, 2, 3, 4) == 3, "dimension-three fixture") + left[0][0] = 1 + try: + verify_pair(field, 2, 3, 4, left, right) + except ValueError: + count += 1 + else: + raise ValueError("mutated projector accepted") + require(minimum(Field(3), 1, 2, 0) == 5, "endpoint correction fixture") + require(minimum(Field(3), 1, 2, 2) == 4, "zero-00 fixture") + return count + + +def main(): + cases, patterns, vector_pairs = 0, 0, 0 + histograms = {} + for order in (3, 4, 5, 7, 8, 9): + field = Field(order) + options, count = pair_types(field) + vector_pairs += count + histogram = {} + for p, q, h in product(range(1, order), range(1, order), range(order)): + if p == q: + continue + expected = minimum(field, p, q, h) + observed, count = enumerated_minimum(field, p, q, h, options) + left, right, sizes = construct(field, p, q, h) + require(sum(sizes) == observed == expected, "dimension minimum") + require(verify_pair(field, p, q, h, left, right) == 2, "sharp commutator") + require(minimum(field, q, p, h) == expected, "pivot exchange symmetry") + histogram[expected] = histogram.get(expected, 0) + 1 + cases += 1 + patterns += count + histograms[order] = histogram + count = controls() + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + hashes = {} + for name in names: + path = root / name + require(path.stat().st_size <= 100_000, "receipt file capacity") + hashes[name] = sha256(path.read_bytes()).hexdigest() + print(json.dumps({"status": "PASS_UNEQUAL_PIVOT_SCHUR_DIMENSION", + "constructed_triples": cases, "sector_patterns": patterns, + "enumerated_vector_pairs": vector_pairs, "minima": histograms, + "rejection_controls": count, "sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()