Current state

Zip/Native/Gzip.lean GzipDecode.decompress processes concatenated
gzip members in a bounded loop (for _ in [:1000]) and, if the input
contains more than 1000 members, throws the exact message:

"Gzip: too many concatenated members"

This is a resource-safety (zip-bomb) guard against pathological
many-tiny-member inputs. It is not triggered by any current test:
the multi-member tests (ZipTest/NativeGzip.lean, ZipTest/Gzip.lean)
only build 2–4 members, and #2577 (maxOutputSize small-cap rejection)
exercises the orthogonal output-size cap, not the member-count cap.

Deliverables

1. A deterministic regression test (in ZipTest/NativeGzip.lean, or a
   small new module if cleaner) that:
   • Builds a concatenation of 1001 minimal valid gzip members
     (e.g. each the gzip encoding of an empty or 1-byte payload via
     Zip.Native.Gzip.compress) in memory.
   • Asserts Zip.Native.GzipDecode.decompress fails with the exact
     substring "too many concatenated members".
   • Includes a passing boundary companion: exactly 1000 members
     still decode successfully (concatenated payload round-trips), so the
     test pins the cap boundary, not just the failure.
2. Register the module in ZipTest.lean if a new module is added.

Keep the per-member payload tiny so the 1001-member stream stays small
(~20 KB in memory, never written to disk).

Context

• Guard site and member cap: Zip/Native/Gzip.lean decompress,
  for _ in [:1000] loop; the post-loop throw "Gzip: too many concatenated members" fires only when the loop exhausts without
  consuming all input.
• The loop is a Std.Legacy.Range.forIn' (opaque loop✝); this is a
  test-only issue — no proof obligation, so the opaque-loop caveat in
  CLAUDE.md does not apply here. Do not refactor the implementation.
• Distinct from: test: native-decoder maxOutputSize enforcement regression suite (GzipDecode/ZlibDecode/Inflate small-cap rejection + n-1 boundary + exact-fit; FFI limit already tested, native paths untested) #2577 (output-size cap), test: adversarial fuzz target for gzip member decode (FuzzGzip.lean — malformed/truncated/field-mutated header+optional-fields+CRC32/ISIZE trailer; native GzipDecode.decompress must reject cleanly, native⊆FFI) #2584 (gzip header/trailer
  fuzz), test: targeted native gzip+zlib container framing/trailer-guard regression suite (bad magic / unsupported CM / FDICT / 31-check / CINFO / truncated header+trailer / CRC32+ISIZE+Adler32 mismatch; exact-message assertions, ZipTest/FramingGuards.lean — message-pinning complement to accept/reject fuzz #2584/#2585) #2590 (gzip/zlib framing/trailer guard message-pinning). This
  pins the member-count cap, which none of those cover.
• Use the error-wording-catalogue skill to confirm the match substring.

Verification

• lake build and lake exe test pass (from project root; NixOS uses
  the nix-shell --run wrapper).
• The 1001-member case fails with the asserted substring; the 1000-member
  case succeeds and round-trips to the concatenated payload.
• grep -rc sorry Zip/ unchanged (0).