From c777c9a4b5f50a0e1561b2e24304486f40e8d001 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 12:08:23 -0500 Subject: [PATCH] Exact determinant characters for truncated-polynomial multiplication tensors --- .../truncated-tensor-characters/README.md | 64 ++++++++++ .../truncated-tensor-characters/SOURCES.json | 18 +++ .../truncated-tensor-characters/TASK.json | 101 +++++++++++++++ .../truncated-tensor-characters/VERIFY.json | 34 ++++++ .../truncated-tensor-characters/verify.py | 115 ++++++++++++++++++ 5 files changed, 332 insertions(+) create mode 100644 research/truncated-tensor-characters/README.md create mode 100644 research/truncated-tensor-characters/SOURCES.json create mode 100644 research/truncated-tensor-characters/TASK.json create mode 100644 research/truncated-tensor-characters/VERIFY.json create mode 100644 research/truncated-tensor-characters/verify.py diff --git a/research/truncated-tensor-characters/README.md b/research/truncated-tensor-characters/README.md new file mode 100644 index 0000000000..9dac5ac07e --- /dev/null +++ b/research/truncated-tensor-characters/README.md @@ -0,0 +1,64 @@ +# Exact determinant characters for truncated-polynomial multiplication tensors + +This scoped proof gives the exact stabilizer determinant image for multiplication tensors of A=F_q[t]/(t^n), for every prime power q and n>=1. It answers the named truncated-polynomial case of the nilpotent-algebra question in Nick Petalas's [PR #5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252), at [proof commit 07e6f55d18d2d3fd6dcea19bd642d71657c5fe14](https://github.com/CrocSwap/integer-mult-bounds/blob/07e6f55d18d2d3fd6dcea19bd642d71657c5fe14/research/etale-tensor-determinant-image/README.md). No new kappa is claimed. + +Let mu in A* tensor A* tensor A be multiplication, with the ordinary covariant action of GL(A*) times GL(A*) times GL(A). Let Delta(mu) be the ordered determinant image of its stabilizer. For r>=0, put H_r={c^r:c in F_q^*}; in particular H_0={1}. Set N=n(n-1)/2. Then + +```text +Delta(mu) = {(u,v,w): v w in H_n, u w in H_n, u v w in H_N}. +``` + +Put m=q-1, g=gcd(n,m), h=gcd(N,m), e=m/g and f=m/h. Equivalently the image has the three bounded monomial equations + +```text +(v w)^e = 1, (u w)^e = 1, (u v w)^f = 1. +``` + +Reduce the exponent rows (0,e,e), (e,0,e), (f,f,f) modulo m. This is the equation format of David Ganz's atlas A029/A030 in [PR #2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849), with the [atlas statement pinned at main](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/pure-math-atlas-400/volumes/01-algebra.md). The image size is m^3/(g^2 h). The single GL orbit splits into exactly g^2 h orbits under the product of the three special linear groups. + +The determinant image is unchanged by independent basis changes in the three factors. Therefore, under the explicit promise that an n-by-n-by-n input tensor lies in the GL orbit of this multiplication tensor, its dimensions and q alone give the three exponent rows. Computing the two greatest common divisors and reducing the rows takes polynomially many bit operations. This is a promise algorithm. It does not recognize the orbit, recover a multiplication basis, or produce a transporter. + +For q=5,n=2 the image has 16 elements and the orbit splits into four special-linear orbits. For q=5,n=3 the image is the entire 64-element determinant group. Thus automorphism determinants for this nilpotent family need not be signs. For q=7,n=3 the image has eight elements and the orbit splits into 27 special-linear orbits. At n=1 the formula reduces to u v w=1. At q=2 the determinant group is trivial. + +**Proof: unit and automorphism characters.** In the basis 1,t,...,t^(n-1), multiplication by a=a_0+a_1 t+... is triangular with diagonal a_0. Thus a is a unit exactly when a_0!=0, and det(L_a)=a_0^n. Its determinant image is exactly H_n, attained already by scalar units. + +For n>=2, an algebra automorphism sends t to c_1 t+c_2 t^2+...+c_(n-1)t^(n-1), with c_1!=0. The constant term is zero because t is nilpotent. Conversely every such substitution is well-defined, and its matrix is triangular with diagonal 1,c_1,c_1^2,...,c_1^(n-1), so it is invertible and is an automorphism. Its determinant is c_1^N. The determinant image is H_N, attained already by t mapping to c_1 t. For n=1 only the identity automorphism exists, which agrees with H_0. + +**Proof: all stabilizers and attainment.** Use the bilinear autotopism identity F(x)G(y)=H(xy), with F,G,H invertible. Put a=F(1), b=G(1). The unit substitutions give H(x)=F(x)b=aG(x), so multiplication by a and b is bijective. A bijective multiplication map makes its element a unit: surjectivity gives an inverse, and commutativity gives both products equal to 1. The map sigma=(ab)^(-1)H is then an algebra automorphism, and + +```text +F=L_a sigma, G=L_b sigma, H=L_(ab) sigma. +``` + +Conversely these maps give an autotopism for all units a,b and every algebra automorphism sigma. This is the classical normalization in atlas A019, retained by PR5252; the argument is included to fix its hypotheses. + +The covariant tensor stabilizer is (F^(-T),G^(-T),H), not (F,G,H). Set x=det L_a, y=det L_b and z=det sigma. Its determinant triple is + +```text +(u,v,w) = (x^(-1) z^(-1), y^(-1) z^(-1), x y z), +where x,y in H_n and z in H_N. +``` + +The inverse coordinate formulas are x=v w, y=u w, z=(u v w)^(-1). They prove both necessity and sufficiency of the three subgroup conditions, with no additional relation. Scalar units and linear substitutions attain every choice of x,y,z. The power subgroup H_r of the cyclic group F_q^* has size m/gcd(r,m) and is defined by the power m/gcd(r,m). This gives the equation rows and image size, including r=0. + +Independent changes of tensor bases conjugate the stabilizer inside the product GL group, and determinants are invariant under conjugacy. Finally the product SL group is the kernel of the surjective determinant map from the product GL group to (F_q^*)^3. Its orbits inside the fixed GL orbit are the cosets of Delta(mu) in that determinant group. Their number is the index g^2 h. This completes the proof. + +**Evidence.** The standalone checker constructs 1,734 literal scalar-unit/substitution autotopisms in 24 contexts, with q=2,3,5,7 and n=1 through 6. Their covariant determinant triples attain every predicted image. Separately, seven complete small domains enumerate all 260,985 invertible input-map pairs, derive the only possible output map from the unit identity, and test every basis product. They accept 1,729 autotopisms, including nonconstant units and nonlinear substitutions, and recover exactly the predicted images. These complete domains are (q,n)=(2,1),(2,2),(2,3),(3,1),(3,2),(5,1),(5,2). + +Seven controls distinguish the inverse-input convention, non-surjective unit norms, automorphism determinants outside the sign subgroup, n=1, q=2, and two unsupported checker domains. In particular at q=7,n=4 the raw autotopism determinant triple (2,1,2) is excluded, while its correct covariant triple (4,1,2) is admitted. Normal and optimized warning-strict CPython 3.12.14 checks pass. The proof covers every finite field; these finite fixtures use prime fields only. No predecessor executable is imported or replayed. + +Credit Nick Petalas's [PR #5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252) for the finite-etale result, the inverse-input convention and the explicit nilpotent follow-up. Its [pinned proof](https://github.com/CrocSwap/integer-mult-bounds/blob/07e6f55d18d2d3fd6dcea19bd642d71657c5fe14/research/etale-tensor-determinant-image/README.md) is context, not an imported algorithm. Credit David Ganz's [PR #2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849) for atlas A019 normalization, A029 character equations and A030 extraction. Classical isotopy, cyclic-group and truncated-polynomial-algebra facts retain their credit. No general literature-priority claim is made. + +**Limits.** This is the single truncated-polynomial local algebra, not every finite local algebra or product of local factors. Orbit recognition, a transporter, physical coefficient preparation, native realization, movement, precision and supplier/outer admission remain open. No new multiplier is supplied. No selected cold replay, predecessor scientific suite, native build, Lean or Docker run was used. No independent human or proof-kernel acceptance is claimed. Base: canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7. Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. + +## Reproduce + +```sh +python3 -B scripts/research_package.py --package research/truncated-tensor-characters +``` + +Use Python 3.12 with the standard library. The normal and optimized commands must print `PASS_TRUNCATED_TENSOR_CHARACTERS`. The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The checker has no external runtime inputs. + +## Open next questions + +Extend the character calculation to a specified multivariable local algebra or recognize the orbit promise. The source binding and physical cost model are not supplied by this package. See `TASK.json` for the structured scope. diff --git a/research/truncated-tensor-characters/SOURCES.json b/research/truncated-tensor-characters/SOURCES.json new file mode 100644 index 0000000000..277ad46954 --- /dev/null +++ b/research/truncated-tensor-characters/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + } + ] +} diff --git a/research/truncated-tensor-characters/TASK.json b/research/truncated-tensor-characters/TASK.json new file mode 100644 index 0000000000..f9ad8df7f3 --- /dev/null +++ b/research/truncated-tensor-characters/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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": "This scoped proof answers the truncated-polynomial nilpotent case left open by PR #5252. For multiplication in F_q[t]/(t^n), it gives the full covariant stabilizer determinant image, three bounded character equations, and the exact splitting of its GL orbit into SL orbits. Extraction uses q and n under an explicit orbit promise.", + "scope_change_reason": "This is a scoped interface theorem. It does not complete the original supplier or uniform-transfer task.", + "bottleneck_link": "Extend the character calculation to a specified multivariable local algebra or recognize the orbit promise.", + "budget_minutes": 60, + "stop_rule": "Stop after the scoped proof, exact controls and bounded registered replay; do not expand to physical lowering.", + "outcome": "completed", + "evidence": "1,734 literal attaining maps, seven complete stabilizer domains with 260,985 input-map pairs and 1,729 autotopisms, and seven controls", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or proof-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "Extend the character calculation to a specified multivariable local algebra or recognize the orbit promise.", + "why_it_matters": "The abstract result needs an actual caller and a complete cost model.", + "first_step": "Extend the character calculation to a specified multivariable local algebra or recognize the orbit promise.", + "blocked_by": "No production caller or physical cost model is supplied." + } + ], + "upstream_checkpoint": { + "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "priority_revision": 7, + "checked_at": "2026-10-23T17:05:58.754176+00:00" + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19150438" +} diff --git a/research/truncated-tensor-characters/VERIFY.json b/research/truncated-tensor-characters/VERIFY.json new file mode 100644 index 0000000000..c123dcdefa --- /dev/null +++ b/research/truncated-tensor-characters/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "1,734 literal attaining maps, seven complete stabilizer domains with 260,985 input-map pairs and 1,729 autotopisms, and seven controls" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "1,734 literal attaining maps, seven complete stabilizer domains with 260,985 input-map pairs and 1,729 autotopisms, and seven controls" + } + ] +} diff --git a/research/truncated-tensor-characters/verify.py b/research/truncated-tensor-characters/verify.py new file mode 100644 index 0000000000..82fb474d54 --- /dev/null +++ b/research/truncated-tensor-characters/verify.py @@ -0,0 +1,115 @@ +"""Truncated-algebra tensor characters. Ali Romman with OpenAI Codex. Apache-2.0.""" +from itertools import product +from math import gcd +import json + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def det(columns, p): + n = len(columns) + a = [[columns[j][i] for j in range(n)] for i in range(n)] + answer = 1 + for j in range(n): + pivot = next((i for i in range(j, n) if a[i][j]), None) + if pivot is None: + return 0 + if pivot != j: + a[j], a[pivot] = a[pivot], a[j] + answer = -answer + value = a[j][j] + answer = answer * value % p + inverse = pow(value, -1, p) + for i in range(j + 1, n): + factor = a[i][j] * inverse % p + a[i] = [(x-factor*y) % p for x, y in zip(a[i], a[j])] + return answer % p + + +def multiply(a, b, p): + n = len(a) + return tuple(sum(a[i]*b[j-i] for i in range(j+1)) % p for j in range(n)) + + +def image(p, n): + require(p in (2, 3, 5, 7) and 1 <= n <= 6, 'bounded prime-field domain') + units = range(1, p) + dn = gcd(n, p-1); da = gcd(n*(n-1)//2, p-1) + e = (p-1)//dn; f = (p-1)//da + return {(u, v, w) for u, v, w in product(units, repeat=3) + if pow(v*w % p, e, p) == pow(u*w % p, e, p) == 1 + and pow(u*v*w % p, f, p) == 1} + + +def complete_census(p, n): + elements = list(product(range(p), repeat=n)) + index = {x: i for i, x in enumerate(elements)} + zero = index[(0,)*n] + mul = [[index[multiply(a, b, p)] for b in elements] for a in elements] + invertible = [] + for indices in product(range(len(elements)), repeat=n): + d = det([elements[i] for i in indices], p) + if d: + invertible.append((indices, d)) + actual = set(); accepted = pairs = 0 + for (a, da), (b, db) in product(invertible, repeat=2): + pairs += 1 + h = tuple(mul[x][b[0]] for x in a) + dh = det([elements[i] for i in h], p) + if not dh: + continue + if all(mul[a[i]][b[j]] == (h[i+j] if i+j < n else zero) + for i, j in product(range(n), repeat=2)): + accepted += 1 + actual.add((pow(da, -1, p), pow(db, -1, p), dh)) + require(actual == image(p, n), ('complete stabilizer image', p, n, actual)) + expected = (p-1)**2 if n == 1 else (p-1)**3 * p**(3*n-4) + require(accepted == expected, ('autotopism count', p, n, accepted)) + return pairs, accepted + + +def attainment(p, n): + actual = set(); count = 0 + for a, b, c in product(range(1, p), repeat=3): + sigma = [tuple(pow(c, j, p) if i == j else 0 for i in range(n)) for j in range(n)] + f = [tuple(a*x % p for x in col) for col in sigma] + g = [tuple(b*x % p for x in col) for col in sigma] + h = [tuple(a*b*x % p for x in col) for col in sigma] + require(all(multiply(f[i], g[j], p) == (h[i+j] if i+j < n else (0,)*n) + for i, j in product(range(n), repeat=2)), 'literal attainment product') + actual.add((pow(det(f, p), -1, p), pow(det(g, p), -1, p), det(h, p))) + count += 1 + require(actual == image(p, n), ('attainment image', p, n)) + require(len(actual)*gcd(n, p-1)**2*gcd(n*(n-1)//2, p-1) == (p-1)**3, 'orbit index') + return count + + +def main(): + generated = sum(attainment(p, n) for p in (2, 3, 5, 7) for n in range(1, 7)) + pairs = accepted = 0 + contexts = ((2, 1), (2, 2), (2, 3), (3, 1), (3, 2), (5, 1), (5, 2)) + for p, n in contexts: + a, b = complete_census(p, n) + pairs += a; accepted += b + require((2, 1, 2) not in image(7, 4) and (4, 1, 2) in image(7, 4), 'inverse-input convention') + require(len(image(5, 2)) == 16, 'non-surjective unit norm') + require(len(image(5, 3)) == 64, 'automorphism determinants need not be signs') + require(len(image(5, 1)) == 16, 'dimension-one boundary') + require(image(2, 6) == {(1, 1, 1)}, 'binary determinant boundary') + for p, n in ((4, 2), (3, 0)): + try: + image(p, n) + except ValueError: + pass + else: + raise ValueError('bounded-domain violation accepted') + print(json.dumps(dict(status='PASS_TRUNCATED_TENSOR_CHARACTERS', generated_maps=generated, + complete_domains=len(contexts), input_map_pairs=pairs, autotopisms=accepted, + controls=7, no_new_kappa=True), sort_keys=True)) + + +if __name__ == '__main__': + main()