Keep IxVM lazy defeq bounded on open Nat terms

[arthurpaulino]

Summary

This PR makes the IxVM's lazy definitional-equality path both more selective and strictly bounded. It avoids eagerly expanding symbolic Nat primitives such as large-offset comparisons, while preventing projection/constant reduction cycles from silently refreshing their fuel budget.

It also adds Batteries as a compile-environment benchmark target so the environment can be included in sharding and compatibility sweeps.

Details

• Add a structural WHNF pass that performs beta, zeta, iota, and projection reduction without delta-unfolding definitions or dispatching primitives. Defeq uses this pass before its no-delta reducer, allowing structurally equal terms to close without exposing large logical implementations.
• Leave open Nat primitives in compact symbolic form. Closed primitive applications still dispatch normally, but applications containing bound variables no longer expand into potentially enormous successor/recursive terms.
• Bound the lazy-delta accelerator end to end:
  • projection and constant retries continue within the same fuel budget instead of re-entering defeq and resetting it;
  • structural comparison shares one reduction credit across the whole expression tree, so work cannot multiply across nested applications or sibling subterms;
  • if the bounded path remains undecided, the compatibility fallback runs full WHNF on the original terms rather than partially unfolded intermediates.
• Reduce projection-headed terms without delta first, then retain a single scrutinee delta step for cases that need a constructor-built instance exposed.
• Add and pin regression coverage for large open Nat offsets, projected/indexed values, and the Int8.toInt64_ne_minValue proof shape that exercises the eager compatibility path.
• Regenerate the native Rust IxVM executor and repin the affected kernel and shard-pipeline FFT costs.
• Add CompileBatteries alongside the existing compile-environment targets.

Validation

• The IxVM FFT regression suite is repinned for the new kernel shape, including bytecode/native-codegen parity coverage.
• The shard-pipeline FFT pin is updated from 6,097,645,626 to 6,098,300,309.
• Environment sweeps completed across 600 shards covering Init, InitStd, Lean, Batteries, Mathlib, and FLT without timeouts or check failures.