diff --git a/research/finite-ring-source-insertions/README.md b/research/finite-ring-source-insertions/README.md new file mode 100644 index 0000000000..74b9c1a2c1 --- /dev/null +++ b/research/finite-ring-source-insertions/README.md @@ -0,0 +1,73 @@ +# Exact dirty-fanout source counts over finite associative rings + +DONE — exact source-insertion counts over every finite associative ring. Scoped algebraic theorem with exact finite checks; no new kappa. No claim remains active. + +The commutative criterion in [Discussion #5266](https://github.com/CrocSwap/integer-mult-bounds/discussions/5266) and the full-matrix-ring criterion in [Discussion #5269](https://github.com/CrocSwap/integer-mult-bounds/discussions/5269) extend to every finite unital ring, including noncommutative rings with a nonzero radical. The correct invariant is the **left** ideal generated by the demands. + +**Contract.** Let R be a finite associative ring with 1!=0. There are k>=1 independent dirty rows a_i and a disjoint preserved source p, all in R^w, w>=1. Allow fixed input-independent words in + +```text +E_ij(c): A_i <- A_i + c A_j, i!=j, +P_i(b): A_i <- A_i + b p, +``` + +with arbitrary coefficients in R, multiplied on the left. Require A_i=a_i+lambda_i p for all input values. No extra rows, clearing or observations are available. Count nonzero source insertions; row additions and coefficient preparation remain separately paid. + +Let L=sum_i R lambda_i. Then the exact minimum source-insertion count is + +```text +0 if every lambda_i=0; +1 if L is nonzero and principal as a left ideal; +2 if L is not principal as a left ideal. +``` + +One insertion can occur at any specified row, with at most 4(k-1) row additions. A two-insertion construction uses at most 2(k-1) row additions and works over every associative unital ring, without finiteness. No shortest total gate word or all-price tariff is asserted. + +**Necessity.** With one insertion beta at row i, the final source column is C e_i beta, where C is the invertible product of subsequent row additions. Thus every demand is a left multiple of beta. Applying C^(-1) expresses beta as a left linear combination of the demands. Hence L=R beta. No insertion leaves the source column zero. These arguments use neither commutativity nor finiteness. + +**Finite-ring shortening lemma.** If a finite left R-module M is cyclic and is generated by x_0,...,x_(k-1), there are a_j in R such that + +```text +beta = x_0 - sum_(j>0) a_j x_j +``` + +generates M. Here is a proof that does not treat a left annihilator as a two-sided ideal. + +Let J be the Jacobson radical. Classical finite-ring structure gives J nilpotent and R/J a product of full matrix rings M_d(F) over finite fields. Since M is cyclic, M/JM is a quotient of the left regular module R/J. In each matrix block, its component has the form F^(d by m), with 0<=m<=d, acted on by left matrix multiplication. The images X_j of the generators have stacked row spaces spanning F^m. + +Put W=sum_(j>0) row(X_j). Choose an invertible row transformation P so the first m-dim(W) rows of P X_0 form a basis modulo W, and all remaining rows lie in W. There are at least dim(W) remaining rows because d>=m. Change those rows, using vectors of W, to a basis of W followed by zeros. Keep the first rows unchanged. The resulting matrix Y has full column rank m and differs from P X_0 by sum_(j>0) B_j X_j for suitable d-by-d matrices B_j. Thus X_0+sum_(j>0) P^(-1)B_j X_j has full column rank and generates the block module. + +Do this in each semisimple block, with signs absorbed in a_j, and lift the coefficients through R -> R/J. The resulting beta satisfies M=R beta+JM. Iterating this equality gives M=R beta+J^t M for every t. Nilpotence of J yields M=R beta. This proves the lemma. The finite-ring structure and this Nakayama argument are classical inputs; the source-insertion consequence is the contribution here. + +**Restoring construction.** Apply the lemma to the cyclic left module L. Then beta=lambda_0-sum_(j>0) a_j lambda_j generates L, so choose r_j with lambda_j=r_j beta. The ordered identities are + +```text +lambda_j = r_j beta, +lambda_0 = (1+sum_(j>0) a_j r_j) beta. +``` + +Let C first perform E_j0(r_j) for all j>0 and then E_0j(a_j) for all j>0. It sends e_0 beta to lambda. Execute the literal inverse word for C, then P_0(beta), then C. All original dirt columns return to identity. This uses one insertion and at most 4(k-1) row additions. The order a_j r_j is essential; no coefficients were commuted. + +For any demand, first perform E_j0(-lambda_j), j>0; insert P_0(1); undo those additions in reverse order; then insert P_0(lambda_0-1). The other rows gain lambda_j p and row zero gains lambda_0 p, with all dirt restored. If L is nonprincipal then lambda_0!=1, so both insertions are nonzero. The necessity result makes this count optimal. + +**Wrong-side counterexample.** In the eight-element ring of upper-triangular two-by-two matrices over F2, take demands (E_11,E_12), using one-based matrix indices. Their generated left ideal is the two-dimensional space of matrices supported on the first row. It is not principal: a generator with nonzero bottom-right entry produces a nonzero second row, while one with zero bottom-right entry has a left ideal of dimension at most one. The source-insertion minimum is therefore two. Yet that same space is the principal right ideal E_11 R. Using right-ideal principality would give a false one-call conclusion. + +**Evidence.** Warning-strict normal and optimized CPython 3.12.14 runs both pass six complete finite contexts: one, two and three dirty rows over UT2(F2), two rows over UT2(F3), two over M2(F2), and two over UT2(F2) x F2. All 1,825 demand lists are checked: six zero, 1,699 one-insertion and 120 two-insertion cases. An independent exhaustive elementary-column orbit search has 38 source orbits and agrees with left-ideal principality. Every constructed word is replayed on its full original-dirt/source coefficient matrix. The right-ideal counterexample and actual noncommutativity are checked directly. No predecessor executable is imported. + +Base: canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7. Refreshed PR/Discussion overlap and the exact source contracts were checked. The semilocal right-vector results use a different paid alphabet; the infinite-ring principal-ideal obstruction is outside this finite theorem. Arbitrary historical diffs and unpublished work remain outside coverage. This is a changed `connector-alphabet-change` side scope that classifies a declared noncommutative carrier, not a selected-supplier admission. + +Credit lee-phys's [PR #5139](https://github.com/CrocSwap/integer-mult-bounds/pull/5139) and [pinned finite-commutative proof](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/finite-commutative-fanout/README.md), Nick Petalas's [PR #4916](https://github.com/CrocSwap/integer-mult-bounds/pull/4916) and [noncommutative gate contract](https://github.com/CrocSwap/integer-mult-bounds/blob/ff3cc58e370d0f678e529246f8c73e8094e18fcf/research/unit-ring-dirty-fanout/README.md), Ross Richardson's [PR #3121](https://github.com/CrocSwap/integer-mult-bounds/pull/3121), and Ali Romman's Discussions5266/5269. Their ideal invariant, restoring echo, matrix-ring case and model retain their credit. No general ring-theory priority is claimed. + +**Remaining task.** A total-price theorem for nonunit demands in a specified noncommutative ring is still separate. Start with the displayed triangular-ring demand and declared complete directional prices. Physical coefficient realization, native frames, precision, tape movement and a supplier/outer invoice remain open. No selected cold replay, native replay, Lean or Docker build was run. Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. No independent human or proof-kernel acceptance is claimed. + +## Reproduce + +```sh +python3 -B scripts/research_package.py --package research/finite-ring-source-insertions +``` + +Use Python 3.12 with the standard library. The normal and optimized commands must print `PASS_FINITE_RING_INSERTIONS`. The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The checker has no external runtime inputs. + +## Open next questions + +Price one concrete noncommutative realization, including native coefficients and movement. The source binding and physical cost model are not supplied by this package. See `TASK.json` for the structured scope. diff --git a/research/finite-ring-source-insertions/SOURCES.json b/research/finite-ring-source-insertions/SOURCES.json new file mode 100644 index 0000000000..277ad46954 --- /dev/null +++ b/research/finite-ring-source-insertions/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/finite-ring-source-insertions/TASK.json b/research/finite-ring-source-insertions/TASK.json new file mode 100644 index 0000000000..6d265dabde --- /dev/null +++ b/research/finite-ring-source-insertions/TASK.json @@ -0,0 +1,67 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "This enabling proof extends the finite-commutative source-count criterion to every finite associative unital ring. The minimum is zero for zero demand, one for a nonzero principal left demand ideal, and two otherwise. It gives restoring constructions and a noncommutative left-versus-right ideal discriminator.", + "scope_change_reason": "This is a scoped interface theorem. It does not complete the original supplier or uniform-transfer task.", + "bottleneck_link": "Price one concrete noncommutative realization, including native coefficients and movement.", + "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,825 demand lists across six ring/row contexts, including 120 nonprincipal demands and 38 elementary source orbits", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or proof-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "Price one concrete noncommutative realization, including native coefficients and movement.", + "why_it_matters": "The abstract result needs an actual caller and a complete cost model.", + "first_step": "Price one concrete noncommutative realization, including native coefficients and movement.", + "blocked_by": "No production caller or physical cost model is supplied." + } + ], + "upstream_checkpoint": { + "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "priority_revision": 7, + "checked_at": "2026-10-23T16:54:04.798419+00:00" + } +} diff --git a/research/finite-ring-source-insertions/VERIFY.json b/research/finite-ring-source-insertions/VERIFY.json new file mode 100644 index 0000000000..e6cff48396 --- /dev/null +++ b/research/finite-ring-source-insertions/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,825 demand lists across six ring/row contexts, including 120 nonprincipal demands and 38 elementary source orbits" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "1,825 demand lists across six ring/row contexts, including 120 nonprincipal demands and 38 elementary source orbits" + } + ] +} diff --git a/research/finite-ring-source-insertions/verify.py b/research/finite-ring-source-insertions/verify.py new file mode 100644 index 0000000000..a289b975d9 --- /dev/null +++ b/research/finite-ring-source-insertions/verify.py @@ -0,0 +1,102 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Check source-insertion counts over finite noncommutative rings.""" +from collections import deque +from itertools import product +import json + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def ring(kind, p): + width = 3 if kind == 'tri' else 4 + values = list(product(range(p), repeat=width)); index = {v:i for i,v in enumerate(values)} + def multiply(x,y): + if kind == 'full': + a,b,c,d=x; e,f,g,h=y + return (a*e+b*g,a*f+b*h,c*e+d*g,c*f+d*h) + a,b,c=x[:3]; d,e,f=y[:3] + z=(a*d,a*e+b*f,c*f) + return z if kind == 'tri' else z+(x[3]*y[3],) + add=[[index[tuple((a+b)%p for a,b in zip(x,y))] for y in values] for x in values] + mul=[[index[tuple(a%p for a in multiply(x,y))] for y in values] for x in values] + neg=[index[tuple(-a%p for a in x)] for x in values] + one=index[(1,0,1) if kind=='tri' else (1,0,0,1) if kind=='full' else (1,0,1,1)] + return dict(values=values,index=index,add=add,mul=mul,neg=neg,one=one,n=len(values)) + + +def run_word(r,k,word): + a=[[r['one'] if i==j else 0 for j in range(k)]+[0] for i in range(k)] + for event in word: + if event[0]=='P': + _,i,c=event;a[i][-1]=r['add'][a[i][-1]][c] + else: + _,i,j,c=event;a[i]=[r['add'][x][r['mul'][c][y]] for x,y in zip(a[i],a[j])] + return a + + +def run(): + contexts=[('tri',2,1),('tri',2,2),('tri',2,3),('tri',3,2),('full',2,2),('prod',2,2)] + total=single=double=zero=orbits=0 + for kind,p,k in contexts: + r=ring(kind,p); n=r['n'];add=r['add'];mul=r['mul'];neg=r['neg'] + principal=[frozenset(mul[a][g] for a in range(n)) for g in range(n)] + def generated(lam): + s={0} + for x in lam: + s={add[a][b] for a in s for b in principal[x]} + return frozenset(s) + reachable=set() + for beta in range(1,n): + start=(beta,)+(0,)*(k-1) + if start in reachable:continue + orbits+=1;reachable.add(start);queue=deque([start]) + while queue: + x=queue.popleft() + for i in range(k): + for j in range(k): + if i==j:continue + for c in range(1,n): + y=list(x);y[i]=add[y[i]][mul[c][y[j]]];y=tuple(y) + if y not in reachable:reachable.add(y);queue.append(y) + for lam in product(range(n),repeat=k): + ideal=generated(lam);is_principal=ideal in principal + need((lam in reachable)==(any(lam) and is_principal),'orbit versus principal LEFT ideal') + if not any(lam): + word=[];zero+=1 + elif is_principal: + chosen=None + for aa in product(range(n),repeat=k-1): + beta=lam[0] + for a,x in zip(aa,lam[1:]):beta=add[beta][neg[mul[a][x]]] + if principal[beta]==ideal:chosen=(aa,beta);break + need(chosen is not None,'finite-ring shortening') + aa,beta=chosen + rr=[next(c for c in range(n) if mul[c][beta]==x) for x in lam[1:]] + cword=[('E',j,0,c) for j,c in enumerate(rr,1)]+[('E',0,j,c) for j,c in enumerate(aa,1)] + inverse=[('E',i,j,neg[c]) for _,i,j,c in reversed(cword)] + word=inverse+[('P',0,beta)]+cword;single+=1 + else: + before=[('E',j,0,neg[x]) for j,x in enumerate(lam[1:],1)] + after=[('E',i,j,neg[c]) for _,i,j,c in reversed(before)] + word=before+[('P',0,r['one'])]+after+[('P',0,add[lam[0]][neg[r['one']]])];double+=1 + actual=run_word(r,k,word) + expected=[[r['one'] if i==j else 0 for j in range(k)]+[lam[i]] for i in range(k)] + need(actual==expected,'all original dirt and source columns') + need(sum(e[0]=='P' and e[-1]!=0 for e in word)==(0 if not any(lam) else 1 if is_principal else 2),'exact nonzero insertion count') + total+=1 + r=ring('tri',2);e11=r['index'][(1,0,0)];e12=r['index'][(0,1,0)] + left=frozenset(r['add'][r['mul'][a][e11]][r['mul'][b][e12]] for a in range(r['n']) for b in range(r['n'])) + need(all(left!=frozenset(r['mul'][a][g] for a in range(r['n'])) for g in range(r['n'])),'left ideal nonprincipal') + need(left==frozenset(r['mul'][e11][a] for a in range(r['n'])),'right ideal gives a false shortcut') + need(r['mul'][e11][e12]!=r['mul'][e12][e11],'actual noncommutativity') + return dict(status='PASS_FINITE_RING_INSERTIONS',contexts=len(contexts),demands=total, + zero=zero,single=single,double=double,source_orbits=orbits, + wrong_side_control=True,no_new_kappa=True) + + +if __name__=='__main__': + print(json.dumps(run(),sort_keys=True))