# Independent from-scratch verifier. Song 011111: lighthouse d(t)=0 if t%6==0 else 1.
# Echo trace: e(6n)=u_n (free), e(6n+1..6n+4)=0, e(6n+5)=1.
# Inverse rule: a[k+1][t] = a[k][t+1] XOR (a[k][t] OR a[k-1][t]).
def trace(u):
    e=[]
    for n,un in enumerate(u):
        e += [un,0,0,0,0,1]
    return e
def columns(u, depth):
    e=trace(u); T=len(e)
    a=[[0 if t%6==0 else 1 for t in range(T)], e]          # a[0]=lighthouse, a[1]=e
    for k in range(1,depth):
        prev,cur=a[k-1],a[k]
        a.append([cur[t+1]^(cur[t]|prev[t]) for t in range(len(cur)-1)])
    return a
def b(u,k): return columns(u,k)[k][0]                       # starting lantern k
def force(prefix, total):
    u=list(prefix)
    while len(u)<total:
        n=len(u)                                            # u_n enters starting lantern 6n+1
        cands=[v for v in (0,1) if b(u+[v],6*n+1)==0]
        assert len(cands)==1, "forcing must be unique (triangularity)"
        u.append(cands[0])
    return u
P=["0000010111010001","0100010111010001","1000010111010001","1100010111010001"]
U=[force([int(c) for c in s], 26) for s in P]
print("claim A  forced bits u16.. identical for all four:", all(x[16:]==U[0][16:] for x in U))
rows=[[b(x,k) for k in range(1,151)] for x in U]
print("claim B  every survivor has b_77..b_98 all dark:", all(all(r[k-1]==0 for k in range(77,99)) for r in rows))
print("         and b_99 lit (eliminated there):", [r[98] for r in rows])
cols=[columns(x,60) for x in U]
def win(c,k): return tuple(c[k][t] for t in range(7))      # nights 0..6 at depth k
for i,(k1,k2) in ((2,(4,5)),(1,(47,48)),(3,(47,48))):
    ok=win(cols[0],k1)==win(cols[i],k1) and win(cols[0],k2)==win(cols[i],k2)
    print(f"claim C  prefix {i+1} vs 1: windows (nights 0-6) agree at depths {k1},{k2}: {ok}")
same_after=all(all(rows[i][k]==rows[0][k] for k in range(47,150)) for i in range(4))
print("check    starting rows identical at every lantern 48..150:", same_after)