Guide one USVM phase with bounded empirical relation challenges

[CaelmBleidd]

One PBT phase can now guide the subsequent USVM phase with explicitly selected empirical numeric relations. The typed opt-in retains CompiledDslProperty for compiler-owned local results; plain entry pairs require explicit permission to use UNKNOWN relevance. Infer and select once from the retained PBT snapshot, challenge each selected relation at most once using the existing entry/local refuters, and confirm or shrink candidates through the existing complete original oracle.

Auxiliary work has a bounded allocation and leaves a positive reserve for the unrestricted original-property query. The existing covered-edge policy remains unchanged. A refuted hypothesis whose original property holds stays separate from a named original-property violation. Artifacts retain the complete inference and excluded evidence, decisions, binding/capability diagnostics, exact inputs and manifest/source identity, timely native receipts, and phase costs. Ordinary campaigns keep their defaults. No DSL IR serialization, second random generation phase, persistent cache or new selector is added.

The optional coverage step of witness confirmation reuses the existing fixed-input replay, so source-qualified admitted evidence is retained rather than losing its identity.

Depends on the exact composition in #602 (5cba39961). Related to #399.

Validation: 67 focused Kotlin campaign/refuter/inference/export tests and 235 Node adapter tests passed on the composition. The six new public campaign cases cover a 417 local refutation with a passing original property, original named-fault priority, a tiny auxiliary timeout, unsupported prefixes, insufficient observations, and explicit UNKNOWN opt-in. Ordinary external-witness regression tests and the final source-qualified native-evidence tests passed. Main/test Detekt passed with zero findings on the final sources. These are functional integration checks, not evidence of experimental benefit.

First-fault behavior: a timely original-property violation confirmed while challenging a relation stops further relation attempts, skips the redundant original query, and is available in canonical result.confirmation with its original named checkId. The original query keeps its reserved allocation whenever no such fault has been confirmed. A public regression retains two eligible sampled candidates but observes exactly one auxiliary attempt after the first confirmed original fault.