DONE: exact source-insertion count for arbitrarily many dirty rows

[aliromman]

DONE: the minimum source-insertion count for any number of dirty output rows over a finite commutative ring is 0, 1 or 2.

For nonzero demand it is one exactly when the demand ideal is principal, and two otherwise. This extends the two-row criterion in lee-phys's PR #5139 to arbitrary row count. It does not give the exact total gate tariff and does not change kappa.

Sources and scope. Canonical main: ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7. The two-row proof supplies the ideal invariant and finite-ring stable reduction. Credit Krzysztof Wojt's PR #5045, the residue-ring extension PR #5089, and the ring-valued fanout PR #4916 for their restoring words and contract. The current PR #5259 gives a stronger total-price theorem for nonprincipal zero-sum triples. Its nineteen-term tariff is neither reproved nor generalized here. The new statement concerns only the minimum number of source insertions for arbitrary demand lists.

There are k>=1 independent dirty rows a_i in R^w and one disjoint preserved source p in R^w, with w>=1. R is a finite commutative unital ring, 1!=0. Require A_i=a_i+lambda_ip for all input values. All elementary row additions E_ij(c): A_i<-A_i+cA_j, i!=j, and source insertions P_i(b): A_i<-A_i+b*p are available. Words are finite and input-independent; there are no extra rows, clearing or observations. Count nonzero source insertions, with all row additions and coefficient preparation still paid separately.

Theorem. Let I=(lambda_0,...,lambda_(k-1)). Then

minimum number of source insertions =
  0, if every lambda_i is zero;
  1, if I is nonzero and principal;
  2, if I is not principal.

A one-insertion word can place its insertion at any chosen row and use at most 4(k-1) row additions. A two-insertion word works over every commutative unital ring, even an infinite one, with at most 2(k-1) row additions. The necessity direction for one insertion also works over any such ring. Finiteness is used for sufficiency of the principal-ideal condition.

Lower bound. With no insertions the source column stays zero. With one insertion P_i(beta), let C be the invertible product of all row additions after it. The final source column is lambda=C*(beta*e_i). Thus I is contained in (beta). Applying C^(-1) shows beta is a linear combination of the lambda_j, giving (beta) contained in I. Hence I=(beta), as in the two-row predecessor. No count of the number of generators of a nonprincipal ideal is a valid stronger lower bound on source insertions.

Principal-ideal construction. Suppose I=(g)!=0. Write lambda_j=u_jg, and set B=R/Ann(g). Since g lies in I, the images of the u_j generate the unit ideal of B. At each maximal ideal of B, choose coefficients a_j for j>0 as follows: if u_0 is nonzero in the residue field, set all a_j=0; otherwise choose one j with nonzero u_j and set a_j=1, with the other coefficients zero. The Chinese remainder theorem over the finitely many maximal ideals gives simultaneous a_j. Then b=u_0-sum_(j>0) a_ju_j is outside every maximal ideal of B, so it is a unit.

Lift these a_j to R and put beta=lambda_0-sum_(j>0) a_jlambda_j. Choose r_j lifting u_jb^(-1). Then

lambda_j = r_j*beta  (j>0),
lambda_0 = (1+sum_(j>0) a_j*r_j)*beta.

Let C be the chronological row word that first performs E_j0(r_j) for all j>0, then E_0j(a_j) for all j>0. It sends beta*e_0 to lambda. Execute C^(-1), P_0(beta), C in that order. The source column becomes lambda and the original dirt matrix returns to identity. There are at most 4(k-1) row additions. Relabel the rows to select another insertion site. The inverse is literal reversal with negated coefficients.

Two-insertion construction. For any demand list, first perform E_j0(-lambda_j) for j>0. Execute P_0(1), undo those row additions in reverse order, then execute P_0(lambda_0-1). Each other row changes by lambda_jp and returns its dirt; row zero ends with lambda_0p. This uses at most two nonzero insertions and 2(k-1) row additions. For a nonprincipal demand ideal, lambda_0 cannot be 1, so both insertions are nonzero and the lower bound is attained. This is the many-row form of the predecessor's repeated-insertion echo.

Unbounded distinction from ideal-generator count. For every k>=2, take

R = F_2[e_1,...,e_k] / (all products e_i*e_j),
lambda = (e_1,...,e_k).

The radical I has F_2-dimension k and needs k ideal generators: multiplication on the radical acts only by the constant coefficient. It is not principal. Yet the exact source-insertion minimum is two, independently of k. The row additions in the construction remain paid. This prevents treating ideal-generator rank as a source-call lower bound.

Verification. The code below tests ten contexts: one through three rows over Z/4, F_2 x F_2 and F_2[e,h]/(e,h)^2, plus four rows over Z/4. For all 1,008 demand lists it independently compares ideal principality with the full elementary-column orbit reached from every nonzero insertion coefficient at row zero. It checks 950 one-insertion witnesses and 48 nonprincipal cases, and replays the full original-dirt/source matrix of the constructions. Ten zero cases account for the remaining demands. It also checks the radical family for k=2,...,5.

Save as many_row_insertions.py. Both modes passed on CPython 3.12.13:

python3.12 -I -W error -B many_row_insertions.py
python3.12 -I -W error -O -B many_row_insertions.py

