diff --git a/research/extension-field-tensor-recognition/README.md b/research/extension-field-tensor-recognition/README.md new file mode 100644 index 0000000000..d0c74a3c49 --- /dev/null +++ b/research/extension-field-tensor-recognition/README.md @@ -0,0 +1,270 @@ +# Extension-field tensor recognition and special-linear orbit labels + +This package recognizes, from an arbitrary square tensor over an explicit +finite field K=F_q of characteristic p, the multiplication tensors of + + K[x_1,...,x_s]/(x_i^(p^h_i)), h_i >= 1. + +It returns the heights and three invertible maps U,V,W with +`t(Ua,Vb)=W mu(a,b)`. The empty height list gives K. The test is necessary +and sufficient. It uses deterministic polynomial time in the tensor dimension +for each fixed field. No algebra-class or common-basis promise is required. + +The result also removes the recognition promise from the determinant-character +formula of PR #5459. For each accepted tensor it returns the exact number of +special-linear orbits in its general-linear orbit and a complete orbit label. +Two accepted tensors over the same explicit field are equivalent under the +product of three special linear groups if and only if their height lists and +labels agree. This supplies an executable input test for that atlas interface. +It also constructs determinant-one factor maps between equivalent accepted +tensors. It supplies no physical tensor implementation, paid supplier or kappa increase. + +## Sources and scope + +Main is `6cf7a683f447b9f1e2333791907fd92be5009a63`, priority revision 7. +The [released handoff and claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19186074) +identify the extension-field gap. A complete cached open-PR and Discussion +search and a search of every tracked main research README/TASK file found no +active claim on this scope. These searches do not prove global novelty. + +The three proof inputs are pinned in `SOURCES.json`, authenticated on replay, +and preserved without changes. No predecessor executable is imported. + +- Ali Romman's [PR #5540](https://github.com/CrocSwap/integer-mult-bounds/pull/5540) + gives the prime-field tensor reconstruction, the regular-module criterion, + and this extension-field handoff. Its + [retained proof](https://github.com/CrocSwap/integer-mult-bounds/blob/6cf7a683f447b9f1e2333791907fd92be5009a63/research/nonreduced-tensor-recognition/README.md) + credits Nick Petalas's [PR #5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252) + for the nucleus method and Ali Romman's + [PR #5525](https://github.com/CrocSwap/integer-mult-bounds/pull/5525) for its implementation. +- apoursh's [PR #5502](https://github.com/CrocSwap/integer-mult-bounds/pull/5502) + gives the prime-field height flag and dimension criterion. Its + [retained proof](https://github.com/CrocSwap/integer-mult-bounds/blob/6cf7a683f447b9f1e2333791907fd92be5009a63/research/frobenius-algebra-recognition/PROOF.md) + explicitly leaves extension fields open. +- Ali Romman's [PR #5459](https://github.com/CrocSwap/integer-mult-bounds/pull/5459) + gives the finite-field stabilizer determinant image under an algebra-class + promise. Its + [retained proof](https://github.com/CrocSwap/integer-mult-bounds/blob/6cf7a683f447b9f1e2333791907fd92be5009a63/research/frobenius-tensor-characters/README.md) + supplies the character theorem used below. David Ganz and the atlas lineage + retain credit for the orbit and character framework. + +The new work supplies the finite-field contract, semilinear kernel correction, +composed recognition and orbit label, proof below, and a separate implementation. +It extends the stated local truncated-polynomial class. It does not extend +PR #5540's general commutative-algebra recovery to all residue fields or products. + +## Input and output contract + +`Field(p, modulus)` uses a monic polynomial over F_p, with coefficients in +constant-first order. An element is the integer whose base-p digits are its +polynomial coefficients of degrees less than the modulus degree e. All entries +must be canonical integers from 0 through q-1, where q=p^e. The constructor +checks primality by trial division, builds quotient-ring addition and +multiplication tables, and checks that each nonzero element has an inverse. +A finite commutative unital ring with this property is a field. Thus this test +rejects every reducible modulus, including repeated factors. + +`recognize(t, field)` uses `t[i][j][k]` for the output coefficient k of basis +inputs i,j. All three dimensions must equal n>0. Invalid shapes or entries +raise `ValueError`. A well-formed tensor outside the class returns +`(None, reason)`. Acceptance returns `(certificate, None)`. The certificate +contains `heights`, `U`, `V`, `W`, `sl_orbit_count` and `sl_orbit_label`. +`sl_transporter(first, second, field)` returns determinant-one matrices F,G,H +with `second(Fu,Gv)=H first(u,v)`, or a rejection reason. +Matrix columns are basis images. The field object must retain its constructed +operation tables. Different presentations of the same field require an +explicit field isomorphism before labels can be compared. + +## Reconstruct the local algebra and its factor maps + +Solve the linear nucleus equations + + B = {(X,Y): t(Xu,v)=Y t(u,v) for all u,v}. + +Require dimension n, injective projections to both matrix algebras, +commutativity, and zero right kernel for t. The nucleus is automatically a +unital algebra under componentwise composition: composing two identities gives +the product identity. The faithful Y projection gives coordinates for its +multiplication table and identity. + +Let Q=q^a be the least q-power at least n. The map b -> b^Q is K-linear, +because each coefficient in K is fixed by q-power Frobenius. Its kernel J is +the nilradical. Indeed, in a finite-dimensional commutative unital algebra the +nilradical is nilpotent and J^n=0. A proof uses a finite nilpotent generating +set and the strictly decreasing power chain until zero. Thus this power kills +every nilpotent and kills no other element. Require `dim J=n-1`. Then B is +local with residue field K: every element outside J is a nonzero scalar plus +a nilpotent and has an inverse by the finite geometric series. + +For each nucleus module M=U or W, form JM from the columns of the radical +matrices and require `dim(M/JM)=1`. Choose a coordinate vector m outside JM. +It generates the quotient. For C=Bm, the quotient M/C satisfies M/C=J(M/C). +Iteration through J^n=0 gives M=C. Its dimension equals dim B, so b -> bm is +an isomorphism. Obtain cyclic vectors u0,w0 and matrices + + alpha(b)=X_b u0, gamma(b)=Y_b w0, Phi(v)=t(u0,v). + +If Phi(v)=0, cyclicity of u0 and the nucleus identity give t(U,v)=0. 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 constructs the three factor maps to B without a search over vectors or +invertible slices. Necessity follows from ordinary multiplication: evaluating +the nucleus identity at 1 in each input shows that both X and Y are +multiplication by the same algebra element. Both modules are regular. +The argument is valid over K; it does not require a prime field. + +## The semilinear height flag + +For h>=0, form C_h by raising each algebra basis element to p^h. With +sigma(c)=c^p on coefficients, the actual map on coordinate vectors is + + F^h(v) = C_h sigma^h(v). + +Consequently a basis of its kernel is obtained by applying sigma^(-h) to a +basis of the ordinary K-linear kernel of C_h. The inverse twist on F_q is +`c -> c^(p^((-h) mod e))`. This is a semilinear change of coordinates, so it +preserves independence and spans the full kernel. An ordinary kernel basis +without this twist need not contain nilpotent elements. Likewise, C_1^h is +not the matrix of F^h: composition twists the next matrix's coefficients. +The implementation computes the actual basis powers separately at each h. + +Let H be the least integer with p^H>=n. Set K_h=ker F^h and + + V_h=(K_h+J^2)/J^2, d_h=dim V_h-dim V_(h-1), + N=p^(sum_h h d_h). + +Choose representatives of each newly independent tangent class directly in +K_h, assign them height h, and call them g_i. Accept exactly when N=n. + +For necessity, in the target algebra J/J^2 has basis the variables. A nonzero +coefficient of x_i with h_i>h survives F^h as a nonzero coefficient of +x_i^(p^h). No other linear term, or term of degree at least two, can cancel +this monomial. The coefficient twist is a field automorphism and cannot turn +a nonzero coefficient into zero. Thus V_h is exactly the span of variables +with height at most h. The flag recovers all heights and N=n. + +For sufficiency, each g_i satisfies its required power relation, and the g_i +span J/J^2. They generate the algebra: expand products in J^k using their +linear parts to obtain `J^k subset C+J^(k+1)`, where C is their unital +subalgebra. Iterate until J^n=0. Substitution therefore gives a surjection +from the proposed truncated-polynomial algebra of dimension N to B. If N=n, +it is an isomorphism. Its matrix C consists of the ordered monomials in g_i. +Compose alpha C, beta C, gamma C to obtain U,V,W. Every basis product of these +maps is checked before acceptance. This proves both directions and supplies +explicit certificates. For n=1, J=0 and the height list is empty. + +The q-power computation is used for the radical. The p-power flag is used for +heights. They cannot be interchanged: over F4, K[x]/x^4 has height two even +though fourth powers already kill its entire radical. + +## Recover the special-linear orbit label + +Let the accepted dimension be n and define + + h=gcd(q-1, n(p^h_1-1)/2, ..., n(p^h_s-1)/2). + +Each exponent is an integer. With no variables, use h=q-1. The pinned PR #5459 +theorem gives the stabilizer determinant image for the covariant action on +`A* tensor A* tensor A`: + + Delta = {(a,b,c): (abc)^((q-1)/h)=1}. + +The empty-height case follows directly: multiplication in K has stabilizer +triples with abc=1. The product of the three determinant-one groups is the +kernel of the determinant map. Hence the number of its orbits in this GL +orbit is h. + +Our certificate gives the tensor action `(U^-T,V^-T,W)`. Its determinant +product is `d=det(W)/(det(U)det(V))`. Define the label + + label = d^((q-1)/h) in K*. + +Two choices of transporter differ by a stabilizer element, whose determinant +product has this power equal to one. The label is therefore intrinsic. The +map `K* -> K*`, d -> d^((q-1)/h), has kernel the h-th power subgroup, exactly +the possible stabilizer products. Its fibers are exactly the cosets of Delta, +so label equality is necessary and sufficient within the fixed height class. +The height list itself is intrinsic by the flag proof. This proves the stated +classification for all accepted tensors. It does not classify tensors outside +this family or claim a new proof of PR #5459's character formula. + +## Construct determinant-one maps + +For two equal-label certificates (U1,V1,W1) and (U2,V2,W2), put +`a=det(U1)/det(U2)`, `b=det(V1)/det(V2)`, `c=det(W1)/det(W2)`. +A model autotopism with these three determinants makes the composite maps +from the first tensor to the second have determinant one. Write the model +autotopism as `(L_x sigma,L_y sigma,L_(xy) sigma)`. Its required automorphism +determinant is `z=ab/c`; its unit determinants must be `a/z` and `b/z`. +Equal labels put z in the character subgroup H_h. + +Find a generator g of K* by enumeration, and write z=g^k. Bezout coefficients +for `h=gcd(q-1,E_1,...,E_s)`, where `E_i=n(p^h_i-1)/2`, give integers b_i +with `sum b_i E_i = h mod (q-1)`. Scale variable i by `g^(b_i k/h)`. +This defines a diagonal algebra automorphism sigma with determinant z. Since +n is a power of p, n is invertible modulo q-1. Scalar units x,y can therefore +supply the required determinants: raise a/z and b/z to that inverse power. +The resulting three model maps have determinants a,b,c. Compose them between +the second certificate and the inverse first certificate. The implementation +checks all three determinants and every transported basis product. This gives +an explicit special-linear transporter without enumerating algebra bases or +automorphisms. Field generator and discrete-log enumeration are bounded by q; +the stated polynomial guarantee remains for fixed q. The empty-height and +q=2 cases use the same formulas with the trivial multiplicative group. + +## Verification and cost + +Run: + +```sh +python3.12 -B scripts/research_package.py --package research/extension-field-tensor-recognition +``` + +The standard library suffices. The registered normal and optimized commands +print `PASS_EXTENSION_FIELD_TENSOR_RECOGNITION`. Every check uses explicit +exceptions and remains active under `-O`. + +The complete F4 2x2x2 domain contains 65,536 tensors. Exactly 13,500 pass, +with exact agreement with a separate orbit generator that applies elementary +GL2 matrices to the three literal coefficient indices. The complete binary +domain gives 54 accepted tensors out of 256. Every accepted transporter is +checked by all basis products. The orbit generator does not use the nucleus, +radical, regular-module or height tests. These complete finite checks do not +replace the written proof in other dimensions. + +Ninety changed-basis presentations cover F2,F3,F4,F8,F9,F16,F25, dimensions +through nine, empty and unequal heights, 2,322 transported products, and 90 +comparisons of orbit labels with known factor maps. Ninety additional +determinant-one transporters pass all 2,322 basis products. The 125 controls include +altered transporters, reducible field polynomials, extra algebra relations, +nonregular dual modules, split algebras and invalid tensors. Over F4, write +a^2=a+1 and use basis `(1,a+x)` for K[x]/x^2. The ordinary kernel of the +squaring columns is `(a^2,1)`, which represents `1+x` and squares to 1. The +correct kernel is `(a,1)`, which represents x and squares to zero. A second +control rejects ordinary matrix iteration. The cutoff-four and two-variable +cutoff-two algebras have orbit counts three and one; all three labels of the +first algebra are attained by explicit output scalings. + +The nucleus has n^3 equations in 2n^2 unknowns. All subsequent steps use +matrix arithmetic, algebra powers and at most ceil(log_p n) kernel levels. +The model monomials are built only after the dimension test accepts, so there +are exactly n. These are deterministic polynomial operations in n at fixed q. +The constructor builds O(q^2) field tables and uses trial-division primality; +there is no polynomial bit-complexity claim in log q. The proof inputs and +finite field operations are checked, but no prior full executable suite, +proof assistant, selected cold replay or independent human review was run. + +## Open next questions + +- Extend the certificate to products and larger residue fields. First specify + component matching and field-isomorphism data; the local residue-K test here + must not be silently removed. +- Use a recognized tensor in a named native producer/consumer pair. Charge its + field representation, coefficients, movement, precision and restoration before + drawing a kappa conclusion. No such physical cost is zero by this result. + +New work: Ali Romman (@aliromman), with substantial OpenAI Codex assistance. +Predecessor methods: apoursh (@apoursh), Nick Petalas (@petalas), David Ganz, +and the linked sources. Apache-2.0. No general literature-priority claim. diff --git a/research/extension-field-tensor-recognition/SOURCES.json b/research/extension-field-tensor-recognition/SOURCES.json new file mode 100644 index 0000000000..c7f94ddda8 --- /dev/null +++ b/research/extension-field-tensor-recognition/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/frobenius-algebra-recognition/PROOF.md", + "usage": "input", + "git_blob": "0a0b7d1fe48576be453df5aa5de0cc66463352fa", + "sha256": "726d9c294f0b4b9085e3994ffb8c93737822b78d6f5d0c63f81e36b718419e28" + }, + { + "path": "research/frobenius-tensor-characters/README.md", + "usage": "input", + "git_blob": "b62f9a906e6ed49605684cca52a221f064924461", + "sha256": "31573ba91ac69caff5b8e5a42ce7fd0d80a6d54673c08d7f225c9ee08e0e0893" + }, + { + "path": "research/nonreduced-tensor-recognition/README.md", + "usage": "input", + "git_blob": "826c6b010725d98b6ca6599a748c4179264140e9", + "sha256": "2eaed94a9f12ad7b6bb7253b14bff95b86549b3e320f0e91fa4e35c0025536de" + } + ] +} diff --git a/research/extension-field-tensor-recognition/TASK.json b/research/extension-field-tensor-recognition/TASK.json new file mode 100644 index 0000000000..a453451d7c --- /dev/null +++ b/research/extension-field-tensor-recognition/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63", + "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 Frobenius-truncated multiplication tensors over explicit finite extension fields, return all three factor maps and an exact special-linear orbit label. Construct determinant-one maps between equivalent accepted tensors.", + "scope_change_reason": "Take the released extension-field handoff of PR5540 and PR5502. This is a written algebraic interface proof and executable certificate, not a proof-assistant claim.", + "bottleneck_link": "Remove the algebra-class promise from PR5459 tensor-character screening. Native realization and the complete paid supplier remain open.", + "budget_minutes": 120, + "stop_rule": "Finish the semilinear kernel proof and complete small-field orbit comparison, or report an explicit failure. Do not expand to arbitrary algebra isomorphism.", + "outcome": "completed", + "evidence": "README.md; recognize.py; verify.py: all 65536 F4 and 256 F2 tensors, 90 changed-basis presentations, 90 determinant-one transporters, 2322 products for each map class, and 125 controls.", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance with proof, code, exact checks and documentation.", + "open_questions": [ + { + "question": "Bind a recognized tensor to a paid native consumer.", + "why_it_matters": "Recognition alone changes no complete kappa bill.", + "first_step": "Specify a producer, consumer and all coefficient, restoration and movement costs.", + "blocked_by": "No such supplier is provided." + } + ] +} diff --git a/research/extension-field-tensor-recognition/VERIFY.json b/research/extension-field-tensor-recognition/VERIFY.json new file mode 100644 index 0000000000..b73dc604f8 --- /dev/null +++ b/research/extension-field-tensor-recognition/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/frobenius-algebra-recognition/PROOF.md", + "research/frobenius-tensor-characters/README.md", + "research/nonreduced-tensor-recognition/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Complete F2/F4 tensor domains, literal factor maps, semilinear failure controls and orbit labels." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Complete F2/F4 tensor domains, literal factor maps, semilinear failure controls and orbit labels." + } + ] +} diff --git a/research/extension-field-tensor-recognition/recognize.py b/research/extension-field-tensor-recognition/recognize.py new file mode 100644 index 0000000000..1066bb74c1 --- /dev/null +++ b/research/extension-field-tensor-recognition/recognize.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/extension-field-tensor-recognition/verify.py b/research/extension-field-tensor-recognition/verify.py new file mode 100644 index 0000000000..a8f8d85d71 --- /dev/null +++ b/research/extension-field-tensor-recognition/verify.py @@ -0,0 +1,216 @@ +"""Check exact certificates and complete small orbits. Apache-2.0.""" +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import random +import time + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('extension_recognize', HERE / 'recognize.py') +r = importlib.util.module_from_spec(spec) +spec.loader.exec_module(r) + + +def require(ok, message): + if not ok: + raise RuntimeError(message) + + +def fields(): + return [r.Field(p, f) for p, f in [(2, (0, 1)), (3, (0, 1)), (2, (1, 1, 1)), + (2, (1, 1, 0, 1)), (3, (1, 0, 1)), (2, (1, 1, 0, 0, 1)), (5, (2, 0, 1))]] + + +def changed(t, u, v, w, f): + ui, vi = r.inverse(u, f), r.inverse(v, f) + n = len(t) + return [[r.mv(w, r.tensor_value(t, r.column(ui, i), r.column(vi, j), f), f) + for j in range(n)] for i in range(n)] + + +def random_gl(n, f, rng): + a = r.identity(n) + for _ in range(5 * n + 3): + i = rng.randrange(n) + c = rng.randrange(1, f.q) + a[i] = [f.mul[c][x] for x in a[i]] + if n > 1: + j = (i + rng.randrange(1, n)) % n + c = rng.randrange(f.q) + a[i] = [f.add[x][f.mul[c][y]] for x, y in zip(a[i], a[j])] + return a + + +def oracle_orbit(f): + """Apply literal invertible matrices to each of the three tensor indices.""" + q = f.q + matrices = [[[0, 1], [1, 0]], [[1, 1], [0, 1]]] + if q > 2: + primitive = next(a for a in range(1, q) if len({f.power(a, i) for i in range(q-1)}) == q-1) + matrices.append([[primitive, 0], [0, 1]]) + powers = [q ** i for i in range(8)] + def pack(t): + return sum(x * powers[i] for i, x in enumerate(t)) + # The standard dual-number table has coefficients 000, 011, 101. + seed = pack([1, 0, 0, 1, 0, 1, 0, 0]) + seen, queue = {seed}, [seed] + for code in queue: + values = [(code // a) % q for a in powers] + for axis in (1, 2, 4): + for a in matrices: + out = values[:] + for i in range(8): + if i & axis: + continue + x, y = values[i], values[i + axis] + out[i] = f.add[f.mul[a[0][0]][x]][f.mul[a[0][1]][y]] + out[i + axis] = f.add[f.mul[a[1][0]][x]][f.mul[a[1][1]][y]] + next_code = pack(out) + if next_code not in seen: + seen.add(next_code) + queue.append(next_code) + return seen + + +def exhaustive(f): + expected = oracle_orbit(f) + accepted = set() + digest = hashlib.sha256() + 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, reason = r.recognize(t, f) + require((cert is not None) == (code in expected), f'orbit disagreement: q={f.q}, tensor={code}, {reason}') + if cert is not None: + accepted.add(code) + require(r.check_certificate(t, cert, f), 'exhaustive transporter') + digest.update(code.to_bytes(4, 'big')) + return {'field': f.q, 'domain': f.q ** 8, 'accepted': len(accepted), 'accepted_sha256': digest.hexdigest()} + + +def main(): + start = time.monotonic() + sources = json.loads((HERE / "SOURCES.json").read_text()) + for item in sources["files"]: + if item["usage"] == "input": + data = (HERE.parents[1] / item["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == item["sha256"], "source bytes changed") + fs = fields() + for f in fs: + for a, b, c in itertools.product(range(f.q), repeat=3): + require(f.add[f.add[a][b]][c] == f.add[a][f.add[b][c]], 'additive associativity') + require(f.mul[f.mul[a][b]][c] == f.mul[a][f.mul[b][c]], 'multiplicative associativity') + require(f.mul[a][f.add[b][c]] == f.add[f.mul[a][b]][f.mul[a][c]], 'distributivity') + for a in range(f.q): + require(f.add[a][f.neg[a]] == 0 and f.mul[a][1] == a and f.power(a, f.q) == a, 'field laws') + controls = 0 + for p, poly in [(4, (0,1)), (2, (0,0,1)), (2, (1,0,1)), (3, (2,0,1)), (2, (1,2,1))]: + try: + r.Field(p, poly) + except ValueError: + controls += 1 + else: + raise RuntimeError('invalid field accepted') + rng = random.Random(9405540) + fixtures = products = labels = 0 + for f in fs: + for hs in [[], [1], [2], [1,1], [1,2]]: + if f.p ** sum(hs) > 9: + continue + t, _ = r.model(hs, f) + n = len(t) + for _ in range(3): + u, v, w = (random_gl(n, f, rng) for _ in range(3)) + original = changed(t, u, v, w, f) + cert, reason = r.recognize(original, f) + require(cert is not None, 'positive fixture rejected: '+str((f.q, hs, reason))) + require(cert['heights'] == hs and r.check_certificate(original, cert, f), 'wrong transporter') + index = cert['sl_orbit_count'] + delta = f.mul[r.determinant(w, f)][f.inv[f.mul[r.determinant(u, f)][r.determinant(v, f)]]] + require(cert['sl_orbit_label'] == f.power(delta, (f.q-1)//index), 'transporter-independent SL label') + labels += 1 + sl = [random_gl(n, f, rng) for _ in range(3)] + for matrix in sl: + scale = f.inv[r.determinant(matrix,f)] + matrix[0] = [f.mul[scale][x] for x in matrix[0]] + second = changed(original, *sl, f) + maps, why = r.sl_transporter(original, second, f) + require(maps is not None, 'equal-label transport failed: '+str(why)) + require(all(r.determinant(maps[k],f) == 1 for k in ('F','G','H')), 'SL determinant') + for i in range(n): + for j in range(n): + require(r.tensor_value(second,r.column(maps['F'],i),r.column(maps['G'],j),f) + == r.mv(maps['H'],original[i][j],f), 'SL transported product') + bad = dict(cert) + bad['W'] = [row[:] for row in cert['W']] + bad['W'][0][0] = f.add[bad['W'][0][0]][1] + require(not r.check_certificate(original, bad, f), 'altered transporter accepted') + controls += 1 + fixtures += 1 + products += n*n + n = 3 + square = [[[0]*n for _ in range(n)] for _ in range(n)] + for i in range(n): + square[0][i][i] = square[i][0][i] = 1 + require(r.recognize(square, f)[1] == 'height dimension', 'extra relation accepted') + controls += 1 + # The dual action has an output module with a two-dimensional top. + 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 module accepted') + controls += 1 + split = [[[int(i == j == k) for k in range(2)] for j in range(2)] for i in range(2)] + require(r.recognize(split, f)[1] == 'residue field or number of components', 'split algebra accepted') + controls += 1 + f = fs[2] + mu, _ = r.model([1], f) + c = [[1, 2], [0, 1]] + table = changed(mu, r.inverse(c,f), r.inverse(c,f), r.inverse(c,f), f) + unit = [1,0] + powers = r.columns([r.algebra_power(table, e, 2, unit, f) for e in r.identity(2)], 2) + wrong_kernel = r.kernel(powers, 2, f) + right_kernel = r.semilinear_kernel(table, unit, 1, f) + require(wrong_kernel == [[3,1]] and right_kernel == [[2,1]], 'explicit semilinear fixture changed') + require(r.algebra_power(table, wrong_kernel[0], 2, unit, f) == [1,0], 'untwisted kernel control') + require(r.algebra_power(table, right_kernel[0], 2, unit, f) == [0,0], 'twisted kernel') + direct_second = r.columns([r.algebra_power(table, e, 4, unit, f) for e in r.identity(2)],2) + require(r.mm(powers,powers,f) != direct_second, 'untwisted matrix iterate control') + controls += 2 + mu, _ = r.model([2], f) + unit = [1,0,0,0] + require(len(r.semilinear_kernel(mu, unit, 1, f)) == 2, 'p-kernel dimension') + require(len(r.semilinear_kernel(mu, unit, 2, f)) == 3, 'q-kernel dimension') + require(r.recognize(mu, f)[0]['heights'] == [2], 'q-power used as height one') + controls += 1 + a = r.recognize(mu,f)[0] + b = r.recognize(r.model([1,1],f)[0],f)[0] + require((a['sl_orbit_count'],b['sl_orbit_count']) == (3,1), 'dimension-only character control') + realized = set() + for scalar in range(1,4): + w = r.identity(4);w[0][0] = scalar + cert,_ = r.recognize(changed(mu,r.identity(4),r.identity(4),w,f),f) + realized.add(cert['sl_orbit_label']) + require(realized == {1,2,3}, 'missing special-linear orbit') + w = r.identity(4);w[0][0] = 2 + different = changed(mu,r.identity(4),r.identity(4),w,f) + require(r.sl_transporter(mu,different,f)[1] == 'different special-linear orbits', 'different labels accepted') + controls += 2 + for bad in [[], [[[4]]], [[[True]]], [[[0,0]]]]: + try: + r.recognize(bad,f) + except ValueError: + controls += 1 + else: + raise RuntimeError('invalid tensor accepted') + out = {'positive_presentations': fixtures, 'transported_basis_products': products, + 'independent_label_comparisons': labels, 'SL_transporters': labels, 'controls': controls, + 'explicit_F4_kernel': {'wrong': wrong_kernel, 'correct': right_kernel}, + 'exhaustive': [exhaustive(fs[0]),exhaustive(fs[2])]} + print(json.dumps(out,sort_keys=True)) + print('PASS_EXTENSION_FIELD_TENSOR_RECOGNITION') + print(f'elapsed_seconds={time.monotonic()-start:.3f}') + + +if __name__ == '__main__': + main()