[TS PBT] Infer bounded numeric hypotheses once from PBT observations #397

Scope agreed on 2026-10-16

One concrete PBT generation phase is followed by one USVM search phase. No return to random generation is required. Concrete replay and optional shrinking validate a USVM candidate; they are not a second PBT generation phase. This replaces the previous repeated-round acceptance.

Existing implementation

#539 implements numeric equality/order over selected observed operands. #544 removes entry relations already implied by supported numeric domains. Keep both changes.

Bounded delivery

• Infer a fixed, small vocabulary (=== and <=) over explicitly selected numeric assertion operands from the first PBT run. Operands may be inputs or an explicitly captured result/intermediate; exact symbolic consumers are owned by [TS PBT] Bind one-time observed relations to exact symbolic challenges #398.
• Preserve original property/assertion/point identity, source provenance, admitted inputs, support counts and contradictions. Honor JavaScript NaN, infinities and signed zero.
• Distinguish independent random samples from replay/shrinking repetitions. A small finite domain must not disable ordinary coverage/property search when relation evidence is insufficient.
• Filter domain-implied facts, tautologies, duplicates and a direct restatement of the original predicate where that identity is known. Report inability to establish relevance rather than manufacturing a relation.
• Bound candidates and inference cost. Run inference once before USVM; no second-round confidence updates or revision/invalidation subsystem is required.

Acceptance

Actual native observations produce a nontrivial candidate, a later native execution can contradict it, and #398 consumes the exact selected evidence without treating it as proof. Empty, incomplete, misleading and finite-support evidence have explicit outcomes. Automatic dependency slicing, affine/length/pre-post families, cross-execution inference and universal invariant discovery are outside this bounded delivery. Scientific value is evaluated in #357.

Delivery status (2026-10-17)

Numeric equality/order inference, domain-tautology filtering, exact local/result capture and deterministic bounded selection are published across #539/#544/#580/#584/#596 and composed in #602/#603. Inference retains support, contradictions, provenance, candidates and exclusions; finite-sample relations never become unrestricted assumptions.

#610 (f2c97a664f31cde9167fdb1ca04fe8e12f04ad1a) fixes usable retained finite samples when later recorder invocations are dropped. Truncation and raw limitations remain visible; missing/corrupt/repeated/ambiguous point evidence stays excluded. Its public 100-input regression fails on the clean prior base and passes with the change; 77 focused Kotlin and 50 native tests passed. It is integrated with #611 in frozen local assembly c447392006cb72b06ead3d857b639a23d7e259c9, whose 42 focused integration tests passed. No correction remains unpublished.

The completed 108-cell scalar study confirms that thousands of PBT invocations still produce bounded one-time relation challenges without reducing generation quota to recorder capacity. Correct inputs can refute the inferred equality while the original property holds; mutant input 417 fails named original check receipt. However, all 18 checked prefix/native diagnostics reach the same rare input without the learned equality. This demonstrates supported finite-sample functionality, not additional empirical observation value; #357/#404 preserve that attribution failure. These implementations remain open PRs, not merged main.