perf(explore): drop the hash3 singleton probe at the deep lazy levels (L7/L8)

[kim-em]

Drop the hash3 singleton probe at the deep lazy levels

The dual hash4 + hash3 finder (hash3Single/hash3Probe, #2742) was added so short (length-3) matches that the 4-byte-keyed chains miss still get found — worth +7.4% on x-ray at shallow depth. But at L7's chain-256 and L8's chain-512, the hash4 chain is already deep enough that most length-3 candidates surface anyway, so the extra per-position hash3 hash + singleton read + hash3Probe verify may be pure overhead there.

Plan (measurement-first)

1. Gate the hash3 consult on level ≤ 7 (or ≤ 6) in the lazy matcher; measure ratio delta and matcher ms at L7/L8 on both a text and a binary member.
2. Keep whichever level cutoff clears a real speed win at negligible ratio cost.

Pure heuristic — the chain is re-verified at emission, so this is re-threading only. Cheap spike; likely noise on ratio, measurable on speed.

🤖 Prepared with Claude Code

[kim-em]

While re-gridding the L6-L8 ladder for #2785 I checked whether this was worth folding in, and hit a premise problem: the hash3 singleton probe is not consulted in the L7/L8 lazy matcher, so there is nothing to gate there.

hash3Single / hash3Probe (Zip/Native/Deflate.lean) are referenced only in Zip/Native/DeflateParse.lean (buildCache, lines ~264/319/322) — the L9/L10 candidate-cache DP build. The L7/L8 lazy chain matcher (lz77ChainLazyIterPMerged) uses lz77Greedy.hash3, which is the 4-byte chain hash, a different function from the 3-byte singleton table. The existing docstring says as much:

The L1–L8 chain matchers deliberately do not probe the singleton (Deflate.lean#L833)

So "gate the hash3 consult on level ≤ 7 in the lazy matcher" has no target in current code — the #2742 singleton was only ever wired into the DP cache, not the lazy tier. This issue likely predates that scoping, or conflates the two hash3es.

Suggest re-scoping before claiming: either (a) close as already-the-case (L7/L8 lazy already skips the singleton), or (b) redirect at the real cost — whether the L9/L10 buildCache should drop the hash3 singleton probe, which is a different (and slower-tier) measurement.

Not folded into #2785 (which is a pure-constant re-grid; mixing a matcher-path change would muddy attribution, and #2785's plan says it should land first to re-baseline the structural bets anyway).