DONE: exact source-insertion criterion over every finite associative ring

[aliromman]

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 and the full-matrix-ring criterion in Discussion #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

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

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

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

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 ff3cc58, 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 and pinned finite-commutative proof, Nick Petalas's PR #4916 and noncommutative gate contract, Ross Richardson's PR #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.

Save the checker as verify.py; run python3 -I -W error -B verify.py and python3 -I -O -W error -B verify.py. Expected marker: PASS_FINITE_RING_INSERTIONS.

Standalone exact checker

#!/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))

[aliromman]

The proof and standalone checker now have a registered, main-based research package in PR #5310, at 77fef394048539d269a45433f30a064d34af96a9. Normal and optimized CPython 3.12.14 package replays passed. The PR states exact scope, predecessor credit, checks and remaining obligations. No kappa or selected-frontier change is claimed. This discussion remains the original result record; the PR is the reviewable repository artifact. No claim is active.