Exact dirty-fanout source counts over finite associative rings

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.

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"
+    }
+  ]
+}

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"
+  }
+}

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"
+    }
+  ]
+}

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))