From f1c2c18b650b8e46590815b09daa6120f50e380d Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 15:26:24 +0000 Subject: [PATCH] feat(research): classify cube-zero local algebra isomorphisms --- .../cube-zero-gorenstein-isomorphism/PROOF.md | 190 +++++++++++++ .../README.md | 116 ++++++++ .../SOURCES.json | 24 ++ .../TASK.json | 124 +++++++++ .../VERIFY.json | 32 +++ .../algebra.py | 249 ++++++++++++++++++ .../verify.py | 237 +++++++++++++++++ 7 files changed, 972 insertions(+) create mode 100644 research/cube-zero-gorenstein-isomorphism/PROOF.md create mode 100644 research/cube-zero-gorenstein-isomorphism/README.md create mode 100644 research/cube-zero-gorenstein-isomorphism/SOURCES.json create mode 100644 research/cube-zero-gorenstein-isomorphism/TASK.json create mode 100644 research/cube-zero-gorenstein-isomorphism/VERIFY.json create mode 100644 research/cube-zero-gorenstein-isomorphism/algebra.py create mode 100644 research/cube-zero-gorenstein-isomorphism/verify.py diff --git a/research/cube-zero-gorenstein-isomorphism/PROOF.md b/research/cube-zero-gorenstein-isomorphism/PROOF.md new file mode 100644 index 0000000000..9d4d505fd2 --- /dev/null +++ b/research/cube-zero-gorenstein-isomorphism/PROOF.md @@ -0,0 +1,190 @@ +# A complete restricted recovered-algebra isomorphism test + +Produced by Nick Petalas. Apache-2.0. + +## 1. Contract and multiplication form + +Let K be a finite field of odd order q. Let A be a finite-dimensional, +commutative, associative, unital local K-algebra, with radical J, residue +A/J=K, nonzero one-dimensional J^2 and J^3=0. Require its socle +Ann_A(J) to equal J^2. Put r=dim_K J/J^2. Necessarily r>=1. + +Choose a nonzero s in J^2 and a K-linear complement V of J^2 in J. +Then A=K*1 direct-sum V direct-sum K*s. Since J^3=0, there is a symmetric +bilinear form B on V such that + +```text +uv = B(u,v)s, us = s^2 = 0, for u,v in V. +``` + +The form is nondegenerate. A vector in its radical annihilates J, so would +belong to the socle J^2 while lying in its chosen complement. Conversely, +every nondegenerate symmetric r-dimensional B defines such an algebra A_B. +Associativity follows because every product of three elements of J is zero. +The socle contains no element with nonzero constant coefficient, and its +intersection with V is zero by nondegeneracy. Thus it is exactly K*s. + +Adding multiples of s to the chosen lifts does not change B. A change of +basis in V replaces B by a congruent form; rescaling s multiplies B by a +nonzero scalar. These choices are the only ambiguity relevant below. + +## 2. Isomorphism is similarity of forms + +A unital K-algebra isomorphism preserves J and J^2. Between A_B and A_D +it therefore has the shape + +```text +1 -> 1, u -> P u + ell(u)s, s -> c s, +P invertible, c nonzero. +``` + +Multiplication preservation is equivalent to + +```text +P^T D P = c B. (1) +``` + +Every such P,c and every linear ell give an isomorphism. In particular, +set ell=0 to construct a transporter. Thus the complete invariant is the +similarity class of the nondegenerate symmetric form, not its congruence +class with a fixed socle generator. + +## 3. Elementary classification and constructive reduction + +We include the classical form argument to specify the maps exactly. +Every nondegenerate symmetric form over odd K has an orthogonal basis. +If every diagonal entry in a nonzero residual block is zero, a nonzero +off-diagonal entry yields a vector e_i+e_j of norm 2B_ij != 0. +Split off that vector and continue on its nondegenerate orthogonal +complement. This terminates after r steps. + +For any nonzero a,b in K, the sets + +```text +{a*u^2 : u in K}, {1-b*v^2 : v in K} +``` + +both have size (q+1)/2, so intersect. Choose u,v with au^2+bv^2=1. +In diag(a,b), the vectors (u,v) and (-bv,au) have respective norms +1 and ab and are orthogonal. Their basis determinant is one. Apply this +two-coordinate reduction successively to obtain diag(1,...,1,d). +The square class of d equals that of the original determinant, since +congruence changes the determinant by a square. Scale the last vector +to make d either 1 or one fixed nonsquare nu. This proves both existence +and necessity of the two congruence classes, including r=1. + +Scaling the entire form by c changes its determinant square class by c^r. +For even r it changes nothing. Therefore precisely two similarity classes +remain, represented by diag(1,...,1) and diag(1,...,1,nu). + +For odd r, multiplying a nonsquare-determinant form by nu makes the +determinant square; a square-determinant form needs no scaling. Apply +the congruence reduction to get the identity. Hence all forms of that odd +dimension are similar. The exact number of algebra isomorphism classes is + +```text +1 if r is odd; +2 if r is even, distinguished by the square class of det(B). +``` + +The distinction cannot be removed by changing lifts or the generator of +J^2 when r is even, by equation (1). For odd r, retaining the determinant +square class would falsely reject isomorphic algebras. + +The implementation returns Q and h with Q^T B Q=hD, where D is the +canonical representative. The map from the canonical algebra to A_B sends +its V basis to the columns of Q and its socle generator to h*s. The +displayed equation verifies every product. Composing the two canonical +charts gives a map between the original tables; every basis product is an +independent checkable certificate. A negative answer uses the invariant, +without a search over candidate maps. + +## 4. Recover the form from an arbitrary supplied table + +Validate the algebra laws and recover the unique unit by linear equations. +For a finite-dimensional commutative local algebra, J is nilpotent and +J^n=0 for n=dim A. One way to see the exponent bound is that the radical +power chain strictly decreases until zero; equality persists and contradicts +nilpotence. These are classical finite-dimensional local-algebra facts. + +Choose q^e>=n. The q^e-power map on A is K-linear and has kernel exactly J: +it kills J, while the residue of a unit remains nonzero. Compute this kernel +by linear algebra. Check codim J=1, dim J^2=1 and J*J^2=0. Choose s from +J^2, extend it to a basis of J, and express all lift products in that basis. +Reject if the resulting symmetric B is singular, which by section 1 is +equivalent to the socle being larger than J^2. This recognizes exactly the +declared class and constructs its chart. It does not recognize every local +algebra. + +For recognition before locality is known, in any finite-dimensional +commutative unital K-algebra the same power kernel is the nilradical: every +nilpotent is killed by exponent n and no nonnilpotent has a zero power. +Codimension one makes the reduced quotient K, so the algebra is local. +This justifies using that check without a locality promise on the input. + +The mathematical algorithm works over any explicit odd finite field. +Searching at most q^2 pairs for each binary reduction and at most q scalars +for a square root gives polynomial arithmetic complexity in n for fixed K. +No complexity polynomial in log q is claimed. The bounded implementation +uses only odd prime fields 3<=p<=31 and table dimensions 3<=n<=10; the +written proof has neither bound. The verifier exercises exact forms and +arbitrary-basis algebra tables within those executable limits. + +## 5. Consequence for the recovered multiplication tensor + +Ali Romman's PR #5540 reconstructs a general commutative unital algebra and +three explicit factor maps from a qualifying square prime-field tensor. +That theorem and its full source lineage are cited premises here. Applying +section 4 to its recovered table decides whether that table belongs to our +class. Applying sections 2 and 3 to two such tables decides their algebra +isomorphism and constructs the missing map when it exists. + +For completeness, independent input/output tensor equivalence introduces +no further classes. Suppose invertible K-linear F,G,H satisfy + +```text +F(x)G(y) = H(xy) +``` + +between two commutative unital algebras. Put a=F(1), b=G(1). Then +F(x)b=H(x) and aG(y)=H(y). Since all maps are bijective, multiplication +by a and by b is surjective, so a,b are units. Also H(1)=ab and +H(x)H(y)=ab H(xy). Consequently phi(x)=(ab)^(-1)H(x) is a unital algebra +isomorphism. Conversely any algebra isomorphism gives a tensor equivalence. +This elementary unital-isotopy argument proves that the signatures above +also classify the multiplication tensors. It does not perform or recheck +the predecessor's nucleus reconstruction. + +## 6. Evidence and limits + +The proof is the all-dimension claim; finite checks corroborate its +construction and class boundary. `verify.py` enumerates all symmetric forms +for (p,r)=(3,1..4),(5,1..3),(7,1..2). For each nonsingular form it verifies +the exact similarity certificate, with a permutation-sum determinant oracle. +An independent complete orbit generator enumerates GL2 at p=3,5,7 and GL3 +at p=3, including every nonzero scalar. It compares the entire resulting +partition with the new signature. New changed-basis algebra tables check +the reconstruction and complete isomorphism maps on every basis product. + +Negative controls include even characteristic, composite primes, malformed +coefficients/tables, noncommutativity, nonassociativity, absence of a unit, +wrong residue, zero radical square, nonzero radical cube and excess socle. +Transporter mutations change the image of the recovered unit, so are actual +mathematical corruptions rather than arbitrary changes that might give +another valid isomorphism. All acceptance checks survive optimized Python. + +This result supplies an algebraic interface only. It leaves physical +coefficient preparation, native realization, storage, movement, dirty-state +restoration, precision and a complete paid recursive caller unknown. It +does not improve kappa, change the selected frontier or prove the complete +multiplication theorem. Independent human and proof-kernel review are +unclaimed. No historical scientific replay is used as the deliverable. + +## Credit + +The new specialization and implementation were produced by Nick Petalas. +Credit Ali Romman #5540 for the explicit isomorphism handoff and recovered +table interface, apoursh #5502, Ali Romman #5525, Nick Petalas #5252, +David Ganz and their retained tensor/algebra predecessors. Finite-field +symmetric-form reduction, radical theory and unital isotopy are classical. +No general mathematical or literature priority is asserted. diff --git a/research/cube-zero-gorenstein-isomorphism/README.md b/research/cube-zero-gorenstein-isomorphism/README.md new file mode 100644 index 0000000000..d2acd106ec --- /dev/null +++ b/research/cube-zero-gorenstein-isomorphism/README.md @@ -0,0 +1,116 @@ +# Isomorphism of cube-zero local multiplication tensors + +This contribution was produced by Nick Petalas. Apache-2.0. + +For an odd finite field K, consider commutative unital local K-algebras A with +residue field K and radical J satisfying + +```text +J^3 = 0, dim_K J^2 = 1, Ann_A(J) = J^2. +``` + +Put r=dim_K(J/J^2), which is positive. There is exactly **one isomorphism +class for each odd r**, and **two for each even r**. Recover the symmetric +multiplication matrix B on J/J^2 using any generator of J^2. When r is even, +the two classes are distinguished by whether det(B) is a square. When r is +odd, rescaling the socle removes that distinction. The same classification +holds for isotopy of their multiplication tensors. + +This is a scoped written algebraic proof with exact finite corroboration. +It answers one restricted part of the recovered-algebra isomorphism question +in Ali Romman's [PR #5540](https://github.com/CrocSwap/integer-mult-bounds/pull/5540). +That reconstruction theorem is a cited premise, not a result rechecked here. +The new package supplies the specialization, explicit maps and bounded +implementation. Symmetric-form classification and its elementary methods +are classical; no general literature-priority claim is made. No new kappa. + +[PROOF.md](PROOF.md) gives the reduction, classification, constructive +congruence algorithm and tensor implication. `algebra.py` accepts supplied +tables in arbitrary bases over odd primes 3 through 31, in dimensions 3 +through 10. It checks the algebra laws and class hypotheses, computes a +canonical signature and chart, and returns a literal isomorphism between +accepted tables with the same signature. Different signatures return `None`; +invalid or out-of-class inputs raise `ValueError`. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/cube-zero-gorenstein-isomorphism/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/cube-zero-gorenstein-isomorphism/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cube-zero-gorenstein-isomorphism +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cube-zero-gorenstein-isomorphism --check-source-history +``` + +Other machines may substitute their CPython 3.12 interpreter path. The direct +checker prints `PASS_CUBE_ZERO_GORENSTEIN_ISOMORPHISM` in a JSON report with +enumerated coverage and SHA256 hashes of every package source/document file. +The default replay writes no files. No receipt is handwritten. + +The finite corroboration checks **51,200 nonsingular forms**. Independent +full GL/similarity orbit generation covers 18, 100 and 294 forms in dimension +two over F3, F5 and F7, and all 468 forms in dimension three over F3. It +enumerates respectively 48, 480, 2,016 and 11,232 invertible matrices. +The new 96 arbitrary-basis algebra presentations check 4,128 transported +basis products. All 96 unit-image transporter mutations and 12 input/class +rejection controls pass. These are new fixtures, not predecessor inventories +or scientific replays. The proof supplies the universal quantifiers. + +## Scope and research decision + +The original `formal-interface-lemma` card is explicitly changed to this +written algebraic side result. The current selected source-binding command +passed; it is metadata orientation only. The actual caller is the recovered +table interface of #5540. The contribution closes isomorphism for this +specified class, without claiming the card's proof-assistant acceptance gate. +Stop after the classification. Physical maps, costs and supplier admission +remain unpriced and provide no basis for a construction expansion. + +The live overlap check included open PRs, this account's recent PRs, handoff +comments, active Discussions, main-tree README searches and merged searches +for the class and its invariants. The cached helper searched only a sparse +subset of local notes; Git-object searches supplemented it. Absence of a +match is not a global novelty certificate. The advance claim is +[Discussion #1166](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220065). + +The proof covers all odd finite fields and all positive r. The executable +supports the bounded prime-field interface above. Characteristic two, +nonsplit residue fields, larger socles, higher nilpotency, arbitrary algebra +isomorphism, native/frame/ownership/restoration costs, precision, movement, +complete recursive invoices and the multiplication theorem are outside scope. +No selected cold replay, predecessor scientific suite, Lean or Docker build +was run. Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +1. Extend this particular isomorphism interface to characteristic two. Start + with the alternating versus nonalternating multiplication form; the odd + pivot and square-class algorithm here does not apply. A separate proof + and field contract are needed. +2. Price the returned maps for one concrete native caller. First identify + its legal coefficients, dirty state and required restoration, then charge + every conversion. The current algebraic maps have no physical tariff. + +## Credit + +Credit Ali Romman #5540, exact head +`831b41da0fc09e3e4cb983c03662da5df7970f68`, for the recovered-table interface +and explicit isomorphism question. Credit apoursh #5502 for the supplied-table +recognition lineage, Ali Romman #5525 for the nucleus reconstruction lineage, +and Nick Petalas #5252, David Ganz and the retained tensor/algebra sources. +Their files and credit lines are unchanged. `SOURCES.json` records historical +provenance at canonical main `19fdb086ea96af9a9f87936a2b888e10af4ed810`, +priority revision 8. No predecessor code is copied or executed. + +## Implementation constraints + +All checks use explicit exceptions and remain enabled under optimized Python. +There is no recursion, dynamic code execution or file-writing path. Loops +are bounded by the validated dimensions and prime, or by the verifier's +literal finite domains. The largest form enumeration has 3^10 candidates; +the largest GL enumeration has 3^9 candidates. Functions stay below 60 lines. +Python's managed allocation is a Power of Ten deviation: the table API caps +dimension at 10 and prime at 31, and each exhaustive loop discards its current +candidate. The finite orbit dictionary is bounded by its enumerated symmetric +form space. No fixed-memory or general runtime-speed claim is made. diff --git a/research/cube-zero-gorenstein-isomorphism/SOURCES.json b/research/cube-zero-gorenstein-isomorphism/SOURCES.json new file mode 100644 index 0000000000..5e45cdedf4 --- /dev/null +++ b/research/cube-zero-gorenstein-isomorphism/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/nonreduced-tensor-recognition/README.md", + "usage": "provenance", + "git_blob": "826c6b010725d98b6ca6599a748c4179264140e9", + "sha256": "2eaed94a9f12ad7b6bb7253b14bff95b86549b3e320f0e91fa4e35c0025536de" + } + ] +} diff --git a/research/cube-zero-gorenstein-isomorphism/TASK.json b/research/cube-zero-gorenstein-isomorphism/TASK.json new file mode 100644 index 0000000000..d9182f35fe --- /dev/null +++ b/research/cube-zero-gorenstein-isomorphism/TASK.json @@ -0,0 +1,124 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "Classify isomorphism and tensor isotopy for split local odd-finite-field algebras with J^3=0 and one-dimensional socle J^2; construct canonical charts and pairwise table maps.", + "scope_change_reason": "The card is changed from a proof-assistant interface check to a new written algebraic side result answering the restricted recovered-algebra isomorphism question in Ali Romman PR5540. No predecessor result is audited and no formalization gate is claimed.", + "bottleneck_link": "Algebraic interface side result: complete the missing comparison step for one specified class of recovered multiplication tensors. Physical map costs and recursive supplier admission remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified classification; no characteristic-two or physical-caller expansion.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-dimension odd-field theorem. Exact replay checks 51200 nonsingular forms, four complete GL/similarity domains, 96 changed presentations, 4128 basis products, 96 transporter mutations and 12 rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Extend this specific isomorphism interface to characteristic two.", + "why_it_matters": "The odd-field form classification does not cover binary coefficient algebras.", + "first_step": "Separate alternating and nonalternating symmetric multiplication forms.", + "blocked_by": "A separate field contract and proof; the current odd-pivot algorithm is inapplicable." + }, + { + "question": "Price one emitted map in a concrete native caller.", + "why_it_matters": "An algebra isomorphism has no physical supplier consequence until all costs are paid.", + "first_step": "List legal coefficients, dirty state, endpoints and restoration, then charge every conversion.", + "blocked_by": "No native realization, complete caller or tariff is supplied." + } + ], + "source_question": { + "pr": 5540, + "author": "aliromman", + "head": "831b41da0fc09e3e4cb983c03662da5df7970f68", + "question": "Given two accepted general commutative tensors, decide whether their recovered algebras are isomorphic." + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220065", + "claim_type": "scoped proof with exact finite corroboration", + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "ownership": { + "initial_branch": "detached HEAD", + "initial_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "preserved": true + }, + "upstream_freshness": { + "commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "priority_revision": 8, + "checked_utc": "2026-10-27T15:23:36.949791+00:00" + } +} diff --git a/research/cube-zero-gorenstein-isomorphism/VERIFY.json b/research/cube-zero-gorenstein-isomorphism/VERIFY.json new file mode 100644 index 0000000000..267c53bb4f --- /dev/null +++ b/research/cube-zero-gorenstein-isomorphism/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete declared form and independent similarity-orbit domains, table reconstruction, canonical charts, every transported basis product and rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete mathematical coverage with interpreter assertions disabled." + } + ] +} diff --git a/research/cube-zero-gorenstein-isomorphism/algebra.py b/research/cube-zero-gorenstein-isomorphism/algebra.py new file mode 100644 index 0000000000..7ff2b1637e --- /dev/null +++ b/research/cube-zero-gorenstein-isomorphism/algebra.py @@ -0,0 +1,249 @@ +"""Exact cube-zero local algebra classification over bounded odd prime fields. + +Produced by Nick Petalas. Apache-2.0. +""" + +from itertools import product + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def transpose(a): + return [list(row) for row in zip(*a)] + + +def eye(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def mm(a, b, p): + return [[sum(x * y for x, y in zip(row, col)) % p + for col in zip(*b)] for row in a] + + +def mv(a, v, p): + return [sum(x * y for x, y in zip(row, v)) % p for row in a] + + +def rref(a, p): + a = [row[:] for row in a] + pivots = [] + for j in range(len(a[0])): + candidates = [i for i in range(len(pivots), len(a)) if a[i][j]] + if not candidates: + continue + k = len(pivots) + i = candidates[0] + a[k], a[i] = a[i], a[k] + a[k] = [(x * pow(a[k][j], -1, p)) % p for x in a[k]] + for i in range(len(a)): + if i != k: + c = a[i][j] + a[i] = [(x - c * y) % p for x, y in zip(a[i], a[k])] + pivots.append(j) + if len(pivots) == len(a): + break + return a, pivots + + +def inverse(a, p): + n = len(a) + b, pivots = rref([row + unit for row, unit in zip(a, eye(n))], p) + need(pivots[:n] == list(range(n)), "singular matrix") + return [row[n:] for row in b] + + +def kernel(a, p): + b, pivots = rref(a, p) + free = [j for j in range(len(a[0])) if j not in pivots] + basis = [] + for j in free: + v = [0] * len(a[0]) + v[j] = 1 + for i, k in enumerate(pivots): + v[k] = -b[i][j] % p + basis.append(v) + return basis + + +def span_basis(vectors, p): + if not vectors: + return [] + _, pivots = rref(transpose(vectors), p) + return [vectors[j] for j in pivots] + + +def determinant(a, p): + a = [row[:] for row in a] + value = 1 + for j in range(len(a)): + candidates = [i for i in range(j, len(a)) if a[i][j]] + if not candidates: + return 0 + i = candidates[0] + if i != j: + a[i], a[j] = a[j], a[i] + value = -value + pivot = a[j][j] + value = value * pivot % p + for i in range(j + 1, len(a)): + c = a[i][j] * pow(pivot, -1, p) % p + a[i] = [(x - c * y) % p for x, y in zip(a[i], a[j])] + return value + + +def multiply(t, a, b, p): + n = len(t) + return [sum(a[i] * b[j] * t[i][j][k] + for i in range(n) for j in range(n)) % p + for k in range(n)] + + +def algebra_power(t, a, exponent, unit, p): + result = unit[:] + for j in range(exponent.bit_length() - 1, -1, -1): + result = multiply(t, result, result, p) + if (exponent >> j) & 1: + result = multiply(t, result, a, p) + return result + + +def validate(t, p): + need(type(p) is int and 3 <= p <= 31 and p % 2 == 1, + "odd prime in [3,31] required") + need(all(p % d for d in range(2, p)), "prime required") + need(type(t) is list and 3 <= len(t) <= 10, "dimension in [3,10] required") + n = len(t) + need(all(type(row) is list and len(row) == n for row in t), "table shape") + need(all(type(v) is list and len(v) == n for row in t for v in row), + "table coefficient shape") + need(all(type(x) is int and 0 <= x < p + for row in t for v in row for x in v), "canonical coefficients") + need(all(t[i][j] == t[j][i] for i in range(n) for j in range(n)), + "commutativity") + basis = eye(n) + for i, j, k in product(range(n), repeat=3): + need(multiply(t, t[i][j], basis[k], p) + == multiply(t, basis[i], t[j][k], p), "associativity") + equations = [[t[i][j][k] for i in range(n)] + [int(j == k)] + for j in range(n) for k in range(n)] + rows, pivots = rref(equations, p) + need(pivots == list(range(n)), "unique unit required") + unit = [rows[i][-1] for i in range(n)] + need(all(multiply(t, unit, v, p) == v for v in basis), "unit") + return unit + + +def recover_form(t, p): + unit = validate(t, p) + n = len(t) + exponent = next(p ** e for e in range(n + 1) if p ** e >= n) + powers = [algebra_power(t, v, exponent, unit, p) for v in eye(n)] + radical = kernel(transpose(powers), p) + need(len(radical) == n - 1, "split local residue required") + square = span_basis([multiply(t, a, b, p) + for a in radical for b in radical], p) + need(len(square) == 1, "radical square must have dimension one") + s = square[0] + need(all(not any(multiply(t, a, s, p)) for a in radical), "radical cube") + lifts = span_basis([s] + radical, p)[1:] + chart = transpose([unit] + lifts + [s]) + chart_inverse = inverse(chart, p) + form = [] + for a in lifts: + row = [] + for b in lifts: + coordinates = mv(chart_inverse, multiply(t, a, b, p), p) + need(not any(coordinates[:-1]), "product outside radical square") + row.append(coordinates[-1]) + form.append(row) + need(determinant(form, p) != 0, "socle larger than radical square") + return form, chart + + +def pairing(b, u, v, p): + return sum(x * y for x, y in zip(u, mv(b, v, p))) % p + + +def combine(a, b, x, y, p): + return [(a * s + b * t) % p for s, t in zip(x, y)] + + +def orthogonal_basis(b, p): + remaining = eye(len(b)) + columns = [] + for _ in range(len(b)): + pivots = [i for i, v in enumerate(remaining) if pairing(b, v, v, p)] + if pivots: + v = remaining.pop(pivots[0]) + else: + pairs = [(i, j) for i in range(len(remaining)) + for j in range(i + 1, len(remaining)) + if pairing(b, remaining[i], remaining[j], p)] + need(bool(pairs), "degenerate residual form") + i, j = pairs[0] + v = combine(1, 1, remaining[i], remaining[j], p) + remaining.pop(i) + norm = pairing(b, v, v, p) + need(norm != 0, "odd characteristic pivot") + remaining = [combine(1, -pairing(b, v, w, p) * pow(norm, -1, p), + w, v, p) for w in remaining] + columns.append(v) + return columns + + +def normalize_form(b, p): + r = len(b) + det = determinant(b, p) + need(det != 0 and all(b[i][j] == b[j][i] + for i in range(r) for j in range(r)), "symmetric unit form") + nonsquare = next(x for x in range(2, p) if pow(x, (p - 1) // 2, p) == p - 1) + square = pow(det, (p - 1) // 2, p) == 1 + scale = nonsquare if r % 2 and not square else 1 + c = [[scale * x % p for x in row] for row in b] + columns = orthogonal_basis(c, p) + for k in range(r - 1): + a = pairing(c, columns[k], columns[k], p) + d = pairing(c, columns[k + 1], columns[k + 1], p) + choices = [(u, v) for u in range(p) for v in range(p) + if (a * u * u + d * v * v) % p == 1] + need(bool(choices), "binary form must represent one") + u, v = choices[0] + x, y = columns[k], columns[k + 1] + columns[k] = combine(u, v, x, y, p) + columns[k + 1] = combine(-d * v, a * u, x, y, p) + last = pairing(c, columns[-1], columns[-1], p) + target = nonsquare if r % 2 == 0 and not square else 1 + roots = [x for x in range(1, p) if last * x * x % p == target] + need(bool(roots), "last square class") + columns[-1] = [(roots[0] * x) % p for x in columns[-1]] + matrix = transpose(columns) + canonical = eye(r) + canonical[-1][-1] = target + need(mm(mm(transpose(matrix), c, p), matrix, p) == canonical, + "complete congruence certificate") + signature = [r, int(r % 2 == 0 and not square)] + return signature, matrix, pow(scale, -1, p) + + +def canonical_chart(t, p): + form, chart = recover_form(t, p) + signature, matrix, socle_scale = normalize_form(form, p) + n = len(t) + block = eye(n) + for i in range(n - 2): + for j in range(n - 2): + block[i + 1][j + 1] = matrix[i][j] + block[-1][-1] = socle_scale + return signature, mm(chart, block, p) + + +def isomorphism(t, other, p): + left, a = canonical_chart(t, p) + right, b = canonical_chart(other, p) + if left != right: + return None + return mm(b, inverse(a, p), p) diff --git a/research/cube-zero-gorenstein-isomorphism/verify.py b/research/cube-zero-gorenstein-isomorphism/verify.py new file mode 100644 index 0000000000..de2d77980b --- /dev/null +++ b/research/cube-zero-gorenstein-isomorphism/verify.py @@ -0,0 +1,237 @@ +"""Bounded independent corroboration of the new isomorphism classification. + +Produced by Nick Petalas. Apache-2.0. +""" + +import hashlib +import itertools +import json +from pathlib import Path +import random + +from algebra import (canonical_chart, determinant, eye, inverse, isomorphism, + mm, mv, need, normalize_form, recover_form, + transpose, validate) + + +def symmetric_forms(p, r): + positions = [(i, j) for i in range(r) for j in range(i, r)] + for values in itertools.product(range(p), repeat=len(positions)): + b = [[0] * r for _ in range(r)] + for (i, j), value in zip(positions, values): + b[i][j] = b[j][i] = value + yield b + + +def literal_determinant(a, p): + r = len(a) + total = 0 + for permutation in itertools.permutations(range(r)): + term = 1 + for i in range(r): + term *= a[i][permutation[i]] + inversions = sum(permutation[i] > permutation[j] + for i in range(r) for j in range(i + 1, r)) + total += (-1) ** inversions * term + return total % p + + +def key(b): + return tuple(x for row in b for x in row) + + +def orbit_oracle(p, r): + nonsquare = next(x for x in range(2, p) if x not in {y * y % p for y in range(p)}) + representatives = [eye(r)] + if r % 2 == 0: + other = eye(r) + other[-1][-1] = nonsquare + representatives.append(other) + classes = {} + matrices = 0 + for entries in itertools.product(range(p), repeat=r * r): + a = [list(entries[i * r:(i + 1) * r]) for i in range(r)] + if literal_determinant(a, p) == 0: + continue + matrices += 1 + for label, b in enumerate(representatives): + for c in range(1, p): + # Direct coefficient formula, independent of normalization. + image = [[c * sum(a[k][i] * b[k][l] * a[l][j] + for k in range(r) for l in range(r)) % p + for j in range(r)] for i in range(r)] + fingerprint = key(image) + need(fingerprint not in classes or classes[fingerprint] == label, + "predicted classes intersect") + classes[fingerprint] = label + checked = 0 + for b in symmetric_forms(p, r): + if literal_determinant(b, p): + signature, _, _ = normalize_form(b, p) + need(key(b) in classes and signature == [r, classes[key(b)]], + "complete orbit disagrees with signature") + checked += 1 + need(len(classes) == checked, "orbit domain coverage") + return matrices, checked + + +def model_table(b, p): + n = len(b) + 2 + t = [[[0] * n for _ in range(n)] for _ in range(n)] + for i in range(n): + t[0][i][i] = t[i][0][i] = 1 + for i in range(n - 2): + for j in range(n - 2): + t[i + 1][j + 1][-1] = b[i][j] + return t + + +def model_product(b, a, c, p): + r = len(b) + middle = [(a[0] * c[i + 1] + c[0] * a[i + 1]) % p for i in range(r)] + last = (a[0] * c[-1] + c[0] * a[-1] + + sum(a[i + 1] * b[i][j] * c[j + 1] + for i in range(r) for j in range(r))) % p + return [a[0] * c[0] % p] + middle + [last] + + +def changed_table(b, q, p): + qi = inverse(q, p) + columns = transpose(q) + return [[mv(qi, model_product(b, a, c, p), p) + for c in columns] for a in columns] + + +def random_chart(n, p, rng): + q = eye(n) + for _ in range(4 * n): + i, j = rng.sample(range(n), 2) + c = rng.randrange(1, p) + q[i] = [(x + c * y) % p for x, y in zip(q[i], q[j])] + # One scale and a swap also move the unit and socle coordinates. + scale = rng.randrange(1, p) + q[0] = [scale * x % p for x in q[0]] + q[0], q[-1] = q[-1], q[0] + need(determinant(q, p) != 0, "fixture chart") + return q + + +def check_homomorphism(t, other, f, p): + need(f is not None and determinant(f, p) != 0, "invertible transporter") + n = len(t) + columns = transpose(f) + count = 0 + for i in range(n): + for j in range(n): + actual = [sum(columns[i][a] * columns[j][b] * other[a][b][k] + for a in range(n) for b in range(n)) % p + for k in range(n)] + need(actual == mv(f, t[i][j], p), "transported basis product") + count += 1 + return count + + +def form_checks(): + total = 0 + for p, r in ((3, 1), (3, 2), (3, 3), (3, 4), + (5, 1), (5, 2), (5, 3), (7, 1), (7, 2)): + for b in symmetric_forms(p, r): + d = literal_determinant(b, p) + need(d == determinant(b, p), "independent determinant") + if not d: + continue + signature, q, scale = normalize_form(b, p) + canonical = eye(r) + if signature[1]: + canonical[-1][-1] = next(x for x in range(2, p) + if pow(x, (p - 1) // 2, p) == p - 1) + expected = [[scale * x % p for x in row] for row in canonical] + need(mm(mm(transpose(q), b, p), q, p) == expected, + "literal similarity certificate") + total += 1 + return total + + +def algebra_checks(): + rng = random.Random(5540) + fixtures = products = mutations = 0 + for p in (3, 5, 7): + nonsquare = next(x for x in range(2, p) if pow(x, (p - 1) // 2, p) == p - 1) + for r in range(1, 5): + for last in (1, nonsquare): + b = eye(r) + b[-1][-1] = last + for _ in range(4): + t = changed_table(b, random_chart(r + 2, p, rng), p) + other = changed_table(b, random_chart(r + 2, p, rng), p) + signature, chart = canonical_chart(t, p) + canonical = eye(r) + canonical[-1][-1] = nonsquare if signature[1] else 1 + products += check_homomorphism(model_table(canonical, p), t, chart, p) + f = isomorphism(t, other, p) + products += check_homomorphism(t, other, f, p) + corrupt = [row[:] for row in f] + unit = validate(t, p) + j = next(j for j, coefficient in enumerate(unit) if coefficient) + corrupt[0][j] = (corrupt[0][j] + 1) % p + try: + check_homomorphism(t, other, corrupt, p) + except ValueError: + mutations += 1 + else: + raise ValueError("changed transporter accepted") + fixtures += 1 + a = model_table(eye(r), p) + b[-1][-1] = nonsquare + result = isomorphism(a, model_table(b, p), p) + need((result is None) == (r % 2 == 0), "odd/even class boundary") + return fixtures, products, mutations + + +def rejection_checks(): + base = model_table(eye(2), 3) + zero_square = model_table([[0, 0], [0, 0]], 3) + extra_socle = model_table([[1, 0], [0, 0]], 3) + truncated = [[[0] * 4 for _ in range(4)] for _ in range(4)] + for i in range(4): + for j in range(4 - i): + truncated[i][j][i + j] = 1 + product_fields = [[[int(i == j == k) for k in range(3)] + for j in range(3)] for i in range(3)] + noncommutative = json.loads(json.dumps(base)) + noncommutative[1][2][-1] = 1 + nonassociative = json.loads(json.dumps(base)) + nonassociative[1][1][1] = 1 + boolean = json.loads(json.dumps(base)) + boolean[0][0][0] = True + bad = [(base, 2), (base, 9), (base, 37), (base[:-1], 3), + (zero_square, 3), (extra_socle, 3), (truncated, 3), + (product_fields, 3), (noncommutative, 3), (nonassociative, 3), + (boolean, 3), ([[[0] * 3 for _ in range(3)] for _ in range(3)], 3)] + for t, p in bad: + try: + recover_form(t, p) + except ValueError: + continue + raise ValueError("invalid or out-of-class algebra accepted") + return len(bad) + + +def main(): + forms = form_checks() + orbit_counts = [orbit_oracle(p, r) for p, r in ((3, 2), (5, 2), (7, 2), (3, 3))] + fixtures, products, mutations = algebra_checks() + controls = rejection_checks() + package = Path(__file__).resolve().parent + hashes = {path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted(package.iterdir()) + if path.is_file() and path.suffix in (".py", ".md", ".json")} + print(json.dumps({"status": "PASS_CUBE_ZERO_GORENSTEIN_ISOMORPHISM", + "nonsingular_forms": forms, "complete_orbit_domains": orbit_counts, + "changed_presentations": fixtures, "basis_products": products, + "transporter_mutations": mutations, "rejections": controls, + "sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()