Add G field arithmetic (Add, Sub, Mul, eqZero), u8/u32 semantic
functions with range predicates, and commutativity theorems to
Goldilocks.lean. Enable precompileModules on Ix library for native
evaluation under Lean's `module` system.

Add `#aiur_gen` command that evaluates an Aiur Toplevel at elaboration
time and writes a .lean file with:
- Semantic types: Lean inductives from Aiur enums with pointers erased,
  type aliases as abbrevs, topologically sorted by type references
  with mutual blocks for cyclic dependencies. Generic type parameters
  (`enum Foo‹T›`) become explicit Lean params `(T : Type)`.
- Semantic propositions: one inductive per function, one constructor per
  control-flow path, with assertEq as Prop conjuncts, store/load
  erased, u8/u32 ops with range constraints, or-patterns expanded,
  IO operations as unconstrained fresh variables, data constructors
  inlined, nested match patterns resolved transitively. Generic
  function parameters become implicit Lean params `{T : Type}`.
  Unconstrained calls (`#fn(…)`) produce universally quantified
  variables with no premises.
- Topological sorting of both types and functions by dependency graph,
  with mutual blocks only for actual cycles. Unconstrained calls are
  excluded from the dependency graph.

Add multi-file example:
- ExampleBase.lean: Expr type, eval, swap, double_eval (forward ref),
  simplify_neg (nested match) → ExampleBaseSem.lean
- ExampleMain.lean: ExprList, Tree/Forest (mutual types), list_sum,
  assert_eval, tree_sum/forest_sum (mutual functions),
  is_even/is_odd (mutual recursion), GList‹T› with length‹T›
  (generic types), add_noise/use_unconstrained (unconstrained calls)
  → ExampleMainSem.lean (imports base)
- Example.lean: theorems over generated semantic propositions
  (determinism, totality, involution, assertEq semantics, spec
  soundness, mutual type/function soundness, mutual recursion path
  exclusivity, generic length soundness, unconstrained call form
  vs constrained determinism)