[ETS] Prove bounded numeric builtin calls

[CaelmBleidd]

Direct exported TypeScript functions can call Number.isInteger, Math.abs, and two-argument Math.min/Math.max, but downstream analysis cannot safely recognize those builtins from a method name alone. Attach an optional source-derived builtin proof to the lowered call and preserve it through Kotlin DTO conversion, with the correct Number or Math owner.

The proof checks default-library symbol identity, supported scalar arguments, module initialization and the evaluated path before the call, including repeated loop bodies. It records the enclosing entry signature and requires a direct isolated runtime entry; consumers must enforce that requirement. Shadowed or overwritten builtins, ambient getter reads, effectful arguments and unsupported call shapes remain unproven. Intrinsic undefined guards retain their proofs without admitting project-global shadows.

This is a frontend prerequisite for USVM #368 and the bounded numeric Calls campaign. The branch is based on the current neo commit containing #364 and retains type-only export metadata.

Validation: final focused frontend tests (14 proof and 9 import/export cases), typecheck and build; Kotlin proof DTO tests (3) and export tests (8); lowering of six original consumers from pinned TheAlgorithms/TypeScript and es-toolkit sources. Independent core, hygiene and serialization/resource review results are recorded with the local implementation evidence. The earlier full frontend suite passed before the focused fixes; final verification targeted the changed proof and export behavior.

[github-actions]

Test Results

  226 files  +1    226 suites  +1   16m 7s ⏱️ -10s
  780 tests +3    768 ✅ +3  12 💤 ±0  0 ❌ ±0 
2 050 runs  +3  2 000 ✅ +3  50 💤 ±0  0 ❌ ±0 

Results for commit 35f248b. ± Comparison against base commit ddb127d.

[CaelmBleidd]

Closing this approach: the current experiment will assume standard builtins and validate model usefulness empirically, without adding source-derived builtin proofs to JacoDB.