/machines/1RB1RC_1LC1LE_1RD0RA_1LB0RA_0LD1LF_1LD---/check_proof.py · raw
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 | #!/usr/bin/env python3 """check_proof.py for W7-1, the table of 740-lines 75, 179, 265, 597 (proof.md, revision 2). Self-contained: its own simulator, token parser and abstract map (stdlib only; nothing from tools/ or work/). Sections (proof.md section in brackets): A chunk lemmas R, S, P, T, A, H, E of the sweep [2] B macro rules: random + exhaustive-small instances vs direct simulation, exact steps [3] C outside cases (informational): the halting pattern '+ 0 +', and J-members that halt [3.3, 6.3] D region counter lemma: exhaustive bit level, and on the abstract map [4] E opening runs of the four starts to the base K(c), then every D:R predicted by the abstract map up to --direct steps (direct simulation) [5] F start-parametric lemma: the four abstract orbits agree up to the first field [5.3] G condition J along the four abstract orbits up to --far steps; legal-event lemma; the one-step exits (a)-(e) from J [6] H dance (C4), climb automaton (C5) and reflection (C6, both branches) on the orbits' own events; random climbs with singletons equal to 1 [4.4-4.6] I fast exact map (jumps over ODD runs by C1/C2), cross-checked against the plain map, and the four orbits to --fast steps [6.4] usage: python3 check_proof.py [--direct 3e7] [--far 1e13] [--fast 1e100] [--seed 20261014] [--quick] The SUMMARY line is PASS only if A, B, D, E, F, G, H and I pass (C is informational). PASS checks the proved parts. It does not prove O1 (proof.md 6.3-6.4). """ import sys, random, time from collections import Counter TM = '1RB1RC_1LC1LE_1RD0RA_1LB0RA_0LD1LF_1LD---' LINES = {'A': (75, '1RB1RC_1LC1LE_1RD0RA_1LB0RA_0LD1LF_1LD---'), 'B': (597, '1RB1RE_1LC0LD_1RA0LD_1LA1LB_0RC1RF_1RC---'), 'C': (265, '1RB0RE_1LC0RE_1LA1LD_0LB1LF_1RC1RA_1LB---'), 'D': (179, '1RB0LD_1RC1RE_1LA0LD_1LB1LC_0RA1RF_1RA---')} ST = 'ABCDEF' def parse_tm(tm): t = {} for i, g in enumerate(tm.split('_')): for s in (0, 1): tr = g[3 * s:3 * s + 3] t[(ST[i], s)] = None if tr[2] == '-' else (int(tr[0]), 1 if tr[1] == 'R' else -1, tr[2]) return t T6 = parse_tm(TM) # ---------------------------------------------------------------- simulator class Sim: """Two-way tape in a bytearray with an offset; grows on demand.""" def __init__(self, cells='', head=None, state='A', pad=64): n = len(cells) self.off = pad self.tape = bytearray(pad) + bytearray(int(c) for c in cells) + bytearray(pad) self.pos = (n if head is None else head) + pad self.state = state self.steps = 0 self.halted = False self.lastdir = 0 def grow(self): n = len(self.tape) self.tape = bytearray(n) + self.tape + bytearray(n) self.off += n self.pos += n def run(self, nsteps, stop=None): """Run up to nsteps; stop(self) is called after each step that moves R in state D.""" tape = self.tape; pos = self.pos; q = self.state; tr = T6 for _ in range(nsteps): if pos <= 0 or pos >= len(tape) - 1: self.pos = pos; self.grow(); tape = self.tape; pos = self.pos s = tape[pos] t = tr[(q, s)] if t is None: self.halted = True break tape[pos] = t[0]; pos += t[1]; q = t[2]; self.steps += 1 if stop is not None and q == 'D' and t[1] == 1: self.pos = pos; self.state = q; self.lastdir = 1 if stop(self): return True self.pos = pos; self.state = q return False def window(self, a, b): return ''.join(str(c) for c in self.tape[self.off + a:self.off + b]) def nonzero_span(self): t = self.tape lo = next((i for i in range(len(t)) if t[i]), None) if lo is None: return None hi = len(t) - 1 - next(i for i in range(len(t)) if t[len(t) - 1 - i]) return lo, hi # ---------------------------------------------------------------- tokens SYM = {2: '|', 0: '+', 3: '#'} PIPE, PLUS, HASH = 2, 0, 3 def cells_of(T): fs, ss = T[0::2], T[1::2] out = ['1' + '01' * fs[0]] for s, f in zip(ss, fs[1:]): out.append('0' * s + '1' + '01' * f) out.append('0011') return ''.join(out) def fmt(T): fs, ss = T[0::2], T[1::2] o = [str(fs[0])] for s, f in zip(ss, fs[1:]): o += [SYM.get(s, '<%d>' % s), str(f)] return ' '.join(o) def parse_at(sim): """Token list if the tape is 0^inf <T cells> 0011 D> 0^inf (head just right of the last 1), else None.""" t = sim.tape; p = sim.pos if sim.state != 'D' or t[p] != 0: return None if any(t[p:]): return None ones = [i for i in range(p) if t[i]] if len(ones) < 3: return None gaps = [b - a - 1 for a, b in zip(ones, ones[1:])] if ones[-1] != p - 1 or gaps[-2:] != [2, 0]: return None gaps = gaps[:-2] T = []; f = 0 for g in gaps: if g == 1: f += 1 else: T += [f, g]; f = 0 T.append(f) return T def sim_from_tokens(T): c = cells_of(T) return Sim(c, head=len(c), state='D') def next_dr(T, limit=10 ** 8): """Run the TM from X(T) to the next D:R configuration that parses as a token list.""" s = sim_from_tokens(T) res = {} def stop(sm): U = parse_at(sm) if U is not None: res['U'] = U return True return False s.run(limit, stop) if s.halted: return 'HALT', s.steps return res.get('U'), s.steps # ---------------------------------------------------------------- abstract map (proof.md section 3) def mk(fs, ss): T = [fs[0]] for s, f in zip(ss, fs[1:]): T += [s, f] return T def step(T): """One half-cycle (D:R to D:R). Returns (T', steps, rule) or (None, None, outside-case label).""" fs, ss = list(T[0::2]), list(T[1::2]) k = len(fs) - 1 i = k; S = 0; n = 0 while True: S += fs[i]; n += 1 if fs[i] % 2 == 1: break if i == 0: nf = [1] + [f + 1 for f in fs] + [1] return mk(nf, [PLUS] * (len(nf) - 2) + [PIPE]), 6 * S + 6 * n + 28, 'overflow-even' s = ss[i - 1] if s == PIPE: i -= 1; continue if s == PLUS: x = fs[i - 1] if x >= 2: fs[i - 1] -= 2; ss[i - 1] = PIPE; fs[k] += 3 return mk(fs, ss), 6 * S + 12 * n + 10, 'plus' if x == 1 and i - 1 == 0: fs = fs[1:]; ss = ss[1:]; fs[-1] += 3 return mk(fs, ss), 6 * S + 12 * n + 10, 'plus-farend-1' if x == 1 and ss[i - 2] == PLUS and i < k: y = fs[i - 2] nfs = fs[:i - 2] + [y + fs[i] + 1] + fs[i + 1:] nss = ss[:i - 2] + ss[i:] nfs[-1] += 3 return mk(nfs, nss), 6 * S + 12 * n + 10, 'plus-merge-1' if x == 0 and i - 1 == 0: # FAR-0-PLUS-EVEN (revision 2): 0 + e_1 | ... | L, all even -> (e_1+3) + (e_2+1) + ... + (L+1) | 1 nf = [fs[1] + 3] + [f + 1 for f in fs[2:]] + [1] return mk(nf, [PLUS] * (len(nf) - 2) + [PIPE]), 6 * S + 6 * n + 30, 'far0plus-even' return None, None, 'out:plus x=%d left=%s' % (x, 'E' if i - 1 == 0 else SYM.get(ss[i - 2])) if s == HASH: a = fs[i - 1] if a >= 1: fs[i - 1] -= 1; fs[k] += 3 return mk(fs, ss), 6 * S + 12 * n + 18, 'hash-odd' if i - 1 == 0: fs = fs[1:]; ss = ss[1:]; fs[-1] += 3 return mk(fs, ss), 6 * S + 12 * n + 18, 'hash-farend-0' return None, None, 'out:hash a=0 interior' return None, None, 'out:sep%d' % s if i == 0: nf = [fs[0] + 2] + [f + 1 for f in fs[1:]] + [1] return mk(nf, [PLUS] * (len(fs) - 1) + [PIPE]), 6 * S + 6 * n + 28, 'overflow-odd' s = ss[i - 1] if s == PIPE: d = fs[i - 1] if d >= 1: fs[i - 1] -= 1; fs[k] += 3 return mk(fs, ss), 6 * S + 12 * n + 12, 'odd' if i - 1 == 0: fs = fs[1:]; ss = ss[1:]; fs[-1] += 3 return mk(fs, ss), 6 * S + 12 * n + 12, 'death-farend' sl = ss[i - 2] if sl == PIPE: nfs = fs[:i - 1] + fs[i:] nss = ss[:i - 2] + [HASH] + ss[i:] nfs[-1] += 3 return mk(nfs, nss), 6 * S + 12 * n + 12, 'death' if sl == PLUS and i < k: a = fs[i - 2] nfs = fs[:i - 2] + [a + fs[i] + 1] + fs[i + 1:] nss = ss[:i - 2] + ss[i:] nfs[-1] += 3 return mk(nfs, nss), 6 * S + 12 * n + 12, 'death-merge' return None, None, 'out:death left=%s' % SYM.get(sl, sl) if s == PLUS: d = fs[i - 1] if d >= 1: fs[i - 1] -= 1; fs[i] -= 1; ss[i - 1] = PIPE; fs[k] += 3 return mk(fs, ss), 6 * S + 12 * n + 8, 'odd-plus' if i - 1 == 0: # FAR-0-PLUS-ODD (revision 2): 0 + j | e_2 | ... | L -> (j-1) | e_2 | ... | (L+3) nf = [fs[1] - 1] + fs[2:]; nf[-1] += 3 return mk(nf, [PIPE] * (len(nf) - 1)), 6 * S + 12 * n + 8, 'far0plus-odd' return None, None, 'out:odd-plus d=0' if s == HASH: nf = fs[:i] + [fs[i] + 2] + [f + 1 for f in fs[i + 1:]] + [1] ns = ss[:i - 1] + [PLUS] * (k - i + 1) + [PIPE] return mk(nf, ns), 6 * S + 6 * n + 28, 'bounce' return None, None, 'out:odd sep%d' % s # ---------------------------------------------------------------- helpers results = {} def report(sec, ok, msg): results[sec] = ok print(f'[{sec}] {"PASS" if ok else "FAIL"}: {msg}', flush=True) def arg(name, default): if name in sys.argv: return sys.argv[sys.argv.index(name) + 1] return default QUICK = '--quick' in sys.argv R = random.Random(int(arg('--seed', 20261014))) # ---------------------------------------------------------------- A. chunk lemmas def chunk(before, bstate, bhead, after, astate, ahead, nsteps): """Run nsteps from (before, bstate on index bhead). The head may not leave the window except with the very last move. Check the window equals `after` and the head is on index ahead.""" s = Sim(before, head=bhead, state=bstate, pad=8) lo, hi = s.off, s.off + len(before) for k in range(nsteps): if not (lo <= s.pos < hi): return False s.run(1) if s.halted: return False return s.window(0, len(before)) == after and s.state == astate and s.pos - s.off == ahead def sec_A(): ok = True # cells written left to right; heads are window indices; -1 means "the cell left of the window" lem = { 'R 0011 D>0 -> D>0 1111 (4)': ('00110', 'D', 4, '01111', 'D', 0, 4), 'S x101 D>0 -> D>x 1111 (8)': (None, 'D', 4, None, 'D', 0, 8), 'P 001 D>0 -> D>0 011 (3)': ('0010', 'D', 3, '0011', 'D', 0, 3), 'T 10 D>0 -> 010 A> (5)': ('1001', 'D', 2, '0101', 'A', 3, 5), 'A A>11 -> 10 A> (2)': ('11', 'A', 0, '10', 'A', 2, 2), 'H 10 A>0 1 -> 010 A>1 (7)': ('1001', 'A', 2, '0101', 'A', 3, 7), 'E 10 A>000 -> 1 0011 D>0 (5)': ('10000', 'A', 2, '10011', 'D', 5, 5), } for name, (b, bs, bh, a, as_, ah, n) in lem.items(): if name.startswith('S'): good = all(chunk(x + '1010', 'D', 4, x + '1111', 'D', 0, 8) for x in '01') elif name.startswith('E'): s = Sim('10000000', head=2, state='A', pad=8); s.run(5) good = s.window(0, 8) == '10011000' and s.state == 'D' and s.pos - s.off == 5 else: good = chunk(b, bs, bh, a, as_, ah, n) print(' ', name, 'ok' if good else 'FAIL') ok &= good # inductive corollaries, checked for small sizes: even field sweep and odd field sweep for f in range(0, 30): cells = '00' + '1' + '01' * f + '0' + '1' * 6 # sep | field | D-cell | 1^6 s = Sim(cells, head=2 + 2 * f + 1, state='D', pad=8) s.run(4 * f + (4 if f % 2 else 0)) if f % 2 == 0: exp = '00' + '1' + '0' + '1' * (2 * f) + '1' * 6 good = s.window(0, len(cells)) == exp and s.state == 'D' and s.pos - s.off == 3 else: exp = '00' + '1' * (2 * f + 2) + '1' * 6 good = s.window(0, len(cells)) == exp and s.state == 'D' and s.pos - s.off == 1 ok &= good report('A', ok, '7 chunk lemmas exact; even/odd field sweeps (4f, 4f+4 steps) for f = 0..29') # ---------------------------------------------------------------- B. macro rules def rnd_even(lo=2, hi=40): return 2 * R.randint(lo // 2, hi // 2) def rnd_odd(lo=1, hi=41): return 2 * R.randint((lo - 1) // 2, (hi - 1) // 2) + 1 def rnd(lo=1, hi=40): return R.randint(lo, hi) def seq(fs, ss=None): ss = ss if ss is not None else [PIPE] * (len(fs) - 1) return mk(fs, ss) def gen(rule): """A random instance on which the rule's case must fire (left context random).""" left = [rnd(3, 40) for _ in range(R.randint(1, 3))] lsep = [R.choice([PIPE, PIPE, PLUS]) for _ in left[1:]] evens = [rnd_even(2, 40) for _ in range(R.randint(0, 3))] L = rnd_even(2, 60) if rule == 'odd': d = rnd(1, 40); j = rnd_odd(1, 41) return mk(left + [d, j] + evens + [L], lsep + [R.choice([PIPE, PLUS]), PIPE] + [PIPE] * (len(evens) + 1)) if rule == 'odd-L': d = rnd(1, 40); Lo = rnd_odd(1, 61) return mk(left + [d, Lo], lsep + [R.choice([PIPE, PLUS]), PIPE]) if rule == 'plus': x = rnd(2, 40) return mk(left + [x] + evens + [L], lsep + [R.choice([PIPE, PLUS])] + [PLUS] + [PIPE] * len(evens)) if rule == 'hash-odd': a = rnd(1, 40) return mk(left + [a] + evens + [L], lsep + [R.choice([PIPE, PLUS])] + [HASH] + [PIPE] * len(evens)) if rule == 'death': b = rnd_odd(1, 41) return mk(left + [0, b] + evens + [L], lsep + [PIPE, PIPE] + [PIPE] * (len(evens) + 1)) if rule == 'death-merge': b = rnd_odd(1, 41); ev = evens or [rnd_even()] return mk(left + [0, b] + ev + [L], lsep + [PLUS, PIPE] + [PIPE] * (len(ev) + 1)) if rule == 'death-merge-far': b = rnd_odd(1, 41); ev = evens or [rnd_even()] return mk([1, 0, b] + ev + [L], [PLUS, PIPE] + [PIPE] * (len(ev) + 1)) if rule == 'odd-plus': d = rnd(1, 40); j = rnd_odd(1, 41) return mk(left + [d, j] + evens + [L], lsep + [R.choice([PIPE, PLUS]), PLUS] + [PIPE] * (len(evens) + 1)) if rule == 'bounce': a = rnd(0, 40); b = rnd_odd(1, 41) return mk(left + [a, b] + evens + [L], lsep + [R.choice([PIPE, PLUS]), HASH] + [PIPE] * (len(evens) + 1)) if rule == 'bounce-L': a = rnd(0, 40); Lo = rnd_odd(1, 61) return mk(left + [a, Lo], lsep + [R.choice([PIPE, PLUS]), HASH]) if rule == 'overflow-even': fs = [rnd_even(0, 40)] + evens + [L] return seq(fs) if rule == 'overflow-odd': fs = [rnd_odd(1, 41)] + evens + [L] return seq(fs) if rule == 'plus-farend-1': return mk([1] + evens + [L], [PLUS] + [PIPE] * len(evens)) if rule == 'plus-merge-1': y = rnd(1, 40); e = rnd_even(0, 40) return mk(left + [y, 1, e] + evens + [L], lsep + [R.choice([PIPE, PLUS]), PLUS, PLUS] + [PIPE] * (len(evens) + 1)) if rule == 'death-farend': b = rnd_odd(1, 41) return mk([0, b] + evens + [L], [PIPE, PIPE] + [PIPE] * len(evens)) if rule == 'hash-farend-0': e = rnd_even(0, 40) return mk([0, e] + evens + [L], [HASH, PIPE] + [PIPE] * len(evens)) if rule == 'far0plus-even': return mk([0] + evens + [L], [PLUS] + [PIPE] * len(evens)) if rule == 'far0plus-odd': j = rnd_odd(1, 41) if R.random() < 0.25: return mk([0, j], [PLUS]) return mk([0, j] + evens + [L], [PLUS, PIPE] + [PIPE] * len(evens)) raise ValueError(rule) def sec_B(): ok = True nper = 40 if QUICK else 150 rules = ['odd', 'odd-L', 'plus', 'hash-odd', 'death', 'death-merge', 'death-merge-far', 'odd-plus', 'bounce', 'bounce-L', 'overflow-even', 'overflow-odd', 'plus-farend-1', 'plus-merge-1', 'death-farend', 'hash-farend-0', 'far0plus-even', 'far0plus-odd'] tot = 0 for r in rules: good = 0 for _ in range(nper): T = gen(r) P, st, rule = step(T) U, s2 = next_dr(T) exp = {'odd-L': 'odd', 'bounce-L': 'bounce', 'death-merge-far': 'death-merge'}.get(r, r) if P is not None and rule == exp and P == U and st == s2: good += 1 else: print(' mismatch', r, fmt(T), '->', U if U in (None, 'HALT') else fmt(U), '| map', rule, None if P is None else fmt(P), st, s2) tot += good print(f' {r:15s} {good}/{nper}') ok &= good == nper # exhaustive small: every token list with <= 4 fields, fields 0..5, seps | + #, on which the map has a rule cnt = Counter(); bad = 0 if not QUICK: import itertools for nf in (1, 2, 3, 4): for fs in itertools.product(range(6), repeat=nf): for ss in itertools.product((PIPE, PLUS, HASH), repeat=nf - 1): if fs[-1] < 1: continue T = mk(list(fs), list(ss)) P, st, rule = step(T) if P is None: cnt['outside'] += 1 continue U, s2 = next_dr(T, 10 ** 6) if P == U and st == s2: cnt['ok'] += 1 else: bad += 1 if bad <= 5: print(' exhaustive mismatch', fmt(T), rule, fmt(P), U, st, s2) print(' exhaustive (<= 4 fields, values 0..5, L >= 1):', dict(cnt), 'mismatches', bad) ok &= bad == 0 report('B', ok, f'{len(rules)} rule cases x {nper} random instances ({tot} total), exact tokens and steps' + ('' if QUICK else f'; exhaustive small: {cnt["ok"]} instances in the domain, 0 mismatches')) # ---------------------------------------------------------------- C. outside cases (informational) def run_map(T, limit=10 ** 6): """Abstract map until an outside case; returns (list of rules, last list, outside label).""" rules = [] for _ in range(limit): P, st, rule = step(T) if P is None: return rules, T, rule rules.append(rule); T = P return rules, T, None def sec_C(): print(' (o1), a 0 between two "+" reached by the scan, halts:') for T in ([0, PLUS, 0, PLUS, 20, PIPE, 14, PIPE, 8, PIPE, 22], [3, PLUS, 0, PLUS, 20, PIPE, 14, PIPE, 8, PIPE, 22], [5, PIPE, 7, PLUS, 0, PLUS, 4, PIPE, 6], [0, PLUS, 0, PLUS, 2, PIPE, 0, PLUS, 2]): U, s2 = next_dr(T, 10 ** 6) print(' ', fmt(T), '->', U if U in (None, 'HALT') else fmt(U), 'after', s2, 'steps;', step(T)[2]) rr = random.Random(5); nh = 0 for _ in range(60 if QUICK else 300): left = [rr.randint(0, 30) for _ in range(rr.randint(0, 3))] lsep = [rr.choice([PIPE, PLUS, HASH]) for _ in left] evens = [2 * rr.randint(0, 30) for _ in range(rr.randint(0, 3))] T = mk(left + [rr.randint(0, 30), 0, 2 * rr.randint(0, 30)] + evens + [2 * rr.randint(1, 40)], lsep + [PLUS, PLUS] + [PIPE] * (len(evens) + 1)) if step(T)[2] == 'out:plus x=0 left=+': nh += next_dr(T, 10 ** 7)[0] == 'HALT' print(f' random "... y + 0 + e | evens | L" (scan reaches the 0): {nh} of {60 if QUICK else 300} halt') print(' other outside cases leave the rule set without halting in one half-cycle:') for T in ([0, PIPE, 1, PLUS, 20, PIPE, 14, PIPE, 8, PIPE, 22], [0, HASH, 0, PIPE, 21, PIPE, 14, PIPE, 8, PIPE, 22], [5, PIPE, 0, HASH, 20, PIPE, 14, PIPE, 22], [5, PLUS, 0, PLUS, 21, PIPE, 14, PIPE, 22]): U, s2 = next_dr(T, 10 ** 6) print(' ', fmt(T), '->', U if U in (None, 'HALT') else fmt(U), 'after', s2, 'steps;', step(T)[2]) # a J-member that halts (proof.md 6.3): the map runs inside the rule set, then meets (o1); direct simulation halts T = [2, PLUS, 1, HASH, 2] rules, last, out = run_map(T) s = sim_from_tokens(T); s.run(10 ** 6) print(f' J-member {fmt(T)}: J {"holds" if check_J(T) is None else "fails"}; map: {", ".join(rules)}, then {out} ' f'at {fmt(last)}; direct simulation: {"HALT after %d steps" % s.steps if s.halted else "no halt"}') # the far-end race (proof.md 6.4): the same prefix, the two directions of the far region print(' far-end race at 1 + 0 | 0 | x (proof.md 6.4):') for L_ in (1201, 1200): T = [1, PLUS, 0, PIPE, 0, PIPE, 23, PIPE, 86, PIPE, 300, PIPE, L_] rules, last, out = run_map(T, 3000) ev = [r for r in rules if r != 'odd'] s = sim_from_tokens(T); s.run(2 * 10 ** 7) print(f' {fmt(T)}: J {"holds" if check_J(T) is None else "fails"}; map: first events {ev[:3]}; ' f'{"outside case " + out + " at " + fmt(last)[:30] if out else "%d half-cycles inside the rule set" % len(rules)}; ' f'direct simulation: {"HALT after %d steps" % s.steps if s.halted else "no halt in 2e7 steps"}') results['C'] = None print('[C] INFO: a 0-field between two "+" reached by the scan halts; the other outside cases leave the rule set') # ---------------------------------------------------------------- D. counter lemma def region_state(fs, L): """B bits (MSB first), N, P for a region g_1..g_n | L.""" B = []; acc = 0 for g in fs: acc ^= g & 1; B.append(acc) P = acc ^ (L & 1) N = 0 for b in B: N = 2 * N + b return B, N, P def sec_D(): ok = True # bit level, exhaustive for n <= 10: the Gray-scan step equals N -> N +/- 1 with the stated carry depth for n in range(1, 11): for bits in range(1 << (n + 1)): b = [(bits >> (n - i)) & 1 for i in range(n + 1)] # b_1..b_n, b_L fs = b[:n]; L = b[n] Bv, N, P = region_state(fs, L) if (N == 0 and P == 0) or (N == (1 << n) - 1 and P == 1): continue j = max(i for i in range(n + 1) if b[i] == 1) # 0-based; n means L if j == 0: ok = False; continue nb = list(b); nb[j - 1] ^= 1; nb[n] ^= 1 B2, N2, P2 = region_state(nb[:n], nb[n]) dep = n - 1 - (j - 1) # depth of the decremented field if P == 1: good = N2 == N + 1 and P2 == 1 and dep == ((N + 1) & -(N + 1)).bit_length() - 1 else: good = N2 == N - 1 and P2 == 0 and dep == (N & -N).bit_length() - 1 ok &= good # on the abstract map: random regions with large fields behind a '+', '#' or the far end cnt = 0 for _ in range(300 if QUICK else 2000): n = R.randint(1, 7) fs = [R.randint(2 ** n + 2, 2 ** n + 60) for _ in range(n)] L = R.randint(1, 50) left = R.choice(['far', 'plus', 'hash']) pre = [] if left == 'far' else [R.randint(5, 40), PLUS if left == 'plus' else HASH] T = pre + seq(fs + [L]) Bv, N, P = region_state(fs, L) if (N == 0 and P == 0) or (N == (1 << n) - 1 and P == 1): continue U, st, rule = step(T) fs2 = U[len(pre)::2][:n]; L2 = U[-1] B2, N2, P2 = region_state(fs2, L2) dec = [a - b for a, b in zip(fs, fs2)] v = ((N + 1) & -(N + 1)).bit_length() - 1 if P == 1 else (N & -N).bit_length() - 1 exp = [1 if (n - 1 - i) == v else 0 for i in range(n)] good = rule == 'odd' and N2 == N + (1 if P else -1) and P2 == P and dec == exp and L2 == L + 3 ok &= good; cnt += 1 report('D', ok, f'counter lemma exhaustive on bits (n <= 10) and on {cnt} random regions of the abstract map') # ---------------------------------------------------------------- E. opening runs BASES = {'A': (30379, 47), 'B': (30722, 51), 'C': (32795, 73), 'D': (32668, 71)} BASE_REST = [PIPE, 66, PIPE, 18, PIPE, 64] def opening(start, direct_limit): s = Sim('', head=0, state=start) log = [] def stop(sm): U = parse_at(sm) if U is not None: log.append((sm.steps, U)) if sm.steps >= BASES[start][0]: return True return False s.run(BASES[start][0] + 10, stop) first = log[0] base = log[-1] ok = base[0] == BASES[start][0] and base[1] == [BASES[start][1]] + BASE_REST four = [x for x in log if 4 in x[1][1::2]] # from the base: predicted D:R configurations must be the actual ones T = base[1]; t = base[0]; npred = 0; rules = Counter() target = [t] def stop2(sm): return sm.steps == target[0] and parse_at(sm) == target[1] while True: P, st, rule = step(T) if P is None or t + st > direct_limit: break target[:] = [t + st, P] hit = s.run(t + st - s.steps, stop2) if s.steps < t + st else False if not hit: ok = False print(' prediction failed at', t, fmt(T), rule) break T = P; t += st; npred += 1; rules[rule] += 1 return ok, first, four, base, npred, t, rules, T def relabel(tm, perm, mirror): """perm maps old state letter -> new letter; returns the table string in the new names.""" t = parse_tm(tm) inv = {v: k for k, v in perm.items()} out = [] for q in ST: old = inv[q] g = '' for sym in (0, 1): tr = t[(old, sym)] if tr is None: g += '---' else: w, d, nq = tr d = -d if mirror else d g += f'{w}{"R" if d == 1 else "L"}{perm[nq]}' out.append(g) return '_'.join(out) def string_map(): """Each listed string is the line-75 table renamed (and maybe mirrored) so that its start state is A.""" import itertools found = {} for st_, (line, tm) in LINES.items(): for p in itertools.permutations(ST): perm = dict(zip(ST, p)) if perm[st_] != 'A': continue for mirror in (False, True): if relabel(TM, perm, mirror) == tm: found[line] = (st_, mirror, ''.join(perm[q] for q in ST)) return found def sec_E(direct_limit): ok = True fm = string_map() for line, (st_, mirror, perm) in sorted(fm.items()): print(f' line {line}: the line-75 table started in {st_}, states renamed ABCDEF -> {perm}' f'{", mirrored" if mirror else ""}') ok &= len(fm) == 4 for st_, (line, tm) in LINES.items(): good, first, four, base, npred, t, rules, T = opening(st_, direct_limit) print(f' line {line} (start {st_}): first token configuration at step {first[0]}: {fmt(first[1])}; ' f'gap-4 configurations at steps {[x[0] for x in four]}; base K({base[1][0]}) = {fmt(base[1])} ' f'at step {base[0]}; then {npred} predicted D:R events, all exact, to step {t} ' f'({dict(rules)})') ok &= good report('E', ok, f'four opening runs reach K(c) = c | 66 | 18 | 64 with c = 47, 51, 73, 71; abstract map exact ' f'from there to {direct_limit:.0e} steps (direct simulation)') # ---------------------------------------------------------------- F. start-parametric lemma FIRST_VALUE_RULES = {'plus-farend-1', 'death-farend', 'hash-farend-0'} def sec_F(far): ok = True runs = {} for s_ in 'ABCD': T = [BASES[s_][1]] + BASE_REST; t = BASES[s_][0] seqr = [] while t < far: P, st, rule = step(T) if P is None: break seqr.append((rule, len(T))) T = P; t += st if len(seqr) % 200000 == 0 and T[0] <= 2: pass runs[s_] = seqr # the four rule sequences agree up to the first event at which some orbit's first field is consumed m = min(len(v) for v in runs.values()) agree = 0 while agree < m and len({runs[s_][agree] for s_ in 'ABCD'}) == 1: agree += 1 print(f' rule sequences of the four orbits agree for the first {agree} of {m} half-cycles up to {far:.0e}') # lemma: two token lists that differ in one field by an even amount 2e take the same rule and again differ in # one field by 2e, until the smaller one's differing field is tested by value (it is <= 1 there) pairs = 0; ends = Counter() for _ in range(100 if QUICK else 400): fs = [R.randint(0, 12) for _ in range(R.randint(2, 7))] fs[-1] = max(fs[-1], 1) ss = [R.choice([PIPE, PIPE, PLUS, HASH]) for _ in fs[1:]] T1 = mk(fs, ss); p = 2 * R.randint(0, len(fs) - 2); e = 2 * R.randint(1, 10) T2 = list(T1); T2[p] += e for _ in range(60): P1, s1, r1 = step(T1); P2, s2, r2 = step(T2) if P1 is None or P2 is None: ends['outside'] += 1; break diff = [q for q in range(len(P1)) if len(P1) == len(P2) and P1[q] != P2[q]] if r1 == r2 and len(P1) == len(P2) and len(diff) == 1 and diff[0] % 2 == 0 and P2[diff[0]] - P1[diff[0]] == e: T1, T2, p = P1, P2, diff[0]; pairs += 1 continue if r1 == r2 and P1 == P2: ends['offset absorbed'] += 1; break if T1[p] <= 1: ends['diverged at a first-value test (smaller field <= 1)'] += 1; break ok = False print(' parametric lemma fails:', fmt(T1), '|', fmt(T2), r1, r2) break else: ends['ran 60'] += 1 print(f' {pairs} paired half-cycles with one field offset by an even amount: same rule, same offset;' f' endings {dict(ends)}') ok &= agree > 1000 report('F', ok, 'start-parametric lemma (even first-field offsets) holds; orbits agree up to the first field') return runs # ---------------------------------------------------------------- G. invariant J def check_J(T): """Condition J of proof.md section 6.1 (revision 2: J3 allows a first field 0 before '+'). Returns None if J holds, else the failing clause.""" fs, ss = T[0::2], T[1::2] k = len(fs) - 1 if fs[-1] < 1 or any(f < 0 for f in fs): return 'J0 fields >= 0, L >= 1' if any(s not in (PIPE, PLUS, HASH) for s in ss): return 'J1 separators | + #' hs = [i for i, s in enumerate(ss) if s == HASH] if len(hs) > 1: return 'J2 at most one #' if hs: h = hs[0] if any(s != PIPE for s in ss[h + 1:]): return 'J2 only | right of #' if fs[h + 1] < 1: return 'J2 field right of # >= 1' if fs[h] < 1 and h != 0: return 'J2 field left of # >= 1 unless first' for i, s in enumerate(ss): if s == PLUS: if fs[i] == 0 and i != 0: return 'J3 field left of + >= 1 unless first' if fs[i] == 1 and i != 0 and ss[i - 1] != PLUS: return 'J3 a 1 left of + is first or follows +' if k >= 1 and ss[k - 1] == PLUS: return 'J4 separator left of L is | or #' if k >= 2 and fs[k - 1] == 0 and ss[k - 2] == PLUS: return 'J5 no + 0 | L' return None def legal_event_exhaustive(): """Legal-event lemma: every token list satisfying J has a rule (step(T) is not None). Exhaustive over <= 5 fields with values 0..4 and separators | + #.""" import itertools n = 0 for nf in range(1, 6 if not QUICK else 5): for fs in itertools.product(range(5), repeat=nf): for ss in itertools.product((PIPE, PLUS, HASH), repeat=nf - 1): T = mk(list(fs), list(ss)) if check_J(T) is None: n += 1 if step(T)[0] is None: print(' legal-event lemma fails at', fmt(T), step(T)[2]) return False, n return True, n def exit_class(T, rule, why): """Label a one-step exit from J by the classes (a)-(e) of proof.md 6.3.""" if rule == 'hash-odd': return 'a' if rule == 'bounce': return 'b' if rule == 'odd' and why.startswith('J2'): return 'c' if rule == 'death': return 'd' if rule == 'odd' and why.startswith('J5'): return 'e' return '?' def one_step_catalogue(): import itertools cat = {}; nj = 0 for nf in range(1, 6 if not QUICK else 5): for fs in itertools.product(range(5), repeat=nf): for ss in itertools.product((PIPE, PLUS, HASH), repeat=nf - 1): T = mk(list(fs), list(ss)) if check_J(T) is not None: continue nj += 1 P, st, rule = step(T) why = check_J(P) if why is None: continue key = (exit_class(T, rule, why), rule, why) c, ex = cat.get(key, (0, None)) if ex is None or sum(T[0::2]) < sum(e for e in map(int, ex.split()[0::2])): ex = fmt(T) cat[key] = (c + 1, ex) return cat, nj def sec_G(runs_far): ok = True for s_ in 'ABCD': T = [BASES[s_][1]] + BASE_REST; t = BASES[s_][0] nev = 0; fails = Counter(); first_fail = None; outside = None rules = Counter() while t < runs_far: bad = check_J(T) if bad: fails[bad] += 1 if first_fail is None: first_fail = (t, bad, fmt(T)[:160]) P, st, rule = step(T) if P is None: outside = (t, rule, fmt(T)[:200]); break rules[rule] += 1 T = P; t += st; nev += 1 good = not fails and outside is None print(f' line {LINES[s_][0]}: {nev} half-cycles to step {t:.4e}, {len(T) // 2 + 1} fields, ' f'J {"holds at every one" if not fails else "FAILS " + str(dict(fails)) + " first " + str(first_fail)}; ' f'outside case: {outside}; rules {dict(rules)}') ok &= good # J is not inductive (proof.md 6.3): a J-configuration that leaves J; (o5) follows three half-cycles later T = [9, PIPE, 0, PIPE, 1, PIPE, 4, PIPE, 6]; chain = [T] for _ in range(7): P_, _, r_ = step(chain[-1]) if P_ is None: chain.append(r_); break chain.append(P_) print(' J not inductive:', ' -> '.join(fmt(x) + ('' if check_J(x) is None else ' [J fails: ' + check_J(x) + ']') if isinstance(x, list) else x for x in chain)) good, n = legal_event_exhaustive() print(f' legal-event lemma (J implies a rule applies): exhaustive over {n} small token lists satisfying J:', 'ok' if good else 'FAIL') ok &= good cat, nj = one_step_catalogue() print(f' one-step exits from J (proof.md 6.3, exits (a)-(e)) over the same {nj} lists:') for (lab, rule, why), (c, ex) in sorted(cat.items(), key=lambda x: -x[1][0]): print(f' ({lab}) {c:6d} {rule:10s} -> {why:42s} e.g. {ex}') ok &= set(lab for lab, _, _ in cat) <= set('abcde') report('G', ok, f'invariant J and "every configuration has a rule" on the four abstract orbits to {runs_far:.0e}') # ---------------------------------------------------------------- H. death / dance / climb / reflection def climb_predict(T, maxstages=400): """The climb automaton of proof.md 4.5 (C5), from C2 and the stage-end events of 4.3 only. Active region g_1 | ... | g_m | L with '+' or the far end left of g_1, g_2.. even, L odd. Mode: g_1 odd -> down-run from 2^m - 1 (D); g_1 even -> up-run from 0 (U). Returns ([(half-cycles so far, predicted list, event)], end).""" fs, ss = list(T[0::2]), list(T[1::2]) k = len(fs) - 1 lo = k - 1 while lo > 0 and ss[lo - 1] == PIPE: lo -= 1 h = 0; out = [] for _ in range(maxstages): m = k - lo if not (all(f % 2 == 0 for f in fs[lo + 1:k]) and fs[k] % 2 == 1): return out, 'not a climb region' mode = 'D' if fs[lo] % 2 else 'U' if mode == 'U' and fs[lo] == 0: nst = (1 << (m - 1)) - 1 # up-run to the first carry into g_1 = 0 for u in range(m - 1): fs[k - 1 - u] -= 1 << (m - 2 - u) fs[k] += 3 * nst; h += nst if any(f < 0 for f in fs[lo:k]): return out, 'death-in-stage' if lo == 0: del fs[0]; del ss[0]; k -= 1; fs[k] += 3; h += 1 out.append((h, mk(fs, ss), 'death-farend')); continue if m >= 2 and ss[lo - 1] == PLUS: y = fs[lo - 1]; j = fs[lo + 1] fs[lo - 1:lo + 2] = [y + j + 1]; del ss[lo - 1:lo + 1]; k -= 2; lo -= 1; fs[k] += 3; h += 1 out.append((h, mk(fs, ss), 'death-merge')) if lo > 0 and ss[lo - 1] != PLUS: return out, 'complete' continue return out, 'outside' nst = (1 << m) - 1 for u in range(m): fs[k - 1 - u] -= 1 << (m - 1 - u) fs[k] += 3 * nst; h += nst if any(f < 0 for f in fs[lo:k]): return out, 'death-in-stage' if lo == 0: return out, 'far end: overflow-%s next' % ('even' if mode == 'D' else 'odd') if ss[lo - 1] != PLUS: return out, 'complete' z = fs[lo - 1]; zl = ss[lo - 2] if lo >= 2 else None if mode == 'D': if z >= 2: fs[lo - 1] -= 2; ss[lo - 1] = PIPE; lab = 'plus' elif z == 1 and zl is None: del fs[0]; del ss[0]; k -= 1; lo -= 1; fs[k] += 3; h += 1 out.append((h, mk(fs, ss), 'plus-farend-1')); continue elif z == 1 and zl == PLUS: y = fs[lo - 2]; g1 = fs[lo] fs[lo - 2:lo + 1] = [y + g1 + 1]; del ss[lo - 2:lo]; k -= 2; lo -= 1; lab = 'plus-merge-1' elif z == 0 and zl is None: return out, 'far0plus-even next' else: return out, 'outside' else: if z >= 1: fs[lo - 1] -= 1; fs[lo] -= 1; ss[lo - 1] = PIPE; lab = 'odd-plus' elif zl is None: return out, 'far0plus-odd next' else: return out, 'outside' lo -= 1; fs[k] += 3; h += 1 out.append((h, mk(fs, ss), lab)) if lo > 0 and ss[lo - 1] != PLUS: return out, 'complete' return out, 'maxstages' def climb_check(T, seq=None): """Compare climb_predict(T) with the abstract map, half-cycle by half-cycle (seq: the map's own lists after T, if known). Returns (status, number of stage ends matched, predicted events, end).""" pred, end = climb_predict(T) cur = T; h = 0; nst = 0; last = None for (hp, Tp, lab) in pred: while h < hp: if seq is not None: if h >= len(seq): return 'short', nst, pred, end last, cur = seq[h] else: P_, st_, last = step(cur) if P_ is None: return 'outside ' + last, nst, pred, end cur = P_ h += 1 if h < hp and last != 'odd': return ('nested ' if last.startswith('death') else 'MISMATCH unpredicted ') + last, nst, pred, end if cur != Tp or last != lab: return 'MISMATCH at %d: %s %s vs %s %s' % (h, last, fmt(cur)[:60], lab, fmt(Tp)[:60]), nst, pred, end nst += 1 return 'ok', nst, pred, end def region_of(fs, ss, idx): """First index of the region that contains field idx.""" lo = idx while lo > 0 and ss[lo - 1] == PIPE: lo -= 1 return lo def sec_H(far): """C4 (dance), C5 (climb automaton) and C6 (reflection, both branches) on the four orbits to `far`, plus random climbs with singletons equal to 1.""" ok = True REPAIR = {'bounce', 'overflow-even', 'overflow-odd', 'far0plus-even'} tot = Counter(); c6 = Counter(); ends = Counter(); branch = Counter() for s_ in 'ABCD': T = [BASES[s_][1]] + BASE_REST; t = BASES[s_][0] hist = [] while t < far: P, st, rule = step(T) if P is None: break hist.append((rule, T, P)) T = P; t += st seqs = [(r, P) for r, _, P in hist] for i, (rule, T0, T1) in enumerate(hist): if rule in REPAIR: st_, n, pred, end = climb_check(T1, seqs[i + 1:]) tot['climbs'] += 1; tot['stage ends'] += n labs = [lab for _, _, lab in pred[:n]] if 'plus-merge-1' in labs or 'odd-plus' in labs: branch['U-branch (a singleton 1 or prefix met in mode U)'] += 1 if st_.startswith('MISMATCH'): ok = False; print(' climb mismatch after', rule, fmt(T1)[:100], st_) elif st_.startswith('nested'): tot['nested death inside the climb'] += 1 elif st_ == 'ok': ends[end] += 1 if rule != 'death' or s_ != 'A': continue # C4: the dance of an interior death on line 75 fs, ss = T0[0::2], T0[1::2] j = max(q for q in range(len(fs)) if fs[q] % 2 == 1) p = j - 1; w = len(fs) - 2 - p lo = region_of(fs, ss, p) Bv, N, Pp = region_state(fs[lo:-1], fs[-1]) h_ = T1[1::2].index(HASH) B1, N1, P1 = region_state(T1[0::2][h_ + 1:-1], T1[-1]) good = N1 == 2 ** w - 1 and P1 == 0 expect = ['odd'] * (2 ** w - 1) + ['hash-odd'] + ['odd'] * (2 ** w - 1) + ['bounce'] got = [r for r, _, _ in hist[i + 1:i + 1 + len(expect)]] if len(got) < len(expect): continue if got != expect: q_ = next(q for q in range(len(expect)) if got[q] != expect[q]) if expect[q_] == 'odd' and got[q_].startswith('death'): tot['nested death inside the dance'] += 1; continue ok = False; print(' dance mismatch', fmt(T0)[:100]); continue tot['dances'] += 1 # C6: follow the climb after the bounce to the event on a (index p - 1), compare with both branches qb = i + len(expect) # index of the bounce in hist a0 = fs[p - 1] st_, n, pred, end = climb_check(hist[qb][2], seqs[qb + 1:]) if st_ != 'ok': c6['climb not completed (' + st_.split()[0] + ')'] += 1; continue hit = None for (hp, Tp, lab) in pred[:n]: if Tp[0::2][p - 1] != a0 - 1 or len(Tp) // 2 < p: hit = (hp, Tp, lab); break if hit is None: c6['nested death inside the climb' if end == 'death-in-stage' else 'event on a not reached'] += 1 continue hp, Tp, lab = hit fs2, ss2 = Tp[0::2], Tp[1::2] lo2 = region_of(fs2, ss2, p - 1) B2, N2, P2 = region_state(fs2[lo2:-1], fs2[-1]) H = Bv[:p - 1 - lo] if lab == 'plus': # D-end: a - 3, a's bit flipped, direction reversed exp_bits = H + [Pp] * (w + 2); exp_P = 1 - Pp; exp_a = a0 - 3 elif lab == 'odd-plus': # U-end: a - 2, a's bit kept, direction kept exp_bits = H + [1 - Pp] * (w + 2); exp_P = Pp; exp_a = a0 - 2 else: c6['other end event ' + lab] += 1; continue good &= (lo2 == lo and B2 == exp_bits and P2 == exp_P and fs2[p - 1] == exp_a) c6[('D-end (reversed)' if lab == 'plus' else 'U-end (kept)')] += 1 if not good: ok = False; print(' C6 fails at', fmt(T0)[:100], lab, B2, exp_bits, P2, exp_P) # random climbs, singletons of value 1 included, and the reviewer's reproducer rr = random.Random(3); rnd_res = Counter() for it in range(400 if QUICK else 3000): r = rr.randint(1, 6) sg = [2 * rr.randint(0, 3 if rr.random() < 0.3 else 60) + 1 for _ in range(r)] sg[-1] = 2 * rr.randint(20, 400) + 1 W = rr.choice([[rr.randint(5, 50), PIPE, rr.randint(0, 9)], [1], [], [rr.randint(3, 30), PLUS, rr.randint(0, 9)]]) fs = (W[0::2] if W else []) + sg + [1] ss = (W[1::2] if W else []) + ([PLUS] if W else []) + [PLUS] * (r - 1) + [PIPE] st_, n, pred, end = climb_check(mk(fs, ss)) rnd_res['mismatch' if st_.startswith('MISMATCH') else 'ok'] += 1 if any(lab == 'plus-merge-1' for _, _, lab in pred[:n]): rnd_res['with PLUS-MERGE-1'] += 1 if any(lab == 'death-merge' for _, _, lab in pred[:n]): rnd_res['with a singleton 1 met in mode U'] += 1 ok &= rnd_res['mismatch'] == 0 T = [9, PLUS, 5, PLUS, 1, PLUS, 7, PLUS, 5, PIPE, 1] st_, n, pred, end = climb_check(T) print(f' reproducer {fmt(T)}: {st_}; events {[lab for _, _, lab in pred[:n]]}, then {end}') ok &= not st_.startswith('MISMATCH') print(f' re-pairings on the four orbits to {far:.0e}: {dict(tot)}; {dict(branch)}; climb ends {dict(ends)}') print(f' C6 on line 75 deaths whose dance and climb complete: {dict(c6)}') print(f' random climbs: {dict(rnd_res)}') report('H', ok, 'C4 dance, C5 climb automaton (both modes, stage by stage, exact lists) and C6 (D-end reversed, ' 'U-end kept) on the orbits; random climbs with singletons 1') # ---------------------------------------------------------------- I. fast exact map (counter-lemma jumps) def jump(T): """Apply the maximal run of ODD half-cycles of the active region that hits no zero field (C1/C2). Returns (T', half-cycles, exact machine steps).""" fs, ss = list(T[0::2]), list(T[1::2]); k = len(fs) - 1 lo = region_of(fs, ss, k) n = k - lo if n <= 0: return T, 0, 0 Bv, N, P = region_state(fs[lo:k], fs[k]) run = (1 << n) - 1 - N if P == 1 else N if run <= 0: return T, 0, 0 def kth(u, kk): m = 1 << (u + 1); hh = 1 << u if P == 1: x0 = N + 1 + ((hh - (N + 1)) % m) return x0 + (kk - 1) * m - N x0 = N - ((N - hh) % m) return N - (x0 - (kk - 1) * m) + 1 def cnt(u, A, B_): return (B_ >> u) - (B_ >> (u + 1)) - ((A >> u) - (A >> (u + 1))) s = run for i in range(lo, k): tt = kth(k - 1 - i, fs[i] + 1) if tt <= s: s = tt - 1 if s <= 0: return T, 0, 0 A, Bv_ = (N, N + s) if P == 1 else (N - s, N) steps = 6 * (s * fs[k] + 3 * s * (s - 1) // 2) cv = [cnt(v, A, Bv_) for v in range(n)] steps += sum(c * (12 * (v + 1) + 12) for v, c in enumerate(cv)) for u in range(n): fu = fs[k - 1 - u]; M = 1 << (u + 1) cm = (Bv_ // M) - (A // M) if cm > 0: c0 = cnt(u, A, (A // M + 1) * M - 1) if P == 1 else cnt(u, (Bv_ // M) * M, Bv_) steps += 6 * (cm * fu - (cm * c0 + cm * (cm - 1) // 2)) for v in range(n): fs[k - 1 - v] -= cv[v] fs[k] += 3 * s return mk(fs, ss), s, steps def fast_run(T, max_steps, log=None): t = 0; h = 0 while t < max_steps: T2, s, st = jump(T) if s: T = T2; h += s; t += st if t >= max_steps: break P, st, rule = step(T) if P is None: return T, h, t, rule if log is not None and rule != 'odd': log.append((h, t, rule)) T = P; h += 1; t += st return T, h, t, None def sec_I(far_fast, cross): """The fast map equals the plain map event for event (cross-check to `cross` steps), and the four orbits meet no outside case up to `far_fast` steps.""" ok = True for s_ in 'ABCD': T = [BASES[s_][1]] + BASE_REST; t = 0; h = 0; ev = [] while t < cross: P, st, rule = step(T) if rule != 'odd': ev.append((h, t, rule)) T = P; t += st; h += 1 log = [] fast_run([BASES[s_][1]] + BASE_REST, cross, log) same = log[:len(ev)] == ev ok &= same log = [] T, h, t, out = fast_run([BASES[s_][1]] + BASE_REST, far_fast, log) ok &= out is None print(f' line {LINES[s_][0]}: fast map = plain map on all {len(ev)} non-ODD events to {cross:.0e} steps: ' f'{same}; to {t:.3e} steps ({h:.3e} half-cycles): outside case {out}, {len(T) // 2 + 1} fields, ' f'{len(log)} non-ODD events; first fields {fmt(T)[:60]}') report('I', ok, f'fast exact map (C1/C2 jumps) cross-checked to {cross:.0e}; no outside case on the four orbits to ' f'{far_fast:.0e} steps') def main(): t0 = time.time() direct = float(arg('--direct', 3e6 if QUICK else 3e7)) far = float(arg('--far', 1e11 if QUICK else 1e13)) sec_A(); sec_B(); sec_C(); sec_D(); sec_E(direct); sec_F(far); sec_G(far); sec_H(min(far, 1e13)) sec_I(float(arg('--fast', 1e40 if QUICK else 1e100)), min(far, 1e11)) need = ['A', 'B', 'D', 'E', 'F', 'G', 'H', 'I'] verdict = all(results.get(s) for s in need) print('SUMMARY:', 'PASS' if verdict else 'FAIL', {s: results.get(s) for s in need}, f'{time.time() - t0:.0f} s') if __name__ == '__main__': main() |