W7-1 abstract runs (evidence for proof.md §5.2 and §6.4)
Scripts: work/proof_runs/ (scratch copies). absmap.py is the scratch version of step() in check_proof.py: it lacks PLUS with x = 2 and the j != L guard of DEATH-MERGE. Neither situation arose in these runs (no UNKNOWN event; the one DEATH-MERGE has j != L).
1. Oracle-checked runs to 1e13 (accel2.py)
ODD and PLUS steps are applied by the abstract map; every other event is run on the real TM (C core, tools/sim) from the rebuilt tape and compared with the abstract map (tokens and exact steps).
| line | start | steps | half-cycles | TM-run events | mismatches against check_proof.py step() |
|---|---|---|---|---|---|
| 75 | A | 1.0000e+13 | 2,208,665 | 158 | 2 (the two opening gap-4 events, outside cases o5/o8 before the base) |
| 597 | B | 1.0000e+13 | 2,208,668 | 161 | 2 (the two opening gap-4 events, outside cases o5/o8 before the base) |
| 265 | C | 1.0000e+13 | 2,208,676 | 161 | 2 (the two opening gap-4 events, outside cases o5/o8 before the base) |
| 179 | D | 1.0000e+13 | 2,208,676 | 162 | 2 (the two opening gap-4 events, outside cases o5/o8 before the base) |
2. Abstract-map runs from K(c) to 1e16 (analyze2.py)
No outside case on any of the four orbits.
| line | half-cycles | fields at 1e16 | rule counts | first-field prefix shapes at non-ODD events | margins |
|---|---|---|---|---|---|
| 75 | 68,096,601 | 25 | odd 68095979, plus 435, death 40, hash-odd 39, bounce 39, odd-plus 28, overflow-even 16, overflow-odd 9, plus-farend-1 7, death-farend 5, plus-merge-1 2, hash-farend-0 1, death-merge 1 | 1 + 295, (none) 196, 1 + 1 + 85, 0 | 30, 1 + 0 | 7, 1 + 0 | 1 | 5, 1 + 1 + 3 | 1, 1 + 0 | 0 | 1, 0 | 0 | 1, 0 # 1 |
death b >= 29, hash-odd a >= 6, bounce a >= 5, PLUS x >= 5, ODD-PLUS d >= 1 |
| 597 | 67,915,198 | 26 | odd 67914577, plus 438, death 40, hash-odd 40, bounce 40, odd-plus 24, overflow-even 14, overflow-odd 10, plus-farend-1 8, death-farend 6, plus-merge-1 1 | 1 + 247, (none) 226, 1 + 1 + 61, 1 + 3 + 51, 0 | 21, 1 + 0 | 13, 0 | 3 | 1, 2 | 1 |
death b >= 29, hash-odd a >= 6, bounce a >= 5, PLUS x >= 3, ODD-PLUS d >= 1 |
| 265 | 71,865,805 | 26 | odd 71865191, plus 427, death 42, hash-odd 42, bounce 42, odd-plus 23, overflow-even 15, plus-farend-1 9, overflow-odd 8, death-farend 5, plus-merge-1 1 | 1 + 337, (none) 183, 1 + 1 + 61, 0 | 21, 1 + 0 | 12 |
death b >= 29, hash-odd a >= 6, bounce a >= 5, PLUS x >= 5, ODD-PLUS d >= 1 |
| 179 | 71,865,805 | 26 | odd 71865191, plus 427, death 42, hash-odd 42, bounce 42, odd-plus 23, overflow-even 15, plus-farend-1 9, overflow-odd 8, death-farend 5, plus-merge-1 1 | 1 + 337, (none) 183, 1 + 1 + 61, 0 | 21, 1 + 0 | 12 |
death b >= 29, hash-odd a >= 6, bounce a >= 5, PLUS x >= 5, ODD-PLUS d >= 1 |
Final configurations at 1e16:
- line 75:
1 + 102 | 2291 | 7641 | 12843 | 32183 | 28866 | 51781 | 19478 | 212965 | 374813 | 35639 | 188853 | 29540 | 899601 | 1637660 | 890529 | 9613307 | 10652555 | 8162056 | 2900946 | 12302489 | 15322246 | 30677023 | 42138061 - line 597:
1 + 109 + 255 | 2005 | 7616 | 12790 | 32079 | 28660 | 51367 | 18651 | 211308 | 371502 | 29018 | 175612 | 3052 | 846628 | 1531720 | 678643 | 9189536 | 13999313 | 3321238 | 19322547 | 1078444 | 4276018 | 44269459 | 36373093 - line 265:
1 + 17 + 101 + 246 | 1987 | 7577 | 12714 | 31926 | 28355 | 50760 | 17436 | 208876 | 366638 | 19291 | 156154 | 804663 | 1447786 | 510776 | 8853804 | 13327847 | 1978304 | 16636680 | 41844052 | 21012207 | 14777432 | 21636271 - line 179:
1 + 15 + 101 + 246 | 1987 | 7577 | 12714 | 31926 | 28355 | 50760 | 17436 | 208876 | 366638 | 19291 | 156154 | 804663 | 1447786 | 510776 | 8853804 | 13327847 | 1978304 | 16636680 | 41844052 | 21012207 | 14777432 | 21636271
3. Divergence of the four orbits (Lemma SP)
Compared at non-ODD events, up to one field differing by an even amount:
- 75 vs the others: agree on 490 non-ODD events; first difference at 5.98e14 (75: far-end
0 | 0 | 117 ..., DEATH at depth 21 next to a 0 first field, then HASH-FAR-0 at 7.07e14). - 597 vs 265/179: agree on 544 non-ODD events; first difference at 2.13e15 (597: DEATH-FAR
0 | 109 | ...). - 265 vs 179: agree on all 614 non-ODD events to 1e16 (first fields differ by 2).
4. Far-end probe (farprobe.py, data/farprobe.out)
Prefixes of 1-3 fields (values 0..3, separators | + #) in front of 20 | 14 | 8 | 22 (all even) or 21 | 14 | 8 | 22 (first bulk field odd): 3,768 cases; 2,847 match the map; 921 are outside cases (o1)-(o8), of which 60 halt, every one of them with a 0-field between two + reached by the scan (o1).