Add ix claim/prove/verify pipeline; ix check becomes the Aiur kernel runner

[arthurpaulino]

Renames the Rust-kernel typechecker ix check to ix check-rs
(verbatim move into Ix/Cli/CheckRsCmd.lean) and rebuilds the
default ix check around the IxVM Aiur kernel — the path
lake exe kernel used to take.

ix check (Aiur kernel runner)

ix check Nat.add_comm                # compiled-in Lean env
ix check --ixe arena.ixe foo bar     # from .ixe, targeted names
ix check --ixe arena.ixe             # iterate every named const
ix check --interp Foo.bar            # Aiur interpreter (richer errors)
ix check --stats-out STATS Foo.bar   # redirect per-circuit stats

Variadic positional names; flags --interp / --keep-going /
--ixe / --stats-out. Per-circuit stats print only on a single
target. IX_QUIET=1 set unconditionally. Kernel.lean collapses
into a thin Cli shim around Ix.Cli.CheckCmd.runCheckCmd; the
lake exe kernel binary stays for fast Lean iteration.

ix prove + ix verify + Ixon.Proof wrapper

Ix/Cli/ProveCmd.lean (replacing a commented-out scaffold):

ix prove <claim-hex> <ixe-path>

Reads the persisted claim, loads the env, resolves every
assumption / env / contains tree the claim references (each tree
must be in the store), builds the kernel witness via
IxVM.ClaimHarness.buildClaimWitness, runs Aiur's prove
against verify_claim, wraps the opaque proof bytes in a new
Ixon.Proof { claim, proof }, persists the wrapper, prints its
blake3 hex.

Ix/Cli/VerifyCmd.lean: ix verify <proof-hex> reads the
wrapper, recomputes blake3(Claim.ser claim) as the
verify_claim public input, rebuilds the Aiur backend, runs
verify. One arg — the wrapper carries the claim. Commitment +
FRI params are private constants in both files and must stay in
sync (TODO: move into the proof header).

Ix/Claim.lean defines Ixon.Proof under Tag4 flag
FLAG_PROOF = 0xF (claims use 0xE), reusing the per-variant
VARIANT_*_PROOF size constants. put / get / ser / de
round-trip every claim variant.

ix claim + ix tree builders

Ix/Cli/ClaimCmd.lean: ix claim {check, check-env, contains, eval} build an Ix.Claim, persist it at blake3(ser claim),
print its address. --asm <root> threads an assumption-tree
merkle root. reveal is a TODO pending a JSON schema for
Ix.RevealConstantInfo.

Ix/Cli/TreeCmd.lean: ix tree canonical <hex,hex,...> and
ix tree env <ixe> build an Ix.AssumptionTree and persist it
under its merkle root (not under blake3(bytes)), so
--asm <root> references resolve with a plain Store.read root.
Ix/Store.lean gains writeAt addr bytes for content whose
canonical key isn't blake3(bytes).

ix addr-of

Ix/Cli/AddrOfCmd.lean: ix addr-of <Lean.Name> [--ixe <path>]
resolves a name to its 32-byte address — from a .ixe (via
Ixon.Env.getAddr?) or from the compiled-in Lean env (via
IxVM.ClaimHarness.loadIxonEnv → lookupAddr). Prints one hex
line so it composes with ix claim … and ix prove ….

ix compile filtering + positional inputs

Ix/Cli/CompileCmd.lean moves the input file to a positional
arg and adds a seed-filter trio:

• --module <prefix,…> — filter by SOURCE MODULE prefix (via
  Lean.Environment.getModuleIdxFor? +
  allImportedModuleNames). Catches macro-emitted decls
  registered under unqualified names because the host module
  still matches.
• --exclude <names> / --exclude-file <path> — strip names
  from the seed set (excluded names still reappear via the
  transitive closure if any other seed references them).

The compile path now threads collectDeps over filtered seeds
into rsCompileEnvBytesFFI rather than dumping the whole env.

Ix/Cli/IngressCmd.lean and Ix/Cli/ValidateCmd.lean get the
same positional-<path> treatment for shape consistency.

dbg_check_const → verify_const

The subject-only kernel entrypoint (transitive deps trusted; not
a claim path) is renamed across Ix/IxVM/Kernel/Claim.lean,
Ix/IxVM/ClaimHarness.lean (buildDbgCheckConst →
buildVerifyConst), and Tests/Ix/Kernel/Arena.lean.
Ix/IxVM.lean gets a fresh docstring on ixVM explaining why
verify_const shares the blake3-verifying loaders with
verify_claim. Ix/IxVM/Ingress.lean reorders so
load_verified_blob sits next to load_verified_constant (no
behavior change).

Arena exclude-list generator

Tests/Ix/Kernel/ArenaExclude.lean + lean_exe arena-exclude
in lakefile.lean emit the names that can't be driven through
the kernel — .bad-outcome decls, knownIncompatible entries,
renamings-tagged collision tests — one per line, ready for
ix compile --exclude-file.

Storage layout (recap)

Everything content-addressed lives under
~/.ix/store/XX/YY/ZZ/<rest>:

• Claims — key = blake3(Ix.Claim.ser claim). First byte 0xE.
• Proofs — key = blake3(Ixon.Proof.ser wrapper). First byte
  0xF. Wrapper carries the claim, so ix verify needs only
  the proof hex.
• Trees — key = merkle root. Written via Store.writeAt.

Main.lean registers the new subcommands and uncomments
proveCmd.