diff --git a/research/fixed-cubic-coframe/PROOF.md b/research/fixed-cubic-coframe/PROOF.md new file mode 100644 index 0000000000..1a001cee77 --- /dev/null +++ b/research/fixed-cubic-coframe/PROOF.md @@ -0,0 +1,167 @@ +# Exact fixed-cubic coframe frontier + +This is a scoped rank-graph theorem with a concrete Clifford realization. It +does not optimize an unrestricted circuit or change the selected supplier. + +## Contract and result + +For an integer m >= 1 let V = F2^m plus F2^m, with + +``` +omega((x,z),(y,w)) = x.w + z.y +S(x,z) = (z,x+z) +L0 = {(0,z): z in F2^m} +d(A,B) = m - dim(A intersect B), for Lagrangians A,B. +``` + +Fix one internal Lagrangian L. Both its entrance from L0 and its exit to L0 +are paid. Every internal occurrence of the prescribed transport S must use +this same L. Write + +``` +a = d(L0,L), b = d(L,S L). +``` + +The exact componentwise minimal attainable pairs are + +``` +(a,b) = (j,m-2j), j = 0,...,floor(m/2). (1) +``` + +In particular, all charts satisfy 2a+b >= m and b = m modulo 2. Every +feasible pair is dominated by a pair in (1), and every pair in (1) is +attained. This characterizes the Pareto frontier, not every attainable pair. + +Let phi be increasing and concave on [0,m], with phi(0)=0, and let k>0. +The exact minimum complete graph bill is + +``` +min_L [2 phi(a) + k phi(b)] + = min(k phi(m), 2 phi(floor(m/2)) + k phi(m mod 2)). (2) +``` + +For the power tariff phi(r)=r^t, 00. Both boundary +transitions are included. At t=1 the values are respectively 1 and 2. + +The contract requires a common internal coframe. Different coframes at +different occurrences and replacement of the prescribed word by another +word are excluded. In particular S^3=I permits cancellations in unrestricted +synthesis. The theorem makes no lower-bound claim for that larger problem. + +## Lower bound and parity + +The distance d is invariant under symplectic transport and satisfies the +triangle inequality. Indeed dim(A intersect C) is at least +dim(A intersect B)+dim(B intersect C)-m, by applying the dimension formula +inside B. Since L0 and S L0 are complementary, d(L0,S L0)=m. Hence + +``` +m <= d(L0,L) + d(L,S L) + d(S L,S L0) = 2a+b. (5) +``` + +Put W=L intersect S L. The polynomial identity S^2+S+I=0 implies +S^-1=I+S. If v is in W, then v is in L and S^-1 v is in L. Consequently +S v = v+S^-1 v is in L. Also S v is in S L. Thus W is S-invariant. + +The polynomial X^2+X+1 is irreducible over F2. On W, multiplication by its +class X can therefore be defined as S, making W a vector space over F4. +Its binary dimension m-b is even. This proves b=m modulo 2. No estimate +from a finite search is used here. + +For any attainable pair, put j=(m-b)/2. Parity makes j an integer in +[0,floor(m/2)], and (5) gives j<=a. Once attainment below is proved, +(j,m-2j)=(j,b) dominates the original pair. The displayed pairs are mutually +incomparable, which establishes exactly the frontier (1). + +## Attainment + +Use the coordinate symplectic planes with bases e_i,f_i. On each of j +disjoint pairs of planes use the two-dimensional subspace + +``` +span(e_(2i-1)+e_(2i), f_(2i-1)+f_(2i)). +``` + +The displayed generators pair to zero because 1+1=0 in F2. Their span is +Lagrangian in its four-dimensional block and is S-invariant. Its +intersection with L0 has dimension one. On each remaining plane use the +original line span(f_i). Its intersection with its S-image is zero. + +Taking their direct sum gives a Lagrangian with a=j and b=m-2j. Every +rank in (1) is therefore attained for every positive m. + +After restriction to (1), the objective is +f(j)=2 phi(j)+k phi(m-2j). It is concave as a function of real j on +[0,floor(m/2)]. A concave function is at least the smaller of its two +endpoint values. Both endpoints are attainable. This proves (2), and +(3)-(4) follow by substitution. No numerical root calculation is needed. + +## A phase-exact Gaussian-dyadic witness + +Let H_g=(1+i)[[1,1],[1,-1]]/2, P=diag(1,i), and U=-P H_g. These are +Gaussian-dyadic Clifford matrices. Direct multiplication gives U^3=I, +U X U*=Z, and U Z U*=Y. Thus U induces exactly S on Pauli labels. +Put + +``` +B = CNOT (H_g tensor I), M = B* (U tensor U) B. +``` + +B takes the standard Z chart to the paired-plane chart above. It has +Fourier rank one; U tensor U has rank two; M is monomial and has rank zero. +The exact monomial phases and its four columns are generated in RESULT.json. +The full forward and inverse identities are + +``` +B M B* = U tensor U +B M* B* = (U tensor U)*. +``` + +They hold on every input, by equality of the full matrices. For any positive +integer k, B M^k B*=(U tensor U)^k. The graph invoice is therefore two +rank-one boundary children and k rank-zero internal occurrences, compared +with k rank-two occurrences in the original common chart. Tensoring these +blocks and adding an unpaired U supplies the general attaining recipe. +No relative or global phase is discarded. A monomial internal operator +still has ordinary arithmetic, routing and precision costs; zero Fourier +rank is not zero machine cost. + +## Relation to earlier work + +Ali Romman's PR6171 proves tensor reduction for a fixed scalar contact +graph with fixed repeated canonical boundaries and no prescribed native +transport equation. That theorem is a cited predecessor, not an object of +verification here. Its projection inequality is credited to Cinna Davis / +PR5140, and the canonical subspace-frame construction to icekylinx. + +The present positive-cost graph prescribes S on a loop at its internal +chart. It therefore changes the native-transport hypothesis excluded by +PR6171. The invariant paired chart demonstrates why that excluded +hypothesis matters, with both boundary costs paid. PR6172's signed graph +instead varies productive boundaries and has negative edges; it supplies +neither this transported model nor this optimum. Classical symplectic +distance, F4 linear algebra and Bell-basis facts are background. The new +contribution is the exact paid rank frontier and all-width tariff formula +for this specified common-coframe native contract. + +Ross Richardson / PR4081 supplies an earlier Gaussian order-three tensor +family and its distinct whole-bank quadratic-response restriction. No new +gate family or quadratic-response theorem is claimed here. The present +objective prices a conjugated native map rather than requiring every +tensor power to satisfy U_m^2+U_m+I=0. + +This contribution was produced by Nick Petalas. Independent human and +formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/fixed-cubic-coframe/README.md b/research/fixed-cubic-coframe/README.md new file mode 100644 index 0000000000..06696719a5 --- /dev/null +++ b/research/fixed-cubic-coframe/README.md @@ -0,0 +1,127 @@ +# Exact paid frontier for a fixed cubic native coframe + +This contribution was produced by Nick Petalas. It is a scoped proof with +exact finite corroboration and a phase-exact Clifford circuit witness. +No new kappa or selected-frontier change is claimed. + +## Result + +On m repeated binary symplectic planes, prescribe S(x,z)=(z,x+z). Choose +one internal Lagrangian L, retain the standard boundary L0 at both ends, +and charge both entrance and exit. Each prescribed S occurrence must use +that same internal coframe. Put a=d(L0,L), b=d(L,S L). + +The exact Pareto frontier is (j,m-2j), for 0<=j<=floor(m/2). All charts +obey 2a+b>=m and b=m modulo 2. For any increasing concave tariff phi with +phi(0)=0 and positive loop weight k, the exact full graph optimum is + +``` +min(k phi(m), 2 phi(floor(m/2)) + k phi(m mod 2)). +``` + +For phi(r)=r^t, 0> bit & 1: + if pivots[bit]: + row ^= pivots[bit] + else: + pivots[bit] = row + count += 1 + break + return count + + +def omega(x, y, m): + mask = (1 << m) - 1 + return (((x & mask) & (y >> m)).bit_count() + + ((y & mask) & (x >> m)).bit_count()) % 2 + + +def transport(v, m): + mask = (1 << m) - 1 + x, z = v & mask, v >> m + return z | ((x ^ z) << m) + + +def validate_chart(rows, m): + require(type(m) is int and 1 <= m <= 32, "chart dimension") + require(len(rows) == m and rank(rows, 2 * m) == m, "chart rank") + require(all(omega(x, y, m) == 0 for x, y in combinations(rows, 2)), + "chart isotropy") + + +def distances(rows, m): + validate_chart(rows, m) + boundary = [1 << (m + j) for j in range(m)] + moved = [transport(v, m) for v in rows] + return rank(rows + boundary, 2 * m) - m, rank(rows + moved, 2 * m) - m + + +def paired_chart(m, a): + require(type(m) is int and 1 <= m <= 32, "chart dimension") + require(type(a) is int and 0 <= a <= m // 2, "pair count") + rows = [] + for j in range(a): + pair = (1 << (2 * j)) | (1 << (2 * j + 1)) + rows.extend((pair, pair << m)) + rows.extend(1 << (m + j) for j in range(2 * a, m)) + validate_chart(rows, m) + return rows + + +def candidates(m): + require(type(m) is int and 1 <= m <= 4, "enumeration dimension") + for pivots in combinations(range(2 * m), m): + free = [(i, j) for i, p in enumerate(pivots) + for j in range(p + 1, 2 * m) if j not in pivots] + require(len(free) <= 16, "RREF capacity") + for mask in range(1 << len(free)): + rows = [1 << p for p in pivots] + for bit, (i, j) in enumerate(free): + if mask >> bit & 1: + rows[i] |= 1 << j + yield rows + + +def points(rows): + require(len(rows) <= 4, "literal-set capacity") + values = {0} + for row in rows: + values |= {value ^ row for value in values} + return values + + +def validate_pair(m, a, b): + require(all(type(v) is int for v in (m, a, b)), "pair integer types") + require(1 <= m <= 32 and 0 <= a <= m and 0 <= b <= m, "pair range") + require(2 * a + b >= m, "boundary triangle bound") + require((m - b) % 2 == 0, "cubic parity") + + +def tariff_checks(m, pairs): + count = 0 + q, delta = divmod(m, 2) + for quarter in range(1, 4 * m + 1): + threshold = Fraction(quarter, 4) + for k in (Fraction(1, 3), Fraction(1), Fraction(2), Fraction(7, 2), Fraction(8)): + endpoint = min(k * min(m, threshold), + 2 * min(q, threshold) + k * min(delta, threshold)) + actual = min(2 * min(a, threshold) + k * min(b, threshold) + for a, b in pairs) + require(actual == endpoint, "exact concave tariff optimum") + count += 1 + return count + + +def exhaustive(): + records = [] + tariff_count = 0 + for m in range(1, 5): + histogram = Counter() + for rows in candidates(m): + if any(omega(x, y, m) for x, y in combinations(rows, 2)): + continue + a, b = distances(rows, m) + values = points(rows) + moved = {transport(v, m) for v in values} + literal_a = m - (sum(v & ((1 << m) - 1) == 0 for v in values).bit_length() - 1) + common = values & moved + literal_b = m - (len(common).bit_length() - 1) + require((a, b) == (literal_a, literal_b), "literal distances") + require({transport(v, m) for v in common} == common, + "intersection is invariant") + validate_pair(m, a, b) + histogram[a, b] += 1 + expected = 1 + for j in range(1, m + 1): + expected *= (1 << j) + 1 + require(sum(histogram.values()) == expected, "complete Lagrangian inventory") + efficient = {(a, b) for a, b in histogram + if not any(c <= a and d <= b and (c, d) != (a, b) + for c, d in histogram)} + require(efficient == {(a, m - 2 * a) for a in range(m // 2 + 1)}, + "exact Pareto frontier") + tariff_count += tariff_checks(m, histogram) + records.append({"m": m, "lagrangians": expected, + "rank_pairs": [[a, b, n] for (a, b), n in sorted(histogram.items())]}) + return records, tariff_count + + +def constructions(): + count = 0 + for m in range(1, 33): + for a in range(m // 2 + 1): + rows = paired_chart(m, a) + require(distances(rows, m) == (a, m - 2 * a), "attaining chart") + count += 1 + return count + + +def gadd(x, y): + return x[0] + y[0], x[1] + y[1] + + +def gmul(x, y): + return x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0] + + +def gaussian(real, imag=0): + return Fraction(real), Fraction(imag) + + +def multiply(a, b): + n = len(a) + require(n in (2, 4) and len(b) == n, "matrix capacity") + require(all(len(row) == n for row in a + b), "square matrices") + result = [[gaussian(0) for _ in range(n)] for _ in range(n)] + for i in range(n): + for j in range(n): + for k in range(n): + result[i][j] = gadd(result[i][j], gmul(a[i][k], b[k][j])) + return result + + +def adjoint(a): + return [[(a[j][i][0], -a[j][i][1]) for j in range(len(a))] + for i in range(len(a))] + + +def tensor(a, b): + require(len(a) == len(b) == 2, "two-plane tensor capacity") + return [[gmul(a[i // 2][j // 2], b[i % 2][j % 2]) for j in range(4)] + for i in range(4)] + + +def identity(n): + require(n in (2, 4), "identity capacity") + return [[gaussian(i == j) for j in range(n)] for i in range(n)] + + +def column_supports(a): + return [sum(a[i][j] != gaussian(0) for i in range(len(a))) + for j in range(len(a))] + + +def native_fixture(): + h = [[gaussian(Fraction(1, 2), Fraction(1, 2)) for _ in range(2)] + for _ in range(2)] + h[1][1] = gaussian(Fraction(-1, 2), Fraction(-1, 2)) + phase = [[gaussian(-1), gaussian(0)], [gaussian(0), gaussian(0, -1)]] + u = multiply(phase, h) + x = [[gaussian(0), gaussian(1)], [gaussian(1), gaussian(0)]] + z = [[gaussian(1), gaussian(0)], [gaussian(0), gaussian(-1)]] + y = [[gaussian(0), gaussian(0, -1)], [gaussian(0, 1), gaussian(0)]] + require(multiply(adjoint(u), u) == identity(2), "native unitarity") + require(multiply(multiply(u, u), u) == identity(2), "actual cubic order") + require(multiply(multiply(u, x), adjoint(u)) == z, "native X image") + require(multiply(multiply(u, z), adjoint(u)) == y, "native Z image") + cnot = [[gaussian(0) for _ in range(4)] for _ in range(4)] + for j in range(4): + cnot[j ^ ((j >> 1) & 1)][j] = gaussian(1) + bell = multiply(cnot, tensor(h, identity(2))) + doubled = tensor(u, u) + changed = multiply(multiply(adjoint(bell), doubled), bell) + require(multiply(adjoint(bell), bell) == identity(4), "Bell unitarity") + require(column_supports(doubled) == [4] * 4, "baseline native rank two") + require(column_supports(bell) == [2] * 4, "Bell boundary rank one") + require(column_supports(changed) == [1] * 4, "changed native rank zero") + require(multiply(multiply(bell, changed), adjoint(bell)) == doubled, + "complete arbitrary-input forward identity") + require(multiply(multiply(bell, adjoint(changed)), adjoint(bell)) == adjoint(doubled), + "complete arbitrary-input inverse identity") + require(multiply(bell, changed) != doubled, "missing exit control") + encoded = [[[str(x), str(y)] for x, y in row] for row in changed] + return {"conjugated_matrix": encoded, "forward_basis_columns": 4, + "inverse_basis_columns": 4, "paid_boundary_ranks": [1, 1], + "old_internal_rank": 2, "new_internal_rank": 0} + + +def controls(): + invalid_pairs = [(0, 0, 0), (33, 0, 0), (2, -1, 2), (2, 3, 0), + (2, 0, 0), (3, 1, 0), (2, 1, 1), (True, 0, 1)] + rejected = 0 + for args in invalid_pairs: + try: + validate_pair(*args) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid rank pair accepted") + for m, rows in ((0, []), (2, [1, 1]), (2, [1, 4]), (33, [])): + try: + validate_chart(rows, m) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid chart accepted") + require(distances(paired_chart(2, 1), 2) == (1, 0), "coupling witness") + require(all(distances(rows, 1)[1] == 1 for rows in ([1], [2], [3])), + "one-copy obstruction") + return rejected + + +def result(): + inventories, tariffs = exhaustive() + evidence = {"schema_version": 1, "inventories": inventories, + "lagrangians": sum(r["lagrangians"] for r in inventories), + "concave_tariff_checks": tariffs, "constructions": constructions(), + "rejections": controls(), "native": native_fixture()} + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + evidence["source_sha256"] = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() + for name in names} + return evidence + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path) + args = parser.parse_args() + evidence = result() + rendered = json.dumps(evidence, indent=2, sort_keys=True) + "\n" + root = Path(__file__).resolve().parent + if args.write_receipt: + require(not args.write_receipt.resolve().is_relative_to(root), + "generate the receipt outside the package") + args.write_receipt.write_text(rendered, encoding="utf-8") + else: + saved = json.loads((root / "RESULT.json").read_text(encoding="utf-8")) + require(json.dumps(saved, sort_keys=True) == json.dumps(evidence, sort_keys=True), + "generated evidence or source hashes differ from RESULT.json") + print("PASS_FIXED_CUBIC_COFRAME", "lagrangians=" + str(evidence["lagrangians"]), + "constructions=" + str(evidence["constructions"]), + "concave_tariffs=" + str(evidence["concave_tariff_checks"]), + "rejections=" + str(evidence["rejections"])) + + +if __name__ == "__main__": + main()