=== Lemma path: random paths, exact rationals ===
failures: 0

=== Proposition red, finite windows with frozen end hubs ===
windows checked: 84, agreeing with the chain reduction: 84, max free vertices 11

=== Lemma chain: boundaries of finite hub sets ===
distinct boundaries: 1024  even subsets of 11 bonds: 1024  each boundary from exactly one A: True
mismatches between 'all even T' and 'k0 is the argmin': 0

=== EVIDENCE: Theorem A chains, U(-1,1), K_k = U_1+..+U_{2m}-m ===
m_k=(|k|+1)^3 (window, argmin |K_k|, min): [(100, -1, 0.00348), (300, -1, 0.00348), (1000, -1, 0.00348), (3000, -1, 0.00348)]
m_k=(|k|+1)^2 (window, argmin |K_k|, min): [(100, -2, 0.01446), (300, -2, 0.01446), (1000, -2, 0.01446), (3000, -2, 0.01446)]
m_k=|k|+1 (window, argmin |K_k|, min): [(100, 48, 0.02462), (300, -298, 0.00592), (1000, -298, 0.00592), (3000, -298, 0.00592)]
Note: for m_k=(|k|+1)^2 the divergence of sum m_k^{-1/2} is logarithmic, so windows of size 3000 cannot exhibit inf=0; this evidence is only meaningful in the convergent case.
