"""Exact finite checks of review inferences; not a proof about LLM auditors."""
from fractions import Fraction as F
from pathlib import Path
import json
def matmul(a,b):return [[sum(x*y for x,y in zip(row,col)) for col in zip(*b)] for row in a]
def mean(a):return [sum(col)/len(a) for col in zip(*a)]
def run(w,beta,gamma,t,q):
 n=len(w);a=[1-b for b in beta]+[gamma]
 assert all(x>0 for row in w for x in row) and all(sum(row)==1 for row in w)
 assert all(0<b<1 for b in beta) and 0<gamma<1
 assert all(x>=0 for row in t for x in row) and all(sum(row)==1 for row in t)
 assert all(x>0 for x in q) and sum(q)==1
 j=[[a[i]*x for x in w[i]]+[beta[i]] for i in range(n)]+[[gamma*x for x in q]+[1-gamma]]
 mixed=matmul(t,j);u=[[x/sum(row[:n]) for x in row[:n]] for row in mixed[:n]]
 d=[sum(t[i][r]*a[r] for r in range(n+1)) for i in range(n)]
 theta=[a[r]/n*sum(t[i][r]/d[i] for i in range(n)) for r in range(n+1)]
 observed=mean(u);pred=[sum(theta[r]*w[r][k] for r in range(n))+theta[-1]*q[k] for k in range(n)]
 assert observed==pred and sum(theta)==1
 qstar=None if theta[-1]==0 else [(mean(w)[k]-sum(theta[r]*w[r][k] for r in range(n)))/theta[-1] for k in range(n)]
 error=[observed[k]-mean(w)[k] for k in range(n)]
 if qstar is not None:assert error==[theta[-1]*(q[k]-qstar[k]) for k in range(n)]
 return {'theta':theta,'qstar':qstar,'incumbent_mean':mean(w),'returned_mean':observed,'error':error}
def strings(x):
 if isinstance(x,F):return str(x)
 if isinstance(x,dict):return {k:strings(v) for k,v in x.items()}
 if isinstance(x,list):return [strings(v) for v in x]
 return x
w=[[F(9,10),F(1,10)],[F(1,5),F(4,5)]]
identity=[[F(i==j) for j in range(3)] for i in range(3)]
zero=run(w,[F(1,2)]*2,F(1,2),identity,[F(3,4),F(1,4)])
assert zero['theta'][-1]==0 and zero['error']==[0,0]
uniform=[[F(1,3)]*3 for _ in range(3)]
unequal=run(w,[F(2,5),F(1,5)],F(3,5),uniform,[F(2,3),F(1,3)])
assert unequal['qstar']!=unequal['incumbent_mean'] and unequal['error']==[0,0]
p=[[F(0) if i==j else F(1,2) for j in range(3)] for i in range(3)]
t=identity;stays=[]
for ell in range(1,4):
 t=matmul(t,p);result=run(w,[F(1,2)]*2,F(1,2),t,[F(3,4),F(1,4)])
 stays.append({'stay':ell,**result})
assert stays[0]['theta'][-1]==F(1,2) and stays[1]['theta'][-1]==F(1,4) and stays[2]['theta'][-1]==F(3,8)
assert max(map(abs,stays[1]['error']))<max(map(abs,stays[0]['error']))
unrestorable=run([[F(9,10),F(1,10)],[F(1,10),F(9,10)]],[F(1,2)]*2,F(1,2),[[F(9,10),0,F(1,10)]]*3,[F(1,2)]*2)
assert any(x<=0 for x in unrestorable['qstar'])
output={'status':'PASS_EXACT_FINITE_CHECKS','scope':'Theorem4.1 prescribed stochastic insertion/mixing/deletion maps only. No LLM, human, ethical or causal-benefit inference.','cases':{
 'zero_influence':{'result':zero,'conclusion':'Dissent need not move the endpoint when newcomer influence is zero; the positive-theta condition matters.'},
 'connected_unequal_masses':{'result':unequal,'conclusion':'Even fully connected doubly stochastic mixing need not give q*=incumbent mean under unequal insertion masses.'},
 'stay_not_monotone':{'results':stays,'conclusion':'With a fixed symmetric mixing matrix, endpoint error need not increase with stay length.'},
 'inadmissible_restorer':{'result':unrestorable,'conclusion':'Required q* may lie outside the strictly positive simplex; restoration is not guaranteed.'}},
 'not_proved':['The general theorem by finite examples','Auditor influence equals capture with opposite sign','Founder influence or tenure ordering','Succession is mathematically endpoint restoration']}
Path(__file__).with_name('EXACT_MEMBERSHIP_CHECKS.json').write_text(json.dumps(strings(output),indent=2)+'\n',encoding='utf-8')
print('PASS:4 scenario families, exact rational formula checks; no empirical extrapolation.')