IxVM kernel: canonical level normalization + FFT-cost pinning (#447)

* IxVM: canonical level normalization for level_equal / level_leq

Port the Rust kernel's canonical-form level machinery (level.rs
normalize_level / norm_level_eq / norm_level_le, itself a line-by-line
port of Lean4Lean's Level.Normalize with the covers-split soundness
fix): normalize_aux with imax-path conditioning, phase-2 subsumption,
and structural/dominance comparison on canonical forms. level_equal and
level_leq now normalize-and-compare; the previous recursive Level.leq
mirror with its two-way param-substitution split per Max/IMax — and its
helpers level_subst_reduce / level_has_param / level_any_param — is
deleted. level_normalize is keyed on the level alone, so each distinct
level normalizes once per run.

The split was exponential in the number of params and every branch
materialized freshly substituted levels. On
_private.…SInt.0.Int16.instRxcHasSize_eq the level family was 93% of
the record at 2^31 ops (level_subst_reduce 60.8M + level_leq 53.2M +
level_max 30.4M entries…), entered through Inductive's ctor-field
universe constraint (level_leq), not def-eq's level_equal.

Measured: Int16.instRxcHasSize_eq goes from NON-COMPLETING (killed at
178 GB RSS after 21 min, growth not converging) to 2m23s / 17.9 GB /
295.7B FFT. Int8 completes in 21s. The bench suite is unaffected (its
level comparisons hit the structural fast path). 297 ixvm tests pass.

* Tests: pin FFT cost per kernel-check target

## Summary

Adds `expectedFftCost : Option Nat` to `AiurTestCase`. When set,
`runTestCase` asserts the rounded `Aiur.computeStats.totalFftCost`
matches exactly. Converts `Tests/Ix/IxVM.lean::kernelCheckNames` to
`kernelCheckEntries : List (String × Nat)` and pins all 41 entries.

## Motivation

Without per-circuit cost pinning, kernel changes that silently shift
FFT cost can land without review. Pinning forces every cost change to
be acknowledged in the test source — failures report `expected X, got
Y` so the new value can be pasted back.

## Coverage

Pins the 38 prior `kernelCheckNames` entries (Stdlib, `IxVMPrim`,
`IxVMInd`, edge-case prelude) plus 3 newly-unlocked targets from the
`level_leq` Géran-normalize fix:

- `Trans.mk`              — 2,732,504
- `Array.append_assoc`    — 3,938,369,542
- `Vector.append`         — 4,023,063,255

`Vector.extract_append` deliberately omitted (too heavy for the suite).

---------

Co-authored-by: samuelburnham <45365069+samuelburnham@users.noreply.github.com>

Author: arthurpaulino