diff --git a/research/nonnested-capacity-rank-count/.gitattributes b/research/nonnested-capacity-rank-count/.gitattributes new file mode 100644 index 0000000000..8abeb4295b --- /dev/null +++ b/research/nonnested-capacity-rank-count/.gitattributes @@ -0,0 +1 @@ +inputs/** -text diff --git a/research/nonnested-capacity-rank-count/ORIGIN.json b/research/nonnested-capacity-rank-count/ORIGIN.json new file mode 100644 index 0000000000..4768631e16 --- /dev/null +++ b/research/nonnested-capacity-rank-count/ORIGIN.json @@ -0,0 +1,7 @@ +{ + "local": "inputs/nested_source.md", + "path": "research/nested-late-capacity-completion/PROOF.md", + "commit": "fdb7b8808ce89cd1738ea49dcd65c19ae1dddedd", + "git_blob": "5416883d22271b525674ed8e4458acff4139117a", + "sha256": "35534ff37cbc97ae182baf5972a7a9d1ddb79a5dab38bea4ddf88b7e15ebc6ad" +} diff --git a/research/nonnested-capacity-rank-count/PROOF.md b/research/nonnested-capacity-rank-count/PROOF.md new file mode 100644 index 0000000000..b3da9344b7 --- /dev/null +++ b/research/nonnested-capacity-rank-count/PROOF.md @@ -0,0 +1,193 @@ +# Exact joint completion with arbitrary target capacities + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +Nick Petalas's PR6489 gives the exact nested-target criterion and count. +This package handles arbitrary simultaneous target subspaces over a finite +field. It is an exponential reference method, not a replacement for that +fast nested criterion. Kernel-subspace inversion, Gaussian coefficients +and projective cross-ratio obstructions are classical. The contribution +is their exact application to this repository's shared-map contract, with +full rank counts, constructive witnesses and joint rejection controls. + +## Contract and linear equations + +Let V and W have dimension n over F_q. Specify any finite list of fixed +images g(u)=v and any finite list of inclusions g(A_i)<=C_i. The spaces +A_i and C_i may overlap or repeat, and the C_i need not be nested. +A fixed partial injection is one permitted list of fixed images. More +general or inconsistent fixed lists are allowed; an inconsistent list +has count zero. No generic-position hypothesis is used. + +Choose bases of V,W and write g as an n-by-n matrix X. A fixed image +supplies n scalar affine equations. For every basis vector a of A_i and +every basis vector lambda of the annihilator C_i^perp, add + + lambda X a = 0. + +Nondegeneracy of the coordinate dual pairing shows these equations are +necessary and sufficient for the full inclusion. Dependent input lists +are harmless. Let L be the resulting affine solution set of matrices. +This construction preserves all joint dependencies; it does not replace +them with separate dimension inequalities. + +## Count by exact rank + +For every subspace K of V, let F(K) be the number of matrices in L that +vanish on K. Add Xk=0 for a basis of K to the affine system. If the +augmented system is inconsistent, F(K)=0. Otherwise + + F(K)=q^(n^2-rho_K), + +where rho_K is its coefficient rank. For 0<=j<=n put + + A_j=sum_(dim K=j) F(K). + +Let N_t count matrices in L with kernel dimension t. Double-count pairs +(X,K), where X is in L and K is a j-subspace of ker X. This gives + + A_j=sum_(t=j..n) [t choose j]_q N_t. (1) + +The Gaussian coefficient is the number of j-subspaces of F_q^t. It is +obtained by dividing the number of independent ordered j-tuples by the +number of ordered bases of a j-space. In particular [j choose j]_q=1. +Thus the following descending recurrence gives every exact count: + + N_j=A_j-sum_(t=j+1..n) [t choose j]_q N_t. (2) + +The number of rank-r completions is N_(n-r). Invertible completion exists +if and only if N_0>0. If N_0=0 but L is not empty, the largest r with +N_(n-r)>0 is the exact maximum feasible rank. This measures an algebraic +rank deficit, not the physical cost of a repair. + +The familiar equivalent formula for the invertible count is + + N_0=sum_(K<=V) (-1)^dim K q^(dim K (dim K-1)/2) F(K). + +It is the classical subspace-lattice Mobius formula. The executable uses +(2), which also provides the entire rank histogram. The double-counting +argument above proves the formula used here without an external theorem. +For historical background, see Richard Stanley's author-hosted +[Enumerative Combinatorics, volume 1](https://math.mit.edu/~rstan/ec/ec1.pdf), +which treats the subspace lattice and its Mobius function. No novelty is +claimed for this inversion machinery. + +## Compress the fixed partial injection + +Suppose the fixed images specify an injection on an independent basis of +a u-dimensional U. Extend this basis and its image to ambient bases P,Q. +In these coordinates every extension has the form + + X = Q [ I_u A ] P^-1. + [ 0 B ] + +Here m=n-u, A is u-by-m, and B is m-by-m. Thus rank X=u+rank B. +There are n*m free scalar entries, not n^2. Substitute this exact affine +form into every capacity equation. For a source with P-coordinates x +and a covector with Q-coordinates y, the resulting equation is + + sum_(i,j) y_i x_(u+j) Y_ij = -sum_(i n: + return 0 + if j in (0,n): + return 1 + return gaussian(n-1,j-1,p)+p**j*gaussian(n-1,j,p) + + +def validate(n, p, equations): + require(type(n) is int and 0 <= n <= 4, 'dimension outside bounded API') + require(type(p) is int and p in (2,3,5), 'unsupported prime field') + require(type(equations) is tuple and all(type(row) is tuple and len(row) == n*n+1 + and all(type(x) is int and 0 <= x < p for x in row) for row in equations), + 'invalid affine equations') + + +def block_counts(rows, m, p, equations): + """Count the rank of the last m rows of a rows-by-m affine matrix.""" + width = rows*m + base = reduce_system(width,equations,p) + if base is None: + return {'rank_counts':[0]*(m+1),'kernel_incidence':[0]*(m+1)} + base = base[0] + incidence = [0]*(m+1) + for space in subspaces(m,p): + extra = [] + for vector in space: + for i in range(rows-m,rows): + row = [0]*(width+1) + row[i*m:(i+1)*m] = vector + extra.append(tuple(row)) + reduced = reduce_system(width,base+tuple(extra),p) + if reduced is not None: + incidence[len(space)] += p**(width-len(reduced[0])) + nullities = [0]*(m+1) + for j in range(m,-1,-1): + nullities[j] = incidence[j]-sum(gaussian(t,j,p)*nullities[t] for t in range(j+1,m+1)) + require(nullities[j] >= 0, 'negative rank count') + require(sum(nullities) == p**(width-len(base)), 'rank partition fails') + return {'rank_counts':list(reversed(nullities)), 'kernel_incidence':incidence} + + +def rank_counts(n, p, equations): + validate(n,p,equations) + return block_counts(n,n,p,equations) + + +def annihilator(n, vectors, p): + rows, pivots = reduce_system(n,[tuple(v)+(0,) for v in vectors],p) + free = [j for j in range(n) if j not in pivots] + basis = [] + for j in free: + v = [0]*n + v[j] = 1 + for row, pivot in zip(rows,pivots): + v[pivot] = -row[j] % p + basis.append(tuple(v)) + return tuple(basis) + + +def capacity_equations(n,p,fixed=(),capacities=()): + validate(n,p,()) + def vector(v): + require(type(v) is tuple and len(v) == n and all(type(x) is int and 0 <= x < p for x in v), + 'invalid vector') + require(type(fixed) is tuple and type(capacities) is tuple,'immutable contract required') + equations = [] + for pair in fixed: + require(type(pair) is tuple and len(pair) == 2,'invalid fixed pair') + source, target = pair + vector(source); vector(target) + for i in range(n): + row = [0]*(n*n)+[target[i]] + row[i*n:(i+1)*n] = source + equations.append(tuple(row)) + for pair in capacities: + require(type(pair) is tuple and len(pair) == 2,'invalid capacity pair') + sources, targets = pair + require(type(sources) is tuple and type(targets) is tuple,'immutable subspaces required') + for v in sources+targets: + vector(v) + for a in sources: + for b in annihilator(n,targets,p): + equations.append(tuple(b[i]*a[j] % p for i in range(n) for j in range(n))+(0,)) + return tuple(equations) + + +def construct_block(rows,m,p,equations,target_rank=None): + counts = block_counts(rows,m,p,equations)['rank_counts'] + if target_rank is not None: + require(type(target_rank) is int and 0 <= target_rank <= m,'invalid target rank') + if not any(counts): + return None + if target_rank is None: + target_rank = max(i for i,c in enumerate(counts) if c) + if counts[target_rank] == 0: + return None + current = equations + entries = [] + for j in range(rows*m): + for value in range(p): + row = tuple(int(i == j) for i in range(rows*m))+(value,) + candidate = current+(row,) + if block_counts(rows,m,p,candidate)['rank_counts'][target_rank]: + current = candidate + entries.append(value) + break + else: + raise ValueError('positive fiber has no next entry') + matrix = tuple(tuple(entries[i*m:(i+1)*m]) for i in range(rows)) + require(rank(matrix[rows-m:],p,m) == target_rank,'constructor rank mismatch') + require(all((sum(x*y for x,y in zip(row[:-1],entries))-row[-1]) % p == 0 + for row in equations),'constructor violates affine equations') + return matrix + + +def construct(n,p,equations,target_rank=None): + validate(n,p,equations) + return construct_block(n,n,p,equations,target_rank) + + +def apply(matrix,vector,p): + return tuple(sum(x*y for x,y in zip(row,vector)) % p for row in matrix) + + +def inverse(matrix,p): + n=len(matrix) + columns=[] + for j in range(n): + result=reduce_system(n,[tuple(row)+(int(i==j),) for i,row in enumerate(matrix)],p) + require(result is not None and len(result[0])==n,'singular chart') + columns.append(tuple(row[-1] for row in result[0])) + return tuple(tuple(columns[j][i] for j in range(n)) for i in range(n)) + + +def prepare_fixed(n,p,fixed,capacities): + require(type(n) is int and 0 <= n <= 12,'ambient dimension outside bounded API') + require(type(p) is int and p in (2,3,5),'unsupported prime field') + require(type(fixed) is tuple and type(capacities) is tuple,'immutable contract required') + def vector(v): + require(type(v) is tuple and len(v)==n and all(type(x) is int and 0 <= x < p for x in v),'invalid vector') + for pair in fixed: + require(type(pair) is tuple and len(pair)==2,'invalid fixed pair') + vector(pair[0]);vector(pair[1]) + source=tuple(pair[0] for pair in fixed);target=tuple(pair[1] for pair in fixed) + u=len(fixed);m=n-u + require(rank(source,p,n)==u and rank(target,p,n)==u,'fixed data must be an injection on a basis') + require(0 <= m <= 4,'unfixed dimension exceeds four') + def extend(basis): + basis=list(basis) + for j in range(n): + e=tuple(int(i==j) for i in range(n)) + if rank(basis+[e],p,n)>len(basis):basis.append(e) + return tuple(tuple(basis[j][i] for j in range(n)) for i in range(n)) + P,Q=extend(source),extend(target);Pi=inverse(P,p) + equations=[] + for pair in capacities: + require(type(pair) is tuple and len(pair)==2,'invalid capacity pair') + A,B=pair + require(type(A) is tuple and type(B) is tuple,'immutable subspaces required') + for v in A+B:vector(v) + for a in A: + x=apply(Pi,a,p) + for b in annihilator(n,B,p): + y=tuple(sum(b[i]*Q[i][j] for i in range(n))%p for j in range(n)) + rhs=-sum(y[i]*x[i] for i in range(u))%p + equations.append(tuple(y[i]*x[u+j]%p for i in range(n) for j in range(m))+(rhs,)) + return u,m,Q,Pi,tuple(equations) + + +def fixed_rank_counts(n,p,fixed,capacities=()): + u,m,_,_,eq=prepare_fixed(n,p,fixed,capacities) + result=block_counts(n,m,p,eq) + return {'rank_counts':[0]*u+result['rank_counts'], 'fixed_dimension':u, + 'quotient_dimension':m, 'kernel_incidence':result['kernel_incidence']} + + +def fixed_construct(n,p,fixed,capacities=(),target_rank=None): + u,m,Q,Pi,eq=prepare_fixed(n,p,fixed,capacities) + if target_rank is not None: + require(type(target_rank) is int and 0 <= target_rank <= n,'invalid target rank') + if target_rank W has image U'. For i=1,...,k, let A_i be +arbitrary subspaces of V and let C_1 <= ... <= C_k be subspaces of W. +The requested map is an isomorphism g:V -> W extending h and satisfying +g(A_i) <= C_i for every i. Inclusions may be equal, sources may overlap, +and zero spaces, k=0 and n=0 are allowed. + +Put + +``` +S_i = A_1 + ... + A_i, +u = dim U, e_0 = 0, +e_i = dim(U+S_i) - u, +c_i = dim C_i, b_i = dim(C_i intersect U'). +``` + +Such a g exists if and only if, for every i, + +``` +h(U intersect S_i) <= C_i, (compatibility) +e_i <= c_i - b_i. (quotient capacity) +``` + +Over F_q, if these conditions hold, the exact number of requested maps is + +``` +product_(i=1..k) [q^(b_i (e_i-e_(i-1))) + product_(j=e_(i-1)..e_i-1) (q^(c_i-b_i)-q^j)] + * product_(j=u+e_k..n-1) (q^n-q^j). +``` + +For k=0, read e_k=0. Empty products equal one. If any condition fails, +the count is zero. The count covers distinct linear maps, without quotienting +by basis choices or charging any physical realization cost. + +## Reduction to cumulative sources + +If g(A_j) <= C_j for j<=i, nesting gives g(A_j) <= C_i, hence +g(S_i) <= C_i. Conversely A_i <= S_i, so the cumulative inclusions imply +the original ones. This equivalence permits arbitrary source intersections; +it requires nesting only on the target side. + +If g exists, its restriction to U intersect S_i is h and has image in C_i. +The induced injection from (U+S_i)/U into W/U' sends the e_i-dimensional +source into (C_i+U')/U', whose dimension is c_i-b_i. This proves necessity. + +## Compatible basis extension + +Choose a basis of U. Extend it successively to bases of U+S_i by choosing +e_i-e_(i-1) new vectors in S_i. Such choices are possible because the +cumulative sources form a flag. This ordered domain basis is fixed for +the remainder of the proof and counting argument. + +Suppose an injective extension has already been defined on U+S_(i-1), +and maps S_(i-1) into C_(i-1). Since S_(i-1) <= S_i, + +``` +(U+S_(i-1)) intersect S_i = (U intersect S_i) + S_(i-1). +``` + +The already prescribed image of this intersection lies in C_i, by +compatibility and nesting. Thus extending by any images in C_i for the +new independent domain vectors preserves the entire inclusion g(S_i)<=C_i. + +Work modulo U'. Images of the previous new basis vectors span an +e_(i-1)-dimensional subspace of (C_i+U')/U'. The latter space has dimension +c_i-b_i >= e_i. Extend these independent images to e_i independent vectors +in this quotient, and lift each new vector to C_i. The resulting map on +U+S_i is injective. This induction works over every field. Finally extend +the domain and image bases to bases of V and W. It yields the required g. + +The bounded reference implements this same constructive choice without +enumerating a field: an available member of a basis of C_i must lie outside +the current image span whenever another independent image is needed. + +## Counting every completion + +Over F_q, fix the domain basis chosen above. At stage i, after a total of +j new basis vectors have been assigned, where e_(i-1)<=j, h(x+y)=z, +A_1=, C_1=, +A_2=, C_2=. +``` + +The individual one-capacity contracts admit 4 and 12 isomorphisms, +respectively. The first sends x to x, then y to x+z, and has four choices +for the image of z outside their plane. The second has three nonzero +choices in C_2 for the image of y, then fixes the image of x through h, +and has four choices for the image of z. Yet no shared map exists: +U <= S_2 and h(U)= is not contained in C_2. This is a new joint-contract +example, rather than a re-evaluation of PR5020's one-capacity examples. + +The quotient condition also detects a different missed obstruction. Take +U=0, A_1=, A_2=, and C_1=C_2=. Both individual contracts are +feasible but S_2 has dimension two against a one-dimensional capacity. +The exact reference and the separate literal GL census check both examples. + +## Scope and attribution + +Brian / JoyboyBrian's PR5020 supplies the one-capacity prescribed-map +contract and asks for a second late capacity. The theorem above settles +its nested-target case, and includes any finite number of nested targets. +The proof is self-contained and does not invoke or recheck PR5020's theorem. +Basis extension, quotient dimensions and finite-field independent-vector +counts are classical; no general literature-priority claim is made. + +The unrestricted GL contract does not supply a symplectic native map, +an absolute phase, chronological contact realization, a changed emitted +word or a favorable complete paid/productive invoice. No helper credit, +physical saving, new kappa, selected-frontier change or complete +multiplication theorem follows. Nonnested targets require a different +compatibility argument; applying this theorem to a nonnested list is invalid. diff --git a/research/nonnested-capacity-rank-count/verify.py b/research/nonnested-capacity-rank-count/verify.py new file mode 100644 index 0000000000..e16b6b7c32 --- /dev/null +++ b/research/nonnested-capacity-rank-count/verify.py @@ -0,0 +1,256 @@ +"""Compare joint rank counts with literal finite maps and vector sets. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from pathlib import Path +from itertools import product, combinations +from collections import Counter +from math import comb +import hashlib +import json +import random +import runpy +import shutil +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent +C = runpy.run_path(str(ROOT/'completion.py')) +check = C['require'] + + +def span(basis,n,p): + vectors = {(0,)*n} + for b in basis: + vectors = {tuple((x+c*y)%p for x,y in zip(a,b)) for a in vectors for c in range(p)} + return frozenset(vectors) + + +def apply(matrix,vector,p): + return tuple(sum(x*y for x,y in zip(row,vector))%p for row in matrix) + + +def matrix_rank(matrix,n,p): + images = {apply(matrix,x,p) for x in product(range(p),repeat=n)} + size,r = len(images),0 + while size>1: + check(size%p == 0,'image size is not a field power') + size//=p;r+=1 + return r + + +def all_maps(n,p): + return [(tuple(tuple(values[i*n:(i+1)*n]) for i in range(n)), + matrix_rank(tuple(tuple(values[i*n:(i+1)*n]) for i in range(n)),n,p)) + for values in product(range(p),repeat=n*n)] + + +def literal_histogram(n,p,fixed,capacities,maps): + targets = [span(b,n,p) for _,b in capacities] + result = [0]*(n+1) + for matrix,r in maps: + if not all(apply(matrix,a,p)==b for a,b in fixed): + continue + if all(all(apply(matrix,a,p) in target for a in source) + for (source,_),target in zip(capacities,targets)): + result[r]+=1 + return result + + +def inspect(n,p,fixed,capacities,maps,counts,witness=False): + eq = C['capacity_equations'](n,p,fixed,capacities) + actual = C['rank_counts'](n,p,eq)['rank_counts'] + expected = literal_histogram(n,p,fixed,capacities,maps) + check(actual==expected,'literal contract rank counts differ') + counts['literal_contracts']+=1 + if witness: + valid_injection=C['rank'](tuple(a for a,_ in fixed),p,n)==len(fixed) and C['rank'](tuple(b for _,b in fixed),p,n)==len(fixed) + if valid_injection: + compressed=C['fixed_rank_counts'](n,p,fixed,capacities)['rank_counts'] + check(compressed==actual,'compressed count differs') + counts['compressed_literal_comparisons']+=1 + for r in range(n+1): + if valid_injection: + other=C['fixed_construct'](n,p,fixed,capacities,r) + check((other is not None)==(actual[r]>0),'compressed witness existence') + if other is not None: + check(matrix_rank(other,n,p)==r and all(apply(other,a,p)==b for a,b in fixed),'compressed witness rank/fixed image') + check(all(all(apply(other,a,p) in span(b,n,p) for a in source) for source,b in capacities),'compressed witness original inclusion') + counts['compressed_rank_witnesses']+=1 + matrix = C['construct'](n,p,eq,r) + check((matrix is not None)==(actual[r]>0),'witness existence differs') + if matrix is not None: + check(matrix_rank(matrix,n,p)==r,'independent witness rank') + check(all(apply(matrix,a,p)==b for a,b in fixed),'fixed image fails') + check(all(all(apply(matrix,a,p) in span(b,n,p) for a in source) + for source,b in capacities),'witness capacity fails') + counts['rank_witnesses']+=1 + return actual + + +def subspace_oracle(n,p): + zero=frozenset({(0,)*n}) + spaces={zero} + for v in product(range(p),repeat=n): + for space in tuple(spaces): + spaces.add(frozenset(tuple((x+c*y)%p for x,y in zip(a,v)) for a in space for c in range(p))) + return spaces + + +def run(): + counts=Counter() + origin=json.loads((ROOT/'ORIGIN.json').read_text());data=(ROOT/origin['local']).read_bytes() + check(hashlib.sha256(data).hexdigest()==origin['sha256'],'source pin') + check(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest()==origin['git_blob'],'source Git blob') + with tempfile.TemporaryDirectory() as tmp: + dest=Path(tmp);(dest/'inputs').mkdir() + for name in ('completion.py','verify.py','ORIGIN.json'): + shutil.copyfile(ROOT/name,dest/name) + (dest/origin['local']).write_bytes(data+b'\n') + try: + runpy.run_path(str(dest/'verify.py'))['run']() + except ValueError as error: + check(str(error)=='source pin','wrong source rejection');counts['source_corruptions']+=1 + else: + raise ValueError('source mutation accepted') + domains=((0,2),(1,2),(2,2),(3,2),(2,3),(2,5)) + for n,p in domains: + exact=subspace_oracle(n,p) + generated=C['subspaces'](n,p) + check(len(generated)==len(exact) and {span(b,n,p) for b in generated}==exact,'RREF space census differs') + counts['subspace_oracle_cases']+=len(exact) + spaces=C['subspaces'](2,2);maps=all_maps(2,2) + nonzero=[v for v in product(range(2),repeat=2) if any(v)] + fixed_cases=[()]+[((a,b),) for a in nonzero for b in nonzero] + for i,(a,b,c,d,fixed) in enumerate(product(spaces,spaces,spaces,spaces,fixed_cases)): + inspect(2,2,fixed,((a,b),(c,d)),maps,counts,witness=i%97==0) + check(counts['literal_contracts']==6250,'incomplete binary joint census') + rng=random.Random(20261103) + for n,p in ((3,2),(2,3),(2,5)): + spaces=C['subspaces'](n,p);maps=all_maps(n,p);vectors=list(product(range(p),repeat=n)) + for i in range(128): + fixed=tuple((rng.choice(vectors),rng.choice(vectors)) for _ in range(rng.randrange(3))) + capacities=tuple((rng.choice(spaces),rng.choice(spaces)) for _ in range(rng.randrange(6))) + inspect(n,p,fixed,capacities,maps,counts,witness=i%17==0) + for _ in range(24): + equations=tuple(tuple(rng.randrange(p) for _ in range(n*n+1)) for _ in range(rng.randrange(n*n+2))) + expected=[0]*(n+1) + for matrix,r in maps: + flat=tuple(x for row in matrix for x in row) + if all(sum(x*y for x,y in zip(row[:-1],flat))%p==row[-1] for row in equations): + expected[r]+=1 + check(C['rank_counts'](n,p,equations)['rank_counts']==expected,'arbitrary affine rank histogram') + counts['arbitrary_affine_systems']+=1 + cross=[] + sources=((1,0),(0,1),(1,1),(1,2));targets=((1,0),(0,1),(1,1),(1,3)) + maps=all_maps(2,5) + expected=((1,144,480),(1,44,80),(1,8,16),(1,0,4),(1,0,0)) + for length in range(5): + for subset in combinations(range(4),length): + capacities=tuple(((sources[i],),(targets[i],)) for i in subset) + actual=inspect(2,5,(),capacities,maps,counts,witness=True) + check(actual==list(expected[length]),'cross-ratio count') + if subset: + source_sets=[span((sources[i],),2,5) for i in subset] + target_sets=[span((targets[i],),2,5) for i in subset] + check(len(span(tuple(sources[i] for i in subset),2,5))==len(span(tuple(targets[i] for i in subset),2,5)),'subset sum dimensions') + check(len(set.intersection(*map(set,source_sets)))==len(set.intersection(*map(set,target_sets))),'subset intersection dimensions') + eq=C['capacity_equations'](2,5,capacities=capacities) + witness=C['construct'](2,5,eq) + cross.append(dict(subset=list(subset),rank_counts=actual, + maximum_rank_witness=None if witness is None else [list(row) for row in witness])) + # Retained nested source: separate counts 4 and 12, joint count zero. + n,p=3,2;maps=all_maps(n,p);fixed=(((1,1,0),(0,0,1)),) + one=(((1,0,0),),((1,0,0),));two=(((0,1,0),),((1,0,0),(0,1,0))) + nested=[inspect(n,p,fixed,c,maps,counts,witness=True)[n] for c in ((one,),(two,),(one,two))] + check(nested==[4,12,0],'retained nested compatibility example') + formulas=[] + for p in (2,3,5): + n=4;unit=tuple(tuple(int(i==j) for i in range(n)) for j in range(n)) + free=C['rank_counts'](n,p,())['rank_counts'] + expected_free=[] + for r in range(n+1): + numerator=denominator=1 + for i in range(r): + numerator*=(p**n-p**i)**2 + denominator*=p**r-p**i + expected_free.append(numerator//denominator) + check(free==expected_free and sum(free)==p**(n*n),'free matrix rank formula') + diagonal=tuple(((v,),(v,)) for v in unit) + eq=C['capacity_equations'](n,p,capacities=diagonal) + actual=C['rank_counts'](n,p,eq)['rank_counts'] + check(actual==[comb(n,r)*(p-1)**r for r in range(n+1)],'diagonal rank formula') + block=((unit[:2],unit[:2]),(unit[2:],unit[2:])) + eq=C['capacity_equations'](n,p,capacities=block) + actual_block=C['rank_counts'](n,p,eq)['rank_counts'] + h=[1,(p*p-1)**2//(p-1),(p*p-1)*(p*p-p)] + convolution=[sum(h[i]*h[j] for i in range(3) for j in range(3) if i+j==r) for r in range(5)] + check(actual_block==convolution,'independent block rank formula') + formulas.append(dict(field=p,free=free,diagonal=actual,block=actual_block)) + counts['dimension_four_formulas']+=3 + for target in (unit,unit[:3]): + eq=C['capacity_equations'](4,5,capacities=((unit,target),)) + matrix=C['construct'](4,5,eq) + check(matrix_rank(matrix,4,5)==len(target),'dimension-four maximum rank') + check(all(apply(matrix,v,5) in span(target,4,5) for v in unit),'dimension-four inclusion') + counts['dimension_four_witnesses']+=1 + compressed_records=[] + for n in (9,12): + p=2;u=n-2 + unit=tuple(tuple(int(i==j) for i in range(n)) for j in range(n)) + # Use different nontrivial ambient domain and target charts. + sources=list(unit);targets=list(unit) + for j in range(n-1): + sources[j]=tuple(x^y for x,y in zip(sources[j],sources[j+1])) + targets[j+1]=tuple(x^y for x,y in zip(targets[j+1],targets[j])) + fixed=tuple(zip(sources[:u],targets[:u])) + hist=C['fixed_rank_counts'](n,p,fixed)['rank_counts'] + check(hist==[0]*u+[2**(2*u)*x for x in (1,9,6)],'compressed free rank formula') + mixed_a=tuple(x^y for x,y in zip(sources[0],sources[-1])) + mixed_b=tuple(x^y for x,y in zip(targets[0],targets[-1])) + capacities=(((sources[-2],),(targets[-2],)),((mixed_a,),(mixed_b,))) + constrained=C['fixed_rank_counts'](n,p,fixed,capacities)['rank_counts'] + literal=[0]*(n+1) + for a,b in product(range(2),repeat=2): + images=targets[:u]+[tuple(a*x for x in targets[-2]), + tuple((b*x+(b-1)*y)%2 for x,y in zip(targets[-1],targets[0]))] + dimension=len(span(tuple(images),n,p)).bit_length()-1 + literal[dimension]+=1 + counts['large_literal_basis_maps']+=1 + check(constrained==literal==[0]*u+[1,2,1],'coupled compressed rank formula') + for r in (u,u+1,n): + matrix=C['fixed_construct'](n,p,fixed,capacities,r) + check(matrix_rank(matrix,n,p)==r,'large independent witness rank') + check(all(apply(matrix,a,p)==b for a,b in fixed),'large fixed image') + check(all(all(apply(matrix,a,p) in span(b,n,p) for a in source) for source,b in capacities),'large joint capacity') + counts['large_compressed_witnesses']+=1 + compressed_records.append(dict(ambient=n,quotient=2,full_lattice_subspaces=sum(C['gaussian'](n,j,p) for j in range(n+1)),used_subspaces=5,free_histogram=hist,coupled_histogram=constrained)) + check(C['rank_counts'](0,2,())['rank_counts']==[1] and C['construct'](0,2,())==(),'zero-dimensional contract') + invalid=[lambda:C['rank_counts'](5,2,()),lambda:C['rank_counts'](-1,2,()), + lambda:C['rank_counts'](1,4,()),lambda:C['rank_counts'](True,2,()), + lambda:C['rank_counts'](1,2,((2,0),)),lambda:C['rank_counts'](1,2,((1,),)), + lambda:C['rank_counts'](1,2,[(1,0)]),lambda:C['construct'](1,2,(),2), + lambda:C['capacity_equations'](2,2,(((1,0),(2,0)),)), + lambda:C['capacity_equations'](2,2,capacities=((((1,),),()),)), + lambda:C['capacity_equations'](2,2,fixed=[])] + invalid += [lambda:C['fixed_rank_counts'](5,2,()), + lambda:C['fixed_rank_counts'](2,2,(((1,0),(1,0)),((1,0),(0,1)))), + lambda:C['fixed_rank_counts'](2,2,(((1,0),(0,0)),))] + for f in invalid: + try:f() + except ValueError:counts['invalid_inputs']+=1 + else:raise ValueError('invalid input accepted') + hashes={name:hashlib.sha256((ROOT/name).read_bytes()).hexdigest() for name in ('completion.py','verify.py','PROOF.md','ORIGIN.json')} + return dict(status='PASS_NONNESTED_CAPACITY_RANK_COUNT',counts=dict(counts),cross_ratio=cross, + nested_source_counts=nested,dimension_four=formulas,compressed=compressed_records,source_hashes=hashes, + scope='Exact finite-field GL count and construction; exponential bounded API; no native admission or kappa.') + + +if __name__=='__main__': + result=run() + if sys.argv[1:]==['--write']: + (ROOT/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else: + check(not sys.argv[1:],'unknown command option') + check(result==json.loads((ROOT/'RESULT.json').read_text()),'receipt differs') + print(json.dumps(result,sort_keys=True))