[TS PBT] Select bounded scalar guidance and retain exclusion evidence

[CaelmBleidd]

Scalar inference now has a separate bounded selection step before USVM. selectScalarGuidance(inference, compiled = ..., maxCandidates = 16) returns the original inference unchanged, candidate relations with explicit relevance, and every excluded relation with its reason and original evidence.

Selection removes unsampled evidence, exact duplicate comparisons, symmetric equality duplicates, existing domain-implied facts, and a known direct original check. For the retained compiler-owned numeric local capture, an original === also excludes both weaker <= orders over the same operands; an original <= retains the stronger equality. Known identity requires the same property, reproduced retained DSL compiler output, the selected source hash and both exact capture operands. Changed source/program/capture metadata or relabeled points leave relevance UNKNOWN.

KNOWN_DSL_CHECK identifies the direct check only; it does not prove the sampled relation or executable body. Plain TypeScript relevance stays UNKNOWN, and the campaign owns whether explicitly selected unknown relevance may guide search. Same-point comparisons that may encounter NaN remain candidates. Tautology classification reuses already established domain facts from #544 instead of adding another domain proof engine.

Review scope

6 files, +297/-21. The existing compiler-output reproduction check moves internally from the symbolic binder to its DSL owner so binding and selection share the same rule. The only prerequisite is #584 at 5ed777d27; this PR does not inherit #590 or change any search, selector, random generation, deadline or replay loop.

This supplies the remaining bounded selection behavior in #397. The campaign consumer in #399 composes it with the existing entry/result refuters and ordinary property/coverage search.

Validation

• 41 focused Kotlin tests passed: inference/domain filtering and the compiler-owned local binder, including actual native PBT observations and the real frontend.
• Seven new tests cover candidate limits, empty/finite/contradictory evidence, preserved exclusions, symmetric equality without temporal alias merging, NaN-capable reflexivity, stronger equality versus the original order, weaker orders versus original equality, and invalid retained identity/source metadata.
• Strict Detekt passed for all changed Kotlin files; diff checks passed.

Executable-build status remains UNVERIFIED. No experiment or benchmark campaign was run.