From d914f77d948ac377bdb9823daca93d08913c3fa7 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sun, 25 Oct 2026 18:09:45 -0500 Subject: [PATCH] Certify the exact dyadic unit-channel capacity of a helper cut --- .../dyadic-helper-channel-capacity/PROOF.md | 112 ++++++++++++++++++ .../dyadic-helper-channel-capacity/README.md | 64 ++++++++++ .../RESULT.json | 17 +++ .../SOURCES.json | 24 ++++ .../dyadic-helper-channel-capacity/TASK.json | 100 ++++++++++++++++ .../VERIFY.json | 34 ++++++ .../capacity.py | 112 ++++++++++++++++++ .../dyadic-helper-channel-capacity/verify.py | 105 ++++++++++++++++ 8 files changed, 568 insertions(+) create mode 100644 research/dyadic-helper-channel-capacity/PROOF.md create mode 100644 research/dyadic-helper-channel-capacity/README.md create mode 100644 research/dyadic-helper-channel-capacity/RESULT.json create mode 100644 research/dyadic-helper-channel-capacity/SOURCES.json create mode 100644 research/dyadic-helper-channel-capacity/TASK.json create mode 100644 research/dyadic-helper-channel-capacity/VERIFY.json create mode 100644 research/dyadic-helper-channel-capacity/capacity.py create mode 100644 research/dyadic-helper-channel-capacity/verify.py diff --git a/research/dyadic-helper-channel-capacity/PROOF.md b/research/dyadic-helper-channel-capacity/PROOF.md new file mode 100644 index 0000000000..c97a6edce3 --- /dev/null +++ b/research/dyadic-helper-channel-capacity/PROOF.md @@ -0,0 +1,112 @@ +# Exact dyadic channel capacity at one cut + +Let D=Z[1/2]. All modules and matrices below use D. The prefix and suffix +of a fixed cut are A and B, with B A=M invertible. There is no live owned +field at the cut. M is a direct sum of the identity on a helper group G and an invertible +map on its complement. All helpers +in G have one input chart S and one output chart T. Let F be one common +cut chart strictly between S and T. Embed its eligible physical fields +in the full field list. + +Let L be the rows v supported at F such that v A has support in G. +Let R be the columns u supported at F such that B u has support in G. +Choose full D-module bases L0 and R0, as rows and columns respectively. +These must be module bases, not arbitrary scaled rational-space bases. +Set K=L0 R0. Empty modules have capacity zero. + +A normalized t-channel interface is a pair of coefficient matrices X,Y +with X K Y=I_t. Its rows and columns give t dual prefix/suffix channels. +The maximum such t is exactly the number of nonzero Smith invariant +factors of K that are units in D. Equivalently, + +```text +capacity_D(K) = min_{odd primes p} rank_(F_p)(K mod p). +``` + +This is the classical Smith theorem applied to the helper-cut pairing. +It does not claim Smith normal form or the field-pairing method as new. + +## Proof of the optimum + +Clear denominators with a power of two d. Integer row and column operations +give U(d K)V=diag(s_1,...,s_r,0), with U,V unimodular, positive s_i and +s_i dividing s_(i+1). Clearing d does not change any unit status in D. +Let t count the initial powers of two among the s_i. Scaling the first t +rows of U by d/s_i and taking the first t columns of V gives X K Y=I_t. +This constructs the full unit block, not only a numerical upper bound. + +If tp[j] for i in range(n) for j in range(i+1,n))* + prod(a[i][p[i]] for i in range(n)) for p in permutations(range(n))) + + +def check(a, c=None): + c=capacity(a) if c is None else c + m,n=len(a),len(a[0]) + need(abs(det(c['U']))==abs(det(c['V']))==1,'Unimodular certificate') + scaled=[[int(c['denominator']*Q(x)) for x in row] for row in a] + need(product(product(c['U'],scaled),c['V'])==c['S'],'Smith identity') + need(all(c['S'][i][j]==0 for i in range(m) for j in range(n) if i!=j), + 'Diagonal certificate') + factors=c['factors'] + need(all(x>0 for x in factors) and all(y%x==0 for x,y in zip(factors,factors[1:])), + 'Positive divisibility chain') + g=1 + for k in range(1,min(m,n)+1): + divisor=0 + for rows in combinations(range(m),k): + for cols in combinations(range(n),k): + divisor=gcd(divisor,det([[scaled[i][j] for j in cols] for i in rows])) + g=g*factors[k-1] if k<=len(factors) else 0 + need(divisor==g,'Independent gcd of every minor') + t=c['capacity'] + if t: + need(product(product(c['left'],a),c['right'])==eye(t),'Constructive unit block') + need(all(x & (x-1)==0 for x in factors[:t]),'Dyadic unit block') + need(t==len(factors) or factors[t] & (factors[t]-1),'Nonunit obstruction') + return c + + +def main(): + pins=json.loads((HERE/'SOURCES.json').read_text())['files'] + for pin in pins: + if pin['usage']=='input': + need(hashlib.sha256((ROOT/pin['path']).read_bytes()).hexdigest()==pin['sha256'], + 'Pinned caller proof') + exhaustive=0 + for entries in tuples(range(-3,4),repeat=4): + check([list(entries[:2]),list(entries[2:])]) + exhaustive+=1 + rng=Random(5611) + wider=0 + for m in range(1,6): + for n in range(1,6): + for _ in range(3): + a=[[Q(rng.randint(-10,10),2**rng.randrange(4)) for _ in range(n)] for _ in range(m)] + check(a) + wider+=1 + # Four elementary ADDs give a unimodular causal prefix. + a=[[1,0,1],[0,1,2],[1,2,6]] + b=[[2,2,-1],[2,5,-2],[-1,-2,1]] + need(product(a,b)==eye(3) and product(b,a)==eye(3),'Exact complete identity word') + left=kernel([[a[0][2],a[1][2]]],2) + right=kernel([[b[2][0],b[2][1]]],2) + pairing=product([list(row) for row in zip(*left)],right) + causal=check(pairing) + need(causal['rational_rank']==1 and causal['capacity']==0 and causal['factors']==[5], + 'Rational cut rank overcounts dyadic channels') + joint=check([[3,0],[0,5]]) + need(joint['capacity']==1 and joint['factors']==[1,15],'Joint pairing exceeds entry test') + lifted=check([[Q(5,8)]]) + need(lifted['capacity']==0,'A power of two does not remove the odd obstruction') + need(check([[8,0],[0,0]])['capacity']==1,'Rank-deficient positive control') + controls=0 + for bad in [[[Q(1,3)]],[[1,2],[3]]]: + try:capacity(bad) + except ValueError:controls+=1 + else:raise ValueError('Invalid matrix accepted') + for field in ['capacity','factors','U']: + bad=capacity([[3,0],[0,5]]) + if field=='capacity':bad[field]=2 + elif field=='factors':bad[field]=[1,1] + else:bad[field][0][0]+=1 + try:check([[3,0],[0,5]],bad) + except ValueError:controls+=1 + else:raise ValueError('False capacity certificate accepted') + result=dict(exhaustive_2_by_2=exhaustive,rectangular_dyadic=wider, + causal_pairing=pairing,causal_rational_rank=1,causal_capacity=0, + joint_factors=joint['factors'],joint_capacity=1,rejected_inputs=controls) + need(result==json.loads((HERE/'RESULT.json').read_text()),'Committed receipt') + print(json.dumps(result,sort_keys=True)) + print('PASS_DYADIC_HELPER_CHANNEL_CAPACITY') + + +if __name__=='__main__':main()