[TS] Measure paired source coverage and search cost

[CaelmBleidd]

Summary

• Add a 30-second paired coverage experiment for the four frozen unknown-call policies using CLOSEST_TO_UNCOVERED_RANDOM.
• Freeze a c8 original-TypeScript statement universe once per function, replay candidates emitted within the search budget, and record coverage numerator/denominator, symbolic steps, and separate preparation, search, replay, and cell times.
• Exclude imports erased by TypeScript when they are used only as types from the runtime source closure. This admits the two previously rejected Thinkmill--emery functions and prevents six other functions from counting type-only files in their denominator.

Validation

• Fast-check adapter: 78/78 tests passed, including the new erased-import regression.
• Updated clean runner at eec98e937f7093da2d8368d59d960abb52a2a879; 13/13 pilot cells and 4/4 pilot universes passed independent validation with no tool, extraction, or replay errors.
• All 264 Z3 full-matrix coverage universes were generated and independently checked against the source manifest and closure scan; every denominator is nonzero. The user stopped the Z3 campaign after 76 terminal cells to run a separate Yices remeasurement. The Z3 prefix is preserved and excluded from the Yices estimates.

Measurement boundary

The 30-second budget is checked between symbolic steps. A diagnostic Z3 call on symbolic floating-point remainder took 165–177 seconds despite the five-second SMT setting. The checkpoint excludes candidates after 30 seconds; actual search time and overrun counts are retained. An isolated Yices comparison on that one function completed in about 0.24 seconds, but it is not part of the paired Z3 matrix.

This PR is stacked on #415. It changes measurement and source-closure handling; it does not change the four unknown-call policies. The Yices solver selection and complete remeasurement are in the next stacked PR.