nx_zstd_seqdec_gate.nx

nx_zstd_seqdec_gate.nx -- proves zstd's repeat-offset machine and sequence loop. The repeat-offset rules are pure logic with no bitstream involved, so they can be proven EXHAUSTIVELY -- and they are the part of zstd most likely to be subtly wrong, because the spec's behaviour is genuinely surprising: T2 pins the ZERO-LITERAL SLIDE. With literals the mapping is 1->rep1, 2->rep2, 3->rep3. WITHOUT literals it slides: 1->rep2, 2->rep3, and 3->rep1 MINUS ONE BYTE. That last case is not a repeat at all. A decoder missing it is correct until the first zero-literal sequence and wrong forever after -- and those are common in exactly the repetitive data zstd is best at, so it fails on the files that matter. T3 pins that Offset_Value 1 WITH literals does NOT reorder the history, while every other repeat case moves the used value to the front. Reordering on that one too looks harmless and silently desynchronises from the encoder. T4 pins that idx 1 leaves Repeated_Offset3 untouched while idx 2 and 3 shift it -- the asymmetry inside the reorder itself. license_tier: ORIGINAL