From ccd6d17483349ad1995369d4776f96482a40fa60 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sat, 24 Oct 2026 15:17:16 -0500 Subject: [PATCH] Classify exact cube-zero outer-product cost by quadratic relations --- research/cube-zero-product-map-cost/README.md | 140 +++++++++++++++++ .../cube-zero-product-map-cost/SOURCES.json | 36 +++++ research/cube-zero-product-map-cost/TASK.json | 95 ++++++++++++ .../cube-zero-product-map-cost/VERIFY.json | 30 ++++ research/cube-zero-product-map-cost/verify.py | 146 ++++++++++++++++++ 5 files changed, 447 insertions(+) create mode 100644 research/cube-zero-product-map-cost/README.md create mode 100644 research/cube-zero-product-map-cost/SOURCES.json create mode 100644 research/cube-zero-product-map-cost/TASK.json create mode 100644 research/cube-zero-product-map-cost/VERIFY.json create mode 100644 research/cube-zero-product-map-cost/verify.py diff --git a/research/cube-zero-product-map-cost/README.md b/research/cube-zero-product-map-cost/README.md new file mode 100644 index 0000000000..255791a528 --- /dev/null +++ b/research/cube-zero-product-map-cost/README.md @@ -0,0 +1,140 @@ +# Exact cost from the cube-zero product map + +This package answers the product-map question in Nick Petalas's PR4764. For the +same two-role outer-product target, it classifies exactly when quadratic +relations lower the paid right-vector cost from three to two. It also gives the +minimum dimension of the product image needed for a cost-three witness. The +complete kappa calculation is unchanged. + +## Theorem + +Let A=K plus J be a split commutative local algebra over a field K, with J cubed +zero. Choose x,y whose images span a two-dimensional subspace U of J/J squared. +Let mu: Sym squared(U) -> J squared be multiplication and let L=ker(mu). +Identify Sym squared(U) with the three-dimensional binary quadratic forms +on formal variables X,Y. Use paid factors I+u v^T, u in A squared and v in +K squared, and arbitrary free GL2(K) maps. Singular paid factors are allowed. +Put M=[[x squared,xy],[xy,y squared]]. Then + +``` +cost(M) = 3 if L contains no nonzero product of two K-linear forms; +cost(M) = 2 otherwise. +``` + +Equivalently, cost is three exactly when L is zero or is a line generated by +an irreducible binary quadratic. This covers every field, including +characteristic two and inseparable irreducible quadratics. It classifies this +outer-product family, not all matrices over a cube-zero algebra. + +## Proof + +The predecessor's three paid factors work unchanged: + +``` +C1 = [[x,0],[y,1]], C2 = [[1,y],[0,0]], C3 = [[x,0],[0,1]], +C1 C2 C3 = M. +``` + +Each factor changes one base-field column direction. The identity uses only +commutativity. All entries of M lie in J squared. The exact two-factor criterion +of PR4276 says that cost is at most two exactly when some N=G M H, with G,H +in GL2(K), satisfies N12 in N11 A. Since J cubed is zero, N11 A=K N11. +Thus this condition is equivalent to a nonzero row phi and column v over K +with phi M v=0. The forward direction subtracts the relevant scalar multiple +of the first column of H from its second. The reverse direction chooses phi +as the first row of G and v as the second column of H. + +For phi=(a,b) and v=(c,d), phi M v=(ax+by)(cx+dy). This is zero exactly when +the nonzero split form (aX+bY)(cX+dY) lies in L. If such a pair exists, choose +G,H as above; then N12=0 and the explicit two-factor construction is + +``` +N = [[N11,0],[N21,1]] [[1,0],[0,N22]], +M = G^-1 N H^-1. +``` + +No zero- or one-factor word can equal M. Its scalar residue is the zero +2-by-2 matrix. A free map has rank two, and the scalar residue of I+u v^T +has rank at least one. Invertible free maps do not change that lower bound. +This includes M=0: the zero matrix has cost two in this alphabet. + +It remains to classify L. If dim(L)>=2, the linear functional that takes the +X squared coefficient has a nonzero kernel on L. A nonzero form there is +Y(bX+cY), hence split. A one-dimensional L avoids all split forms exactly +when its generator is irreducible. The zero space also avoids them. This +proves the classification without a census or a field-size restriction. + +## Minimum product image and finite-field count + +The rank of mu is three minus dim(L). A cost-three witness therefore needs +at least two product directions. Rank two suffices exactly when K has an +irreducible quadratic. For such a form Q, the five-dimensional algebra +K[X,Y]/((X,Y) cubed,Q) attains rank two and cost three. If K has no irreducible +quadratic, rank three is necessary and K[X,Y]/(X,Y) cubed attains it. +The minimum concerns this two-plane witness. It is not a minimum dimension +for every possible right-vector obstruction or every local algebra. + +Over F_q, there are 1+q(q-1)/2 relation subspaces with cost three: the zero +space and the irreducible quadratic lines. A nonzero irreducible binary +quadratic has nonzero leading coefficient and gives one monic irreducible +quadratic. Of the q squared monic quadratics, q(q+1)/2 are products with an +unordered pair of roots in F_q. This gives the stated count. All other +subspaces give cost two. The total number of subspaces of F_q cubed is +2q squared+2q+4. Extra unused directions in J squared do not change the cost. + +For F2 the minimal example imposes X squared+XY+Y squared=0. Its product +image has dimension two, and every pair of nonzero forms on U has nonzero +product. Thus the predecessor's six-dimensional coefficient algebra is not +minimal for this witness. + +## Evidence and reproduction + +```sh +python3.12 -B scripts/research_package.py --package research/cube-zero-product-map-cost +``` + +Use Python 3.12 and the standard library. The verifier enumerates every +quadratic relation subspace over F2,F3,F5,F7. It compares literal products of +all projective pairs with a separate polynomial-root test, checks the full +three-factor word, and constructs a two-factor free chart in every low-cost +case. It applies each word to all independent quotient-basis input columns. +Controls reject reversed order, deleted factors and a split relation mistaken +for an irreducible one. Normal and optimized replay use explicit exceptions. +The written proof supplies the all-field claim. No extension-field census, +predecessor scientific replay, Lean or selected cold replay is claimed. + +## Sources, scope and overlap + +Nick Petalas's [PR #4764](https://github.com/CrocSwap/integer-mult-bounds/pull/4764) +and its [retained proof and open question](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/cube-zero-three-factor/README.md) +supply the word and product-map question. His +[PR #4276](https://github.com/CrocSwap/integer-mult-bounds/pull/4276) supplies the +[pinned two-factor criterion](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/right-vector-two-factor-criterion/PROOF.md). +The higher-nilpotency and common-chart lineage retains its source credit. +[PR #5320](https://github.com/CrocSwap/integer-mult-bounds/pull/5320) instead +classifies quadratic lifts of a nonzero first-order pencil; this package has +zero first-order target. Exact source objects are in SOURCES.json. + +The live all-state cube-zero search and current note/Discussion search found +no same product-map classification. Unposted work and arbitrary historical +diffs remain outside coverage. Source coefficient preparation, physical maps, +routing, restoration, precision, stock and the whole supplier bill are unpriced. +This result does not admit a supplier, change the selected frontier or prove +a complete multiplication theorem. + +## Open next questions + +Find a physical realization of the five-dimensional irreducible-quotient +algebra and price each coefficient operation in the three-factor word. Start +with the explicit F2 relation above. Coefficient preparation and the complete +producer/consumer cost are the blockers; fewer coefficient dimensions alone +do not give a recursive saving. A different two-plane in a specified larger +cube-zero algebra can be tested directly by the proved kernel criterion. + +## Credit + +Nick Petalas (@petalas) supplies the exact criterion, original witness and open +question. Wentao Li's right-vector alphabet and ToikY's shared-chart context +retain the attribution in those sources. Binary quadratic factorization and +finite-field counts are classical. Ali Romman with substantial OpenAI Codex +assistance; Apache-2.0. No independent human or proof-kernel acceptance is claimed. diff --git a/research/cube-zero-product-map-cost/SOURCES.json b/research/cube-zero-product-map-cost/SOURCES.json new file mode 100644 index 0000000000..961d6b3caf --- /dev/null +++ b/research/cube-zero-product-map-cost/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "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/cube-zero-three-factor/README.md", + "usage": "provenance", + "git_blob": "3a697077366e762de8b1b7304768e7ae8c4a1f62", + "sha256": "05c1e3d04630243bf2078059c6f13cce3361d0c9ed518190f5dba585d2e9d383" + }, + { + "path": "research/right-vector-two-factor-criterion/PROOF.md", + "usage": "provenance", + "git_blob": "71888afa0db63d6d332cbbdc408abf1aa879681c", + "sha256": "c1065c51c839d11b0d31bccb8d39ebc07a869eb0f29899038518e3090a58c895" + }, + { + "path": "research/cube-zero-lift-obstruction/README.md", + "usage": "provenance", + "git_blob": "10044ad7c5bdce30e67d756805b790f8fab1f07e", + "sha256": "36fc090489e43f8d73355aeeb7eac717d3d3a359b3abdf22530fc51a4068da20" + } + ] +} diff --git a/research/cube-zero-product-map-cost/TASK.json b/research/cube-zero-product-map-cost/TASK.json new file mode 100644 index 0000000000..72c8bb8d72 --- /dev/null +++ b/research/cube-zero-product-map-cost/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "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": "Classify the exact two- or three-factor cost of every cube-zero two-plane outer-product witness by its quadratic relation space.", + "scope_change_reason": "Take PR4764 open question 2 as an algebraic interface theorem and exact census rather than a Lean formalization.", + "bottleneck_link": "Determine which coefficient multiplication maps retain the right-vector separation before pricing a physical realization.", + "budget_minutes": 60, + "stop_rule": "Finish the kernel theorem, minimal image dimension and complete small-field checks; do not infer a physical cost.", + "outcome": "completed", + "evidence": "README.md proof and verify.py complete relation-space census with attaining words.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance.", + "open_questions": [ + { + "question": "Can the five-dimensional irreducible-quotient algebra be realized and priced physically?", + "why_it_matters": "The formal cost separation helps only if coefficient production and use fit the complete bill.", + "first_step": "Realize the explicit binary quotient and price the three-factor word.", + "blocked_by": "No physical coefficient, routing or restoration model is supplied." + } + ] +} diff --git a/research/cube-zero-product-map-cost/VERIFY.json b/research/cube-zero-product-map-cost/VERIFY.json new file mode 100644 index 0000000000..ecea8d39aa --- /dev/null +++ b/research/cube-zero-product-map-cost/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete relation spaces, projective products, explicit words and all quotient-basis inputs." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete relation spaces, projective products, explicit words and all quotient-basis inputs." + } + ] +} diff --git a/research/cube-zero-product-map-cost/verify.py b/research/cube-zero-product-map-cost/verify.py new file mode 100644 index 0000000000..4f383c1aa7 --- /dev/null +++ b/research/cube-zero-product-map-cost/verify.py @@ -0,0 +1,146 @@ +#!/usr/bin/env python3 +"""Check every quadratic relation space over four prime fields. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from itertools import product +import json + + +def require(c,m): + if not c: raise ValueError(m) + + +def rref(rows,p): + rows=[list(r) for r in rows if any(r)]; k=0 + for j in range(3): + pivot=next((i for i in range(k,len(rows)) if rows[i][j]%p),None) + if pivot is None: continue + rows[k],rows[pivot]=rows[pivot],rows[k]; t=pow(rows[k][j],-1,p) + rows[k]=[x*t%p for x in rows[k]] + for i in range(len(rows)): + if i!=k: + t=rows[i][j]; rows[i]=[(x-t*y)%p for x,y in zip(rows[i],rows[k])] + k+=1 + return tuple(tuple(r) for r in rows[:k]) + + +def projective(n,p): + return [v for v in product(range(p),repeat=n) if any(v) and next(x for x in v if x)==1] + + +def subspaces(p): + lines=projective(3,p); out={()} + for v in lines: out.add(rref([v],p)) + for v in lines: + j=next(i for i,x in enumerate(v) if x) + basis=[] + for k in range(3): + if k!=j: + a=[0]*3; a[k]=1; a[j]=-v[k]*pow(v[j],-1,p)%p; basis.append(a) + out.add(rref(basis,p)) + out.add(((1,0,0),(0,1,0),(0,0,1))) + return sorted(out,key=lambda x:(len(x),x)) + + +def reduce3(v,K,p): + v=list(v) + for row in K: + j=next(i for i,x in enumerate(row) if x); t=v[j] + v=[(x-t*y)%p for x,y in zip(v,row)] + return tuple(v) + + +MONOMIALS=[(0,0),(1,0),(0,1),(2,0),(1,1),(0,2)] + + +class Ring: + def __init__(self,p,K): + self.p,self.K=p,K; self.zero=(0,)*6; self.one=(1,0,0,0,0,0) + self.x=(0,1,0,0,0,0); self.y=(0,0,1,0,0,0) + def add(self,a,b): return tuple((x+y)%self.p for x,y in zip(a,b)) + def neg(self,a): return tuple(-x%self.p for x in a) + def scalar(self,a): return (a%self.p,0,0,0,0,0) + def mul(self,a,b): + out=[0]*6 + for i,u in enumerate(MONOMIALS): + for j,v in enumerate(MONOMIALS): + m=(u[0]+v[0],u[1]+v[1]) + if sum(m)<=2: out[MONOMIALS.index(m)]+=a[i]*b[j] + return tuple(x%self.p for x in out[:3])+reduce3(out[3:],self.K,self.p) + def mm(self,A,B): + return [[self.add(self.mul(A[i][0],B[0][j]),self.mul(A[i][1],B[1][j])) + for j in range(2)] for i in range(2)] + def sm(self,A): return [[self.scalar(x) for x in r] for r in A] + def act(self,A,v): return [self.add(self.mul(A[i][0],v[0]),self.mul(A[i][1],v[1])) for i in range(2)] + + +def inverse(A,p): + a,b=A[0]; c,d=A[1]; t=pow((a*d-b*c)%p,-1,p) + return [[d*t%p,-b*t%p],[-c*t%p,a*t%p]] + + +def main(): + contexts=cost_three=cost_two=basis_actions=zero_tests=controls=0 + by_field={} + for p in (2,3,5,7): + spaces=subspaces(p); require(len(spaces)==2*p*p+2*p+4,'complete subspace count') + directions=projective(2,p); high=0 + for K in spaces: + ring=Ring(p,K); z,o,x,y=ring.zero,ring.one,ring.x,ring.y + M=[[ring.mul(x,x),ring.mul(x,y)],[ring.mul(x,y),ring.mul(y,y)]] + C1=[[x,z],[y,o]]; C2=[[o,y],[z,z]]; C3=[[x,z],[z,o]] + require(ring.mm(ring.mm(C1,C2),C3)==M,'three-factor word') + zeros=[] + for a,b in directions: + for c,d in directions: + polynomial=((a*c)%p,(a*d+b*c)%p,(b*d)%p) + if not any(reduce3(polynomial,K,p)): zeros.append(((a,b),(c,d))) + zero_tests+=1 + if len(K)==0: predicted=True + elif len(K)==1: + a,b,c=K[0] + predicted=(a!=0 and all((a*t*t+b*t+c)%p!=0 for t in range(p))) + else: predicted=False + require(predicted==(not zeros),'independent root and product classifications') + if predicted: + cost_three+=1; high+=1; word=[C1,C2,C3] + else: + cost_two+=1; phi,v=zeros[0] + psi=next(w for w in directions if (phi[0]*w[1]-phi[1]*w[0])%p) + t=next(w for w in directions if (w[0]*v[1]-w[1]*v[0])%p) + G=[list(phi),list(psi)]; H=[[t[0],v[0]],[t[1],v[1]]] + N=ring.mm(ring.mm(ring.sm(G),M),ring.sm(H)) + require(N[0][1]==z,'zero chart') + F1=[[N[0][0],z],[N[1][0],o]]; F2=[[o,z],[z,N[1][1]]] + word=[ring.sm(inverse(G,p)),F1,F2,ring.sm(inverse(H,p))] + result=ring.sm([[1,0],[0,1]]) + for A in word: result=ring.mm(result,A) + require(result==M,'two-factor free-chart construction') + free=[i for i in range(3) if all(not row[i] or next(j for j,a in enumerate(row) if a)!=i for row in K)] + for j in [0,1,2]+[i+3 for i in free]: + basis=[0]*6; basis[j]=1 + for coordinate in range(2): + vector=[z,z]; vector[coordinate]=tuple(basis) + expected=ring.act(M,vector); actual=vector + for A in reversed(word): actual=ring.act(A,actual) + require(actual==expected,'complete input basis action') + basis_actions+=1 + if not K: + require(ring.mm(ring.mm(C3,C2),C1)!=M,'order control') + for factors in ([C2,C3],[C1,C3],[C1,C2]): + require(ring.mm(*factors)!=M,'dropped factor control'); controls+=1 + controls+=1 + contexts+=1 + require(high==1+p*(p-1)//2,'finite-field irreducible count') + by_field[str(p)]={'relation_spaces':len(spaces),'cost_three':high} + # A split quadratic line must not be called irreducible. + for p in (2,3,5,7): + K=rref([(0,1,0)],p) + require(reduce3((0,1,0),K,p)==(0,0,0),'split-relation control'); controls+=1 + print('PASS_CUBE_ZERO_PRODUCT_MAP_COST '+json.dumps(dict(contexts=contexts,cost_two=cost_two, + cost_three=cost_three,basis_actions=basis_actions,projective_products=zero_tests, + controls=controls,fields=by_field),sort_keys=True)) + + +if __name__=='__main__': main()