diff --git a/research/residue-product-tensor-recognition/PROOF.md b/research/residue-product-tensor-recognition/PROOF.md new file mode 100644 index 0000000000..0a5e6af366 --- /dev/null +++ b/research/residue-product-tensor-recognition/PROOF.md @@ -0,0 +1,160 @@ +# Frobenius products over arbitrary finite residue fields + +Fix an explicit finite field K=F_q of characteristic p. For each j, let +L_j=F_(q^d_j) be a finite extension of K and let h_ji be positive integers. +Define + + B_j=L_j[x_ji]/(x_ji^(p^h_ji)), N_j=p^(sum_i h_ji), A=product_j B_j. + +Empty height lists are allowed and give field factors. The dimension over K +is n=sum_j d_j N_j. All tensor factor maps and determinants below are over K. + +**Recognition theorem.** From an arbitrary square K-tensor, the algorithm +decides whether it is isotopic to multiplication in such an A. It returns +the residue degrees, height lists, explicit coefficient-field tables, and +three invertible factor maps U,V,W with t(Ua,Vb)=W ab. It uses deterministic +polynomial time in n for fixed K. Neither a decomposition nor a field section +is supplied. In particular, the algorithm does not enumerate q^d_j elements. + +This extends the recognition part of PR5661 beyond split residue fields. +Nick Petalas's PR5252 supplies the finite-etale nucleus and spectral-projector +precedent. PR5637 and PR5502 supply the local semilinear height argument. +The new result recovers nonsplit coefficient fields and composes the complete +recognition test and factor maps. No physical supplier or new kappa is claimed. + +During the submission refresh, apoursh's concurrent claim on supplied-field +characters was found in Discussion5655, comment 19187845. That claim explicitly +excludes arbitrary tensor recognition and coefficient-field discovery. This +package is narrowed to those complementary outputs. The character formula, +labels and transporter work remain with that claim and are not outputs here. + +## 1. Recover the nucleus and primitive factors + +Use the nucleus equations and acceptance gates of PR5661: + + B={(X,Y):t(Xu,v)=Yt(u,v)}, dim_K B=n, + +with both projections injective, commutative image, and zero right kernel of t. +The nucleus is a unital commutative matrix algebra. Recover its multiplication +table and unit from a faithful projection. + +The least q-power Q>=n has ker(b -> b^Q)=J, the nilradical. The proof of J^n=0 +and the construction of primitive idempotents through ker(Frob_q-I) in PR5661 +do not require split residues. On each local factor the q-fixed algebra is +exactly K; its basis separates the factors by spectral projectors. Retain that +construction but remove the split-residue test dim(B/J)=number of factors. + +For each primitive e_j, calculate + + B_j=e_jB, J_j=e_jJ, d_j=dim_K B_j-dim_K J_j. + +The residue is the field F_(q^d_j). All these quantities use K-linear algebra. +This primitive decomposition is an exact algebra decomposition, with no +recognition assumption about the final truncated-polynomial class. + +## 2. Recover regular modules over nonsplit residues + +For either nucleus module M, require + + dim_K(e_jM / J e_jM)=d_j + +for every component. Choose any vector m_j outside J e_jM. The quotient is +one-dimensional over the residue field, so this vector generates it as a +B_j-module. The usual nilpotence argument is elementary here: if C=B_jm_j, +then N=e_jM/C satisfies N=JN, whence N=J^nN=0. The sum m=sum_jm_j is cyclic. +Since dim B=dim M=n, b -> bm is an isomorphism. Both matrices are checked. + +Necessity holds for a regular module. This changes the split test from a +one-dimensional K-top to a d_j-dimensional K-top; rejecting all larger tops +would incorrectly reject every nonsplit residue field. + +As in PR5661, choose generators u0,w0 for the two actions, put +alpha(b)=X_bu0, gamma(b)=Y_bw0, and Phi(v)=t(u0,v). Cyclicity and the zero right +kernel make Phi invertible. With beta=Phi^-1 gamma, + + t(alpha(a),beta(b))=gamma(ab). + +This gives factor maps from the recovered algebra before any local class test. + +## 3. Recover the unique coefficient field by a power kernel + +Let B be one local component, J its radical, d its residue degree, e its unit, +and D=q^d. The set + + L={b in B : b^D=b} + +is a K-subalgebra: the D-power map is additive and multiplicative in the +commutative algebra, and it fixes every scalar in K. It maps bijectively onto +B/J. For existence, lift a residue c to t and choose a power R=D^a at least +dim_K B. Then (t^D-t)^R=0, so t^R lies in L; its residue remains c. For +uniqueness, the difference of two lifts is a fixed nilpotent z, so +z=z^(D^a)=0 for large a. Thus reduction gives a field isomorphism L -> B/J. +Every K-algebra automorphism preserves this uniquely defined L. + +Compute the K-linear kernel of Frob_D-I. Its dimension is d. Put e first in +its basis and extend by independent kernel vectors. Multiplication gives an +explicit d-dimensional field table in that basis. There is no search over the +elements of L. Exponent D has only d*log_2(q)+1 bits, so repeated squaring is +polynomial in d and log q. + +The separate certificate check verifies the coefficient table is a field: +check commutativity, associativity, identity, zero nilradical and +dim ker(Frob_q-I)=1. A finite reduced commutative K-algebra is a product of +finite fields, and the last dimension is its number of factors. These tests +therefore prove that the supplied table has one field factor, without an +elementwise inverse search. + +## 4. Recover heights over the coefficient field + +Use the semilinear p-power kernels K_h=ker(b -> b^(p^h)). The matrices and +their inverse coefficient twists are computed over K as in PR5637. Each K_h +is also an L-subspace: raising an L-scalar to p^h is an automorphism of L. +Likewise J^2 is an L-subspace. + +Start with J^2. For h in increasing order, inspect a K-basis of K_h. When a +vector v adds a new tangent direction, add the full L-span Lv by multiplying +v with every coefficient-field basis element. Its K-dimension increment is +exactly d: a nonzero line over L has dimension d over K. Record v as one +generator of height h. This does not record d copies of the same generator. + +The result is a list g_i with g_i^(p^h_i)=0 whose classes form an L-basis of +J/J^2. They generate B over L by the radical-power argument of PR5502: +expand each J^k modulo J^(k+1), then iterate to J^n=0. Therefore substitution +gives a surjective L-algebra map + + L[x_i]/(x_i^(p^h_i)) -> B. + +Accept precisely when d*p^(sum_i h_i)=dim_K B. The dimensions then agree and +the map is an isomorphism. In the target algebra the p-power tangent flag +recovers exactly its variable heights; no nonlinear term can cancel the +surviving single-variable monomial of a lower-degree linear term. This proves +necessity as well as sufficiency. + +The model basis consists of each ordered variable monomial multiplied by every +coefficient-field basis element. These explicit columns are checked for full +rank. Combining the local model maps with alpha,beta,gamma gives U,V,W. The +certificate checker verifies all n^2 transported basis products independently +of the discovery kernels. This proves the recognition theorem. + +## 5. Complexity and the kappa boundary + +The nucleus elimination costs O(n^7) base-field operations. Radical and fixed +spaces use K-linear systems. Powers q^d require O(d log q) algebra products, +not q^d operations. Tangent tests use coefficient-field basis vectors, not +all coefficient-field elements. The primitive splitting enumerates q scalars +for each fixed-algebra basis vector. A conservative bound for the complete +algorithm and certificate check is O(n^9+q*n^6*log(q*n)) K-operations, after +the explicit base-field table is built. Space is polynomial in n. This is a +fixed-q statement; no polynomial bit bound in log q is claimed. + +The package closes recognition and explicit factor-map extraction for the full +declared family of finite residue-field Frobenius products. The tensor atlas +can apply it directly to tensor coefficients. General local algebras with other +relations, efficient canonical field isomorphisms, physical native maps, +coefficient costs, ownership, restoration, precision, storage and a complete +caller remain separate. Unknown physical costs are not zero. The selected +frontier and complete kappa calculation are unchanged. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. The same +assistant wrote the proof and checks. Independent scientific review remains +open; no proof-kernel acceptance is claimed. diff --git a/research/residue-product-tensor-recognition/README.md b/research/residue-product-tensor-recognition/README.md new file mode 100644 index 0000000000..3a3c8984af --- /dev/null +++ b/research/residue-product-tensor-recognition/README.md @@ -0,0 +1,102 @@ +# Recognize Frobenius products with arbitrary finite residue fields + +This package recognizes arbitrary square K-tensors that are isotopic to +products of L[x_i]/(x_i^(p^h_i)), where K=F_q and each L is any finite extension +of K. It returns every residue degree, height list, coefficient-field table, +and all three factor maps. No decomposition or coefficient-field section is +supplied. The output is an explicit algebra model and a literal tensor-isotopy certificate. + +This removes the split-residue restriction of +[PR #5661](https://github.com/CrocSwap/integer-mult-bounds/pull/5661). +The new coefficient field is the kernel of Frob_(q^d)-I inside a local component +of residue degree d. Height tests use spans over that recovered field. Both +steps use base-field linear algebra and avoid enumeration of q^d elements. +The regular-module top has base-field dimension d. + +The algorithm is necessary and sufficient for the stated class, and polynomial +in tensor dimension for each fixed K. Read [PROOF.md](PROOF.md), +[recognize.py](recognize.py), [RESULT.json](RESULT.json) and +[SOURCES.json](SOURCES.json). The result supplies an input test for the tensor +atlas. It supplies no paid physical construction or complete kappa increase. + +## Contract + +`recognize(t, field)` returns `(certificate, None)` or `(None, reason)`. +Invalid tensor shapes or noncanonical field elements raise `ValueError`. +The base field uses the exact explicit representation retained from PR5637. +The certificate has `components`, `U`, `V` and `W`. +Each component has `degree`, sorted `heights`, and a `field` multiplication +table whose first basis vector is one. Model basis order is variable monomial +first, then coefficient-field basis. All maps satisfy `t(Ua,Vb)=W mu(a,b)`. + +The coefficient-field tables use discovered bases. Character images, +canonical orbit labels and determinant-one transporters between different +field tables are outside this package. The separate +[concurrent character claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5655#discussioncomment-19187845) +uses supplied decompositions and explicitly leaves this discovery task open. +The package was narrowed after the submission overlap refresh to preserve +that separation. No field-presentation conversion is silently assumed. + +## Verification + +Use Python 3.12 and the standard library: + +```sh +python3 -B scripts/research_package.py --package research/residue-product-tensor-recognition +``` + +Both normal and optimized commands must print +`PASS_RESIDUE_PRODUCT_TENSOR_RECOGNITION`. A separate coefficient-index GL orbit +generator agrees on every one of the 72,353 two-dimensional tensors over +F2/F3/F4, accepting 174/4,320/62,460. The new accepted cases include nonsplit +quadratic fields. This oracle does not use the nucleus or discovery kernels. + +Further presentations over F2/F3/F4/F9 check nonsplit nilpotent factors, +repeated factors, mixed residue types, and residue degrees two and three. +Controls reject false maps and fields, wrong residue degrees, extra local +relations and nonregular modules. The coefficient-field validator also rejects +a reduced product of two fields. [RESULT.json](RESULT.json) gives the exact +counts, and [VALIDATION.md](VALIDATION.md) records the execution boundary. + +## Credit and scope + +Base is canonical main `df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority 7. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5655#discussioncomment-19187846) +records the fresh overlap check and changed residue premise. No selected file +or predecessor package is changed. + +- [PR #5661](https://github.com/CrocSwap/integer-mult-bounds/pull/5661), exact + `5d722279f4292c63361f1e958ff4ed5a6ec638aa`, supplies the split-product framework, + basic linear-algebra helpers and the independent finite orbit-check routines. +- [PR #5637](https://github.com/CrocSwap/integer-mult-bounds/pull/5637) supplies + the retained finite-field arithmetic and semilinear-kernel code. Its local + height proof uses apoursh's [PR #5502](https://github.com/CrocSwap/integer-mult-bounds/pull/5502). +- apoursh's [PR #5656](https://github.com/CrocSwap/integer-mult-bounds/pull/5656) + supplies split-product characters. Nick Petalas's + [PR #5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252) supplies + the finite-etale nucleus, spectral projectors, norms and Galois-sign precedent. + David Ganz and the retained atlas authors keep their credit. + +Exact executable and proof inputs are retained byte-for-byte and authenticated +before imports. The new code extends the nucleus/module composition and orbit +checks; it does not claim those predecessor methods as new. Coefficient-field +lifting is classical finite algebra. The new result is the complete recognition +interface for the stated nonsplit nonreduced family, with exact +certificates and checks. No literature-priority claim is made. + +Physical native realization, coefficient costs, ownership, restoration, storage, +precision and a complete caller remain unpriced. Unknown costs are not zero. +Independent human or proof-kernel acceptance, hosted CI and the selected cold +replay are separate from these author-side checks. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +## Open next questions + +- Connect these recovered field tables to the concurrent supplied-decomposition + character interface. Coordinate there before implementing field isomorphisms, + labels or transporters. +- Choose an actual accepted tensor and price its maps in a complete native + caller before treating the algebraic result as a kappa improvement. + +First steps and blockers are also recorded in [TASK.json](TASK.json). diff --git a/research/residue-product-tensor-recognition/RESULT.json b/research/residue-product-tensor-recognition/RESULT.json new file mode 100644 index 0000000000..f2a27b2133 --- /dev/null +++ b/research/residue-product-tensor-recognition/RESULT.json @@ -0,0 +1,25 @@ +{ + "basis_products": 1392, + "controls": 272, + "exhaustive": [ + { + "accepted": 174, + "q": 2, + "sha256": "366c04b598dc02e7935e6319f2ad5b456c8b6d0255a9c4f9e173f40a4af6ebbe", + "tensors": 256 + }, + { + "accepted": 4320, + "q": 3, + "sha256": "eadf8e8ac6baeff11383ef29909bb4820bc0264f50045c8625a54c2ac59a25c1", + "tensors": 6561 + }, + { + "accepted": 62460, + "q": 4, + "sha256": "f328c998c3346bf59d15818429d6d04597321ea4e424da4e51d233a5d845fc0d", + "tensors": 65536 + } + ], + "presentations": 52 +} diff --git a/research/residue-product-tensor-recognition/SOURCES.json b/research/residue-product-tensor-recognition/SOURCES.json new file mode 100644 index 0000000000..718e440e6b --- /dev/null +++ b/research/residue-product-tensor-recognition/SOURCES.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "research/etale-tensor-determinant-image/README.md", + "usage": "provenance", + "git_blob": "0f07df6ce2a8c43ea1fcc5f0081ee3532da28208", + "sha256": "2ec18042a1a63d5fd5da246f4f6060c5fb66cff338f25a2a1b95e3ea8b4f0fba" + }, + { + "path": "research/residue-product-tensor-recognition/vendor/split.py", + "usage": "input", + "git_blob": "21f134736133fbe8f2e2b8eb75fecbf8a0194670", + "sha256": "127d226258a781a050c6c80779dd392b403194d81d5d69e20debb811e8e8bceb", + "pin": "head:fccecc22b51b502a2428130448fd644e103e02e1:research/residue-product-tensor-recognition/vendor/split.py" + }, + { + "path": "research/residue-product-tensor-recognition/vendor/local.py", + "usage": "input", + "git_blob": "1066bb74c19d180bfef7d9dd1c0650ec6bbd7780", + "sha256": "6daa160346d04691c6ca3c9c820b3df8982de4320ec01e5db10e3cb932f42c00", + "pin": "head:fccecc22b51b502a2428130448fd644e103e02e1:research/residue-product-tensor-recognition/vendor/local.py" + }, + { + "path": "research/residue-product-tensor-recognition/vendor/PR5661.md", + "usage": "input", + "git_blob": "c3d085b38a02d3c854ece5b87e958c96993ff32b", + "sha256": "5da97eed522c0a158fd192d242425fed028fa8aace234b9d66fe6afac97390bb", + "pin": "head:fccecc22b51b502a2428130448fd644e103e02e1:research/residue-product-tensor-recognition/vendor/PR5661.md" + }, + { + "path": "research/residue-product-tensor-recognition/vendor/PR5656.md", + "usage": "input", + "git_blob": "a9f931a378ebf7a67881d209f46c2f7fe47d1041", + "sha256": "0eb6c9f9eba70dc339e54b72a98b5b0fdcef706bcff5e02546ab2d0426a85ad9", + "pin": "head:fccecc22b51b502a2428130448fd644e103e02e1:research/residue-product-tensor-recognition/vendor/PR5656.md" + } + ], + "external_inputs": [ + { + "local_path": "vendor/split.py", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "5d722279f4292c63361f1e958ff4ed5a6ec638aa", + "source_path": "research/split-product-tensor-recognition/recognize.py", + "sha256": "127d226258a781a050c6c80779dd392b403194d81d5d69e20debb811e8e8bceb", + "git_blob": "21f134736133fbe8f2e2b8eb75fecbf8a0194670" + }, + { + "local_path": "vendor/local.py", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "5d722279f4292c63361f1e958ff4ed5a6ec638aa", + "source_path": "research/split-product-tensor-recognition/vendor/local.py", + "sha256": "6daa160346d04691c6ca3c9c820b3df8982de4320ec01e5db10e3cb932f42c00", + "git_blob": "1066bb74c19d180bfef7d9dd1c0650ec6bbd7780" + }, + { + "local_path": "vendor/PR5661.md", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "5d722279f4292c63361f1e958ff4ed5a6ec638aa", + "source_path": "research/split-product-tensor-recognition/PROOF.md", + "sha256": "5da97eed522c0a158fd192d242425fed028fa8aace234b9d66fe6afac97390bb", + "git_blob": "c3d085b38a02d3c854ece5b87e958c96993ff32b" + }, + { + "local_path": "vendor/PR5656.md", + "source_repository": "aliromman/integer-mult-bounds", + "source_commit": "5d722279f4292c63361f1e958ff4ed5a6ec638aa", + "source_path": "research/split-product-tensor-recognition/vendor/PR5656.md", + "sha256": "0eb6c9f9eba70dc339e54b72a98b5b0fdcef706bcff5e02546ab2d0426a85ad9", + "git_blob": "a9f931a378ebf7a67881d209f46c2f7fe47d1041" + } + ] +} diff --git a/research/residue-product-tensor-recognition/TASK.json b/research/residue-product-tensor-recognition/TASK.json new file mode 100644 index 0000000000..5dd3d52a40 --- /dev/null +++ b/research/residue-product-tensor-recognition/TASK.json @@ -0,0 +1,112 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "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": "Recognize finite residue-field Frobenius products from arbitrary tensors, with explicit coefficient-field tables and all three factor maps.", + "scope_change_reason": "Change the split-residue premise of PR5661. Narrow the draft after the submission refresh found the concurrent supplied-character claim posted seconds earlier. Character images and transporters remain outside this package.", + "bottleneck_link": "Extend the tensor atlas input test to nonsplit nonreduced products. A complete physical caller is still needed for a kappa gain.", + "budget_minutes": 120, + "stop_rule": "Complete nonsplit recognition, coefficient-field discovery and literal factor maps. Do not duplicate the concurrent supplied-character claim.", + "outcome": "completed", + "evidence": "PROOF.md, recognize.py, verify.py and RESULT.json.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance. The same assistant supplied the proof and verifier; no independent human review.", + "open_questions": [ + { + "question": "Can canonical coefficient-field isomorphisms give cross-presentation SL labels and transporters?", + "why_it_matters": "The returned determinant image alone does not compare model bases.", + "first_step": "Specify reference field bases and verify explicit isomorphisms with determinant signs.", + "blocked_by": "No canonical field-isomorphism routine is supplied." + }, + { + "question": "Can one recognized tensor give a paid native supplier?", + "why_it_matters": "This is the missing link to complete kappa.", + "first_step": "Price all factor maps and restoration in one actual chronological caller.", + "blocked_by": "No physical cost contract is supplied." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5655#discussioncomment-19187846", + "upstream": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "priority_revision": 7, + "overlap_utc": "2026-10-26T03:40:36+00:00", + "local_notes": 7676, + "open_prs": 350, + "discussion_records": 4965, + "coverage": "Complete cached pagination and all tracked main notes; no arbitrary diff or unpublished-work claim.", + "concurrent_scope": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5655#discussioncomment-19187845" + } +} diff --git a/research/residue-product-tensor-recognition/VALIDATION.md b/research/residue-product-tensor-recognition/VALIDATION.md new file mode 100644 index 0000000000..caf4da431f --- /dev/null +++ b/research/residue-product-tensor-recognition/VALIDATION.md @@ -0,0 +1,19 @@ +# Validation + +Python 3.12.14 registered normal and optimized replay passed with identical +RESULT.json data. Both returned PASS_RESIDUE_PRODUCT_TENSOR_RECOGNITION; +the runner returned PASS_REGISTERED_RESEARCH_PACKAGE. + +The complete 72,353-tensor orbit comparison, 52 presentations, 1,392 basis +products and 272 controls passed. These include nonsplit nilpotent, +residue-degree, field and module checks passed. The same assistant constructed +and checked the proof. No independent human or proof-kernel acceptance is +claimed. Hosted CI is separate. + +The exact source copies are retained in this branch's first commit and are +hash-checked before imports. The checkout is shallow, so full-history source +preflight is not claimed. Immediate base/source ancestry, committed bytes, +export integrity and Git-free replay are recorded in the public handoff. + +No selected cold replay, native supplier or complete multiplier was run. +No complete kappa gain is claimed. diff --git a/research/residue-product-tensor-recognition/VERIFY.json b/research/residue-product-tensor-recognition/VERIFY.json new file mode 100644 index 0000000000..37b74350dd --- /dev/null +++ b/research/residue-product-tensor-recognition/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/residue-product-tensor-recognition/vendor/split.py", + "research/residue-product-tensor-recognition/vendor/local.py", + "research/residue-product-tensor-recognition/vendor/PR5661.md", + "research/residue-product-tensor-recognition/vendor/PR5656.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Check complete small tensor orbits; nonsplit nilpotent products and all factor maps; residue-degree, field and nonregular-module controls." + }, + { + "argv": [ + "{python}", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Check complete small tensor orbits; nonsplit nilpotent products and all factor maps; residue-degree, field and nonregular-module controls." + } + ] +} diff --git a/research/residue-product-tensor-recognition/recognize.py b/research/residue-product-tensor-recognition/recognize.py new file mode 100644 index 0000000000..e7e61c2dd8 --- /dev/null +++ b/research/residue-product-tensor-recognition/recognize.py @@ -0,0 +1,243 @@ +"""Recover residue-field products. Ali Romman with OpenAI Codex. Apache-2.0.""" +from itertools import product +from vendor import local as a +from vendor.split import span, coordinate_map, linear_combination + + +def radical(table, unit, f): + n = len(table) + power = 1 + while power < n: + power *= f.q + return a.kernel(a.columns([a.algebra_power(table, v, power, unit, f) + for v in a.identity(n)], n), n, f) + + +def fixed_space(table, unit, power, f): + n = len(table) + cols = [a.algebra_power(table, v, power, unit, f) for v in a.identity(n)] + return a.kernel([[f.add[cols[j][i]][f.neg[int(i == j)]] + for j in range(n)] for i in range(n)], n, f) + + +def primitive_parts(table, unit, f): + fixed = fixed_space(table, unit, f.q, f) + parts = [unit] + for c in fixed: + refined = [] + for e in parts: + for scalar in range(f.q): + shifted = [f.add[x][f.neg[f.mul[scalar][y]]] for x,y in zip(c,unit)] + power = a.algebra_power(table, shifted, f.q-1, unit, f) + selector = [f.add[x][f.neg[y]] for x,y in zip(unit,power)] + piece = a.tensor_value(table,e,selector,f) + if any(piece): + refined.append(piece) + parts = refined + if len(parts) == len(fixed): + break + if len(parts) != len(fixed): + raise ArithmeticError('primitive decomposition') + return parts + + +def regular_generator(module, jbasis, parts, degrees, f): + n = len(module) + seed = [0]*n + actions = [linear_combination(c,module,f) for c in jbasis] + for e,d in zip(parts,degrees): + projection = linear_combination(e,module,f) + block = span([a.column(projection,i) for i in range(n)],n,f) + jm = span([a.mv(m,v,f) for m in actions for v in block],n,f) + if len(block)-len(jm) != d: + return None + v = next(v for v in block if a.rank(jm+[v],f)>len(jm)) + seed = [f.add[x][y] for x,y in zip(seed,v)] + matrix = a.columns([a.mv(m,seed,f) for m in module],n) + if not a.determinant(matrix,f): + raise ArithmeticError('regular generator') + return matrix,seed + + +def local_model(component,f): + field,hs = component['field'],component['heights'] + d = len(field) + bounds = [f.p**h for h in hs] + exponents = list(product(*(range(b) for b in bounds))) + positions = {e:i for i,e in enumerate(exponents)} + n = d*len(exponents) + table = [[[0]*n for _ in range(n)] for _ in range(n)] + for i,x in enumerate(exponents): + for j,y in enumerate(exponents): + z = tuple(v+w for v,w in zip(x,y)) + if any(v>=b for v,b in zip(z,bounds)): + continue + start = d*positions[z] + for u,v in product(range(d),repeat=2): + table[d*i+u][d*j+v][start:start+d] = field[u][v] + return table,exponents + + +def product_model(components,f): + models = [local_model(c,f)[0] for c in components] + n = sum(map(len,models)) + table = [[[0]*n for _ in range(n)] for _ in range(n)] + offset = 0 + for mu in models: + for i,row in enumerate(mu): + for j,v in enumerate(row): + table[offset+i][offset+j][offset:offset+len(mu)] = v + offset += len(mu) + return table + + +def field_table_valid(table,f): + try: + a.validate_tensor(table,f) + d = len(table) + identity = a.identity(d) + if any(table[0][i]!=identity[i] or table[i][0]!=identity[i] for i in range(d)): + return False + if any(table[i][j]!=table[j][i] for i,j in product(range(d),repeat=2)): + return False + for i,j,k in product(range(d),repeat=3): + if a.tensor_value(table,table[i][j],identity[k],f) != a.tensor_value(table,identity[i],table[j][k],f): + return False + if radical(table,identity[0],f): + return False + return len(fixed_space(table,identity[0],f.q,f)) == 1 + except (ValueError,TypeError,IndexError): + return False + + +def classify_local(table,unit,f): + n = len(table) + jbasis = radical(table,unit,f) + degree = n-len(jbasis) + candidates = fixed_space(table,unit,f.q**degree,f) + coefficients = [unit] + for v in candidates: + if a.rank(coefficients+[v],f)>len(coefficients): + coefficients.append(v) + if len(coefficients)!=degree: + raise ArithmeticError('coefficient field dimension') + coord = coordinate_map(coefficients,n,f) + field = [[coord(a.tensor_value(table,x,y,f)) for y in coefficients] for x in coefficients] + if not field_table_valid(field,f): + raise ArithmeticError('coefficient field certificate') + tangent = span([a.tensor_value(table,x,y,f) for x in jbasis for y in jbasis],n,f) + generators,heights = [],[] + power,h = 1,0 + while powerlen(tangent): + if len(enlarged)-len(tangent)!=degree: + raise ArithmeticError('coefficient-field tangent dimension') + tangent = enlarged + generators.append(v) + heights.append(h) + if degree*f.p**sum(heights)!=n: + return None,'height dimension' + component = dict(degree=degree,heights=heights,field=field) + _,exponents = local_model(component,f) + images = [] + for es in exponents: + monomial = unit[:] + for g,e in zip(generators,es): + monomial = a.tensor_value(table,monomial,a.algebra_power(table,g,e,unit,f),f) + images.extend(a.tensor_value(table,c,monomial,f) for c in coefficients) + change = a.columns(images,n) + if not a.determinant(change,f): + raise ArithmeticError('local model basis') + return (component,change),None + + +def check_certificate(t,cert,f): + try: + a.validate_tensor(t,f) + n = len(t) + cs = cert['components'] + if not cs: + return False + for c in cs: + hs = c['heights'] + if type(c['degree']) is not int or c['degree']<1 or c['degree']!=len(c['field']): + return False + if hs!=sorted(hs) or any(type(h) is not int or h<1 for h in hs): + return False + if not field_table_valid(c['field'],f): + return False + if sum(c['degree']*f.p**sum(c['heights']) for c in cs)!=n: + return False + mats = [cert[k] for k in ('U','V','W')] + if any(len(m)!=n or any(len(row)!=n or any(type(x) is not int or not 0<=x= 1 +and define + + B_j = K[x_(j,1),...,x_(j,r_j)] / (x_(j,i)^(p^h_(j,i))), + A = product_(j=1)^s B_j, + N_j = dim_K B_j = p^(sum_i h_(j,i)), + n = dim_K A = sum_j N_j. + +Each height is a positive integer. An empty height list means B_j = K +and N_j = 1. A factor's **type** is its sorted height list. Within a factor, +use the monomial basis with lexicographically ordered exponent tuples. The +canonical product model orders factor types lexicographically; equal types +are consecutive copies of the same model. + +Set L = q-1, and for every variable define the integer + + E_(j,i) = N_j * (p^h_(j,i) - 1) / 2. + +It is integral: for odd p the second factor is even; for p = 2 every factor +containing a variable has even dimension. Include a swap generator precisely +when q is odd and some type occurs at least twice with odd component +dimension. Its exponent is T = L/2. Set + + g = gcd(L, all E_(j,i), T if that swap generator exists), + H_g = {c^g : c in K*}. + +The gcd of the singleton list (L) is L. This includes field factors with +empty height lists and q = 2, where L = g = 1. Every N_j in this family is +odd when q is odd; the dimension condition identifies the sign's source. + +**Theorem.** The image of Aut_K(A) under determinant is exactly H_g. For +multiplication mu_A and the covariant action on A* tensor A* tensor A, the +full stabilizer determinant image is + + Delta(mu_A) = {(u,v,w) in (K*)^3 : uvw in H_g} + = {(u,v,w) : (uvw)^(L/g) = 1}. + +It has L^3/g elements. The general-linear orbit of mu_A contains exactly g +orbits under SL_n(K)^3. Every allowed determinant triple is attained by an +explicit autotopism. For tensors supplied with verified factor maps, the +canonical type multiset and Section 6's label completely decide +special-linear equivalence. + +## 2. Local type and local determinant character + +We restate the local argument of PR5459 to identify the input to the product +calculation. In B = K[x_1,...,x_r]/(x_i^(p^h_i)), let J = (x_1,...,x_r). +An element with nonzero constant term is a unit by a finite geometric +series; all elements of J are nilpotent. Thus B is local with residue field +K. Its only idempotents are zero and one: one of e and 1-e is a unit, and +e(1-e) = 0 determines an idempotent e. + +The tangent quotient J/J^2 has the variables as a basis. Its intrinsic +height flag is + + V_e = (ker(a -> a^(p^e)) + J^2)/J^2. + +These kernels are K-subspaces even though the power map is semilinear over +an extension field. Frobenius removes mixed terms. A nonzero linear term +in x_i survives the p^e power exactly when h_i > e, and no term of degree +at least two can cancel its degree-p^e monomial. Therefore V_e is exactly +the span of variables of height at most e. Its dimension increments recover +the height multiset. Two displayed local factors are isomorphic if and only +if their types agree; equal dimension alone is insufficient. + +An automorphism's tangent map preserves this flag. Conversely, an invertible +flag-preserving linear substitution respects the defining power relations: +a variable of height h is sent only to variables whose heights are at most +h. Its inverse preserves the same flag, so this substitution is an +automorphism. A general automorphism and its linear substitution induce the +same map on the associated graded algebra for powers of J. A monomial basis +ordered by total degree shows that they have equal determinants. + +The flag-preserving group is generated by allowed elementary substitutions +and diagonal scalings. For an allowed substitution x_i -> x_i + c*x_k, +the monomial expansion is triangular when ordered by x_i exponent, with +diagonal one. Its determinant is one. Scaling x_i -> c*x_i has determinant +c^E_i: the sum of the x_i exponents over the N monomials is + + E_i = N * (p^h_i - 1) / 2. + +Elementary and diagonal matrices generate the full general-linear group +within each equal-height block, while the other allowed elementary matrices +generate the off-diagonal flag-preserving part. Thus the local determinant +image is generated exactly by the subgroups {c^E_i : c in K*}. With an empty +height list, the K-algebra K has only the identity automorphism. + +## 3. Primitive idempotents and the permutation contribution + +An idempotent of A has each coordinate zero or one. The nonzero primitive +idempotents are precisely the e_j supported on a single factor: any +idempotent supported on more than one factor splits into nonzero orthogonal +idempotents. Algebra automorphisms preserve this intrinsic property. + +An automorphism sending e_j to e_k restricts to an isomorphism e_j A -> e_k A, +so those factors have the same type. Conversely, any permutation among +copies of one type, together with an independent automorphism on each factor, +defines an automorphism of A. These are all the possibilities; there are +no additional maps mixing primitive factors. + +Factorwise automorphisms contribute the product of their local determinants. +Swapping two identical factors of dimension N swaps N pairs of matching +basis vectors, so its determinant is (-1)^N. This remains true for blocks +separated by other blocks: those same N basis-vector transpositions describe +the operation. Equivalently, conjugate by a fixed reordering that places the +copies together. For any allowed permutation the sign contribution is + + product_over_types type_permutation_sign^(dimension_of_that_type). + +Hence signs contribute only for repeated isomorphic odd-dimensional factors +in odd characteristic. In characteristic two every sign is one. Unequal +types cannot be swapped, even when they have the same dimension. + +The finite group K* is cyclic of order L. Relative to a generator zeta, the +determinant generators have exponents E_(j,i) and, when present, T = L/2. +They generate precisely = H_g. Each generator is attained by a +literal variable scaling or permitted block transposition. This proves +the automorphism image and its attainment. + +## 4. Unit determinants and the full tensor stabilizer + +For a unit a = (a_j), multiplication by a_j is triangular on its monomials +ordered by total degree. Its constant term c_j is on every diagonal entry. +Consequently + + det(L_a) = product_j c_j^N_j. + +This map is onto K*: choose one component and let all other components +equal one. The chosen N_j is a power of p and is coprime to L, so its scalar +constant can attain any desired determinant. For q = 2 the unit one suffices. +This uses one component dimension N_j, not the total dimension n, which +need not be coprime to L. + +We use the classical unital commutative autotopism normalization retained in +PR5252 and PR5459. Suppose invertible F,G,H satisfy + + F(x) * G(y) = H(x*y). + +Put a = F(1), b = G(1). Evaluation at one gives H(x) = F(x)*b = a*G(x). +Invertibility of F,G,H implies that multiplication by a and b is invertible, +so a and b are units. Then sigma = L_(ab)^(-1) H is a unital algebra +automorphism and + + F = L_a sigma, G = L_b sigma, H = L_(ab) sigma. + +Conversely these maps always form an autotopism. Write x = det L_a, +y = det L_b, z = det sigma. The corresponding covariant stabilizer element +is (F^(-T),G^(-T),H), with determinant triple + + (u,v,w) = (x^(-1) z^(-1), y^(-1) z^(-1), x*y*z). + +Its product is z^(-1), in H_g. Conversely, for a requested triple with +uvw in H_g, set + + z = (u*v*w)^(-1), x = v*w, y = u*w. + +The automorphism and unit determinant constructions attain these three +values and hence the requested triple. This proves the full image formula. +There are L^2 choices for the first two entries and L/g possible products, +so its cardinality is L^3/g. + +## 5. Constructive determinant witnesses + +Fix a generator zeta of K*. For a desired z in H_g, write z = zeta^k +with 0 <= k < L; membership is equivalent to g dividing k. Bezout +coefficients give + + g = b_0 L + sum_(j,i) b_(j,i) E_(j,i) + b_T T, + +omitting the final term when no swap generator exists. Scale variable (j,i) +by zeta^(b_(j,i)*k/g), and compose one fixed permitted transposition to +power b_T*k/g if needed. The resulting determinant is z. Negative +coefficients are allowed because the maps are invertible. If all character +generators are trivial, only z = 1 is requested and the identity suffices. + +For desired unit determinant x, choose a component j and an inverse r of +N_j modulo L. The unit with scalar x^r in that component and one elsewhere +has determinant x. In the trivial multiplicative group use the identity. +Together with Section 4 this constructs every allowed determinant triple. + +Primitive-element and discrete-log enumeration in an explicit finite field +suffice for a fixed q. This is not a polynomial bit-complexity claim in log q. +A different exact subgroup witness search can be used, provided it verifies +the same determinants and transported basis products. + +## 6. Supplied certificates and special-linear labels + +A tensor t: K^n x K^n -> K^n is supplied with model factor types and three +invertible matrices U,V,W, in the convention + + t(U*a,V*b) = W*mu_A(a,b). + +Columns are basis images from the declared model to the tensor. Check the +dimensions, invertibility and all n^2 model basis products. By bilinearity +these finite identities verify the supplied decomposition for all inputs. +They do not provide a procedure for discovering the certificate. + +The reference model must be fixed before comparing labels. Heights inside +each factor are sorted, and factor types are sorted lexicographically. +For another supplied component order, construct the monomial permutation +R from the canonical model to the supplied model, matching full types and +monomial coordinates. Normalize the factor maps to + + U_c = U*R, V_c = V*R, W_c = W*R. + +Thus, with d_raw = det(W)/(det(U)*det(V)), + + d = det(W_c)/(det(U_c)*det(V_c)) = d_raw/det(R), + label(t) = d^(L/g). + +Sorting type metadata alone can lose this permutation sign. If variable +order is also changed inside a supplied factor, its monomial permutation +must also be included, or the interface must require sorted heights from +the start. R changes the reference model coordinates, not the ambient +coordinates of t. + +Two choices of matching among identical factors differ by a model +automorphism, whose determinant lies in H_g, so the label is unchanged. +More generally, two valid certificates from the same canonical model differ +by a tensor stabilizer. Their determinant products differ by an element of +H_g. The label is therefore independent of the certificate. + +For completeness, let G = GL_n(K)^3 and S = SL_n(K)^3. The determinant map +G -> (K*)^3 has kernel S. Since S is normal, its orbits within a fixed +G-orbit correspond to cosets of the stabilizer determinant image. The product +map identifies these cosets with K*/H_g. The map d -> d^(L/g) has kernel +H_g, so its value is a complete label, with exactly g possible values. + +Different type multisets cannot be general-linearly equivalent. An isotopy +between multiplication in two unital commutative algebras normalizes exactly +as in Section 4, using units in the target algebra, to an algebra isomorphism. +It must match primitive idempotents and then local types. Conversely a type +matching gives a literal product algebra isomorphism. For verified +certificates over the same explicit field, therefore, + + SL-equivalent iff canonical type multisets agree and labels agree. + +Different presentations of the finite field need an explicit, checked field +isomorphism before their element-valued labels can be compared. + +## 7. Determinant-one transporters + +Let two normalized certificates (U_1,V_1,W_1) and (U_2,V_2,W_2) have the +same canonical model and label. Put + + a = det(U_1)/det(U_2), + b = det(V_1)/det(V_2), + c = det(W_1)/det(W_2). + +We need a model autotopism (P,Q,R_0) with determinants (a,b,c). In +Section 4's notation choose + + z = a*b/c, x = a/z, y = b/z. + +Equal labels imply (c/(a*b))^(L/g) = 1, hence z belongs to H_g. +Section 5 constructs the required automorphism and units. Then + + F = U_2 * P * U_1^(-1), + G = V_2 * Q * V_1^(-1), + H = W_2 * R_0 * W_1^(-1) + +all have determinant one and satisfy + + t_2(F*x,G*y) = H*t_1(x,y). + +Substitution in the certificate identities proves this. An executable can +also verify the three determinants and every transported basis product. +Unequal labels preclude such maps. + +## 8. Discriminating examples and boundary cases + +Over F_3, let B = F_3[x]/(x^9). Its height list is (2), dimension nine, +and local exponent 9*(9-1)/2 = 36. Since L = 2, the local automorphism +determinant image is {1}; its multiplication orbit splits into two +special-linear orbits. For B x B, a block transposition has determinant +(-1)^9 = -1. The product gcd is gcd(2,36,36,1) = 1, giving only one +special-linear orbit. A product rule using only local characters misses +this change. + +The factors F_3[x]/(x^9) and F_3[y,z]/(y^3,z^3) both have dimension nine, +but their height lists (2) and (1,1) have different tangent dimensions. +A proposed swap is not an algebra automorphism. Equal component size +does not authorize a permutation generator or component match. + +If all heights are empty, A = K^s. For s = 1 the automorphism image is +trivial and g = L. For s >= 2 and odd q, permutations add -1 and g = L/2; +in characteristic two they add nothing and g = L. This agrees with the +split finite-etale case of PR5252. For q = 2 every nonzero determinant and +label is one, and g = 1 for every model. + +Unequal component dimensions add no automorphism generators, but their block +ordering still affects normalization of a supplied certificate. The empty +product and zero-dimensional zero algebra are excluded. An empty height +list inside a nonempty product is a valid field factor. + +## 9. Cost, credit and remaining obligations + +The gcd formula only needs exponents modulo L. Compute +p^(sum_i h_(j,i)) * (p^h_(j,i)-1) modulo 2L and halve its even residue +to obtain E_(j,i) modulo L without materializing a large component dimension. +Modular powers, type comparison and gcd are polynomial in the parameter bit +lengths, given p,q and the finite-field contract. Building and checking +explicit matrices is instead polynomial in the explicit algebra dimension +at fixed q. These are different size statements: a short symbolic height +list can specify an algebra too large to materialize. The executable builds +literal model dimensions and local exponents; the modular method just +described is an arithmetic consequence of the formula, not an implemented +compressed-model runtime guarantee. + +Ali Romman's [PR5459 at bef3575ddb19c44434a7e2460a353eac7c4d9387](https://github.com/aliromman/integer-mult-bounds/blob/bef3575ddb19c44434a7e2460a353eac7c4d9387/research/frobenius-tensor-characters/README.md) +supplies the local height flag and determinant character; those local +results are predecessor work. His +[PR5637 at 86389e525d3efafe236e929f6ae401c68be1d115](https://github.com/aliromman/integer-mult-bounds/blob/86389e525d3efafe236e929f6ae401c68be1d115/research/extension-field-tensor-recognition/README.md) +supplies extension-field recognition, local special-linear labels and the +explicit product handoff. [apoursh's PR5502](https://github.com/CrocSwap/integer-mult-bounds/pull/5502) +supplies the prime-field table height criterion. +[Nick Petalas's PR5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252) +supplies finite-etale tensor determinants and the normalization lineage. +David Ganz and the retained atlas framework retain their credit. Primitive +idempotents, cyclic subgroup arithmetic and unital isotopy normalization are +classical; no general literature-priority claim is made. + +Open next questions are recovery of this decomposition from an arbitrary +tensor and local factors with residue fields larger than the base. The +latter requires coefficient-field identifications, norms and additional +automorphisms; it does not follow by dropping the residue-field hypothesis. +Neither task is supplied here. Physical coefficient preparation, native +implementation, precision, movement, restoration, supplier admission and +a new multiplication exponent remain outside this result. + +The written theorem covers general finite fields. Executable coverage is +limited to the field contract and domains stated in the package's README; +finite checks are corroboration, not a proof-kernel verification. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +No independent human or formal proof-kernel acceptance is claimed. diff --git a/research/residue-product-tensor-recognition/vendor/PR5661.md b/research/residue-product-tensor-recognition/vendor/PR5661.md new file mode 100644 index 0000000000..c3d085b38a --- /dev/null +++ b/research/residue-product-tensor-recognition/vendor/PR5661.md @@ -0,0 +1,202 @@ +# Recover split products from arbitrary tensors + +Let K=F_q be an explicitly represented finite field of characteristic p. +For a nonempty list of sorted height lists H=(h_1,...,h_s), put + + A_H = product_j K[x_ji] / (x_ji^(p^h_ji)). + +An empty height list is a field factor K. Sort the component height lists +lexicographically. Each local model uses the monomial order of the retained +PR5637 implementation. This fixes one reference tensor for each type multiset. + +**Result.** For any square tensor t:K^n x K^n -> K^n, the algorithm decides +whether t is isotopic to some A_H. On acceptance it returns H and invertible +U,V,W such that t(Ua,Vb)=W ab. It also returns a complete special-linear orbit +label and constructs determinant-one factor maps between equal-label tensors. +No algebra promise, component list, common input basis or invertible slice is +supplied. The algorithm is deterministic and polynomial in n for fixed K. + +The new result removes the supplied-decomposition premise of PR5656. It uses +the nucleus and local recognition results of PR5252, PR5540 and PR5637, the +height criterion of PR5502, and the product character theorem of PR5656. +These sources retain their credit. This is an algebraic interface result. +It supplies no physical supplier, paid implementation or complete kappa gain. + +## 1. Recover the algebra + +Solve the linear equations + + B = {(X,Y): t(Xu,v)=Y t(u,v) for every u,v}. + +Require dim B=n, injective projections to X and Y, commutativity of the Y +projection, and zero right kernel of t. B is a unital algebra under componentwise +composition. The injective Y projection identifies it with a commutative matrix +algebra and gives a multiplication table and unit by linear coordinates. + +For multiplication in any commutative unital algebra A, setting u=1 shows +Y(v)=X(1)v, and setting v=1 shows X=Y. Thus B is exactly the regular copy of +A. Isotopy transports both representations. All four tests are necessary. +They are not sufficient alone: both nucleus modules must also be regular. + +## 2. Find the radical and every primitive idempotent + +This extends Nick Petalas's fixed-algebra spectral projectors in PR5252 from +the reduced case to algebras with a nilradical. The projector formula itself +is retained mathematical precedent. + +Write J for the nilradical of B. A finite-dimensional commutative algebra has +a decomposition into local Artinian factors. Here is the needed nilpotence +bound. Its radical is nilpotent: choose a finite basis of nilpotent generators; +every sufficiently long monomial contains a generator to a zero power. If two +successive nonzero powers J^k and J^(k+1) were equal, iteration would contradict +nilpotence. Their dimensions strictly decrease until zero. Therefore J^n=0. + +Let Q be the least q-power at least n. The map b -> b^Q is K-linear. Its kernel +is J: it kills J by the bound above, and any element it kills is nilpotent. +This calculates J with exact linear algebra. + +The reduced quotient B/J is a product of finite residue fields. Primitive +idempotents lift uniquely through J. For existence, lift an idempotent to b; +then (b^2-b)^Q=0 gives an idempotent b^Q with the same residue. For uniqueness, +if idempotents e,f differ by an element of J, their commuting products e(1-f) +and f(1-e) are nilpotent idempotents, hence zero. Thus e=f. + +Let C=ker(b -> b^q-b). On each local factor the only fixed elements are the +scalars in K times that factor's unit. Indeed, its residue must lie in F_q. +After subtracting that scalar, a fixed nilpotent z satisfies z=z^(q^a)=0 for +large a. Hence C is K^s, where s is the number of local factors. The dimensions +give the exact split-residue test + + dim(B/J) = dim C. + +Each residue-field degree is positive. Equality holds precisely when every +degree is one. A nonsplit residue field is rejected, even when its q-power +map is invertible. + +Choose any K-basis c_1,...,c_s of C. Start with the part 1. For each c_i and +each lambda in K, refine every current part e by + + e * (1 - (c_i-lambda*1)^(q-1)), + +and discard zero results. In C=K^s this is the characteristic function of the +coordinates where c_i=lambda. The full basis separates every pair of distinct +coordinates. The resulting nonzero parts are exactly the s primitive +idempotents. Stop once s parts are present. This works when s>q; it does not +assume that one element separates all components. It also works with nonzero +nilpotent directions because every c_i belongs to the fixed subalgebra. + +## 3. Recover regular-module generators without enumeration + +For either nucleus module M, let M_j=e_j M. Compute JM_j from the literal +matrix actions. Require dim(M_j/JM_j)=1 for every j. Choose a basis vector of +M_j outside JM_j and call it m_j. Set m=sum_j m_j. + +In a regular module these dimensions are one because the residue fields are +K. Conversely, the cyclic submodule Bm maps onto each component's top. The +quotient N=M/Bm satisfies N=JN. Iteration and J^n=0 give N=0. Thus m is cyclic. +Since dim B=dim M=n, b -> bm is an isomorphism. This proves sufficiency and +gives a deterministic generator selection, without enumerating q^n vectors. + +Let u0,w0 be the generators for the X and Y actions. Define + + alpha(b)=X_b u0, gamma(b)=Y_b w0, Phi(v)=t(u0,v). + +If Phi(v)=0, the nucleus identity and cyclicity give t(u,v)=0 for every u. +The zero right kernel makes Phi invertible. Set beta=Phi^-1 gamma. Then + + t(alpha(a),beta(b)) = Y_a gamma(b) = gamma(ab). + +This gives three factor maps from B to the original tensor. The algorithm +checks each primitive component separately and then checks the generator +matrices for invertibility. + +## 4. Recognize each local factor and fix its basis + +For e_j, obtain a basis for e_j B from the columns of multiplication by e_j. +Restrict the recovered table to that basis. Apply the retained finite-field +recognizer of PR5637. It accepts exactly the split Frobenius-truncated local +algebras. Its semilinear p-power kernels recover the height flag; q-power +Frobenius is used only for the radical. The two operations are not exchanged. + +The local routine returns maps U_j,V_j,W_j with + + U_j(a) V_j(b) = W_j(ab). + +They need not be the same map. Put c=W_j(1). Setting one argument to 1 shows +that U_j(1) and V_j(1) are units: their multiplication maps are compositions of +invertible factor maps. Their product is c. The normalized map + + sigma_j = L_c^-1 W_j + +is a unital algebra isomorphism. Indeed, evaluation at 1 gives +U_j=L_(U_j(1)) sigma_j and V_j=L_(V_j(1)) sigma_j; substitution gives the +multiplication identity for sigma_j. The algorithm applies this normalization. +Treating W_j itself as an algebra isomorphism would be incorrect. + +Embed each sigma_j into B, sort the components by their full height lists, +and concatenate the actual basis columns into C. Set + + U=alpha C, V=beta C, W=gamma C. + +All n^2 transported basis products are checked. Bilinearity makes this a +certificate for all inputs. Rejected local factors cannot be replaced by +equal-dimensional ones: the height multiset is intrinsic. Necessity follows +from the primitive decomposition of A_H and the local recognition theorem. +Sufficiency follows from the explicit maps. This proves the recognition result. + +## 5. Product characters and determinant-one maps + +Use the exact theorem of PR5656. For component dimension N_j=p^(sum_i h_ji), +let E_ji=N_j(p^h_ji-1)/2. Let g be the gcd of q-1 and all these integers, +including (q-1)/2 if q is odd and some full component type repeats. If there +are no variables and no such repetition, g=q-1. The automorphism determinant +image is the subgroup of g-th powers in K*. The covariant tensor stabilizer +has determinant products in that same subgroup. + +Define + + d=det(W)/(det(U)det(V)), label=d^((q-1)/g). + +The full height-type multiset and label decide special-linear equivalence. +The basis concatenation above fixes the component-order determinant sign; +sorting metadata without reordering the matrix columns would lose it. + +For two equal-label certificates, set a=det(U1)/det(U2), b=det(V1)/det(V2), +c=det(W1)/det(W2). Construct a model automorphism sigma of determinant z=ab/c. +Bezout coefficients for the character exponents give it as variable scalings +and, when needed, one transposition of identical odd-dimensional components. +The implementation uses the literal block permutation, not a free scalar sign. + +The unit-multiplication determinant map is onto K*: choose one component of +dimension N_j, which is coprime to q-1, and vary only its scalar constant. +Choose units x,y with determinants a/z,b/z. Then +(L_x sigma,L_y sigma,L_(xy) sigma) has determinants a,b,c. Compose these maps +between the second certificate and the inverse first certificate. The resulting +F,G,H have determinant one and satisfy t2(Fu,Gv)=H t1(u,v). The checker verifies +all three determinants and every basis product. The total product dimension +need not be coprime to q-1; no inverse of that total dimension is used. + +## 6. Cost, use and limits + +The nucleus has n^3 equations in 2n^2 unknowns. Dense elimination uses O(n^7) +field operations. The component refinements use at most n^2 q exponentiations +with exponent q-1; dense algebra multiplication costs O(n^3). The local +recognizers cost at most the sum of their dimension-seventh powers, bounded +by n^7. Module, coordinate and product checks are polynomial as well. A +conservative total bound is O(n^8 + q*n^6*log(q*n) + q^2) field operations, +with polynomial space. This is polynomial in n for fixed q. The explicit +field tables and primitive-element/discrete-log enumeration are not polynomial +bit algorithms in log q. No such uniform claim is made. + +This closes the decomposition-discovery task for the declared split product +class, including extension fields, repeated factors, nilpotents, and independent +tensor factor bases. It does not recognize arbitrary commutative algebras or +nontrivial residue extensions. The tensor atlas can now check this class from +raw tensors and return exact maps. A physical application must still pay for +coefficient operations, native realization, ownership, restoration, storage, +precision and the whole supplier/caller. These costs are unknown here. The +complete kappa calculation and selected frontier are unchanged. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. The same +assistant supplied the proof and checks. Independent human and formal review +remain open. diff --git a/research/residue-product-tensor-recognition/vendor/local.py b/research/residue-product-tensor-recognition/vendor/local.py new file mode 100644 index 0000000000..1066bb74c1 --- /dev/null +++ b/research/residue-product-tensor-recognition/vendor/local.py @@ -0,0 +1,370 @@ +"""Exact finite-field tensor recognition. Ali Romman with OpenAI Codex. Apache-2.0.""" +from itertools import product +from math import gcd, isqrt + + +class Field: + """Use base-p digits and a monic polynomial, in constant-first order.""" + + def __init__(self, p, modulus): + if type(p) is not int or p < 2 or any(p % d == 0 for d in range(2, isqrt(p) + 1)): + raise ValueError('p must be prime') + if (not isinstance(modulus, (tuple, list)) or len(modulus) < 2 + or modulus[-1] != 1 + or any(type(c) is not int or not 0 <= c < p for c in modulus)): + raise ValueError('modulus must be monic with canonical prime-field coefficients') + self.p, self.e = p, len(modulus) - 1 + self.modulus = tuple(modulus) + self.q = p ** self.e + digits = [[(a // p ** i) % p for i in range(self.e)] for a in range(self.q)] + self.add = [[sum(((x + y) % p) * p ** i for i, (x, y) in enumerate(zip(a, b))) + for b in digits] for a in digits] + self.neg = [sum((-x % p) * p ** i for i, x in enumerate(a)) for a in digits] + self.mul = [] + for a in digits: + row = [] + for b in digits: + c = [0] * (2 * self.e - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + c[i + j] = (c[i + j] + x * y) % p + for k in range(len(c) - 1, self.e - 1, -1): + for j in range(self.e): + c[k - self.e + j] = (c[k - self.e + j] - c[k] * modulus[j]) % p + row.append(sum(c[i] * p ** i for i in range(self.e))) + self.mul.append(row) + self.inv = [0] + [self.power(a, self.q - 2) for a in range(1, self.q)] + if any(self.mul[a][self.inv[a]] != 1 for a in range(1, self.q)): + raise ValueError('modulus is reducible') + + def power(self, a, n): + if n < 0: + raise ValueError('negative exponent') + r = 1 + while n: + if n & 1: + r = self.mul[r][a] + a = self.mul[a][a] + n //= 2 + return r + + def total(self, xs): + r = 0 + for x in xs: + r = self.add[r][x] + return r + + +def identity(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def columns(xs, n): + return [[v[i] for v in xs] for i in range(n)] + + +def column(a, j): + return [r[j] for r in a] + + +def rref(a, width, f): + rows = [r[:] for r in a] + pivots = [] + k = 0 + for j in range(width): + pivot = next((i for i in range(k, len(rows)) if rows[i][j]), None) + if pivot is None: + continue + rows[k], rows[pivot] = rows[pivot], rows[k] + rows[k] = [f.mul[f.inv[rows[k][j]]][x] for x in rows[k]] + for i in range(len(rows)): + if i != k and rows[i][j]: + c = f.neg[rows[i][j]] + rows[i] = [f.add[x][f.mul[c][y]] for x, y in zip(rows[i], rows[k])] + pivots.append(j) + k += 1 + if k == len(rows): + break + return rows, pivots + + +def rank(a, f): + return len(rref(a, len(a[0]) if a else 0, f)[1]) + + +def kernel(a, width, f): + rows, pivots = rref(a, width, f) + out = [] + for j in range(width): + if j in pivots: + continue + v = [0] * width + v[j] = 1 + for i, p in enumerate(pivots): + v[p] = f.neg[rows[i][j]] + out.append(v) + return out + + +def inverse(a, f): + n = len(a) + rows, pivots = rref([r + e for r, e in zip(a, identity(n))], n, f) + if len(pivots) != n: + raise ValueError('singular matrix') + return [r[n:] for r in rows] + + +def mv(a, v, f): + return [f.total(f.mul[x][y] for x, y in zip(r, v)) for r in a] + + +def mm(a, b, f): + return columns([mv(a, column(b, j), f) for j in range(len(b[0]))], len(a)) + + +def determinant(a, f): + rows = [r[:] for r in a] + d = 1 + for j in range(len(rows)): + k = next((i for i in range(j, len(rows)) if rows[i][j]), None) + if k is None: + return 0 + if k != j: + rows[k], rows[j] = rows[j], rows[k] + d = f.neg[d] + c = rows[j][j] + d = f.mul[d][c] + for i in range(j + 1, len(rows)): + z = f.neg[f.mul[rows[i][j]][f.inv[c]]] + rows[i] = [f.add[x][f.mul[z][y]] for x, y in zip(rows[i], rows[j])] + return d + + +def tensor_value(t, u, v, f): + n = len(t) + out = [0] * n + for i, x in enumerate(u): + if x: + for j, y in enumerate(v): + if y: + c = f.mul[x][y] + out = [f.add[z][f.mul[c][a]] for z, a in zip(out, t[i][j])] + return out + + +def algebra_power(t, u, exponent, unit, f): + r = unit[:] + while exponent: + if exponent & 1: + r = tensor_value(t, r, u, f) + u = tensor_value(t, u, u, f) + exponent //= 2 + return r + + +def model(heights, f): + bounds = [f.p ** h for h in heights] + exponents = list(product(*(range(b) for b in bounds))) + ix = {v: i for i, v in enumerate(exponents)} + n = len(exponents) + t = [[[0] * n for _ in range(n)] for _ in range(n)] + for i, a in enumerate(exponents): + for j, b in enumerate(exponents): + c = tuple(x + y for x, y in zip(a, b)) + if all(x < bound for x, bound in zip(c, bounds)): + t[i][j][ix[c]] = 1 + return t, exponents + + +def semilinear_kernel(t, unit, h, f): + """Return ker(a -> a^(p^h)), with the coefficient twist removed.""" + n = len(t) + c = columns([algebra_power(t, v, f.p ** h, unit, f) for v in identity(n)], n) + untwist = f.p ** ((-h) % f.e) + return [[f.power(x, untwist) for x in v] for v in kernel(c, n, f)] + + +def validate_tensor(t, f): + if not isinstance(f, Field): + raise ValueError('field contract required') + if not isinstance(t, (list, tuple)) or not t: + raise ValueError('positive square tensor required') + n = len(t) + if any(not isinstance(a, (list, tuple)) or len(a) != n for a in t): + raise ValueError('input dimensions differ') + for a in t: + for b in a: + if not isinstance(b, (list, tuple)) or len(b) != n: + raise ValueError('output dimension differs') + if any(type(x) is not int or not 0 <= x < f.q for x in b): + raise ValueError('noncanonical field entry') + + +def check_certificate(t, cert, f): + """Check the factor maps by all basis products, without nucleus tests.""" + n = len(t) + mu, _ = model(cert['heights'], f) + if len(mu) != n: + return False + u, v, w = (cert[k] for k in ('U', 'V', 'W')) + if any(determinant(a, f) == 0 for a in (u, v, w)): + return False + for i in range(n): + for j in range(n): + if tensor_value(t, column(u, i), column(v, j), f) != mv(w, mu[i][j], f): + return False + return True + + +def recognize(t, f): + """Return (certificate, None), or (None, mathematical rejection reason).""" + validate_tensor(t, f) + n = len(t) + equations = [] + for i, j, k in product(range(n), repeat=3): + row = [0] * (2 * n * n) + for a in range(n): + row[a * n + i] = f.add[row[a * n + i]][t[a][j][k]] + index = n * n + k * n + a + row[index] = f.add[row[index]][f.neg[t[i][j][a]]] + equations.append(row) + basis = kernel(equations, 2 * n * n, f) + if len(basis) != n: + return None, 'nucleus dimension' + xb = [[b[i * n:(i + 1) * n] for i in range(n)] for b in basis] + yb = [[b[n * n + i * n:n * n + (i + 1) * n] for i in range(n)] for b in basis] + if rank([b[:n*n] for b in basis], f) != n or rank([b[n*n:] for b in basis], f) != n: + return None, 'nucleus projection' + if any(mm(a, b, f) != mm(b, a, f) for a in yb for b in yb): + return None, 'noncommutative nucleus' + right = [[t[i][j][k] for j in range(n)] for i in range(n) for k in range(n)] + if rank(right, f) != n: + return None, 'right kernel' + flat = [sum(a, []) for a in yb] + _, positions = rref(flat, n * n, f) + coord_inverse = inverse([[a[j] for a in flat] for j in positions], f) + + def coordinates(a): + v = sum(a, []) + c = mv(coord_inverse, [v[j] for j in positions], f) + if [f.total(f.mul[c[k]][flat[k][j]] for k in range(n)) for j in range(n*n)] != v: + raise ArithmeticError('nucleus closure') + return c + + table = [[coordinates(mm(a, b, f)) for b in yb] for a in yb] + unit = coordinates(identity(n)) + exponent = 1 + while exponent < n: + exponent *= f.q + qmap = columns([algebra_power(table, v, exponent, unit, f) for v in identity(n)], n) + radical = kernel(qmap, n, f) + if len(radical) != n - 1: + return None, 'residue field or number of components' + + def cyclic(module): + actions = [[[f.total(f.mul[c[k]][module[k][i][j]] for k in range(n)) + for j in range(n)] for i in range(n)] for c in radical] + jm = [column(a, j) for a in actions for j in range(n)] + if rank(jm, f) != n - 1: + return None + seed = next(v for v in identity(n) if rank(jm + [v], f) == n) + return columns([mv(a, seed, f) for a in module], n), seed + + ux, wy = cyclic(xb), cyclic(yb) + if ux is None or wy is None: + return None, 'nonregular nucleus module' + u, u0 = ux + w, _ = wy + phi = columns([tensor_value(t, u0, e, f) for e in identity(n)], n) + v = mm(inverse(phi, f), w, f) + span = [tensor_value(table, a, b, f) for a in radical for b in radical] + current = rank(span, f) + generators, heights = [], [] + h, power = 0, 1 + while power < n: + h += 1 + power *= f.p + for a in semilinear_kernel(table, unit, h, f): + new_rank = rank(span + [a], f) + if new_rank > current: + span.append(a) + generators.append(a) + heights.append(h) + current = new_rank + if f.p ** sum(heights) != n: + return None, 'height dimension' + mu, exponents = model(heights, f) + images = [] + for exps in exponents: + value = unit[:] + for g, e in zip(generators, exps): + value = tensor_value(table, value, algebra_power(table, g, e, unit, f), f) + images.append(value) + c = columns(images, n) + if determinant(c, f) == 0: + raise ArithmeticError('height criterion did not produce a basis') + cert = {'heights': heights, 'U': mm(u, c, f), 'V': mm(v, c, f), 'W': mm(w, c, f)} + if not check_certificate(t, cert, f): + raise ArithmeticError('transported product mismatch') + index = gcd(f.q - 1, *(n * (f.p ** h - 1) // 2 for h in heights)) + detu, detv, detw = (determinant(cert[k], f) for k in ('U', 'V', 'W')) + delta = f.mul[detw][f.inv[f.mul[detu][detv]]] + cert['sl_orbit_count'] = index + cert['sl_orbit_label'] = f.power(delta, (f.q - 1) // index) + return cert, None + + +def bezout(a, b): + x, y, u, v = 1, 0, 0, 1 + while b: + quotient, remainder = divmod(a, b) + a, b = b, remainder + x, u = u, x - quotient * u + y, v = v, y - quotient * v + return a, x, y + + +def sl_transporter(first, second, f): + """Return determinant-one maps F,G,H with second(Fu,Gv)=H first(u,v).""" + a, why = recognize(first, f) + if a is None: + return None, 'first tensor: ' + why + b, why = recognize(second, f) + if b is None: + return None, 'second tensor: ' + why + if a['heights'] != b['heights'] or a['sl_orbit_label'] != b['sl_orbit_label']: + return None, 'different special-linear orbits' + n, m = len(first), f.q - 1 + du, dv, dw = [f.mul[determinant(a[k], f)][f.inv[determinant(b[k], f)]] + for k in ('U', 'V', 'W')] + z = f.mul[f.mul[du][dv]][f.inv[dw]] + primitive = next(c for c in range(1, f.q) + if len({f.power(c, i) for i in range(m)}) == m) + logz = next(i for i in range(m) if f.power(primitive, i) == z) + g, coefficients = m, [] + for h in a['heights']: + g, x, y = bezout(g, n * (f.p ** h - 1) // 2) + coefficients = [x * c for c in coefficients] + [y] + if logz % g: + raise ArithmeticError('orbit label disagrees with determinant image') + scalars = [f.power(primitive, (c * (logz // g)) % m) for c in coefficients] + _, exponents = model(a['heights'], f) + diagonal = [1] * n + for j, es in enumerate(exponents): + for c, e in zip(scalars, es): + diagonal[j] = f.mul[diagonal[j]][f.power(c, e)] + inverse_n = pow(n, -1, m) + unit_a = f.power(f.mul[du][f.inv[z]], inverse_n) + unit_b = f.power(f.mul[dv][f.inv[z]], inverse_n) + factors = [unit_a, unit_b, f.mul[unit_a][unit_b]] + out = {} + for key, target, scalar in zip(('U', 'V', 'W'), ('F', 'G', 'H'), factors): + middle = [[f.mul[scalar][diagonal[i]] if i == j else 0 for j in range(n)] for i in range(n)] + out[target] = mm(mm(b[key], middle, f), inverse(a[key], f), f) + if determinant(out[target], f) != 1: + raise ArithmeticError('determinant correction failed') + for i in range(n): + for j in range(n): + if tensor_value(second, column(out['F'], i), column(out['G'], j), f) != mv(out['H'], first[i][j], f): + raise ArithmeticError('special-linear product mismatch') + return out, None diff --git a/research/residue-product-tensor-recognition/vendor/split.py b/research/residue-product-tensor-recognition/vendor/split.py new file mode 100644 index 0000000000..21f1347361 --- /dev/null +++ b/research/residue-product-tensor-recognition/vendor/split.py @@ -0,0 +1,258 @@ +"""Recover split local products. Ali Romman with OpenAI Codex. Apache-2.0.""" +from itertools import product +from math import gcd +from vendor import local as a + + +def span(vectors, n, f): + rows, pivots = a.rref(vectors, n, f) + return rows[:len(pivots)] + + +def coordinate_map(basis, n, f): + _, pivots = a.rref(basis, n, f) + inv = a.inverse([[v[j] for v in basis] for j in pivots], f) + + def coordinates(v): + c = a.mv(inv, [v[j] for j in pivots], f) + if a.mv(a.columns(basis, n), c, f) != v: + raise ArithmeticError('value is outside the declared subspace') + return c + + return coordinates + + +def linear_combination(coefficients, matrices, f): + n = len(matrices[0]) + return [[f.total(f.mul[c][m[i][j]] for c, m in zip(coefficients, matrices)) + for j in range(n)] for i in range(n)] + + +def split_algebra(table, unit, f): + """Return the radical and primitive idempotents, or a residue rejection.""" + n = len(table) + power = 1 + while power < n: + power *= f.q + radical = a.kernel(a.columns([a.algebra_power(table, e, power, unit, f) + for e in a.identity(n)], n), n, f) + qcols = [a.algebra_power(table, e, f.q, unit, f) for e in a.identity(n)] + fixed = a.kernel([[f.add[qcols[j][i]][f.neg[int(i == j)]] + for j in range(n)] for i in range(n)], n, f) + if len(radical) + len(fixed) != n: + return None, 'nonsplit residue field' + parts = [unit] + for c in fixed: + refined = [] + for e in parts: + for scalar in range(f.q): + shifted = [f.add[x][f.neg[f.mul[scalar][y]]] for x, y in zip(c, unit)] + v = a.algebra_power(table, shifted, f.q - 1, unit, f) + projector = [f.add[x][f.neg[y]] for x, y in zip(unit, v)] + piece = a.tensor_value(table, e, projector, f) + if any(piece): + refined.append(piece) + parts = refined + if len(parts) == len(fixed): + break + if len(parts) != len(fixed): + raise ArithmeticError('primitive idempotent count') + return (radical, parts), None + + +def regular_generator(matrices, radical, parts, f): + n = len(matrices[0]) + seed = [0] * n + radical_actions = [linear_combination(c, matrices, f) for c in radical] + for e in parts: + projector = linear_combination(e, matrices, f) + block = span([a.column(projector, j) for j in range(n)], n, f) + jm = span([a.mv(action, v, f) for action in radical_actions for v in block], n, f) + if len(block) - len(jm) != 1: + return None + v = next(v for v in block if a.rank(jm + [v], f) > len(jm)) + seed = [f.add[x][y] for x, y in zip(seed, v)] + matrix = a.columns([a.mv(m, seed, f) for m in matrices], n) + if not a.determinant(matrix, f): + raise ArithmeticError('component generators did not give a regular module') + return matrix, seed + + +def product_model(types, f): + models = [a.model(h, f)[0] for h in types] + n = sum(map(len, models)) + table = [[[0] * n for _ in range(n)] for _ in range(n)] + offset = 0 + for mu in models: + for i, row in enumerate(mu): + for j, value in enumerate(row): + table[offset+i][offset+j][offset:offset+len(mu)] = value + offset += len(mu) + return table + + +def character_index(types, f): + exponents = [f.q-1] + for heights in types: + n = f.p ** sum(heights) + exponents.extend(n * (f.p ** h - 1) // 2 for h in heights) + if f.p != 2 and len({tuple(h) for h in types}) < len(types): + exponents.append((f.q-1)//2) + return gcd(*exponents) + + +def check_certificate(t, cert, f): + """Check literal products and the canonical character label.""" + try: + a.validate_tensor(t, f) + types = cert['types'] + if not types or types != sorted(types): + return False + if any(hs != sorted(hs) or any(type(h) is not int or h < 1 for h in hs) for hs in types): + return False + n = len(t) + if sum(f.p ** sum(hs) for hs in types) != n: + return False + matrices = [cert[k] for k in ('U', 'V', 'W')] + if any(len(m) != n or any(len(row) != n or any(type(x) is not int or not 0 <= x < f.q for x in row) + for row in m) for m in matrices): + return False + if any(not a.determinant(m, f) for m in matrices): + return False + u, v, w = matrices + mu = product_model(types, f) + for i, j in product(range(n), repeat=2): + if a.tensor_value(t, a.column(u, i), a.column(v, j), f) != a.mv(w, mu[i][j], f): + return False + g = character_index(types, f) + delta = f.mul[a.determinant(w, f)][f.inv[f.mul[a.determinant(u, f)][a.determinant(v, f)]]] + return cert['sl_orbit_count'] == g and cert['sl_orbit_label'] == f.power(delta, (f.q-1)//g) + except (KeyError, TypeError, ValueError, IndexError): + return False + + +def recognize(t, f): + """Return a complete product certificate, or a mathematical rejection.""" + a.validate_tensor(t, f) + n = len(t) + equations = [] + for i, j, k in product(range(n), repeat=3): + row = [0] * (2*n*n) + for z in range(n): + row[z*n+i] = f.add[row[z*n+i]][t[z][j][k]] + row[n*n+k*n+z] = f.add[row[n*n+k*n+z]][f.neg[t[i][j][z]]] + equations.append(row) + basis = a.kernel(equations, 2*n*n, f) + if len(basis) != n: + return None, 'nucleus dimension' + xb = [[b[i*n:(i+1)*n] for i in range(n)] for b in basis] + yb = [[b[n*n+i*n:n*n+(i+1)*n] for i in range(n)] for b in basis] + if any(a.rank([b[start:start+n*n] for b in basis], f) != n for start in (0, n*n)): + return None, 'nucleus projection' + if any(a.mm(x, y, f) != a.mm(y, x, f) for x in yb for y in yb): + return None, 'noncommutative nucleus' + if a.rank([[t[i][j][k] for j in range(n)] for i in range(n) for k in range(n)], f) != n: + return None, 'right kernel' + coordinates = coordinate_map([sum(m, []) for m in yb], n*n, f) + table = [[coordinates(sum(a.mm(x, y, f), [])) for y in yb] for x in yb] + unit = coordinates(sum(a.identity(n), [])) + split, reason = split_algebra(table, unit, f) + if split is None: + return None, reason + radical, parts = split + ux, wy = (regular_generator(ms, radical, parts, f) for ms in (xb, yb)) + if ux is None or wy is None: + return None, 'nonregular nucleus module' + u, u0 = ux + w, _ = wy + phi = a.columns([a.tensor_value(t, u0, e, f) for e in a.identity(n)], n) + v = a.mm(a.inverse(phi, f), w, f) + factors = [] + for e in parts: + block = span([a.tensor_value(table, e, x, f) for x in a.identity(n)], n, f) + coord = coordinate_map(block, n, f) + local = [[coord(a.tensor_value(table, x, y, f)) for y in block] for x in block] + cert, reason = a.recognize(local, f) + if cert is None: + return None, 'local factor: '+reason + # Normalize the local output map to a unital algebra isomorphism. + image_one = a.column(cert['W'], 0) + multiply_one = a.columns([a.tensor_value(local, image_one, x, f) + for x in a.identity(len(block))], len(block)) + sigma = a.mm(a.inverse(multiply_one, f), cert['W'], f) + images = a.mm(a.columns(block, n), sigma, f) + factors.append((cert['heights'], images)) + factors.sort(key=lambda item: item[0]) + change = a.columns([a.column(m, j) for _, m in factors for j in range(len(m[0]))], n) + cert = {'types': [hs for hs, _ in factors], 'U': a.mm(u, change, f), + 'V': a.mm(v, change, f), 'W': a.mm(w, change, f)} + g = character_index(cert['types'], f) + du, dv, dw = (a.determinant(cert[k], f) for k in ('U', 'V', 'W')) + cert['sl_orbit_count'] = g + cert['sl_orbit_label'] = f.power(f.mul[dw][f.inv[f.mul[du][dv]]], (f.q-1)//g) + if not check_certificate(t, cert, f): + raise ArithmeticError('product certificate failed') + return cert, None + + +def sl_transporter(first, second, f): + one, why = recognize(first, f) + if one is None: + return None, 'first tensor: '+why + two, why = recognize(second, f) + if two is None: + return None, 'second tensor: '+why + if one['types'] != two['types'] or one['sl_orbit_label'] != two['sl_orbit_label']: + return None, 'different special-linear orbits' + types, n, length = one['types'], len(first), f.q-1 + du, dv, dw = [f.mul[a.determinant(one[k], f)][f.inv[a.determinant(two[k], f)]] + for k in ('U', 'V', 'W')] + z = f.mul[f.mul[du][dv]][f.inv[dw]] + primitive = next(x for x in range(1, f.q) if len({f.power(x, j) for j in range(length)}) == length) + logz = next(j for j in range(length) if f.power(primitive, j) == z) + generators = [] + offset = 0 + starts = [] + for hs in types: + size = f.p ** sum(hs) + starts.append((offset, size)) + for i, h in enumerate(hs): + generators.append((size*(f.p**h-1)//2, ('scale', offset, hs, i))) + offset += size + repeated = next((i for i in range(1, len(types)) if types[i] == types[i-1]), None) + if f.p != 2 and repeated is not None: + generators.append((length//2, ('swap', repeated-1, repeated))) + g, weights = length, [] + for exponent, _ in generators: + g, x, y = a.bezout(g, exponent) + weights = [x*c for c in weights]+[y] + if logz % g: + raise ArithmeticError('character witness failed') + sigma = a.identity(n) + for weight, (_, operation) in zip(weights, generators): + coefficient = weight*(logz//g) + if operation[0] == 'scale': + _, start, hs, index = operation + scalar = f.power(primitive, coefficient % length) + for j, exps in enumerate(a.model(hs, f)[1]): + sigma[start+j] = [f.mul[f.power(scalar, exps[index])][x] for x in sigma[start+j]] + elif coefficient % 2: + _, left, right = operation + lstart, size = starts[left] + rstart, _ = starts[right] + for j in range(size): + sigma[lstart+j], sigma[rstart+j] = sigma[rstart+j], sigma[lstart+j] + size = starts[0][1] + inverse_size = pow(size, -1, length) + x = f.power(f.mul[du][f.inv[z]], inverse_size) + y = f.power(f.mul[dv][f.inv[z]], inverse_size) + out = {} + for key, target, scalar in zip(('U', 'V', 'W'), ('F', 'G', 'H'), (x, y, f.mul[x][y])): + middle = [[f.mul[scalar if i < size else 1][value] for value in row] for i, row in enumerate(sigma)] + out[target] = a.mm(a.mm(two[key], middle, f), a.inverse(one[key], f), f) + if any(a.determinant(m, f) != 1 for m in out.values()): + raise ArithmeticError('special-linear determinant') + for i, j in product(range(n), repeat=2): + if a.tensor_value(second, a.column(out['F'], i), a.column(out['G'], j), f) != a.mv(out['H'], first[i][j], f): + raise ArithmeticError('special-linear product') + return out, None diff --git a/research/residue-product-tensor-recognition/verify.py b/research/residue-product-tensor-recognition/verify.py new file mode 100644 index 0000000000..1859308cd7 --- /dev/null +++ b/research/residue-product-tensor-recognition/verify.py @@ -0,0 +1,184 @@ +"""Check residue products. Ali Romman with OpenAI Codex. Apache-2.0.""" +import copy +import hashlib +import itertools +import json +from pathlib import Path +import random +import sys +from collections import deque +HERE = Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) + +def require(ok, message): + if not ok: + raise RuntimeError(message) + + +def changed(t, u, v, w, f): + n = len(t) + ui, vi = r.a.inverse(u, f), r.a.inverse(v, f) + return [[r.a.mv(w, r.a.tensor_value(t, r.a.column(ui, i), r.a.column(vi, j), f), f) + for j in range(n)] for i in range(n)] + + +def random_gl(n, f, rng, special=False): + m = r.a.identity(n) + for _ in range(4*n): + if n > 1: + i, j = rng.sample(range(n), 2) + c = rng.randrange(f.q) + m[i] = [f.add[x][f.mul[c][y]] for x, y in zip(m[i], m[j])] + if not special: + for i in range(n): + c = rng.randrange(1, f.q) + m[i] = [f.mul[c][x] for x in m[i]] + return m + + +def orbit(f, seeds): + """Apply GL2 generators directly to the three coefficient indices.""" + generators = [[[0,1],[1,0]]] + generators.extend([[[1,c],[0,1]] for c in range(1,f.q)]) + generators.extend([[[c,0],[0,1]] for c in range(2,f.q)]) + + def pack(vals): + return sum(c*f.q**i for i,c in enumerate(vals)) + + seen = {pack(sum(sum(t, []), [])) for t in seeds} + queue = deque(seen) + while queue: + code = queue.popleft() + vals = [(code//f.q**i)%f.q for i in range(8)] + for axis in (1,2,4): + for m in generators: + out = vals[:] + for i in range(8): + if not i & axis: + x,y = vals[i],vals[i+axis] + out[i] = f.add[f.mul[m[0][0]][x]][f.mul[m[0][1]][y]] + out[i+axis] = f.add[f.mul[m[1][0]][x]][f.mul[m[1][1]][y]] + value = pack(out) + if value not in seen: + seen.add(value) + queue.append(value) + return seen + + +def polynomial_field(modulus,f): + d = len(modulus)-1 + table = [] + for i in range(d): + row = [] + for j in range(d): + v = [0]*(2*d-1) + v[i+j] = 1 + for k in range(len(v)-1,d-1,-1): + for z in range(d): + v[k-d+z] = f.add[v[k-d+z]][f.neg[f.mul[v[k]][modulus[z]]]] + row.append(v[:d]) + table.append(row) + require(r.field_table_valid(table,f),'fixture field is reducible') + return table + + +def quadratic(f): + for c,d in itertools.product(range(f.q),repeat=2): + if all(f.total([f.mul[x][x],f.mul[d][x],c]) for x in range(f.q)): + return polynomial_field([c,d,1],f) + raise RuntimeError('quadratic fixture absent') + + +def exhaustive(f): + field1 = [[[1]]] + components = [[dict(degree=1,heights=[],field=field1)]*2, + [dict(degree=2,heights=[],field=quadratic(f))]] + if f.p==2: + components.append([dict(degree=1,heights=[1],field=field1)]) + expected = orbit(f,[r.product_model(cs,f) for cs in components]) + digest = hashlib.sha256() + accepted = 0 + for code in range(f.q**8): + vals = [(code//f.q**i)%f.q for i in range(8)] + t = [[vals[4*i+2*j:4*i+2*j+2] for j in range(2)] for i in range(2)] + cert,why = r.recognize(t,f) + require((cert is not None)==(code in expected),str((f.q,code,why))) + if cert is not None: + require(r.check_certificate(t,cert,f),'exhaustive literal map') + accepted += 1 + digest.update(code.to_bytes(4,'big')) + return dict(q=f.q,tensors=f.q**8,accepted=accepted,sha256=digest.hexdigest()) + + +def main(): + source = json.loads((HERE/'SOURCES.json').read_text()) + for item in source['external_inputs']: + require(hashlib.sha256((HERE/item['local_path']).read_bytes()).hexdigest()==item['sha256'],'retained source changed') + global r + import recognize as r + fs = [r.a.Field(2,[0,1]),r.a.Field(3,[0,1]),r.a.Field(2,[1,1,1]),r.a.Field(3,[1,0,1])] + rng = random.Random(56615656) + fixtures = products = controls = 0 + for f in fs: + field1 = [[[1]]] + field2 = quadratic(f) + unit = dict(degree=1,heights=[],field=field1) + ext = dict(degree=2,heights=[],field=field2) + nil = dict(degree=2,heights=[1],field=field2) + field3 = polynomial_field([1,1,0,1] if f.p==2 else [1,2,0,1],f) + ext3 = dict(degree=3,heights=[],field=field3) + nil3 = dict(degree=3,heights=[1],field=field3) + cases = [[ext],[nil],[unit,nil],[ext,ext],[nil,nil],[ext3],[nil3]] + if f.p==2: + cases.append([dict(degree=2,heights=[2],field=field2)]) + for cs in cases: + mu = r.product_model(cs,f) + n = len(mu) + if n>8: + continue + target_types = sorted((c['degree'],c['heights']) for c in cs) + for _ in range(2): + u,v,w = (random_gl(n,f,rng) for _ in range(3)) + t = changed(mu,u,v,w,f) + cert,why = r.recognize(t,f) + require(cert is not None,str((f.q,target_types,why))) + require(sorted((c['degree'],c['heights']) for c in cert['components'])==target_types,'residue or height type') + require(r.check_certificate(t,cert,f),'literal product') + fixtures += 1 + products += n*n + for key in ('U','V','W'): + bad = copy.deepcopy(cert);bad[key][0][0]=f.add[bad[key][0][0]][1] + require(not r.check_certificate(t,bad,f),'changed factor accepted') + controls += 1 + bad = copy.deepcopy(cert);bad['components'][0]['field'][0][0][0]=0 + require(not r.check_certificate(t,bad,f),'false coefficient field accepted') + bad = copy.deepcopy(cert);bad['components'][0]['degree']+=1 + require(not r.check_certificate(t,bad,f),'false residue degree accepted') + controls += 2 + # A local square-zero algebra of rank three over the extension has an extra relation. + d = 2 + square = [[[0]*(3*d) for _ in range(3*d)] for _ in range(3*d)] + for i,j in itertools.product(range(3),repeat=2): + if i and j: + continue + for x,y in itertools.product(range(d),repeat=2): + square[d*i+x][d*j+y][d*(i+j):d*(i+j+1)] = field2[x][y] + require(r.recognize(square,f)[0] is None,'extra residue-local relation accepted') + n = len(square) + dual = [[[square[i][k][j] for k in range(n)] for j in range(n)] for i in range(n)] + require(r.recognize(dual,f)[1]=='nonregular nucleus module','nonregular nonsplit module accepted') + controls += 2 + # A reduced product of two fields is not a coefficient field. + split = r.product_model([unit,unit],f) + require(not r.field_table_valid(split,f),'reduced product called a field') + controls += 1 + report = dict(presentations=fixtures,basis_products=products,controls=controls, + exhaustive=[exhaustive(f) for f in fs[:3]]) + print(json.dumps(report,sort_keys=True)) + print('PASS_RESIDUE_PRODUCT_TENSOR_RECOGNITION') + + +if __name__=='__main__': + main() + +