diff --git a/research/scalar-pivot-schur-dimension/PROOF.md b/research/scalar-pivot-schur-dimension/PROOF.md new file mode 100644 index 0000000000..ebfb0d1b1c --- /dev/null +++ b/research/scalar-pivot-schur-dimension/PROOF.md @@ -0,0 +1,142 @@ +# Exact scalar-pivot dimension + +This proof was produced by Nick Petalas. Apache-2.0. + +Let K be any field, let lambda be nonzero, and prescribe h in K. Among +commuting idempotents P,Q on K^n with P11=Q11=lambda and (PQ)11=h, let +N(lambda,h) be the least n for which their one-coordinate Schur complements +have commutator rank two. Then + +```text + 4 + [1-2lambda != 0], h=0, +N(lambda,h) = 5 + [lambda != 1], h=lambda, + 3 + [1-2lambda+h != 0], otherwise. +``` + +The brackets denote the indicator of a field inequality. The first two cases +are disjoint because lambda is nonzero. Every minimum is attained. Matrices +need not be symmetric. This is a scalar-pivot theorem, not a theorem about a +prescribed matrix product for a larger deleted block. + +## Sector compression + +Put U=K, V=K^n. Let i:U -> V be coordinate inclusion and pi:V -> U the +coordinate projection. Since pi i=1, V=i(U) direct-sum ker pi. +The four joint eigenspace projectors are + +```text +E00=(I-P)(I-Q), E10=P(I-Q), E01=(I-P)Q, E11=PQ. +``` + +These mutually annihilating projectors sum to I in every characteristic. Set +Vj=im Ej, rj=dim Vj, Yj=Ej i and Xj=pi restricted to Vj. Their products are + +```text +t00=X00 Y00=1-2lambda+h, +t10=X10 Y10=lambda-h, +t01=X01 Y01=lambda-h, +t11=X11 Y11=h. (1) +``` + +They sum to 1. Conversely, any such four pairs of maps with these products +give pi i=1. Equip their direct sum with diagonal P0,Q0 having eigenvalues +00,10,01,11. Complete i to a basis [i N], with N a basis of ker pi. +Conjugation into this basis gives commuting idempotents with exactly the +required coordinate pivots and leading product. This standard sector +construction is the predecessor method of ssafwann's #4671 and Nick Petalas's +#4746. The products and sharpness conditions below change with lambda. + +## Rank-two criterion + +Use the scalar factorization from Nick Petalas's #4278, with equal pivots +lambda. Its ambient factors are + +```text +A = [PQ i - (h/lambda)Q i, (P-Q)i/lambda] : K^2 -> V, +B = [pi(P-Q)/lambda; -pi PQ + (h/lambda)pi Q] : V -> K^2. +``` + +They satisfy pi A=0 and Bi=0. The Schur commutator is the product of A's +coordinates in ker pi and B's restriction to ker pi. Therefore it has rank +two exactly when A has rank two and B has rank two. Indeed, a rank-two A is +injective and a rank-two B is onto. The identity Bi=0 and the displayed direct +sum imply that B restricted to ker pi is still onto. + +For each sector, A is Yj times the following row, and B is the following +column times Xj: + +```text +sector row for A column for B +00 (0,0) (0,0)^T +10 (0,1/lambda) (1/lambda,0)^T +01 (-h/lambda,-1/lambda) (-1/lambda,h/lambda)^T +11 ((lambda-h)/lambda,0) (0,-(lambda-h)/lambda)^T +``` + +Since the sectors form a direct sum, rank A is the span dimension of the +listed rows whose Yj is nonzero. Similarly, rank B is the span dimension of +the listed columns whose Xj is nonzero. There is no cross-sector cancellation. + +If h is neither 0 nor lambda, all three active products in (1) are nonzero. +Thus Xj and Yj are nonzero in sectors 10,01,11. The 10 and 01 rows are +independent since h!=0; the corresponding columns are also independent. +Both factors automatically have rank two. + +If h=0, A's first column is supported only in sector 11. It is nonzero +exactly when Y11 is nonzero. The nonzero products t10=t01=lambda already +give the second independent direction. The dual statement for B requires +X11 nonzero. Hence sharpness is exactly X11!=0 and Y11!=0. + +If h=lambda, A's first column is supported only in sector 01. Its 01 row +is proportional to (lambda,1), whereas its only possible independent row is +the 10 row. The 11 row vanishes. Therefore rank A=2 exactly when Y01 and +Y10 are both nonzero. Dually, rank B=2 exactly when X01 and X10 are both +nonzero. The nonzero t11=lambda already ensures a nonzero 11 sector. + +These are exact replacement criteria for the identity-pivot six-map argument; +they do not assume that all three sectors always require both maps. + +## Lower bounds and attainment + +One scalar compressed product t!=0 needs at least one dimension. If t=0 +and both X and Y must be nonzero, at least two dimensions are necessary: +nonzero maps between one-dimensional spaces have nonzero product. +If neither map is required, a zero product needs no dimension. + +For h outside {0,lambda}, sectors 10,01,11 each need one dimension, and +sector 00 needs exactly [1-2lambda+h!=0]. This gives the third case. +For h=0, sectors 10,01 need one each, sector 11 needs two, and sector 00 +needs [1-2lambda!=0]. This gives the first case. +For h=lambda, sectors 10,01 need two each, sector 11 needs one, and sector +00 needs [1-lambda!=0]. This gives the second case. + +Attain all these bounds by choosing, independently in each sector, + +```text +nonzero t: Y=(1), X=(t), +zero t, both maps required: Y=(1,0)^T, X=(0,1), +zero t, no maps required: zero-dimensional sector. +``` + +The products are (1), so their sum is 1 and the coordinate construction +above applies. Each stated sharpness criterion holds. This proves existence +at exactly the lower bound over every field, and completes the proof. + +## Consequences and boundary + +For a nonidentity scalar pivot lambda, the prescribed product h=lambda +forces dimension six. Thus substituting lambda into the old identity-pivot +formula, which would predict five for an endpoint product, is invalid. +For example, over F3, lambda=h=2 has exact minimum six, whereas h=0 or h=1 +with the same pivot has exact minimum four. + +The generic minimum three occurs exactly when h=2lambda-1 avoids 0 and +lambda. Such lambda exists over every finite field with at least four +elements. F2 and F3 give minima five and four respectively when lambda,h +are unrestricted. The F2/F3/F5 unrestricted minima were already established +by Ryanson Jonathan's #4609. The contribution here is the exact dependence +on both prescribed scalar values over every field. + +No header frequency, later Schur-state law, physical caller, supplier +admission, new kappa or complete multiplication theorem follows. Uniform +physical and analytic costs remain separate unknown obligations. diff --git a/research/scalar-pivot-schur-dimension/README.md b/research/scalar-pivot-schur-dimension/README.md new file mode 100644 index 0000000000..7ccd8ef743 --- /dev/null +++ b/research/scalar-pivot-schur-dimension/README.md @@ -0,0 +1,139 @@ +# Exact Schur dimension for a prescribed scalar pivot and product + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped algebraic proof with finite corroboration. Let P,Q be +commuting idempotents over any field, with the same nonzero scalar first +entry lambda and prescribed first entry h of PQ. The least ambient dimension +in which their one-coordinate Schur complements have commutator rank two is + +```text + 4 + [1-2lambda != 0], h=0, +N(lambda,h) = 5 + [lambda != 1], h=lambda, + 3 + [1-2lambda+h != 0], otherwise. +``` + +Here brackets mean the indicator of a field inequality. Every minimum is +attained by the explicit sector construction in [PROOF.md](PROOF.md). +In particular, a nonidentity pivot with h=lambda requires exactly six +dimensions. Over F3, lambda=h=2 requires six, while the same pivot with +h=0 or h=1 requires four. Nonidentity pivots therefore change the endpoint +dimension law, rather than simply replacing the symbol 1 in the old formula. + +This answers the scalar part of Open next question 1 in +[PR #4746](https://github.com/CrocSwap/integer-mult-bounds/pull/4746), pinned at +`5f014560d6225cae17598ac479fb29d2947d8e6b`. Its identity-pivot formula, +ssafwann's binary theorem in #4671 and Ryanson Jonathan's earlier unrestricted +small-field minima in #4609 are predecessor results, not new claims here. +The new result is the exact dependence on both prescribed scalars, including +the replacement sharpness criterion, over every field. No new kappa. + +## Evidence and reproduction + +The written proof decomposes the commuting projectors into their four joint +eigenspaces. The compression products are +`(1-2lambda+h,lambda-h,lambda-h,h)`. Nick Petalas's #4278 factorization +reduces sharpness to two explicit rank-two conditions. Their zero-product +sectors need two dimensions precisely in the endpoint cases above. + +The independently written standard-library verifier imports no predecessor +executable. It constructs actual P,Q and checks idempotence, commutation, +both pivots, the prescribed product, direct Schur multiplication and the +ordered factor identity. It covers every nonzero lambda and every h over +F2,F3,F4,F5,F7,F8,F9, totaling **210 parameter pairs**. This includes the +known identity-pivot specialization as a calibration case. + +A separate finite optimization enumerates **14,291 scalar vector pairs** +through sector dimensions zero, one and two, recording every possible +zero/nonzero map type and its minimum dimension. It evaluates **1,212 +four-sector patterns** and matches the formula in all 210 cases. Two +dimensions suffice to realize any scalar map type, as explained in the +proof; this is not a truncated search over ambient matrices. + +Seven controls detect omitted necessary zero-product sectors in both +endpoint cases, a zero pivot, an incorrect sector sign, a mutated projector, +a singular coordinate basis and an unsupported nonfield order. F4,F8,F9 +use polynomial quotient fields, not arithmetic modulo their orders. All +checks remain enabled under optimized Python. + +From the repository root, using CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/scalar-pivot-schur-dimension/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/scalar-pivot-schur-dimension/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/scalar-pivot-schur-dimension +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/scalar-pivot-schur-dimension --check-source-history +``` + +Another CPython 3.12 path may replace the local path. The direct verifier +writes nothing and emits `PASS_SCALAR_PIVOT_SCHUR_DIMENSION` with a generated +receipt binding all six package files by SHA256. The metadata runner and +publication preflight are separate from the mathematical claim. + +The selected source-binding orientation passed after its declared inputs +were materialized. Its source hashes and budget metadata are consistent; +no selected scientific replay was run. The card's historical first command +has been replaced by `scripts/research_selected_baseline.py` in current +repository guidance. + +## Scope and code constraints + +The theorem concerns one scalar deletion, equal nonzero pivots and commuting +idempotents over a field. Unequal pivots, larger deleted blocks with prescribed +matrix product, coefficient rings, later-state transitions and header +probabilities are outside scope. Producer selection, header emission, +dispatch, dirty restoration, stock, precision and the complete consumer +cost are unknown. No physical supplier admission, selected-frontier change +or complete multiplication theorem is claimed. Independent human and formal +proof-kernel review are unclaimed. Lean, Docker and selected cold replay were +not run. All registered local checks are required before publication. + +The fixed verifier uses seven fields of size at most nine. Matrices have at +most six rows, elimination at most twelve columns, and vector scans at most +q^4=6561 iterations per field. Each pattern product has four finite factors, +each containing at most four map types. Only counters, small field tables +and the current construction persist. There is no recursion, subprocess, +code generation or user-controlled input. Functions stay below 60 physical +lines. Explicit exceptions enforce bounds and invariants under -O. Warnings +are errors in both registered commands; syntax and function lengths are +also inspected locally. No external static analyzer is installed or claimed. + +Power of Ten rule 3 deviation: CPython arithmetic, iterators and collections +allocate dynamically. This bounded standalone verifier cannot prohibit +runtime allocation. The fixed field, vector, matrix and six-file receipt +capacities bound live data; no state accumulates across the 210 cases. +Both registered modes exercise the bounds and seven rejection controls. +Reassess fixed storage and input validation before adding larger domains +or an external parameter interface. The deviation is confined to this +verifier, which owns no external mutable resources. + +## Open next questions + +1. Determine the minimum for unequal nonzero scalar pivots p,q with + prescribed h. The same four-sector method starts with products + `(1-p-q+h,p-h,q-h,h)`, but its independent-direction cases need a new + classification. This would separate equality of pivots from scalarity. +2. Determine the prescribed-matrix-product minimum for a common nonidentity + scalar block lambda I_d. Start with one nondiagonal H; scalar sector-map + nonvanishing no longer determines rank. This theorem gives no all-d bound. +3. Count complete headers for one fixed nonidentity scalar profile. Dimension + feasibility does not provide frequency or a paid header producer. Specify + the header ensemble before deriving a count or claiming a physical gain. + +## Credit and task scope + +Nick Petalas's #4746 supplies the explicit open question and all-field +identity-pivot predecessor. ssafwann's #4671/#4657 supplies the binary +dimension theorem, six-map method and split sector construction. +Nick Petalas's #4278/#4597 supplies the scalar and ordered block Schur +factorizations. Ryanson Jonathan's #4609/#4617 and lee-phys's #4634 supply +preceding 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 theorem. The work supplies a new prescribed-boundary dimension law, +without auditing another contributor or expanding a physical mechanism. +Exact citations, source provenance, overlap coverage, the advance claim and +the preserved checkout state are recorded in TASK.json and SOURCES.json. diff --git a/research/scalar-pivot-schur-dimension/SOURCES.json b/research/scalar-pivot-schur-dimension/SOURCES.json new file mode 100644 index 0000000000..47254b197a --- /dev/null +++ b/research/scalar-pivot-schur-dimension/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b", + "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/scalar-pivot-schur-dimension/TASK.json b/research/scalar-pivot-schur-dimension/TASK.json new file mode 100644 index 0000000000..c0ae9bec85 --- /dev/null +++ b/research/scalar-pivot-schur-dimension/TASK.json @@ -0,0 +1,243 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b", + "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 equal prescribed nonzero scalar pivot lambda, prescribed scalar leading product h and Schur-commutator rank two.", + "scope_change_reason": "Answer the scalar case of the explicit open question in PR4746 by changing the identity-pivot premise. This is an original written algebraic side theorem, not a formalization or audit.", + "bottleneck_link": "Clarifies how a changed shared-header boundary alters attainable Schur noncommutativity. Header probabilities and full physical costs remain unpriced.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original dimension classification; leave block and unequal-pivot extensions open.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-field classification and attaining construction. verify.py checks all 210 parameter pairs over seven fields, 14291 vector pairs, 1212 sector patterns and seven controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Unequal nonzero scalar pivots with prescribed product", + "why_it_matters": "Separates equality of pivots from scalarity.", + "first_step": "Classify directions for sector products (1-p-q+h,p-h,q-h,h).", + "blocked_by": "Current proof fixes equal pivots." + }, + { + "question": "Common nonidentity scalar blocks lambda I_d with prescribed H", + "why_it_matters": "Matrix products couple sector ranks.", + "first_step": "Derive the map-rank criterion for one nondiagonal H.", + "blocked_by": "No all-d nonidentity-pivot theorem is supplied." + }, + { + "question": "Complete-header frequency for one nonidentity scalar profile", + "why_it_matters": "Dimension feasibility does not determine a paid header cover.", + "first_step": "Specify a fixed sector profile and weighted header domain.", + "blocked_by": "Counting and physical producer costs remain open." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131156", + "playbook": "Autonomous local run", + "preserved_checkout": { + "branch": null, + "detached_head": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "prior_commits": [ + "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "6044f37b1f75a57f5fea6d17077b6985893062c1", + "4f19cedcd8d81e4a2359449309fa6e9f17dfd22e", + "f626db5c3a3d781d8f7695038776c621651f75e1" + ] + }, + "checkpoint": { + "initial_main": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "branch_base": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b", + "reason": "Shared origin/main advanced before branch creation; archive base read with unchanged task/priorities/selection guidance. The claim gave the earlier intake checkpoint; this records the actual branch base.", + "priority_revision": 7, + "selected_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "selected_kappa": "60403/20000000" + }, + "citations": [ + { + "pr": 4746, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4746", + "head": "5f014560d6225cae17598ac479fb29d2947d8e6b", + "author": "Nick Petalas", + "contribution": "Explicit nonidentity-pivot open question and all-field identity theorem.", + "usage": "Cited theorem/context only; no runtime dependency or ancestry claim." + }, + { + "pr": 4671, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4671", + "head": "8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9", + "author": "ssafwann", + "contribution": "Binary fixed-product theorem and split-sector method.", + "usage": "Cited theorem/context only; no runtime dependency or ancestry claim." + }, + { + "pr": 4597, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4597", + "head": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb", + "author": "Nick Petalas", + "contribution": "Ordered block factorization.", + "usage": "Cited theorem/context only; no runtime dependency or ancestry claim." + }, + { + "pr": 4609, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4609", + "head": "eb5ccf9288808d973551e6264300d30d2f6e48a0", + "author": "Ryanson Jonathan", + "contribution": "Known unrestricted small-field minima.", + "usage": "Cited theorem/context only; no runtime dependency or ancestry claim." + }, + { + "pr": 4634, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4634", + "head": "9f053f7051e5fc3327d4337bb4bd8ac52cf5fcd0", + "author": "lee-phys", + "contribution": "Unrestricted binary block-pivot construction.", + "usage": "Cited theorem/context only; no runtime dependency or ancestry claim." + }, + { + "pr": 4657, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4657", + "head": "b79f90bc8d839a4998a40b10bcb437e87baa8397", + "author": "ssafwann", + "contribution": "Identity-pivot precursor.", + "usage": "Cited theorem/context only; no runtime dependency or ancestry claim." + }, + { + "pr": 4617, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4617", + "head": "96c01a2124e234d798e9e97643c20fb5b430840d", + "author": "Ryanson Jonathan", + "contribution": "Binary identity-pivot 5d family.", + "usage": "Cited theorem/context only; no runtime dependency or ancestry claim." + } + ], + "overlap": { + "initial_open_limit": 100, + "own_pr_limit": 60, + "helper_coverage": { + "open_prs": { + "fetched_at": "2026-10-22T19:19:45.008535+00:00", + "complete_pagination": true, + "records": 426 + }, + "discussions": { + "fetched_at": "2026-10-22T19:20:33.657699+00:00", + "complete_pagination": true, + "records": 3682 + } + }, + "local_coverage": "Sparse helper notes incomplete; separate git grep searches all origin/main research READMEs.", + "main_and_merged_terms": [ + "nonidentity pivot", + "non-identity pivot", + "scalar pivot", + "prescribed-product" + ], + "related_open_prs": [ + 4746, + 4671, + 4657, + 4634, + 4678, + 4689, + 4735, + 4762 + ], + "limitations": "No exhaustive code-diff or unpublished-result search. Claims checked through 2026-10-22T19:20Z.", + "final_checkpoint_utc": "2026-10-22T19:27:27.141120+00:00", + "final_main": "1f87c3578ae546c8f903f7f4d83dc2e2fb99650b", + "final_main_readme_search": "No matching new scalar-pivot dimension result; raw search retained outside checkout.", + "merged_search_results": [ + { + "number": 4278, + "relation": "Cited scalar factorization; not the prescribed-pivot dimension law." + }, + { + "number": 3985, + "relation": "QQ16 recovery false-positive; different object." + } + ] + }, + "verification": { + "python": "CPython 3.12.15 / macOS arm64", + "direct_check_seconds": [ + 0.042707083048298955, + 0.04146383295301348 + ], + "normal_and_optimized": "pass", + "syntax_and_function_capacity": "pass; longest function 35 lines", + "external_static_analyzer": "not installed", + "selected_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY" + } +} diff --git a/research/scalar-pivot-schur-dimension/VERIFY.json b/research/scalar-pivot-schur-dimension/VERIFY.json new file mode 100644 index 0000000000..15decaa59d --- /dev/null +++ b/research/scalar-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": "210 attaining pairs over F2,F3,F4,F5,F7,F8,F9; 14291 vector pairs; 1212 sector patterns; direct Schur products and seven rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "210 attaining pairs over F2,F3,F4,F5,F7,F8,F9; 14291 vector pairs; 1212 sector patterns; direct Schur products and seven rejection controls." + } + ] +} diff --git a/research/scalar-pivot-schur-dimension/verify.py b/research/scalar-pivot-schur-dimension/verify.py new file mode 100644 index 0000000000..dcaacaee1b --- /dev/null +++ b/research/scalar-pivot-schur-dimension/verify.py @@ -0,0 +1,296 @@ +#!/usr/bin/env python3 +"""Exact scalar-pivot Schur constructions, produced by Nick Petalas. Apache-2.0.""" + +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 compressed_products(field, pivot, h): + require(0 < pivot < field.q and 0 <= h < field.q, "invalid pivot/product") + return [field.add[field.sub(1, field.add[pivot][pivot])][h], + field.sub(pivot, h), field.sub(pivot, h), h] + + +def predicted_minimum(field, pivot, h): + t00 = compressed_products(field, pivot, h)[0] + if h == 0: + return 4 + int(t00 != 0) + if h == pivot: + return 5 + int(pivot != 1) + return 3 + int(t00 != 0) + + +def construct(field, pivot, h, fill_zero=True, wrong_sign=False): + targets = compressed_products(field, pivot, h) + if wrong_sign: + targets[0] = field.add[field.add[1][field.add[pivot][pivot]]][h] + active = {1, 2} if h == pivot else {3} if h == 0 else set() + inclusion, projection, p_mask, q_mask, sizes = [], [], [], [], [] + for sector, target in enumerate(targets): + size = 1 if target else 2 if sector in active and fill_zero 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) + p = mm(field, back, [[field.mul[p_mask[i]][a] for a in row] + for i, row in enumerate(basis)]) + q = mm(field, back, [[field.mul[q_mask[i]][a] for a in row] + for i, row in enumerate(basis)]) + return p, q, sizes + + +def schur(field, matrix): + scale = field.inv[matrix[0][0]] + require(matrix[0][0] != 0, "zero Schur pivot") + 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, pivot, h, p, q): + pq = mm(field, p, q) + require(mm(field, p, p) == p and mm(field, q, q) == q, "idempotence") + require(pq == mm(field, q, p), "commutation") + require(p[0][0] == q[0][0] == pivot and pq[0][0] == h, "prescribed compression") + s, z = schur(field, p), schur(field, q) + commutator = subtract(field, mm(field, s, z), mm(field, z, s)) + scale = field.inv[pivot] + hp = field.mul[h][scale] + left = [[field.sub(pq[i][0], field.mul[hp][q[i][0]]), + field.mul[scale][field.sub(p[i][0], q[i][0])]] + for i in range(1, len(p))] + right = [[field.mul[scale][field.sub(p[0][j], q[0][j])] + for j in range(1, len(p))], + [field.sub(field.mul[hp][q[0][j]], pq[0][j]) + for j in range(1, len(p))]] + require(mm(field, left, right) == commutator, "ordered scalar factors") + return eliminate(field, commutator)[1] + + +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 independent_minimum(field, pivot, h, options): + """Minimize sector dimensions using only enumerated X/Y types and factor ranks.""" + scale = field.inv[pivot] + hp, wp = field.mul[h][scale], field.mul[field.sub(pivot, h)][scale] + a = [[0, 0], [0, scale], [field.neg[hp], field.neg[scale]], [wp, 0]] + b = [[0, 0], [scale, 0], [field.neg[scale], hp], [0, field.neg[wp]]] + choices = [list(options[t].items()) for t in compressed_products(field, pivot, h)] + best, patterns = 99, 0 + for combination in product(*choices): + a_rows = [row if flags[1] else [0, 0] + for row, (flags, _) in zip(a, combination, strict=True)] + b_rows = [row if flags[0] else [0, 0] + for row, (flags, _) in zip(b, combination, strict=True)] + if eliminate(field, a_rows)[1] == eliminate(field, b_rows)[1] == 2: + best = min(best, sum(size for _, size in combination)) + patterns += 1 + require(best != 99, "no sharp sector pattern") + return best, patterns + + +def controls(): + field = Field(5) + count = 0 + for h in (0, 2): + p, q, _ = construct(field, 2, h, fill_zero=False) + require(verify_pair(field, 2, h, p, q) < 2, "zero-sector omission undetected") + count += 1 + for pivot, h, sign in ((0, 1, False), (2, 1, True)): + try: + construct(field, pivot, h, wrong_sign=sign) + except ValueError: + count += 1 + else: + raise ValueError("invalid construction accepted") + p, q, _ = construct(field, 2, 1) + p[0][0] = 1 + try: + verify_pair(field, 2, 1, p, q) + except ValueError: + count += 1 + else: + raise ValueError("mutated projector accepted") + try: + inverse(field, [[0, 0], [0, 0]]) + except ValueError: + count += 1 + else: + raise ValueError("singular basis accepted") + try: + Field(6) + except ValueError: + count += 1 + else: + raise ValueError("nonfield order accepted") + return count + + +def main(): + cases, patterns, vector_pairs = 0, 0, 0 + histograms = {} + for order in (2, 3, 4, 5, 7, 8, 9): + field = Field(order) + options, count = pair_types(field) + vector_pairs += count + histogram = {} + for pivot, h in product(range(1, order), range(order)): + expected = predicted_minimum(field, pivot, h) + minimum, count = independent_minimum(field, pivot, h, options) + p, q, sizes = construct(field, pivot, h) + require(sum(sizes) == minimum == expected, "dimension minimum") + require(verify_pair(field, pivot, h, p, q) == 2, "sharp commutator") + histogram[expected] = histogram.get(expected, 0) + 1 + cases += 1 + patterns += count + histograms[order] = histogram + negative_controls = 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_SCALAR_PIVOT_SCHUR_DIMENSION", + "constructed_pairs": cases, "sector_patterns": patterns, + "enumerated_vector_pairs": vector_pairs, "minima": histograms, + "negative_controls": negative_controls, "sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()