feat(streaming): Count-Min sketch with fixed-query accuracy #1201

Start the streaming/sketching direction with an executable insertion-only Count-Min sketch and its fixed-query accuracy theorem.

Scope: natural-number weighted updates; positive row and bucket counts; exact update/concatenation/merge invariants for the same hash bank; no underestimation; independently sampled universal-hash rows; an explicit additive-error/failure bound (in particular width * epsilon >= 2 gives failure at most 2^(-depth)). Reuse the existing universal-hashing, finite probability, and concentration APIs.

The source is Cormode–Muthukrishnan, “An Improved Data Stream Summary: The Count-Min Sketch and its Applications,” Section 3 and Section 4.1, Theorem 1:
https://www.cs.ox.ac.uk/people/graham.cormode/pubs/papers/cm-full.pdf
The source theorem bounds a point estimate between its true frequency and that frequency plus epsilon times total mass, with probability at least 1-delta. The stream and queried item are fixed independently of the sampled hashes. Our initial stream model is insertion-only.

Acceptance: checked Lean statements for deterministic correctness and probability, a concrete instantiated hash family/example, meaningful tests covering collisions and updates, explicit counter/seed representation scope, source attribution, and the repository validation gates. Runtime/space claims must describe the representation actually proved.

This is the first milestone of a broader streaming program. Communication lower-bound transfer, CountSketch/AMS, heavy hitters, and turnstile extensions remain separate follow-ups. The wider direction is not completed by this milestone.

Owner: worker-chatgpt-streaming-cb399a98, branch feat/streaming-count-min-cb399a98. AI-assisted implementation and agent review; maintainer/coordinator review required before merge.