Expected output:

PASS_MANY_ROW_INSERTIONS contexts=10 demands=1008 single=950 nonprincipal=48 radical_families=4 no_new_kappa

from itertools import product
from collections import deque

def ck(x,s):
 if not x:raise ValueError(s)
def ring(kind,size):
 if kind=='Z':return size,1,lambda a,b:(a+b)%size,lambda a,b:a*b%size,lambda a:(-a)%size
 if kind=='B':return size,size-1,lambda a,b:a^b,lambda a,b:a&b,lambda a:a
 return size,1,lambda a,b:a^b,lambda a,b:((a&1)*(b&1))|(((a&1)*(b&~1))^((b&1)*(a&~1))),lambda a:a
def ideal(xs,R):
 size,one,add,mul,neg=R;s={0}
 for x in xs:s={add(y,mul(a,x)) for y in s for a in range(size)}
 return s
def principal(xs,R):
 target=ideal(xs,R)
 return any(ideal([b],R)==target for b in range(R[0]))
def orbit(n,R):
 size,one,add,mul,neg=R;s={(b,)+(0,)*(n-1) for b in range(1,size)};todo=deque(s)
 while todo:
  x=todo.popleft()
  for i in range(n):
   for j in range(n):
    if i==j:continue
    for a in range(1,size):
     y=list(x);y[i]=add(y[i],mul(a,y[j]));y=tuple(y)
     if y not in s:s.add(y);todo.append(y)
 return s
def one_word(xs,R):
 size,one,add,mul,neg=R;n=len(xs)
 for aa in product(range(size),repeat=n-1):
  b=xs[0]
  for a,x in zip(aa,xs[1:]):b=add(b,neg(mul(a,x)))
  rr=[next((r for r in range(size) if mul(r,b)==x),None) for x in xs[1:]]
  if any(r is None for r in rr):continue
  C=[('E',j,0,r) for j,r in enumerate(rr,1) if r]+[('E',0,j,a) for j,a in enumerate(aa,1) if a]
  return [(k,i,j,neg(a)) for k,i,j,a in reversed(C)]+[('P',0,0,b)]+C
 raise ValueError('missing principal witness')
def two_word(xs,R):
 size,one,add,mul,neg=R
 return [('E',j,0,neg(x)) for j,x in enumerate(xs[1:],1) if x]+[('P',0,0,one)]+[('E',j,0,x) for j,x in reversed(list(enumerate(xs[1:],1))) if x]+[('P',0,0,add(xs[0],neg(one)))]
def replay(xs,word,R):
 size,one,add,mul,neg=R;n=len(xs);a=[[one if i==j else 0 for j in range(n)]+[0] for i in range(n)]
 for k,i,j,b in word:
  if k=='P':a[i][-1]=add(a[i][-1],b)
  else:a[i]=[add(x,mul(b,y)) for x,y in zip(a[i],a[j])]
 ck(a==[[one if i==j else 0 for j in range(n)]+[xs[i]] for i in range(n)],'all dirty and source columns')
contexts=[(kind,size,n) for kind,size in [('Z',4),('B',4),('R',8)] for n in range(1,4)]+[('Z',4,4)]
cases=nonprincipal=single=0
for kind,size,n in contexts:
 R=ring(kind,size);reachable=orbit(n,R)
 for xs in product(range(size),repeat=n):
  iszero=not any(xs);pr=principal(xs,R)
  ck((xs in reachable)==(pr and not iszero),'principal criterion versus elementary orbit')
  if not iszero:
   replay(xs,two_word(xs,R),R)
   if pr:
    w=one_word(xs,R);replay(xs,w,R);ck(sum(k=='P' and b!=0 for k,i,j,b in w)==1,'one insertion');single+=1
   else:nonprincipal+=1
  cases+=1
for n in range(2,6):
 R=ring('R',1<<(n+1));xs=tuple(1<<(i+1) for i in range(n))
 ck(not principal(xs,R),'radical generator obstruction');replay(xs,two_word(xs,R),R)
print('PASS_MANY_ROW_INSERTIONS contexts='+str(len(contexts))+' demands='+str(cases)+' single='+str(single)+' nonprincipal='+str(nonprincipal)+' radical_families=4 no_new_kappa')

Limits and handoff. The result does not optimize row-addition counts, directed tariffs or total price after minimizing insertions. The finite-ring restriction is material: @petalas's PR #5211 gives a principal-ideal polynomial-ring obstruction in two rows. No predecessor executable, physical source producer, coefficient emitter, tape implementation, Lean, Docker or selected cold replay was run. Complete physical costs and supplier admission remain open. A useful next step is to minimize the row-addition bill within these one- or two-insertion classes for one specified larger demand and price model.

Current-main notes, targeted all-state PR search, and the Discussion/open-PR feed were checked; #5259 was read before fixing this distinct scope. The earlier proposed metric question was dropped because #5213 already resolves it. Arbitrary diffs and unpublished work are outside overlap coverage. Prepared by @aliromman with OpenAI Codex assistance. Stable reduction and CRT are classical; no external priority, independent human review or proof-kernel review is claimed. New text and code: Apache-2.0.