diff --git a/research/p104-fixed-contact-ceiling/INPUTS.json b/research/p104-fixed-contact-ceiling/INPUTS.json new file mode 100644 index 0000000000..bfe4aa632a --- /dev/null +++ b/research/p104-fixed-contact-ceiling/INPUTS.json @@ -0,0 +1,34 @@ +[ + { + "file": "inputs/WORD.json.gz", + "sha256": "b2a98c4bd0dbe86c09e9d15ee060dcf1aab09dbef90aa1e2127676f4039f406b", + "head": "6efa248cf456d6101d757e9d09ba29711d18a13a", + "source": "research/p104-event-contact-step/WORD.json.gz", + "credit": "Ali Romman, GamingPuzzled, DreamingOfClouds and the retained P104 authors", + "git_blob": "9434855e7dad0d0236d23210b3e71a2b83a9ae64" + }, + { + "file": "inputs/local.py", + "sha256": "878734dfd64c4b9d362d0ae476cc5c2a19fe93e48b7378763b23f3e0dd0a5a71", + "head": "18968423711fd902aaee1099979497d55603e1dc", + "source": "research/p104-productive-controller/local.py", + "credit": "Credited PR5545 source closure; source notices retained", + "git_blob": "dbb3d56a4f5b733bb0c32a91249d1f6a7e1ab5d2" + }, + { + "file": "inputs/clifford_exact.py", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "head": "18968423711fd902aaee1099979497d55603e1dc", + "source": "research/p104-native-channel/vendor/clifford_exact.py", + "credit": "Credited PR5545 source closure; source notices retained", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2" + }, + { + "file": "inputs/native_verify.py", + "sha256": "3049471905b47b385c88378a1a3be7a18b8858aadd035b8a6da2f4a03b470f38", + "head": "18968423711fd902aaee1099979497d55603e1dc", + "source": "research/p104-native-channel/vendor/native_verify.py", + "credit": "Credited PR5545 source closure; source notices retained", + "git_blob": "2c209dfa9cfade3bc20ac5fc9d876b433a147f8c" + } +] diff --git a/research/p104-fixed-contact-ceiling/PROOF.md b/research/p104-fixed-contact-ceiling/PROOF.md new file mode 100644 index 0000000000..ad383efdc3 --- /dev/null +++ b/research/p104-fixed-contact-ceiling/PROOF.md @@ -0,0 +1,138 @@ +# A sharp price floor for fixed scalar contacts + +## Claim and domain + +Fix the ordered ADD, COPY, SCALE, INIT and CLEAR records and their frames. +Fix the main entry and exit frames. Each helper has an independent public +input. Its scalar endpoint is its own input, with no other input term. +Keep the source frame interface: a register carries one field in one +canonical chart. A transition between two charts is a paid Gaussian job +between monomial maps. No joint query on several registers is introduced. + +Allow every binary subspace as an intermediate chart, any number of +transitions between contacts, and arbitrary public helper entry and exit +charts. No nesting condition is imposed. Grant every added ordinary map +for free. The result is therefore a favorable bound for this larger model. + +For every power tariff r^t with 0 < t < 1, the PR5580 word attains the +maximum of helper credit minus paid transition cost in this model. +Thus changes confined to these paths or endpoints cannot improve its +complete recursive moment. The scalar contacts themselves can change +this bound. This is not an optimum over all P104 words. + +## Exact native rank for two charts + +For binary subspaces U,V of F2^n define + + d(U,V) = dim(U) + dim(V) - 2 dim(U intersection V). + +This is the subspace distance. It is a metric. In particular, an arbitrary +path from U to V has sum of edge distances at least d(U,V). + +Use the canonical chart G_U in the pinned Clifford source. Ignore Pauli +signs only in this rank calculation. Its image of the Z Lagrangian is + + L_U = {(x,z): x in U, x+z in U-perp}. + +To check the formula directly, put the basis of U first in an invertible +matrix G and put H=G^-1. The source chart conjugates the first dim(U) +coordinate C gates by D_Q P_G, where Q=I+H^T H. A Z vector z has image +x=G P G^T z and z'=z+Qx, where P is the first-coordinate projector. +Then x is in U and x+z' is orthogonal to U. Both spaces have dimension n, +so the inclusion is equality. The zero and full charts give the same rule. +The symplectic action of each chart is an involution. The square of the +chart is a Pauli, not necessarily the identity including its phase. + +The intersection L_U intersection L_V is parameterized by x in U +intersection V and x+z in (U+V)-perp. Its dimension is + + n - dim(U) - dim(V) + 2 dim(U intersection V). + +The X block of G_V G_U^-1 therefore has rank d(U,V). Monomial maps +preserve the Z Lagrangian. They cannot reduce this rank. The retained +Gaussian normal form gives monomial left and right factors and one +rank-d Gaussian. All scalar phases belong to the factors. The price is +d(U,V), not abs(dim(U)-dim(V)) for a nonnested pair. For example, two +distinct lines cost rank two even though their dimensions agree. + +These identities concern one address column. For width f, lift each +native operator columnwise, with its scalar phase raised to the f-th +power. Each rank-d block then has d*f address axes and remains a rank-d +job in the source width convention. Owner scalar coefficients are not +tensored. No identity on a sum is inferred by tensoring that sum. + +## Internal paths + +For nonnegative a,b and 0>i)&1)<>j&1);a[j],a[k]=a[k],a[j] + for i in range(n): + if i!=j and a[i]>>j&1:a[i]^=a[j] + assert [r&((1<>n for r in a) +def basis_extend(cols,n): + out=[] + for x in list(cols)+[1<len(out):out.append(x) + assert len(out)==n + return tuple(out) +def nullspace(rows,n): + a=list(rows);p=[];k=0 + for j in range(n): + t=next((i for i in range(k,len(a)) if a[i]>>j&1),None) + if t is None:continue + a[t],a[k]=a[k],a[t] + for i in range(len(a)): + if i!=k and a[i]>>j&1:a[i]^=a[k] + p.append(j);k+=1 + return tuple((1<>j)&1)<>i&1:out=pmul(out,T[i]) + for i in range(n): + if z>>i&1:out=pmul(out,T[n+i]) + return out +def compose(A,B):return tuple(apply(A,p) for p in B) +def inverse(T): + n=len(T)//2;cols=[x|(z<>n;u,v,p=apply(T,(x,z,0));assert (u,v)==identity(n)[j][:2];out.append((x,z,(-p)%4)) + return tuple(out) +def qvalue(Q,alpha,x,n): + return (sum(alpha[i] for i in range(n) if x>>i&1)+2*sum(parity((Q[i]>>(i+1))&(x>>(i+1))) for i in range(n) if x>>i&1))%4 +def mul_i(a,p): + x,y=a;p%=4 + return [(x,y),(-y,x),(-x,-y),(y,-x)][p] +@dataclass +class Op: + n:int + tab:tuple + circuit:list + def then(self,b): + assert self.n==b.n + return Op(self.n,compose(b.tab,self.tab),self.circuit+b.circuit) + def adjoint(self): + circ=[] + for e in reversed(self.circuit): + if e[0]=='P':circ.append(('P',inv(e[1],self.n))) + elif e[0]=='D':circ.append(('D',e[1],tuple((-x)%4 for x in e[2]))) + elif e[0]=='C':circ.append(('C',e[1],-e[2])) + elif e[0]=='phase':circ.append(('phase',(-e[1])%4)) + else:circ.append(e) + return Op(self.n,inverse(self.tab),circ) + def zero_state(self,basis=0): + N=1<>i)&1 for i in range(n)) + assert all(alpha[i]%2==(Q[i]>>i)&1 for i in range(n)) + return Op(n,tuple([(1<>i&1 else 0,1<>i&1 else 0) for i in range(n)]),[('C',q,sgn)]) +def xgate(n,b):return Op(n,tuple([(1<>i)&1)) for i in range(n)]),[('X',b)]) +def fourier(n,axes=None): + out=ident(n) + for i in range(n) if axes is None else axes:out=out.then(cgate(n,1<len(selected):picks.append(j);selected.append(x) + assert len(picks)==r and all(x>>r==0 for x in Bcols) + Br=transpose(selected,r);Bi=inv(Br,r);Dr=transpose([Dcols[j]&((1<= 735 and r not in live_owned, 'Owned initialization') + live_owned.add(r) + peak = max(peak, len(live_owned)) + rows[r] = {} + current[r] = e[2] + scalar += 2 + elif op == 'CLEAR': + need(r in live_owned and current[r] == e[2], 'Owned erasure at declared frame') + rows[r] = {} + current[r] = None + live_owned.remove(r) + scalar += 2 + else: + q, f = Q(e[-2]), e[-1] + need(q and current[r] == f, 'Scalar destination and coefficient') + n, d = abs(q.numerator), q.denominator + need(d & (d-1) == 0, 'Dyadic scalar coefficient') + need(abs(q)+1 < 2**16, 'Fixed scalar growth bound') + if op == 'SCALE': + need(n & (n-1) == 0, 'Dyadic unit SCALE') + rows[r] = {k:q*x for k,x in rows[r].items()} + scalar += 2*(abs(n.bit_length()-d.bit_length()) + int(q < 0)) + else: + s = e[2] + need(s != r and 0 <= s < 743 and current[s] == f, 'Common scalar chart') + if op == 'COPY': + need(r in live_owned and not rows[r], 'COPY into cleared owned field') + rows[r] = {k:q*x for k,x in rows[s].items()} + else: + need(op == 'ADD', 'Scalar opcode') + add(rows[r], rows[s], q) + scalar += 2*(3+n.bit_length()-1+n.bit_count()+d.bit_length()-1) + need(not live_owned and peak == 1 and current[:735] == w['final'], 'All public and owned exits') + live = set(w['live']) + for r,row in enumerate(rows): + expected = {r:Q(1)} if r < 735 else {} + if r-112 in live: + expected[r-112] = Q(1) + need(row == expected, 'All 743 public and owned rows') + main = live | {r+112 for r in live} + helpers = Counter(len(w['frames'][w['final'][r]])-len(w['frames'][w['initial'][r]]) for r in range(735) if r not in main) + need(len(live) == len(w['ports']) == 104 and len(main) == 208 and min(helpers) > 0, 'Independent productive inputs') + return {'paid':dict(paid), 'helpers':dict(helpers), 'public_inputs':735, 'owned_lifetimes':8, + 'peak_owned_fields':peak, 'real_scalar_allowance':scalar, 'endpoint_coefficients':743*743} + + +def reverse_columns(w): + """Check the transpose with dense dyadic rows and the reverse chronology.""" + n = 743 + rows = [[int(i == j) for j in range(n)] for i in range(n)] + exponents = [0]*n + for e in reversed(w['program']): + op,r = e[:2] + if op == 'MOVE': + continue + if op in ('INIT','CLEAR'): + rows[r] = [0]*n + exponents[r] = 0 + continue + q = Q(e[-2]) + qe = q.denominator.bit_length()-1 + if op == 'SCALE': + rows[r] = [q.numerator*x for x in rows[r]] + exponents[r] += qe + else: + s = e[2] + level = max(exponents[s], exponents[r]+qe) + a, b = 1 << (level-exponents[s]), q.numerator << (level-exponents[r]-qe) + rows[s] = [a*x+b*y for x,y in zip(rows[s],rows[r])] + exponents[s] = level + if op == 'COPY': + rows[r] = [0]*n + exponents[r] = 0 + r = s + while exponents[r] and not any(x & 1 for x in rows[r]): + rows[r] = [x//2 for x in rows[r]] + exponents[r] -= 1 + for r,row in enumerate(rows): + expected = [0]*n + if r < 735: + expected[r] = 1 << exponents[r] + if r in w['live']: + expected[r+112] = 1 << exponents[r] + need(row == expected, 'Independent dense transpose columns') + return {'columns':n, 'coefficients':n*n, 'arithmetic':'Dense integer rows with binary denominators; reverse chronology'} + + +def native(w): + C = load(ROOT/'research/p104-native-channel/vendor/clifford_exact.py', 'p104_productive_clifford') + V = load(ROOT/'research/p104-native-channel/vendor/native_verify.py', 'p104_productive_gaussian') + @lru_cache(None) + def chart(i): + return C.canonical_frame(9, tuple(w['frames'][i])) + recipes = {} + def check(a,b): + if (a,b) not in recipes: + recipe,_ = C.lower_child(chart(a).adjoint().then(chart(b))) + expected = V.adjoint(V.frame(w['frames'][a],9)) + V.frame(w['frames'][b],9) + V.equal(V.recipe(recipe),expected,'Native chart change and exact global phase') + need(recipe['rank'] == abs(len(w['frames'][a])-len(w['frames'][b])), 'Native boundary rank') + recipes[a,b] = recipe + return recipes[a,b] + for e in w['program']: + if e[0] == 'MOVE': + check(e[2],e[3]) + main = set(w['live']) | {r+112 for r in w['live']} + helper_profile = Counter() + for r in range(735): + if r not in main: + helper_profile[check(w['initial'][r],w['final'][r])['rank']] += 1 + adapters = [] + for r,q in zip(w['live'],w['ports']): + need(w['frames'][w['initial'][r]] == [q], 'Literal central port') + need(span(w['frames'][w['final'][r+112]]) == frozenset(x for x in range(512) if not (x&q).bit_count()%2), 'Literal output hyperplane') + tests = [ + (C.cgate(9,q,1).adjoint().then(chart(w['initial'][r])), V.adjoint((('C',q,1),))+V.frame(w['frames'][w['initial'][r]],9)), + (chart(w['final'][r+112]).adjoint().then(C.cgate(9,q,-1).then(C.fourier(9))), V.adjoint(V.frame(w['frames'][w['final'][r+112]],9))+(('C',q,-1),)+V.fourier(9))] + for actual,expected in tests: + recipe,_ = C.lower_child(actual) + need(recipe['rank'] == 0, 'Free intrinsic main adapter') + V.equal(V.recipe(recipe),expected,'Main endpoint phase') + adapters.append(recipe) + bad = json.loads(json.dumps(next(iter(recipes.values())))) + bad['left']['phase'] = (bad['left']['phase']+1)%4 + a,b = next(iter(recipes)) + try: + V.equal(V.recipe(bad),V.adjoint(V.frame(w['frames'][a],9))+V.frame(w['frames'][b],9),'Wrong phase control') + except ValueError: + pass + else: + raise ValueError('Wrong native phase accepted') + payload = [[a,b,recipes[a,b]] for a,b in sorted(recipes)] + adapters + return {'distinct_maps':len(recipes),'main_adapters':len(adapters),'helper_normalizers':2*sum(helper_profile.values()), + 'helpers':dict(helper_profile),'recipe_payload_sha256':sha256(json.dumps(payload,sort_keys=True,separators=(',',':')).encode()).hexdigest(), + 'wrong_phase_rejected':True, 'proof':'Every signed Pauli image and exact global phase; frame induction at every positive tensor width'} diff --git a/research/p104-fixed-contact-ceiling/inputs/native_verify.py b/research/p104-fixed-contact-ceiling/inputs/native_verify.py new file mode 100644 index 0000000000..2c209dfa9c --- /dev/null +++ b/research/p104-fixed-contact-ceiling/inputs/native_verify.py @@ -0,0 +1,277 @@ +"""Check native operators with exact Gaussian dyadic arithmetic. + +The interpreter is adapted from the independent campaign native review. +It does not import the source-code producer or the Clifford compiler. +Research used OpenAI Codex under the user's direction. +""" + +from functools import lru_cache + + +def require(condition, label): + if not condition: + raise ValueError(label) + + +def parity(value): + return value.bit_count() % 2 + + +def mul(matrix, vector): + return sum(parity(row & vector) << i for i, row in enumerate(matrix)) + + +def transpose(matrix): + return tuple(sum(((row >> j) & 1) << i for i, row in enumerate(matrix)) for j in range(len(matrix))) + + +def inverse(matrix): + n = len(matrix) + rows = [row | (1 << (n+i)) for i, row in enumerate(matrix)] + for j in range(n): + pivot = next((i for i in range(j, n) if rows[i] >> j & 1), None) + require(pivot is not None, 'singular binary chart') + rows[j], rows[pivot] = rows[pivot], rows[j] + for i in range(n): + if i != j and rows[i] >> j & 1: + rows[i] ^= rows[j] + require([row & ((1 << n)-1) for row in rows] == [1 << i for i in range(n)], 'binary inverse') + return tuple(row >> n for row in rows) + + +def extend(vectors, n): + columns, pivots = [], {} + for value in tuple(vectors) + tuple(1 << i for i in range(n)): + reduced = value + while reduced: + j = reduced.bit_length()-1 + if j not in pivots: + pivots[j] = reduced + columns.append(value) + break + reduced ^= pivots[j] + require(len(columns) == n, 'frame basis extension') + return tuple(columns) + + +def adjoint(circuit): + out = [] + for gate in reversed(circuit): + if gate[0] == 'P': + out.append(('P', inverse(gate[1]))) + elif gate[0] == 'D': + out.append(('D', gate[1], tuple(-a % 4 for a in gate[2]))) + elif gate[0] == 'C': + out.append(('C', gate[1], -gate[2])) + elif gate[0] == 'phase': + out.append(('phase', -gate[1] % 4)) + else: + require(gate[0] == 'X', 'adjoint gate type') + out.append(gate) + return tuple(out) + + +def fourier(rank): + return tuple(('C', 1 << i, 1) for i in range(rank)) + + +def frame(vectors, n): + rank = len(vectors) + if rank == 0: + return () + if rank == n: + return fourier(n) + matrix = transpose(extend(vectors, n)) + columns = transpose(inverse(matrix)) + quadratic = tuple((1 << i) ^ sum(parity(a & b) << j for j, b in enumerate(columns)) for i, a in enumerate(columns)) + diagonal = tuple((row >> i) & 1 for i, row in enumerate(quadratic)) + chart = (('P', matrix), ('D', quadratic, diagonal)) + return adjoint(chart) + fourier(rank) + chart + + +def monomial(record): + matrix = tuple(record['matrix_rows']) + quadratic = tuple(record['quadratic_rows']) + linear = tuple(record['linear_Z4']) + require(transpose(quadratic) == quadratic, 'quadratic symmetry') + require(len(matrix) == len(quadratic) == len(linear) == 9, 'monomial dimension') + require(all(a % 2 == (quadratic[i] >> i) & 1 for i, a in enumerate(linear)), 'diagonal parity') + inverse(matrix) + return (('D', quadratic, linear), ('P', matrix), ('X', record['offset']), ('phase', record['phase'])) + + +def recipe(record): + rank = record['rank'] + require(isinstance(rank, int) and 0 <= rank <= 9, 'child rank') + if rank == 0: + require(record['right'] is None, 'rank zero right factor') + return monomial(record['left']) + return monomial(record['right']) + fourier(rank) + monomial(record['left']) + + +def tableau(circuit, n=9): + rows = [(1 << i, 0, 0) for i in range(n)] + [(0, 1 << i, 0) for i in range(n)] + for gate in circuit: + tag = gate[0] + out = [] + inverse_transpose = transpose(inverse(gate[1])) if tag == 'P' else None + for x, z, phase in rows: + if tag == 'P': + x, z = mul(gate[1], x), mul(inverse_transpose, z) + elif tag == 'X': + phase += 2 * parity(z & gate[1]) + elif tag == 'C': + if parity(z & gate[1]): + x ^= gate[1] + phase += 3 * gate[2] + elif tag == 'D': + quadratic, linear = gate[1:] + phase += sum(linear[i] for i in range(n) if x >> i & 1) + phase += 2 * sum(parity((quadratic[i] >> (i+1)) & (x >> (i+1))) for i in range(n) if x >> i & 1) + z ^= mul(quadratic, x) + else: + require(tag == 'phase', 'tableau gate type') + out.append((x, z, phase % 4)) + rows = out + return tuple(rows) + + +@lru_cache(maxsize=512) +def action(gate): + if gate[0] == 'P': + return tuple(mul(gate[1], x) for x in range(512)) + require(gate[0] == 'D', 'state action type') + quadratic, linear = gate[1:] + return tuple((sum(linear[i] for i in range(9) if x >> i & 1) + + 2 * sum(parity((quadratic[i] >> (i+1)) & (x >> (i+1))) for i in range(9) if x >> i & 1)) % 4 for x in range(512)) + + +def rotate(pair, power): + a, b = pair + return ((a, b), (-b, a), (-a, -b), (b, -a))[power % 4] + + +def state(circuit, basis=0): + value, denominator = {basis: (1, 0)}, 0 + for gate in circuit: + tag = gate[0] + result = {} + if tag == "C": + direction, sign = gate[1:] + for address, (a, b) in value.items(): + for target, pair in ((address, (a - sign*b, b + sign*a)), + (address ^ direction, (a + sign*b, b - sign*a))): + old = result.get(target, (0, 0)) + result[target] = (old[0] + pair[0], old[1] + pair[1]) + denominator += 1 + else: + for address, pair in value.items(): + if tag == "P": + target = mul(gate[1], address) + elif tag == "X": + target = address ^ gate[1] + else: + target = address + if tag == "D": + pair = rotate(pair, action(gate)[address]) + else: + require(tag == "phase", "Unknown Gaussian state gate") + pair = rotate(pair, gate[1]) + require(target not in result, "A monomial address map is not injective") + result[target] = pair + value = {address: pair for address, pair in result.items() if pair != (0, 0)} + while denominator and all((a | b) % 2 == 0 for a, b in value.values()): + denominator -= 1 + value = {address: (a//2, b//2) for address, (a, b) in value.items()} + return value, denominator + + +def equal(actual, expected, label): + require(tableau(actual) == tableau(expected), label + ": signed Pauli action") + require(state(actual) == state(expected), label + ": exact global phase") + + +def verify(data, certificate): + word = data["word"] + original, clean = data["programs"], data["clean_programs"] + source_recipes = data["recipes"] + residuals = data["residuals"]["recipes"] + native_tags = {"climb", "adapter", "residual_adapter"} + for orientation in ("forward", "backward"): + native = [event for event in clean[orientation] if event[0] in native_tags] + require(native == [event for event in original[orientation] if event[0] in native_tags], + "A retained native event changed") + require(len(native) == 5056, "The retained native event count changed") + frames = [frame(tuple(vectors), 9) for vectors in word["frames"]] + used = {(event[3], event[4]) for program in clean.values() + for event in program if event[0] == "climb"} + children = {(record["old"], record["new"]): record for record in source_recipes["children"]} + require(len(children) == len(source_recipes["children"]) and used <= set(children), + "The retained child recipe coverage is incomplete") + for old, new in sorted(used): + record = children[old, new] + require(record["rank"] == len(word["frames"][new]) - len(word["frames"][old]), + "A retained child has the wrong rank") + equal(recipe(record), adjoint(frames[old]) + frames[new], "Retained child") + endpoints = {(record["role"], record["port"]): record + for record in source_recipes["endpoint_adapters"]} + require(len(endpoints) == len(source_recipes["endpoint_adapters"]) + and set(endpoints) == {(role, p) for role in ("source", "target") for p in range(112)}, + "The endpoint adapter coverage is incomplete") + for (role, port), record in endpoints.items(): + direction = word["ports"][port] + conventional = (("C", direction, 1),) if role == "source" else ( + ("C", direction, -1),) + fourier(9) + index = word["start"][port] if role == "source" else word["final"][112 + port] + require(record["frame"] == index and record["rank"] == 0, "An endpoint frame changed") + equal(recipe(record), adjoint(conventional) + frames[index], "Endpoint adapter") + used_residuals = set() + for program in clean.values(): + for event in program: + if event[0] != "residual_adapter": + continue + _, position, register, entry, *tail = event + terminal = tail[0] if tail else 1 + key = str(entry) if terminal == 1 else str(entry) + ":" + str(terminal) + require(key in residuals and position in ("pre", "post"), "A residual binding changed") + require(entry == word["start"][register] and terminal == word["final"][register], + "A residual endpoint changed") + used_residuals.add(key) + for key in sorted(used_residuals): + record = residuals[key] + equal(recipe(record), adjoint(frames[record["frame"]]) + frames[record.get("terminal", 1)], + "Residual adapter") + records = certificate["input_recipes"] + ports = certificate["compensation_ports"] + require([record["port"] for record in records] == ports and len(records) == 8, + "The eight input recipes changed") + columns = 0 + for item in records: + port, label = item["port"], item["label"] + require(label == word["ports"][port] and item["canonical_start_frame_id"] == word["start"][port], + "An input recipe has the wrong supplier label") + record = item["recipe"] + require(record["rank"] == 1, "An input copy has the wrong child rank") + for side in ("left", "right"): + factor = record[side] + require(factor["quadratic_rows"] == [0] * 9 and factor["linear_Z4"] == [0] * 9 + and factor["offset"] == factor["phase"] == 0, + "An input factor is not an address permutation") + actual, expected = recipe(record), (("C", label, 1),) + equal(actual, expected, "Positive inherited input line") + for basis in range(512): + require(state(actual, basis) == state(expected, basis), "A complete input Gaussian column differs") + columns += 1 + negative = monomial(record["right"]) + (("C", 1, -1),) + monomial(record["left"]) + require(tableau(negative) != tableau(expected) or state(negative) != state(expected), + "An inverse input child was not detected") + phased = actual + (("phase", 1),) + require(tableau(phased) == tableau(actual) and state(phased) != state(expected), + "An input phase-only error was not detected") + return {"status": "PASS_EXACT_INPUT_NATIVE_FRAMES", "retained_native_events_per_orientation": 5056, + "retained_child_recipes": len(used), "endpoint_adapter_recipes": len(endpoints), + "residual_adapter_recipes": len(used_residuals), "new_input_recipes": len(records), + "new_exact_gaussian_columns": columns, "inverse_input_child_controls": len(records), + "phase_only_controls": len(records), "address_permutation_factors": 2 * len(records), + "method": "Independent signed Pauli and exact Gaussian interpretation; no compiler import", + "scope": "Positive inherited input frames before every retained adapter. No recursive hosting claim."} diff --git a/research/p104-fixed-contact-ceiling/verify.py b/research/p104-fixed-contact-ceiling/verify.py new file mode 100644 index 0000000000..e1d7eff20a --- /dev/null +++ b/research/p104-fixed-contact-ceiling/verify.py @@ -0,0 +1,176 @@ +"""Check the exact price floor for fixed P104 scalar contacts. + +Ali Romman with OpenAI Codex assistance. Apache-2.0. +The input modules retain their source notices. +""" +from collections import Counter +from functools import lru_cache +from hashlib import sha256 +from pathlib import Path +import gzip +import importlib.util +import json +import sys + +HERE = Path(__file__).resolve().parent + + +def need(ok, label): + if not ok: + raise ValueError(label) + + +def load(name): + spec = importlib.util.spec_from_file_location(name, HERE / 'inputs' / (name + '.py')) + mod = importlib.util.module_from_spec(spec) + sys.modules[name] = mod + spec.loader.exec_module(mod) + return mod + + +def rank(vectors): + pivots = {} + for value in vectors: + while value: + bit = value.bit_length() - 1 + if bit in pivots: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return len(pivots) + + +def distance(a, b): + return 2 * rank(tuple(a) + tuple(b)) - len(a) - len(b) + + +def spaces(n): + out = {frozenset([0]): ()} + for _ in range(n): + for span, basis in tuple(out.items()): + for x in range(1, 1 << n): + if x not in span: + larger = span | frozenset(v ^ x for v in span) + out.setdefault(larger, basis + (x,)) + return out + + +def contact_floor(w): + main = set(w['live']) | {r + 112 for r in w['live']} + contacts = [[] for _ in range(743)] + for r in main: + contacts[r].append((-1, w['initial'][r])) + for k, e in enumerate(w['program']): + if e[0] in ('ADD', 'COPY'): + for r in e[1:3]: + contacts[r].append((k, e[-1])) + elif e[0] in ('SCALE', 'INIT', 'CLEAR'): + contacts[e[1]].append((k, e[-1])) + for r in main: + contacts[r].append((len(w['program']), w['final'][r])) + paid, helpers, intervals = Counter(), Counter(), [] + for r, seq in enumerate(contacts): + for (i, a), (j, b) in zip(seq, seq[1:]): + d = distance(w['frames'][a], w['frames'][b]) + if d: + paid[d] += 1 + intervals.append([r, i, j, a, b, d]) + if r < 735 and r not in main and seq: + helpers[distance(w['frames'][seq[0][1]], w['frames'][seq[-1][1]])] += 1 + helpers.pop(0, None) + unused = [r for r in range(735) if r not in main and not contacts[r]] + return paid, helpers, intervals, unused + + +def main(): + for pin in json.loads((HERE / 'INPUTS.json').read_text()): + need(sha256((HERE / pin['file']).read_bytes()).hexdigest() == pin['sha256'], 'Source pin') + c, local, v = load('clifford_exact'), load('local'), load('native_verify') + w = json.loads(gzip.decompress((HERE / 'inputs/WORD.json.gz').read_bytes())) + replay = local.replay(w) + small = {} + for n in (2, 3, 4): + all_spaces = spaces(n) + ops = {s: c.canonical_frame(n, b) for s, b in all_spaces.items()} + for a, ba in all_spaces.items(): + for b, bb in all_spaces.items(): + actual = ops[a].adjoint().then(ops[b]) + r = rank([x for x, z, phase in actual.tab[n:]]) + expected = len(ba) + len(bb) - 2 * ((len(a & b)).bit_length() - 1) + need(r == expected == distance(ba, bb), 'All-frame rank law') + small[str(n)] = len(all_spaces) ** 2 + + @lru_cache(None) + def chart(i): + frame = w['frames'][i] + op = c.canonical_frame(9, tuple(frame)) + span = {0} + for x in frame: + span |= {v ^ x for v in tuple(span)} + need(all(x in span and all(((x ^ z) & u).bit_count() % 2 == 0 for u in frame) + for x, z, phase in op.tab[9:]), 'Source chart Lagrangian') + return op + + paid, helpers, intervals, unused = contact_floor(w) + pairs = {(a, b) for r, i, j, a, b, d in intervals} + main_roles = set(w['live']) | {r + 112 for r in w['live']} + pairs |= {(w['initial'][r], w['final'][r]) for r in range(735) if r not in main_roles} + for a, b in pairs: + actual = chart(a).adjoint().then(chart(b)) + need(rank([x for x, z, phase in actual.tab[9:]]) == distance(w['frames'][a], w['frames'][b]), + 'Source rank floor') + # Bind nonnested examples to the retained compiler, including global phase. + examples = [([1], [2]), ([3, 5], [9, 17]), ([1, 2, 4], [8, 16, 32])] + for a, b in examples: + target = c.canonical_frame(9, tuple(a)).adjoint().then(c.canonical_frame(9, tuple(b))) + recipe, _ = c.lower_child(target) + need(recipe['rank'] == distance(a, b), 'Nonnested recipe price') + v.equal(v.recipe(recipe), v.adjoint(v.frame(a, 9)) + v.frame(b, 9), 'Nonnested phase') + + old_paid = Counter({int(k): n for k, n in replay['paid'].items()}) + old_helpers = Counter({int(k): n for k, n in replay['helpers'].items()}) + need(unused == [711], 'Complete unused-helper set') + need(old_paid - paid == old_helpers - helpers == Counter({5: 1}), 'Neutral unused helper') + need(not paid - old_paid and not helpers - old_helpers, 'No hidden floor cost') + need({r: old_helpers[r] - old_paid[r] for r in old_paid.keys() | old_helpers.keys()} == + {r: helpers[r] - paid[r] for r in old_paid.keys() | old_helpers.keys()}, 'Exact signed profile optimum') + + need(distance([1], [2]) == 2 and len([1]) - len([2]) == 0, 'False rank control') + wrong = json.loads(json.dumps(w)) + e = next(e for e in wrong['program'] if e[0] == 'ADD') + e[-2] = '3/8' + try: + local.replay(wrong) + except ValueError: + pass + else: + raise ValueError('Changed scalar identity accepted') + mutant = json.loads(json.dumps(w)) + e = next(e for e in mutant['program'] if e[0] == 'ADD') + e[-1] = next(i for i in range(len(w['frames'])) if i != e[-1]) + try: + local.replay(mutant) + except ValueError: + pass + else: + raise ValueError('Wrong scalar chart accepted') + out = {'status': 'PASS_P104_FIXED_CONTACT_CEILING', 'source_pr': 5580, + 'small_pair_counts': small, 'source_pairs': len(pairs), 'nonzero_intervals': len(intervals), + 'interval_sha256': sha256(json.dumps(intervals, separators=(',', ':')).encode()).hexdigest(), + 'paid_floor': {str(k): v for k, v in sorted(paid.items())}, + 'helper_core': {str(k): v for k, v in sorted(helpers.items())}, + 'unused_helpers': unused, 'neutral_target_paid_pair': {'5': 1}, + 'public_inputs': replay['public_inputs'], 'owned_lifetimes': replay['owned_lifetimes'], + 'scope': 'All nonnested paths and helper endpoints, fixed scalar contacts; every 0