diff --git a/research/dyadic-rotation-switch-tariff/PROOF.md b/research/dyadic-rotation-switch-tariff/PROOF.md new file mode 100644 index 0000000000..4f0bd381a4 --- /dev/null +++ b/research/dyadic-rotation-switch-tariff/PROOF.md @@ -0,0 +1,118 @@ +# Optimal edge-switch routing of a dyadic rotation + +This is a scoped combinatorial proof. It counts active swaps, with unit price +per swap of two occupied addresses that differ in exactly one binary bit. +There are N=2^h addresses, h>=1, and no additional addresses. Tokens may be +arbitrary distinct records. A routing network must send the token initially +at x to x+c modulo N, where 0<=c=2 they are distinct. + +## An explicit h-layer circuit + +Process bits i=h-1,h-2,...,0. Put b=2^i, r=c mod b, and c_i=floor(c/b) mod 2. +For every edge (x,x+b) with x_i=0, swap that edge precisely when + + c_i XOR [ (x mod b)+r >= b ] = 1. + +Each layer consists of disjoint edges. Its predicate is independent of bit i, +so the two endpoints agree on whether to swap. At entry to layer i, the lower +bits and bit i of any token's current address still equal those of its +original address. Only higher bits have changed. The displayed predicate is +exactly the change to bit i in addition of c modulo 2^h. Induction down the +bits proves the required endpoint for every token, with no empty workspace +and with arbitrary payloads preserved. + +There are 2^(h-i-1) copies of each lower-bit value. If c_i=0, exactly r of +the b lower-bit values cause a swap. If c_i=1, exactly b-r do. Thus the number +of active edges in this layer is + + 2^(h-i-1) min(c mod 2^(i+1), 2^(i+1)-(c mod 2^(i+1))). + +Summing gives S_h(c). Each token crosses each bit dimension at most once. + +## Global optimality in the stated swap model + +For any current token placement, sum the Hamming distances from every token +to its required destination. One hypercube-edge swap changes the sum by at +most two, since each of its two tokens changes one bit. Every routing needs +at least half the initial distance sum. This is the standard token-swapping +distance bound, for example Lemma 4 in Miltzow, Narins, Okamoto, Rote, Thomas +and Uno, *Approximation and Hardness for Token Swapping*: +https://page.mi.fu-berlin.de/rote/Papers/pdf/Approximation%2Band%2Bhardness%2Bfor%2Btoken%2Bswapping.pdf + +The circuit above moves each token in a bit dimension at most once and ends +at its destination. Consequently each token moves exactly its original +Hamming distance. Its S_h(c) swaps therefore meet the lower bound. This +proves optimality against arbitrary edge-swap sequences, rather than only +against circuits in the chosen layer order. The standard distance bound and +binary carry rule are not claimed as new. + +## Sharp maximum and equality + +Let q_k=(c mod 2^k)/2^k, t_k=min(q_k,1-q_k), and t_0=0. Reading successive +bits of c from least significant to most significant gives + + q_(k+1) = (q_k+epsilon_k)/2, epsilon_k in {0,1}. + +The possible next distances are t_k/2 and (1-t_k)/2. Every choice is +realizable by a next bit, and the two choices coincide only at t_k=1/2. +Also S_h(c)/2^h=sum_{k=1}^h t_k. + +For n>=1, let H_n(t) be the largest sum over n consecutive distances, +including the present distance t in [0,1/2]. Then H_1(t)=t and + + H_n(t) = t + max(H_(n-1)(t/2), H_(n-1)((1-t)/2)). + +Inductively H_n is affine with strictly positive slope A_n. Since t/2 is +at most (1-t)/2, its maximum branch is always the second one. The slope +recurrence is A_1=1 and A_n=1-A_(n-1)/2, which keeps 1/2<=A_n<=1. +Thus every optimal path chooses + + t_(k+1)=(1-t_k)/2. + +Starting at zero this gives t_k=(1-(-1/2)^k)/3. Therefore + + sum_{k=1}^h t_k = h/3 + (1-(-1/2)^h)/9. + +Multiplication by 2^h proves the displayed M_h. All maximizing choices are +strict except the one following t_1=1/2. For h>=2 there are exactly two +maximizing bit strings. Their final q_h values are t_h and 1-t_h, so their +offsets are exactly (2^h-(-1)^h)/3 and its complement. For h=1 the unique +maximizer is c=1. This also proves the formula's integrality. + +## The first fixture + +For h=3,c=3, descending bit layers have 3,2,4 active switches. Their total +is 9 and the initial Hamming-distance sum is 18. Both c=3 and c=5 attain +M_3=9. A full eight-wire Beneš layout has 20 available switch sites, while +this circuit has three layers and uses nine active sites. Available sites +and active swaps are different quantities; no physical time ratio follows. + +## Scope at the CRT caller + +Cinna Davis's CRT.md section 2 in PR #4100 requires rotations on x=s. The present theorem covers s=2^h. It does not +supply the strict s<2^h prime-modulus rotations used there. Unpaidmoon's +PR #4377 prices generic Beneš reconstruction in that larger setting. +This theorem adds an exact optimal tariff for a changed dyadic routing +premise. It does not replace either predecessor's full evaluator argument. + +Control computation, table generation, the cost to access or swap a record +on a sequential tape, scanner ownership, physical head motion, CRT repair, +stock, the ordinary callee and all-size multiplication remain external. +A smaller logical switch count alone gives no new kappa. diff --git a/research/dyadic-rotation-switch-tariff/README.md b/research/dyadic-rotation-switch-tariff/README.md new file mode 100644 index 0000000000..98f5ecc05f --- /dev/null +++ b/research/dyadic-rotation-switch-tariff/README.md @@ -0,0 +1,104 @@ +# Exact optimal switch tariff for dyadic rotations + +For N=2^h occupied binary addresses, rotating x to x+c modulo N requires +exactly + + S_h(c) = sum_{k=1}^h 2^(h-k) dist(c, 2^k Z) + +hypercube-edge swaps, for every h>=1 and 0<=c= bit) + if not (x & bit) and (((c >> i) & 1) ^ carry): + edges.append(x) + result.append((i, tuple(edges))) + return tuple(result) + + +def execute(h, program): + """Track token identities at positions, without using the carry formula.""" + require(type(h) is int and 1 <= h <= 8, "execution width outside 1..8") + tokens = list(range(1 << h)) + for i, endpoints in program: + bit = 1 << i + for x in endpoints: + tokens[x], tokens[x ^ bit] = tokens[x ^ bit], tokens[x] + return tokens + + +def endpoint(h, c, tokens): + n = 1 << h + return all(tokens[(x + c) % n] == x for x in range(n)) + + +def check_routes(): + cases = 0 + for h in range(1, 9): + n = 1 << h + for c in range(n): + program = layers(h, c) + require(endpoint(h, c, execute(h, program)), "wrong routed token") + count = sum(len(edges) for _, edges in program) + distance = sum((x ^ ((x + c) % n)).bit_count() for x in range(n)) + require(2 * count == distance, "not distance optimal") + require(count == tariff(h, c), "wrong switch tariff") + cases += 1 + return cases + + +def check_maxima(): + rows = [] + for h in range(1, MAX_WIDTH + 1): + n = 1 << h + values = [tariff(h, c) for c in range(n)] + maximum = max(values) + numerator = (3 * h + 1) * n - (-1) ** h + require(numerator % 9 == 0, "nonintegral maximum") + require(maximum == numerator // 9, "wrong maximum") + a = (n - (-1) ** h) // 3 + maximizers = [c for c, value in enumerate(values) if value == maximum] + require(maximizers == sorted({a, n - a}), "wrong equality cases") + rows.append({"h": h, "maximum": maximum, "offsets": maximizers}) + return rows + + +def cube_distances(h): + """Independent BFS over every token permutation, only for h <= 3.""" + require(1 <= h <= 3, "BFS width outside 1..3") + n = 1 << h + edges = [(x, x ^ (1 << i)) for x in range(n) + for i in range(h) if not x & (1 << i)] + identity = tuple(range(n)) + distances = {identity: 0} + queue = deque([identity]) + capacity = {2: 2, 4: 24, 8: 40320}[n] + # Connected edge transpositions generate S_n, with n! <= 40320 states. + for _ in range(capacity): + require(bool(queue), "BFS ended before its factorial bound") + state = queue.popleft() + for x, y in edges: + successor = list(state) + successor[x], successor[y] = successor[y], successor[x] + key = tuple(successor) + if key not in distances: + require(len(distances) < capacity, "BFS capacity exceeded") + distances[key] = distances[state] + 1 + queue.append(key) + require(not queue and len(distances) == capacity, "incomplete BFS") + for c in range(n): + target = tuple((position - c) % n for position in range(n)) + require(distances[target] == tariff(h, c), "BFS optimum disagrees") + return capacity + + +def check_controls(): + program = layers(3, 3) + i, edges = program[0] + damaged = ((i, edges[1:]),) + program[1:] + require(not endpoint(3, 3, execute(3, damaged)), "omission control accepted") + require(not endpoint(3, 3, execute(3, tuple(reversed(program)))), + "order control accepted") + invalid = [(0, 0), (13, 0), (3, -1), (3, 8), (True, 0), (3, False)] + for h, c in invalid: + try: + tariff(h, c) + except ValueError: + continue + raise ValueError("invalid input accepted") + return 2 + len(invalid) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write generated evidence outside checkout") + args = parser.parse_args() + report = {"claim_type": "scoped combinatorial proof with finite corroboration", + "route_cases": check_routes(), "maxima": check_maxima(), + "bfs_states": [cube_distances(h) for h in range(1, 4)], + "controls": check_controls()} + names = ("verify.py", "PROOF.md", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json") + report["source_sha256"] = { + name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() for name in names} + output = json.dumps(report, indent=2, sort_keys=True) + "\n" + if args.receipt is not None: + args.receipt.write_text(output) + print(output, end="") + print("PASS_DYADIC_ROTATION_SWITCH_TARIFF") + + +if __name__ == "__main__": + main()