diff --git a/.github/workflows/bench-pr.yml b/.github/workflows/bench-pr.yml
index 37ad84b23..7e1c05d83 100644
--- a/.github/workflows/bench-pr.yml
+++ b/.github/workflows/bench-pr.yml
@@ -9,6 +9,10 @@
 #   BENCH_SHARD=1                  # restrict to the multi-shard target constants
 #   BENCH_PHASES=1                 # add per-constant phase drill-downs to the comment
 #   RUST_LOG=info                  # passthrough env (allowlisted)
+#   IX_COMPILE_EAGER=1             # compile-knob passthrough (also IX_COMPILE_DEMOTE /
+#                                  # IX_COMPILE_WORKERS); reaches the measured `ix
+#                                  # compile` and keys its caches, so a knob run gets
+#                                  # its own row instead of the default run's
 #
 # Mode defaults per backend (the registry's defaultMode): `aiur` runs
 # `prove` — the real-workload simulation, whose report also carries the
@@ -197,14 +201,22 @@ jobs:
           ref: ${{ inputs.head-sha }}
           # The job runs PR code; never leave the token in .git.
           persist-credentials: false
-      # Re-running !benchmark on the same commit: the .ixe is already
-      # published — nothing to do.
+      # Allowlisted KEY=VALUE lines from the !benchmark comment. Applied
+      # here so IX_COMPILE_* knobs reach the measured compile, and staged
+      # to a file so the cache keys below can hash it — a knob run must
+      # not reuse (or overwrite) the default run's published .ixe/row.
+      - name: Apply passthrough env
+        env:
+          PTENV: ${{ needs.build.outputs.passthrough-env }}
+        run: printf '%s\n' "$PTENV" | sed '/^[[:space:]]*$/d' | tee ptenv.txt >> "$GITHUB_ENV"
+      # Re-running !benchmark on the same commit with the same config: the
+      # .ixe is already published — nothing to do.
       - name: Check for published .ixe
         id: pr-ixe
         uses: actions/cache/restore@v5
         with:
           path: ${{ matrix.env }}.ixe
-          key: bench-pr-ixe-${{ inputs.head-sha }}-${{ matrix.env }}
+          key: bench-pr-ixe-${{ inputs.head-sha }}-${{ matrix.env }}-${{ hashFiles('ptenv.txt') }}
           lookup-only: true
       - name: Restore PR binaries
         if: steps.pr-ixe.outputs.cache-hit != 'true'
@@ -242,7 +254,7 @@ jobs:
         uses: actions/cache/save@v5
         with:
           path: ${{ matrix.env }}.ixe
-          key: bench-pr-ixe-${{ inputs.head-sha }}-${{ matrix.env }}
+          key: bench-pr-ixe-${{ inputs.head-sha }}-${{ matrix.env }}-${{ hashFiles('ptenv.txt') }}
       # The measured row: the compile cell reuses it as its PR side (same
       # runner class, same binaries, same command it would run itself).
       - name: Publish compile row
@@ -250,7 +262,7 @@ jobs:
         uses: actions/cache/save@v5
         with:
           path: compile.json
-          key: bench-pr-row-${{ inputs.head-sha }}-${{ matrix.env }}
+          key: bench-pr-row-${{ inputs.head-sha }}-${{ matrix.env }}-${{ hashFiles('ptenv.txt') }}
 
   benchmark:
     # Explicit name: the default would append EVERY matrix value (backend,
@@ -294,7 +306,7 @@ jobs:
       - name: Apply passthrough env
         env:
           PTENV: ${{ needs.build.outputs.passthrough-env }}
-        run: printf '%s\n' "$PTENV" | sed '/^[[:space:]]*$/d' >> "$GITHUB_ENV"
+        run: printf '%s\n' "$PTENV" | sed '/^[[:space:]]*$/d' | tee ptenv.txt >> "$GITHUB_ENV"
       # Restore the once-built PR binaries (see the build job) into the PR
       # tree's own bin dir: `ix bench run` resolves the measured tools from
       # <repo>/.lake/build/bin first, then PATH, so staging in-tree keeps the
@@ -334,7 +346,7 @@ jobs:
         uses: actions/cache/restore@v5
         with:
           path: ${{ matrix.cell.env }}.ixe
-          key: bench-pr-ixe-${{ env.HEAD_SHA }}-${{ matrix.cell.env }}
+          key: bench-pr-ixe-${{ env.HEAD_SHA }}-${{ matrix.cell.env }}-${{ hashFiles('ptenv.txt') }}
           fail-on-cache-miss: true
       # Compile cells reuse the compile job's measured row as their PR side.
       - name: Restore compile row
@@ -342,7 +354,7 @@ jobs:
         uses: actions/cache/restore@v5
         with:
           path: compile.json
-          key: bench-pr-row-${{ env.HEAD_SHA }}-${{ matrix.cell.env }}
+          key: bench-pr-row-${{ env.HEAD_SHA }}-${{ matrix.cell.env }}-${{ hashFiles('ptenv.txt') }}
           fail-on-cache-miss: true
       # zkVM cells additionally need the Rust toolchain + the backend's toolchain
       # and system deps (the shared composite install actions).
diff --git a/Ix/Cli/BenchReport.lean b/Ix/Cli/BenchReport.lean
index 01c58940f..c9e963629 100644
--- a/Ix/Cli/BenchReport.lean
+++ b/Ix/Cli/BenchReport.lean
@@ -595,9 +595,13 @@ def parseError (msg : String) : IO UInt32 := do
       BENCH_FULL=1                 (full curated set, not just primary)
       BENCH_SHARD=1                (only the multi-shard target constants)
       BENCH_PHASES=1 / RUST_LOG=… / WITHOUT_VK_VERIFICATION=… /
-      RUSTFLAGS=…                  (passthrough; BENCH_PHASES=1 adds the
+      RUSTFLAGS=… / IX_COMPILE_EAGER=… / IX_COMPILE_DEMOTE=… /
+      IX_COMPILE_WORKERS=…         (passthrough; BENCH_PHASES=1 adds the
                                     per-constant phase drill-downs to the
-                                    comment)
+                                    comment; the IX_COMPILE_* knobs reach
+                                    the measured `ix compile` and key its
+                                    caches, so knob runs don't reuse a
+                                    default run's published row)
 
     The KEY=VALUE config may sit on its own lines below the command (the
     comment form) or inline on the command line, whitespace-separated
@@ -694,13 +698,15 @@ def runParseCmd (p : Cli.Parsed) : IO UInt32 := do
       | "BENCH_FULL" => if val == "1" then full := "1"
       | k =>
         if ["BENCH_PHASES", "RUST_LOG", "WITHOUT_VK_VERIFICATION",
-            "RUSTFLAGS"].contains k then
+            "RUSTFLAGS", "IX_COMPILE_EAGER", "IX_COMPILE_DEMOTE",
+            "IX_COMPILE_WORKERS"].contains k then
           passthrough := passthrough.push s!"{k}={val}"
         else if strict then
           return ← parseError s!"unknown config key `{k}` in the \
             benchmark command (expected BENCH_ENVS / BENCH_FULL / \
             BENCH_SHARD, or passthrough: BENCH_PHASES, RUST_LOG, \
-            WITHOUT_VK_VERIFICATION, RUSTFLAGS)"
+            WITHOUT_VK_VERIFICATION, RUSTFLAGS, IX_COMPILE_EAGER, \
+            IX_COMPILE_DEMOTE, IX_COMPILE_WORKERS)"
     | [] => continue
   if envs.isEmpty then envs := #["InitStd"]
 
diff --git a/Ix/Cli/CompileCmd.lean b/Ix/Cli/CompileCmd.lean
index edf323db4..c9c2464ff 100644
--- a/Ix/Cli/CompileCmd.lean
+++ b/Ix/Cli/CompileCmd.lean
@@ -134,11 +134,17 @@ def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do
   if benched then
     TracingTexray.startSampler
     TracingTexray.resetPeakTreeRss
+
+  -- Rust compiles and writes the `.ixe` directly (streamed — no
+  -- env-sized ByteArray crosses the FFI; `<out>.tmp` + atomic rename).
+  -- The file is the canonical `Ixon.Env::put` format and round-trips
+  -- through `Ixon.Env::get`, so later runs (e.g. `ix check-ixon`) can
+  -- skip the Lean → IxOn compile step.
   let start ← IO.monoMsNow
-  let bytes ← Ix.CompileM.rsCompileEnvBytesFFI constList
+  let size ← Ix.CompileM.rsCompileEnvBytesFFI constList outPath
   let elapsed := (← IO.monoMsNow) - start
-
-  println! "Compiled {fmtBytes bytes.size} env in {elapsed.formatMs}"
+  println! "Compiled and wrote {fmtBytes size} env to {outPath} in {elapsed.formatMs}"
+  IO.println s!"##benchmark## {elapsed} {size} {totalConsts}"
   if let some flag := p.flag? "json" then
     let key := (p.flag? "json-name").map (·.as! String)
       |>.getD ((FilePath.mk pathStr).fileStem.getD "env")
@@ -148,20 +154,10 @@ def runCompileCmd (p : Cli.Parsed) : IO UInt32 := do
     let peakRss ← TracingTexray.peakTreeRssBytes
     Ix.Benchmark.Results.writeRow (flag.as! String) key "ok"
       [ ("compile-time", Ix.Benchmark.Results.jsonRound 3 secs)
-      , ("file-size", Lean.toJson bytes.size)
+      , ("file-size", Lean.toJson size)
       , ("constants", Lean.toJson totalConsts)
       , ("throughput", Ix.Benchmark.Results.jsonRound 2 tput)
       , ("peak-rss", Lean.toJson peakRss) ]
-
-  -- Persist the serialized IxonEnv (`Env::put` bytes) to disk so subsequent
-  -- runs (e.g. `ix check-ixon`) can skip the Lean → IxOn compile step. The
-  -- resulting file is the canonical streaming format produced by
-  -- `Ixon.Env::put` (see `src/ix/ixon/serialize.rs:1093-1297`); it round-trips
-  -- through `Ixon.Env::get`.
-  let writeStart ← IO.monoMsNow
-  IO.FS.writeBinFile outPath bytes
-  let writeMs := (← IO.monoMsNow) - writeStart
-  println! "Wrote {fmtBytes bytes.size} to {outPath} in {writeMs.formatMs}"
   return 0
 
 
diff --git a/Ix/CompileM.lean b/Ix/CompileM.lean
index b803d1394..701608a55 100644
--- a/Ix/CompileM.lean
+++ b/Ix/CompileM.lean
@@ -1916,9 +1916,14 @@ def compileEnvParallel (env : Ix.Environment) (blocks : Ix.CondensedBlocks)
 
 /-! ## Rust Compilation FFI -/
 
-/-- FFI: Compile a Lean environment to serialized Ixon.Env bytes using Rust. -/
+/-- FFI: Compile a Lean environment and write the serialized Ixon.Env
+    bytes straight to `outPath` from Rust (streamed; no env-sized
+    ByteArray crosses the FFI). Writes to `<outPath>.tmp` then renames,
+    so a crash cannot leave a truncated file. Returns the byte count
+    written. -/
 @[extern "rs_compile_env"]
-opaque rsCompileEnvBytesFFI : @& List (Lean.Name × Lean.ConstantInfo) → IO ByteArray
+opaque rsCompileEnvBytesFFI
+  : @& List (Lean.Name × Lean.ConstantInfo) → @& String → IO Nat
 
 /-- FFI: 8-phase validation of the aux_gen compile pipeline (compile +
     decompile + roundtrip + alpha-equivalence + nested-detect checks).
@@ -1932,10 +1937,12 @@ opaque rsCompileEnvBytesFFI : @& List (Lean.Name × Lean.ConstantInfo) → IO By
 opaque rsCompileValidateAuxFFI
   : @& List (Lean.Name × Lean.ConstantInfo) → USize
 
-/-- Compile a Lean environment to Ixon.Env bytes using the Rust compiler. -/
-def rsCompileEnvBytes (leanEnv : Lean.Environment) : IO ByteArray := do
+/-- Compile a Lean environment and write the serialized Ixon.Env bytes
+    to `outPath` using the Rust compiler. Returns the byte count. -/
+def rsCompileEnvBytes (leanEnv : Lean.Environment) (outPath : String)
+    : IO Nat := do
   let constList := leanEnv.constants.toList
-  rsCompileEnvBytesFFI constList
+  rsCompileEnvBytesFFI constList outPath
 
 -- Re-export RawEnv types from Ixon for backwards compatibility
 export Ixon (RawConst RawNamed RawBlob RawComm RawEnv)
diff --git a/Tests/Main.lean b/Tests/Main.lean
index 3606f5d35..165805972 100644
--- a/Tests/Main.lean
+++ b/Tests/Main.lean
@@ -60,10 +60,14 @@ def ignoredSuites : Std.HashMap String (List LSpec.TestSeq) := .ofList [
   ("parallel-canon-roundtrip", Tests.CanonM.parallelSuiteIO),
   ("graph-cross", Tests.Ix.GraphM.suiteIO),
   ("condense-cross", Tests.Ix.CondenseM.suiteIO),
-  -- Lean compilation & kernel tests currently broken, disabled
+  -- Lean-side compilation/decompilation currently broken, disabled
   --("compile", Tests.Compile.compileSuiteIO),
   --("decompile", Tests.Decompile.decompileSuiteIO),
   ("rust-serialize", Tests.RustSerialize.rustSerializeSuiteIO),
+  -- Rust decompile of synthesized `_sparseCasesOn` aux constants fails
+  -- ("missing Ref metadata": their aux_gen metadata arena misaligns
+  -- with the serialized expr, and pure-aux constants have no
+  -- `Named.original` sidecar to recover from), disabled
   --("rust-decompile", Tests.RustDecompile.rustDecompileSuiteIO),
   ("commit-io", Tests.Commit.suiteIO),
   ("kernel-ixon-roundtrip", Tests.Ix.Kernel.Roundtrip.suite),
diff --git a/crates/common/src/env.rs b/crates/common/src/env.rs
index b2d6675a6..ff4a57b21 100644
--- a/crates/common/src/env.rs
+++ b/crates/common/src/env.rs
@@ -1462,8 +1462,276 @@ impl ConstantInfo {
   }
 }
 
-/// The Lean kernel environment: a map from names to their constant declarations.
-pub type Env = FxHashMap<Name, ConstantInfo>;
+/// Guard returned by [`Env::get`]: derefs to [`ConstantInfo`].
+///
+/// Eager environments hand out plain borrows (zero cost); lazy
+/// environments hand out `Arc`s so the entry stays alive even if the
+/// backing cache evicts it concurrently.
+pub enum EnvEntry<'a> {
+  Borrowed(&'a ConstantInfo),
+  Owned(Arc<ConstantInfo>),
+}
+
+impl std::ops::Deref for EnvEntry<'_> {
+  type Target = ConstantInfo;
+  fn deref(&self) -> &ConstantInfo {
+    match self {
+      EnvEntry::Borrowed(c) => c,
+      EnvEntry::Owned(c) => c,
+    }
+  }
+}
+
+impl EnvEntry<'_> {
+  /// Owned copy of the constant. Cheap only when a caller genuinely
+  /// needs ownership — prefer deref for reads.
+  pub fn cloned(&self) -> ConstantInfo {
+    (**self).clone()
+  }
+}
+
+/// Host-only lazy backing for [`Env`]: a name index plus an injected
+/// fetch that decodes one constant on demand (in practice from Lean
+/// objects held as `LeanShared` handles — see `decode_env_lazy` in the
+/// ffi crate), fronted by a lock-partitioned bounded cache. Avoids materializing
+/// the full owned copy of the environment up front, which costs a large
+/// multiple of the working set the compile pipeline actually touches at
+/// any one time.
+#[cfg(not(target_arch = "riscv64"))]
+pub struct LazyEnv {
+  /// All names, in the source env's iteration order.
+  names: Vec<Name>,
+  /// Membership index into `names`.
+  index: FxHashMap<Name, usize>,
+  /// Decode one constant. Must be pure and thread-safe.
+  fetch: Box<dyn Fn(&Name) -> Option<ConstantInfo> + Send + Sync>,
+  /// Independently locked cache segments so concurrent
+  /// `get`s rarely contend; per-segment capacity bounds resident
+  /// decoded constants. Eviction is `swap_remove_index(0)` — cheap
+  /// oldest-biased pseudo-FIFO, adequate for the scheduler's
+  /// topological locality.
+  segments: Vec<std::sync::Mutex<indexmap::IndexMap<Name, Arc<ConstantInfo>>>>,
+  cap_per_segment: usize,
+  /// Never-evicted overlay for hot names, installed once via
+  /// [`Env::pin`] before concurrent readers start. Each slot decodes
+  /// on first access and stays resident; reads after that are
+  /// lock-free. Names outside the overlay fall through to the
+  /// segments.
+  pinned: std::sync::OnceLock<
+    FxHashMap<Name, std::sync::OnceLock<Option<Arc<ConstantInfo>>>>,
+  >,
+}
+
+#[cfg(not(target_arch = "riscv64"))]
+impl LazyEnv {
+  /// Segment count: 4× the hardware threads (the scheduler runs at
+  /// most one worker per thread), rounded up to a power of two so the
+  /// hash mask in `segment_for` stays uniform. The 4× headroom keeps
+  /// expected pairwise collisions low when every worker is in `get`
+  /// at once; a mutexed segment costs ~40 bytes, so overprovisioning
+  /// is free.
+  fn segment_count() -> usize {
+    let threads = std::thread::available_parallelism().map_or(1, usize::from);
+    // Capped at the two-byte selector's range (`segment_for`).
+    (threads * 4).next_power_of_two().min(1 << 16)
+  }
+
+  /// Two low hash bytes masked down to the segment count: uniform by
+  /// hash uniformity because the count is a power of two.
+  fn segment_for(&self, name: &Name) -> usize {
+    let bytes = name.get_hash().as_bytes();
+    let window = usize::from(u16::from_le_bytes([bytes[0], bytes[1]]));
+    window & (self.segments.len() - 1)
+  }
+
+  fn get(&self, name: &Name) -> Option<Arc<ConstantInfo>> {
+    if !self.index.contains_key(name) {
+      return None;
+    }
+    if let Some(pinned) = self.pinned.get()
+      && let Some(slot) = pinned.get(name)
+    {
+      return slot.get_or_init(|| (self.fetch)(name).map(Arc::new)).clone();
+    }
+    let segment_idx = self.segment_for(name);
+    if let Some(hit) = self.segments[segment_idx].lock().unwrap().get(name) {
+      return Some(hit.clone());
+    }
+    // Decode outside the segment lock: fetches can be slow and other
+    // names hashing to this segment shouldn't wait on them.
+    let decoded = Arc::new((self.fetch)(name)?);
+    let mut segment = self.segments[segment_idx].lock().unwrap();
+    if segment.len() >= self.cap_per_segment {
+      segment.swap_remove_index(0);
+    }
+    segment.insert(name.clone(), decoded.clone());
+    Some(decoded)
+  }
+}
+
+/// The Lean kernel environment: a map from names to their constant
+/// declarations. Eager (an owned map — the default, and the only
+/// variant on the guest) or, on the host, a lazy on-demand view (see
+/// [`LazyEnv`]).
+///
+/// Keeps the plain-map API shape, with [`Env::get`] returning the
+/// [`EnvEntry`] guard instead of a plain borrow, so both variants
+/// serve reads through one signature.
+#[derive(Default)]
+pub struct Env {
+  eager: FxHashMap<Name, ConstantInfo>,
+  #[cfg(not(target_arch = "riscv64"))]
+  lazy: Option<LazyEnv>,
+}
+
+impl std::fmt::Debug for Env {
+  fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+    f.debug_struct("Env").field("len", &self.len()).finish()
+  }
+}
+
+impl Clone for Env {
+  /// Clones the eager map. Lazy environments are read-only views and
+  /// are never cloned (the compile pipeline shares them via `Arc`).
+  fn clone(&self) -> Self {
+    #[cfg(not(target_arch = "riscv64"))]
+    assert!(
+      self.lazy.is_none(),
+      "Env::clone on a lazy environment (share via Arc instead)"
+    );
+    Env {
+      eager: self.eager.clone(),
+      #[cfg(not(target_arch = "riscv64"))]
+      lazy: None,
+    }
+  }
+}
+
+impl Env {
+  /// Build a lazy env from a name list and a fetch function.
+  /// `cache_entries` bounds resident decoded constants (total across
+  /// segments; minimum one per segment).
+  #[cfg(not(target_arch = "riscv64"))]
+  pub fn new_lazy(
+    names: Vec<Name>,
+    fetch: Box<dyn Fn(&Name) -> Option<ConstantInfo> + Send + Sync>,
+    cache_entries: usize,
+  ) -> Self {
+    let index: FxHashMap<Name, usize> =
+      names.iter().enumerate().map(|(i, n)| (n.clone(), i)).collect();
+    let segment_count = LazyEnv::segment_count();
+    let cap_per_segment = (cache_entries / segment_count).max(1);
+    let segments = (0..segment_count)
+      .map(|_| {
+        std::sync::Mutex::new(indexmap::IndexMap::with_capacity(
+          cap_per_segment.min(4096),
+        ))
+      })
+      .collect();
+    Env {
+      eager: FxHashMap::default(),
+      lazy: Some(LazyEnv {
+        names,
+        index,
+        fetch,
+        segments,
+        cap_per_segment,
+        pinned: std::sync::OnceLock::new(),
+      }),
+    }
+  }
+
+  /// Pin `names` in the lazy cache: they decode on first access and
+  /// are never evicted. Install once, before concurrent readers start
+  /// (later calls are ignored); no-op on eager envs.
+  #[cfg(not(target_arch = "riscv64"))]
+  pub fn pin(&self, names: impl IntoIterator<Item = Name>) {
+    if let Some(lazy) = &self.lazy {
+      let overlay: FxHashMap<_, _> =
+        names.into_iter().map(|n| (n, std::sync::OnceLock::new())).collect();
+      let _ = lazy.pinned.set(overlay);
+    }
+  }
+
+  pub fn get(&self, name: &Name) -> Option<EnvEntry<'_>> {
+    #[cfg(not(target_arch = "riscv64"))]
+    if let Some(lazy) = &self.lazy {
+      return lazy.get(name).map(EnvEntry::Owned);
+    }
+    self.eager.get(name).map(EnvEntry::Borrowed)
+  }
+
+  pub fn contains_key(&self, name: &Name) -> bool {
+    #[cfg(not(target_arch = "riscv64"))]
+    if let Some(lazy) = &self.lazy {
+      return lazy.index.contains_key(name);
+    }
+    self.eager.contains_key(name)
+  }
+
+  pub fn len(&self) -> usize {
+    #[cfg(not(target_arch = "riscv64"))]
+    if let Some(lazy) = &self.lazy {
+      return lazy.names.len();
+    }
+    self.eager.len()
+  }
+
+  pub fn is_empty(&self) -> bool {
+    self.len() == 0
+  }
+
+  /// Insert a constant. Eager only — lazy environments are read-only
+  /// views.
+  pub fn insert(
+    &mut self,
+    name: Name,
+    info: ConstantInfo,
+  ) -> Option<ConstantInfo> {
+    #[cfg(not(target_arch = "riscv64"))]
+    assert!(self.lazy.is_none(), "Env::insert on a lazy environment");
+    self.eager.insert(name, info)
+  }
+
+  pub fn get_mut(&mut self, name: &Name) -> Option<&mut ConstantInfo> {
+    #[cfg(not(target_arch = "riscv64"))]
+    assert!(self.lazy.is_none(), "Env::get_mut on a lazy environment");
+    self.eager.get_mut(name)
+  }
+
+  /// All names, in map order (eager) or source order (lazy). No
+  /// decode.
+  pub fn keys(&self) -> Box<dyn Iterator<Item = &Name> + '_> {
+    #[cfg(not(target_arch = "riscv64"))]
+    if let Some(lazy) = &self.lazy {
+      return Box::new(lazy.names.iter());
+    }
+    Box::new(self.eager.keys())
+  }
+
+  /// Iterate `(name, constant)`. Lazy mode decodes each entry fresh,
+  /// bypassing the cache — whole-env passes are single-visit, and
+  /// caching them would just churn the segments.
+  pub fn iter(&self) -> Box<dyn Iterator<Item = (&Name, EnvEntry<'_>)> + '_> {
+    #[cfg(not(target_arch = "riscv64"))]
+    if let Some(lazy) = &self.lazy {
+      return Box::new(lazy.names.iter().filter_map(move |n| {
+        (lazy.fetch)(n).map(|ci| (n, EnvEntry::Owned(Arc::new(ci))))
+      }));
+    }
+    Box::new(self.eager.iter().map(|(n, c)| (n, EnvEntry::Borrowed(c))))
+  }
+}
+
+impl FromIterator<(Name, ConstantInfo)> for Env {
+  fn from_iter<T: IntoIterator<Item = (Name, ConstantInfo)>>(it: T) -> Self {
+    Env {
+      eager: it.into_iter().collect(),
+      #[cfg(not(target_arch = "riscv64"))]
+      lazy: None,
+    }
+  }
+}
 
 #[cfg(any(test, feature = "quickcheck"))]
 pub mod arbitrary {
diff --git a/crates/compile/src/compile.rs b/crates/compile/src/compile.rs
index 0200d9afa..63a4cc6b4 100644
--- a/crates/compile/src/compile.rs
+++ b/crates/compile/src/compile.rs
@@ -312,7 +312,7 @@ impl CompileState {
       self.name_to_addr.insert(name.clone(), aux_addr.clone());
     }
     if let Some(mut entry) = self.env.named.get_mut(name) {
-      entry.value_mut().original = Some((orig_addr, orig_meta));
+      entry.value_mut().set_original(orig_addr, orig_meta);
     }
     Ok(())
   }
@@ -798,11 +798,7 @@ pub fn compile_expr(
                 cache.compiling.as_ref().is_some_and(|c| {
                   crate::decompile::is_aux_gen_suffix(c)
                     && (stt.aux_name_to_addr.contains_key(c)
-                      || stt
-                        .env
-                        .named
-                        .get(c)
-                        .is_some_and(|n| n.original.is_some()))
+                      || stt.env.named.get(c).is_some_and(|n| n.has_original()))
                 });
               if !compiling_is_aux_regen {
                 if let Some(plan) = stt.call_site_plans.get(name)
@@ -2574,7 +2570,9 @@ pub fn mk_indc(
 ) -> Result<Ind, CompileError> {
   let mut ctors = Vec::with_capacity(ind.ctors.len());
   for ctor_name in &ind.ctors {
-    if let Some(LeanConstantInfo::CtorInfo(c)) = env.as_ref().get(ctor_name) {
+    if let Some(LeanConstantInfo::CtorInfo(c)) =
+      env.as_ref().get(ctor_name).as_deref()
+    {
       ctors.push(c.clone());
     } else {
       return Err(CompileError::MissingConstant {
@@ -3254,7 +3252,7 @@ pub fn compile_const_no_aux(
   let mut lean_all: Vec<Name> = Vec::new();
   for n in all {
     if let Some(ci) = lean_env.get(n) {
-      let block_all = match ci {
+      let block_all = match &*ci {
         LeanConstantInfo::InductInfo(v) => &v.all,
         LeanConstantInfo::RecInfo(v) => &v.all,
         LeanConstantInfo::DefnInfo(v) => &v.all,
@@ -3281,7 +3279,7 @@ pub fn compile_const_no_aux(
     if !stt.aux_gen_extra_names.contains(n) {
       return None;
     }
-    match lean_env.get(n) {
+    match lean_env.get(n).as_deref() {
       Some(LeanConstantInfo::RecInfo(_)) => {
         // Distinguish .rec from .below.rec
         if matches!(n.as_data(), NameData::Str(p, _, _) if p.last_str() == Some("below"))
@@ -3319,7 +3317,10 @@ pub fn compile_const_no_aux(
       // SCC including rec_N names.
       for n in all {
         if stt.aux_gen_extra_names.contains(n)
-          && matches!(lean_env.get(n), Some(LeanConstantInfo::RecInfo(_)))
+          && matches!(
+            lean_env.get(n).as_deref(),
+            Some(LeanConstantInfo::RecInfo(_))
+          )
         {
           filtered.insert(n.clone());
         }
@@ -3328,10 +3329,13 @@ pub fn compile_const_no_aux(
     Phase::BelowIndc => {
       // Use .below's own .all, keep only inductives + their ctors.
       for n in all {
-        if let Some(LeanConstantInfo::InductInfo(v)) = lean_env.get(n) {
+        if let Some(LeanConstantInfo::InductInfo(v)) =
+          lean_env.get(n).as_deref()
+        {
           for a in &v.all {
             if stt.aux_gen_extra_names.contains(a)
-              && let Some(LeanConstantInfo::InductInfo(bi)) = lean_env.get(a)
+              && let Some(LeanConstantInfo::InductInfo(bi)) =
+                lean_env.get(a).as_deref()
             {
               filtered.insert(a.clone());
               for ctor in &bi.ctors {
@@ -3348,7 +3352,10 @@ pub fn compile_const_no_aux(
       // (from DefnInfo.all = [EqC.below]), so use directly.
       for a in &lean_all {
         if stt.aux_gen_extra_names.contains(a)
-          && matches!(lean_env.get(a), Some(LeanConstantInfo::DefnInfo(_)))
+          && matches!(
+            lean_env.get(a).as_deref(),
+            Some(LeanConstantInfo::DefnInfo(_))
+          )
         {
           filtered.insert(a.clone());
         }
@@ -3361,7 +3368,7 @@ pub fn compile_const_no_aux(
         let below_rec = Name::str(ind_name.clone(), "rec".to_string());
         if stt.aux_gen_extra_names.contains(&below_rec)
           && matches!(
-            lean_env.get(&below_rec),
+            lean_env.get(&below_rec).as_deref(),
             Some(LeanConstantInfo::RecInfo(_))
           )
         {
@@ -3649,7 +3656,9 @@ fn compile_const_inner(
 
     LeanConstantInfo::CtorInfo(val) => {
       // Constructors are compiled as part of their inductive
-      if let Some(LeanConstantInfo::InductInfo(_)) = lean_env.get(&val.induct) {
+      if let Some(LeanConstantInfo::InductInfo(_)) =
+        lean_env.get(&val.induct).as_deref()
+      {
         let _ =
           compile_mutual(&val.induct, all, lean_env, cache, stt, kctx, aux)?;
         stt
@@ -3691,10 +3700,9 @@ fn compile_mutual(
   // Collect all constants in the mutual block
   let mut cs = Vec::new();
   for n in all {
-    // `lean_env` is an `FxHashMap` (see `Env` alias in env.rs); `.get()`
-    // returns a plain reference, so there's no read guard to release —
-    // just clone the value and move on.
-    let Some(const_info) = lean_env.get(n).cloned() else {
+    // Clone out of the `EnvEntry` guard so the block owns its constants
+    // and no env borrow is held across the compile below.
+    let Some(const_info) = lean_env.get(n).map(|e| e.cloned()) else {
       return Err(CompileError::MissingConstant {
         name: n.pretty(),
         caller: "compile_mutual".into(),
diff --git a/crates/compile/src/compile/aux_gen.rs b/crates/compile/src/compile/aux_gen.rs
index 9e90449e7..103bc200d 100644
--- a/crates/compile/src/compile/aux_gen.rs
+++ b/crates/compile/src/compile/aux_gen.rs
@@ -256,7 +256,7 @@ pub fn generate_aux_patches(
     expanded_probe.types.len() > expanded_probe.n_originals;
   let metadata_has_nested = original_all.iter().any(|name| {
     matches!(
-      lean_env.get(name),
+      lean_env.get(name).as_deref(),
       Some(ix_common::env::ConstantInfo::InductInfo(v))
         if crate::compile::nat_conv::nat_to_usize(&v.num_nested) > 0
     )
@@ -759,13 +759,13 @@ pub fn generate_aux_patches(
               Some(PatchedConstant::BelowIndc(_))
             )
           {
-            let rep_ctors = match lean_env.get(rep) {
+            let rep_ctors = match lean_env.get(rep).as_deref() {
               Some(ix_common::env::ConstantInfo::InductInfo(v)) => {
                 v.ctors.clone()
               },
               _ => vec![],
             };
-            let alias_ctors = match lean_env.get(alias) {
+            let alias_ctors = match lean_env.get(alias).as_deref() {
               Some(ix_common::env::ConstantInfo::InductInfo(v)) => {
                 v.ctors.clone()
               },
@@ -964,7 +964,7 @@ pub fn generate_aux_patches(
       // are outside the supported rewrite domain; skipping leaves the
       // original compile, which kernel-check reports per constant.
       let target_ok = matches!(
-        lean_env.get(&target_name),
+        lean_env.get(&target_name).as_deref(),
         Some(ix_common::env::ConstantInfo::RecInfo(r))
           if crate::compile::nat_conv::nat_to_usize(&r.num_motives) == 1
       );
diff --git a/crates/compile/src/compile/aux_gen/below.rs b/crates/compile/src/compile/aux_gen/below.rs
index 407dc5e7d..2d68204db 100644
--- a/crates/compile/src/compile/aux_gen/below.rs
+++ b/crates/compile/src/compile/aux_gen/below.rs
@@ -127,7 +127,7 @@ pub fn generate_below_constants(
     let class_rep = &sorted_classes[ci][0];
 
     let ind_ref = lean_env.get(class_rep);
-    let ind = match ind_ref {
+    let ind = match ind_ref.as_deref() {
       Some(ConstantInfo::InductInfo(v)) => v,
       _ => {
         return Err(CompileError::MissingConstant {
@@ -181,7 +181,7 @@ pub fn generate_below_constants(
     if n_aux > 0 {
       let first_class_name = &sorted_classes[0][0];
       let first_ind_ref = lean_env.get(first_class_name);
-      let first_ind = match first_ind_ref {
+      let first_ind = match first_ind_ref.as_deref() {
         Some(ConstantInfo::InductInfo(v)) => v,
         _ => {
           return Err(CompileError::MissingConstant {
@@ -413,7 +413,7 @@ fn extract_major_head_ind(
   };
   let (head, _) = decompose_apps(major_dom);
   match head.as_data() {
-    ExprData::Const(name, _, _) => match lean_env.get(name) {
+    ExprData::Const(name, _, _) => match lean_env.get(name).as_deref() {
       Some(ConstantInfo::InductInfo(v)) => Some(v.clone()),
       _ => None,
     },
@@ -639,7 +639,7 @@ fn build_below_indc(
   for class_idx in 0..n_classes {
     let class_rep = &sorted_classes[class_idx][0];
     let class_ind_ref = lean_env.get(class_rep);
-    let class_ind = match class_ind_ref {
+    let class_ind = match class_ind_ref.as_deref() {
       Some(ConstantInfo::InductInfo(v)) => v,
       _ => {
         return Err(CompileError::MissingConstant {
@@ -656,7 +656,7 @@ fn build_below_indc(
       if class_idx == ci {
         // This ctor belongs to our class — build a .below ctor for it
         let ctor_ref = lean_env.get(ctor_name);
-        let ctor = match ctor_ref {
+        let ctor = match ctor_ref.as_deref() {
           Some(ConstantInfo::CtorInfo(c)) => c,
           _ => {
             return Err(CompileError::MissingConstant {
@@ -803,7 +803,7 @@ fn build_below_indc_ctor(
   let orig_below_ctor_name = below_name.append_components(&ctor_suffix);
   let orig_field_names: Vec<Name> = lean_env
     .get(&orig_below_ctor_name)
-    .and_then(|ci| match ci {
+    .and_then(|ci| match &*ci {
       ConstantInfo::CtorInfo(cv) => {
         let mut names = Vec::new();
         let mut ty = cv.cnst.typ.clone();
@@ -871,7 +871,7 @@ fn build_below_indc_ctor(
   let all_ind_names: Vec<(Name, usize)> = (0..n_classes)
     .flat_map(|j| {
       sorted_classes[j].iter().filter_map(move |name| {
-        lean_env.get(name).map(|ci| match ci {
+        lean_env.get(name).map(|ci| match &*ci {
           ConstantInfo::InductInfo(v) => (v.cnst.name.clone(), j),
           _ => (name.clone(), j),
         })
diff --git a/crates/compile/src/compile/aux_gen/brecon.rs b/crates/compile/src/compile/aux_gen/brecon.rs
index fdcd0582b..6f340cd13 100644
--- a/crates/compile/src/compile/aux_gen/brecon.rs
+++ b/crates/compile/src/compile/aux_gen/brecon.rs
@@ -79,7 +79,7 @@ pub fn generate_brecon_constants(
     let (_, rec_val) = &canonical_recs[ci];
     let class_rep = &sorted_classes[ci][0];
     let ind_ref = lean_env.get(class_rep);
-    let ind = match ind_ref {
+    let ind = match ind_ref.as_deref() {
       Some(ConstantInfo::InductInfo(v)) => v,
       _ => {
         return Err(CompileError::MissingConstant {
@@ -147,7 +147,7 @@ pub fn generate_brecon_constants(
     if n_aux > 0 {
       // all[0] from the first class's inductive — Lean hangs _N names here.
       let first_class_name = &sorted_classes[0][0];
-      let all0 = match lean_env.get(first_class_name) {
+      let all0 = match lean_env.get(first_class_name).as_deref() {
         Some(ConstantInfo::InductInfo(v)) => v.all[0].clone(),
         _ => first_class_name.clone(),
       };
@@ -991,7 +991,7 @@ fn build_type_brecon_fvar(
   // NestedParam.RoseA α: List.casesOn needs (α := RoseA α).
   let cases_on_spec: Vec<LeanExpr> = if ci >= n_classes {
     let (_, major_args) = decompose_apps(&major_decls[0].domain);
-    let ext_n_params = match lean_env.get(&target_ind_name) {
+    let ext_n_params = match lean_env.get(&target_ind_name).as_deref() {
       Some(ConstantInfo::InductInfo(v)) => try_nat_to_usize(&v.num_params)?,
       _ => 0,
     };
@@ -1500,7 +1500,7 @@ fn build_type_brecon_eq_fvar(
       let (head, _) = decompose_apps(&last_dom);
       match head.as_data() {
         ExprData::Const(name, _, _) | ExprData::Fvar(name, _) => {
-          match lean_env.get(name) {
+          match lean_env.get(name).as_deref() {
             Some(ConstantInfo::InductInfo(v)) => v.ctors.len(),
             _ => 0,
           }
@@ -1509,7 +1509,7 @@ fn build_type_brecon_eq_fvar(
       }
     })
     .collect();
-  let target_ctors: Vec<Name> = match lean_env.get(target_ind_name) {
+  let target_ctors: Vec<Name> = match lean_env.get(target_ind_name).as_deref() {
     Some(ConstantInfo::InductInfo(v)) => v.ctors.clone(),
     _ => vec![],
   };
diff --git a/crates/compile/src/compile/aux_gen/cases_on.rs b/crates/compile/src/compile/aux_gen/cases_on.rs
index b14a41638..bad60eee0 100644
--- a/crates/compile/src/compile/aux_gen/cases_on.rs
+++ b/crates/compile/src/compile/aux_gen/cases_on.rs
@@ -75,7 +75,7 @@ pub fn generate_cases_on(
   let target_idx = rec_val.all.iter().position(|n| *n == target_ind)?;
 
   // Determine elimination level
-  let ind_n_lparams = match lean_env.get(&target_ind) {
+  let ind_n_lparams = match lean_env.get(&target_ind).as_deref() {
     Some(ConstantInfo::InductInfo(v)) => v.cnst.level_params.len(),
     _ => return None,
   };
@@ -90,7 +90,7 @@ pub fn generate_cases_on(
   let ctor_counts: Vec<usize> = rec_val
     .all
     .iter()
-    .map(|ind_name| match lean_env.get(ind_name) {
+    .map(|ind_name| match lean_env.get(ind_name).as_deref() {
       Some(ConstantInfo::InductInfo(v)) => v.ctors.len(),
       _ => 0,
     })
@@ -355,7 +355,7 @@ fn get_minor_name(
   lean_env: &LeanEnv,
 ) -> Name {
   let ctor_idx = minor_idx - target_range.start;
-  if let Some(ConstantInfo::InductInfo(v)) = lean_env.get(target_ind)
+  if let Some(ConstantInfo::InductInfo(v)) = lean_env.get(target_ind).as_deref()
     && let Some(ctor_name) = v.ctors.get(ctor_idx)
   {
     // Strip prefix to get suffix (e.g., "A.mk" → "mk")
diff --git a/crates/compile/src/compile/aux_gen/expr_utils.rs b/crates/compile/src/compile/aux_gen/expr_utils.rs
index ec024ee52..5d7ca9f78 100644
--- a/crates/compile/src/compile/aux_gen/expr_utils.rs
+++ b/crates/compile/src/compile/aux_gen/expr_utils.rs
@@ -1969,7 +1969,7 @@ fn ensure_in_kenv_of_inner_env(
     }
   }
 
-  let Some(ci) = lean_env.get(name).cloned() else { return };
+  let Some(ci) = lean_env.get(name).map(|e| e.cloned()) else { return };
   // Helper: convert a LeanExpr to KExpr with the given level param names,
   // using the KEnv's persistent ingress cache. Callers are top-level, so
   // we start with an empty binder-name stack.
@@ -1998,7 +1998,7 @@ fn ensure_in_kenv_of_inner_env(
       let ty_z = to_z(&ind.cnst.typ, lp, kenv);
       let mut ctor_zids = Vec::new();
       for ctor_name in &ind.ctors {
-        if let Some(LCI::CtorInfo(ctor)) = lean_env.get(ctor_name) {
+        if let Some(LCI::CtorInfo(ctor)) = lean_env.get(ctor_name).as_deref() {
           let ctor_zid = KId::new(
             resolve_lean_name_addr(ctor_name, n2a, aux_n2a),
             ctor_name.clone(),
diff --git a/crates/compile/src/compile/aux_gen/nested.rs b/crates/compile/src/compile/aux_gen/nested.rs
index b7841a091..1ddaf41b3 100644
--- a/crates/compile/src/compile/aux_gen/nested.rs
+++ b/crates/compile/src/compile/aux_gen/nested.rs
@@ -247,7 +247,7 @@ impl<'a> ExpandCtx<'a> {
 
     // Verify head is an external inductive.
     let ext_ind_ref = self.lean_env.get(&head_name);
-    let ext_ind = match ext_ind_ref {
+    let ext_ind = match ext_ind_ref.as_deref() {
       Some(ConstantInfo::InductInfo(v)) => v,
       _ => return None,
     };
@@ -313,7 +313,7 @@ impl<'a> ExpandCtx<'a> {
 
     for j_name in &ext_all {
       let j_info_ref = self.lean_env.get(j_name);
-      let j_info = match j_info_ref {
+      let j_info = match j_info_ref.as_deref() {
         Some(ConstantInfo::InductInfo(v)) => v,
         _ => continue,
       };
@@ -356,7 +356,7 @@ impl<'a> ExpandCtx<'a> {
       let mut aux_ctors: Vec<ExpandedCtor> = Vec::new();
       for j_ctor_name in &j_info.ctors {
         let j_ctor_ref = self.lean_env.get(j_ctor_name);
-        let j_ctor = match j_ctor_ref {
+        let j_ctor = match j_ctor_ref.as_deref() {
           Some(ConstantInfo::CtorInfo(c)) => c,
           _ => continue,
         };
@@ -436,7 +436,7 @@ pub fn expand_nested_block(
     }
   })?;
   let first_ind_ref = lean_env.get(first_name);
-  let first_ind = match first_ind_ref {
+  let first_ind = match first_ind_ref.as_deref() {
     Some(ConstantInfo::InductInfo(v)) => v,
     _ => {
       return Err(CompileError::MissingConstant {
@@ -481,7 +481,7 @@ pub fn expand_nested_block(
   // Seed with original inductives.
   for name in ordered_originals {
     let ind_ref = lean_env.get(name);
-    let ind = match ind_ref {
+    let ind = match ind_ref.as_deref() {
       Some(ConstantInfo::InductInfo(v)) => v,
       _ => {
         return Err(CompileError::MissingConstant {
@@ -493,7 +493,7 @@ pub fn expand_nested_block(
     let ctors: Vec<ExpandedCtor> = ind
       .ctors
       .iter()
-      .filter_map(|cn| match lean_env.get(cn) {
+      .filter_map(|cn| match lean_env.get(cn).as_deref() {
         Some(ConstantInfo::CtorInfo(c)) => Some(ExpandedCtor {
           name: c.cnst.name.clone(),
           typ: c.cnst.typ.clone(),
@@ -1694,7 +1694,7 @@ pub fn build_compile_flat_block_with_overlay(
   let first_ind_ref = overlay
     .and_then(|o| o.get(first_name))
     .or_else(|| lean_env.get(first_name));
-  let first_ind = match first_ind_ref {
+  let first_ind = match first_ind_ref.as_deref() {
     Some(ConstantInfo::InductInfo(v)) => v,
     _ => {
       return Err(CompileError::MissingConstant {
@@ -1729,7 +1729,7 @@ pub fn build_compile_flat_block_with_overlay(
   for name in ordered_originals {
     let ind_ref =
       overlay.and_then(|o| o.get(name)).or_else(|| lean_env.get(name));
-    let ind = match ind_ref {
+    let ind = match ind_ref.as_deref() {
       Some(ConstantInfo::InductInfo(v)) => v,
       _ => {
         return Err(CompileError::MissingConstant {
@@ -1764,7 +1764,7 @@ pub fn build_compile_flat_block_with_overlay(
     let member_ref = overlay
       .and_then(|o| o.get(&member.name))
       .or_else(|| lean_env.get(&member.name));
-    let (ctor_names, level_params) = match member_ref {
+    let (ctor_names, level_params) = match member_ref.as_deref() {
       Some(ConstantInfo::InductInfo(v)) => {
         (v.ctors.clone(), v.cnst.level_params.clone())
       },
@@ -1775,7 +1775,7 @@ pub fn build_compile_flat_block_with_overlay(
       let ctor_ref = overlay
         .and_then(|o| o.get(ctor_name))
         .or_else(|| lean_env.get(ctor_name));
-      let (ctor_n_fields, ctor_typ) = match ctor_ref {
+      let (ctor_n_fields, ctor_typ) = match ctor_ref.as_deref() {
         Some(ConstantInfo::CtorInfo(c)) => {
           let fields = nat_to_usize(&c.num_fields);
           (fields, c.cnst.typ.clone())
@@ -1989,7 +1989,7 @@ fn try_detect_nested_fvar(
   let head_ref = overlay
     .and_then(|o| o.get(&head_name))
     .or_else(|| lean_env.get(&head_name));
-  let (ext_n_params, ext_n_indices) = match head_ref {
+  let (ext_n_params, ext_n_indices) = match head_ref.as_deref() {
     Some(ConstantInfo::InductInfo(v)) => {
       let p = nat_to_usize(&v.num_params);
       let i = nat_to_usize(&v.num_indices);
@@ -2110,29 +2110,42 @@ pub fn compute_lean_ind_flags(
 /// Validate that every inductive group in `lean_env` carries exactly the flags
 /// `compute_lean_ind_flags` recomputes.
 pub fn validate_lean_ind_flags(lean_env: &LeanEnv) -> Result<(), CompileError> {
-  let mut groups: FxHashMap<&Name, &[Name]> = FxHashMap::default();
-  for ci in lean_env.values() {
-    if let ConstantInfo::InductInfo(v) = ci
+  let mut groups: FxHashMap<Name, Vec<Name>> = FxHashMap::default();
+  for (_, ci) in lean_env.iter() {
+    if let ConstantInfo::InductInfo(v) = &*ci
       && let Some(first) = v.all.first()
     {
-      groups.entry(first).or_insert(v.all.as_slice());
+      groups.entry(first.clone()).or_insert_with(|| v.all.clone());
     }
   }
-  //let groups: Vec<(&Name, &[Name])> = groups.into_iter().collect();
+  validate_ind_groups(&groups, lean_env)
+}
+
+/// Per-group half of [`validate_lean_ind_flags`], for callers that
+/// already hold the inductive groups from a wider env pass.
+pub fn validate_ind_groups(
+  groups: &FxHashMap<Name, Vec<Name>>,
+  lean_env: &LeanEnv,
+) -> Result<(), CompileError> {
   groups.par_iter().try_for_each(|(_, all)| {
     for member in all.iter() {
-      let Some(ConstantInfo::InductInfo(v)) = lean_env.get(member) else {
+      let entry = lean_env.get(member);
+      let Some(ConstantInfo::InductInfo(v)) = entry.as_deref() else {
         return Ok(());
       };
       for cn in &v.ctors {
-        if !matches!(lean_env.get(cn), Some(ConstantInfo::CtorInfo(_))) {
+        if !matches!(
+          lean_env.get(cn).as_deref(),
+          Some(ConstantInfo::CtorInfo(_))
+        ) {
           return Ok(());
         }
       }
     }
     let flags = compute_lean_ind_flags(all, lean_env)?;
     for member in all.iter() {
-      let Some(ConstantInfo::InductInfo(v)) = lean_env.get(member) else {
+      let entry = lean_env.get(member);
+      let Some(ConstantInfo::InductInfo(v)) = entry.as_deref() else {
         continue; // unreachable
       };
       if v.is_rec != flags.is_rec
@@ -2525,8 +2538,12 @@ mod tests {
   fn validate_lean_ind_flags_skips_unresolvable_group() {
     // Wrong flags, but the ctor entry is removed → group unresolvable →
     // skipped (grounding owns partial envs), not rejected.
-    let mut env = flags_env(false, false, 0);
-    env.remove(&mk_name_for("N.mk"));
+    let full = flags_env(false, false, 0);
+    let env: LeanEnv = full
+      .iter()
+      .filter(|(n, _)| **n != mk_name_for("N.mk"))
+      .map(|(n, ci)| (n.clone(), ci.cloned()))
+      .collect();
     assert!(validate_lean_ind_flags(&env).is_ok());
   }
 }
diff --git a/crates/compile/src/compile/aux_gen/recursor.rs b/crates/compile/src/compile/aux_gen/recursor.rs
index 1eb607c9d..111f25a4e 100644
--- a/crates/compile/src/compile/aux_gen/recursor.rs
+++ b/crates/compile/src/compile/aux_gen/recursor.rs
@@ -79,7 +79,7 @@ pub fn generate_recursors_from_expanded(
   // the correct `RecursorVal::is_unsafe` / `DefinitionSafety`.
   let block_is_unsafe = original_names
     .first()
-    .and_then(|n| match lean_env.get(n) {
+    .and_then(|n| match lean_env.get(n).as_deref() {
       Some(ConstantInfo::InductInfo(v)) => Some(v.is_unsafe),
       _ => None,
     })
@@ -93,7 +93,7 @@ pub fn generate_recursors_from_expanded(
     // when available. For auxiliary types (not in lean_env), fall back to
     // block-wide defaults.
     let (all_field, is_rec, is_reflexive, ind_is_unsafe) =
-      match lean_env.get(&member.name) {
+      match lean_env.get(&member.name).as_deref() {
         Some(ConstantInfo::InductInfo(orig)) => {
           (orig.all.clone(), orig.is_rec, orig.is_reflexive, orig.is_unsafe)
         },
@@ -121,7 +121,7 @@ pub fn generate_recursors_from_expanded(
       // Look up original ctor's safety when available; fall back to the
       // containing inductive's flag (ctor safety always matches its parent
       // inductive — the kernel rejects unsafe ctors on safe inductives).
-      let ctor_is_unsafe = match lean_env.get(&ctor.name) {
+      let ctor_is_unsafe = match lean_env.get(&ctor.name).as_deref() {
         Some(ConstantInfo::CtorInfo(orig)) => orig.is_unsafe,
         _ => ind_is_unsafe,
       };
@@ -478,8 +478,8 @@ pub fn generate_canonical_recursors_with_layout(
   // Lookup helper: check overlay first, then base env.
   let env_get = |name: &Name| -> Option<ConstantInfo> {
     overlay
-      .and_then(|o| o.get(name).cloned())
-      .or_else(|| lean_env.get(name).cloned())
+      .and_then(|o| o.get(name).map(|e| e.cloned()))
+      .or_else(|| lean_env.get(name).map(|e| e.cloned()))
   };
 
   let mut classes: Vec<FlatInfo> = sorted_classes
@@ -954,8 +954,8 @@ fn build_rec_type(
 ) -> LeanExpr {
   let env_get = |name: &Name| -> Option<ConstantInfo> {
     overlay
-      .and_then(|o| o.get(name).cloned())
-      .or_else(|| lean_env.get(name).cloned())
+      .and_then(|o| o.get(name).map(|e| e.cloned()))
+      .or_else(|| lean_env.get(name).map(|e| e.cloned()))
   };
   let n_flat = flat.len();
 
@@ -1234,7 +1234,9 @@ fn build_motive_type_aux(
 ) -> LeanExpr {
   // Look up the external inductive (check overlay first for expanded aux types).
   let env_get_local = |n: &Name| -> Option<ConstantInfo> {
-    overlay.and_then(|o| o.get(n).cloned()).or_else(|| lean_env.get(n).cloned())
+    overlay
+      .and_then(|o| o.get(n).map(|e| e.cloned()))
+      .or_else(|| lean_env.get(n).map(|e| e.cloned()))
   };
   let ind = match env_get_local(&member.name) {
     Some(ConstantInfo::InductInfo(v)) => v,
@@ -2558,7 +2560,7 @@ fn ingress_target_type_deps(
       continue;
     }
     if let Some(ci) = lean_env.get(&name) {
-      ingress_aux_gen_dep(&name, ci, lean_env, stt, kctx, &mut queue);
+      ingress_aux_gen_dep(&name, &ci, lean_env, stt, kctx, &mut queue);
     }
   }
 }
@@ -2588,7 +2590,7 @@ fn ingress_field_deps(
     }
 
     let Some(ci) = lean_env.get(&name) else { continue };
-    ingress_aux_gen_dep(&name, ci, lean_env, stt, kctx, &mut queue);
+    ingress_aux_gen_dep(&name, &ci, lean_env, stt, kctx, &mut queue);
   }
 }
 
@@ -2610,7 +2612,9 @@ fn ingress_aux_gen_dep(
       super::expr_utils::ensure_full_in_kenv_of(name, lean_env, stt, kctx);
       collect_const_refs(&v.cnst.typ, queue);
       for ctor_name in &v.ctors {
-        if let Some(ConstantInfo::CtorInfo(ctor)) = lean_env.get(ctor_name) {
+        if let Some(ConstantInfo::CtorInfo(ctor)) =
+          lean_env.get(ctor_name).as_deref()
+        {
           collect_const_refs(&ctor.cnst.typ, queue);
         }
       }
@@ -3566,7 +3570,7 @@ mod tests {
 
     let mut cs = Vec::new();
     for name in [&a, &b] {
-      match env.get(name) {
+      match env.get(name).as_deref() {
         Some(LeanCI::InductInfo(v)) => {
           cs.push(MutConst::Indc(
             mk_indc(v, &std::sync::Arc::new(env.clone())).unwrap(),
diff --git a/crates/compile/src/compile/env.rs b/crates/compile/src/compile/env.rs
index 4b92f7455..1afba1661 100644
--- a/crates/compile/src/compile/env.rs
+++ b/crates/compile/src/compile/env.rs
@@ -1,6 +1,34 @@
 //! Top-level environment compilation with work-stealing parallelism.
 //!
 //! Extracted from `compile.rs` to keep the scheduler independently readable.
+//!
+//! # Memory
+//!
+//! Peak RSS is kept a small multiple of the environment's serialized
+//! size (Mathlib: ~19 GB for a 3 GB `.ixe`) by holding compact
+//! representations everywhere the structured forms aren't actually
+//! read: the Lean environment decodes on demand behind a bounded cache
+//! (`decode_env_lazy` in the ffi crate) rather than as a whole-env
+//! owned copy, accumulator constants and named metadata live as their
+//! serialized bytes rather than ~20×-larger structured forms, worker
+//! kernel envs clear periodically, the setup passes share one
+//! whole-env decode, and the `.ixe` streams to disk from Rust rather
+//! than crossing the FFI as an env-sized ByteArray. All of it is
+//! always on, and every mode produces a bit-identical `.ixe`.
+//!
+//! Three knobs:
+//! - `IX_COMPILE_WORKERS=N` — scheduler worker count (default: all
+//!   cores). Scales the per-worker transients.
+//! - `IX_COMPILE_DEMOTE=0` — keep materialized caches next to the
+//!   accumulator's bytes instead of demoting to bytes-only. Spends
+//!   RAM to make post-compile structural reads free, which only pays
+//!   in flows that re-read the compiled env in-process (`ix check` /
+//!   `ix validate`); `ix compile` itself never reads them back.
+//! - `IX_COMPILE_EAGER=1` — decode the whole Lean environment up
+//!   front instead of on demand. Spends the single largest memory
+//!   term (FLT: +13 GiB for −8 % wall; Mathlib needs a large-memory
+//!   machine) to shave the last few percent on hardware with RAM to
+//!   spare.
 
 use std::panic::{AssertUnwindSafe, catch_unwind};
 use std::sync::{
@@ -16,12 +44,11 @@ use rustc_hash::FxHashSet;
 
 use crate::compile::{
   BlockCache, CompileOptions, CompileState,
-  aux_gen::nested::validate_lean_ind_flags, compile_const,
-  compile_const_no_aux,
+  aux_gen::nested::validate_ind_groups, compile_const, compile_const_no_aux,
 };
 use crate::condense::compute_sccs;
-use crate::graph::{NameSet, build_ref_graph};
-use crate::ground::ground_consts;
+use crate::graph::{NameSet, setup_scan};
+use crate::ground::proliferate_ungrounded;
 use ix_common::address::Address;
 use ix_common::env::{Env as LeanEnv, Name};
 use ixon::CompileError;
@@ -48,6 +75,14 @@ static IX_PROGRESS_MS: LazyLock<u64> = LazyLock::new(|| {
     .unwrap_or(2000)
 });
 
+/// Clear each worker's kernel env every this many completed blocks
+/// (releasing allocations). The kenv is a pure cache of
+/// Lean-env-derived data (`ensure_in_kenv` re-ingresses on demand), so
+/// clearing at block boundaries is semantics-free; unbounded it grows
+/// to several GB on Mathlib-scale envs, and this cadence measures at
+/// zero wall-clock cost there.
+const KENV_CLEAR_EVERY: usize = 64;
+
 /// Recover a short string description from a panic payload.
 fn panic_message(panic: &(dyn std::any::Any + Send)) -> String {
   panic
@@ -113,28 +148,50 @@ pub fn compile_env_with_options(
   options: CompileOptions,
 ) -> Result<CompileState, CompileError> {
   let setup_start = Instant::now();
+  // Whole-env scan: ref graph + immediate groundedness + inductive
+  // groups in one decode per constant — the env decodes lazily, so
+  // each additional full sweep would decode every constant again.
   let phase_start = Instant::now();
-  let graph = build_ref_graph(lean_env.as_ref());
+  let scan = setup_scan(lean_env.as_ref());
+  let graph = scan.graph;
   if !*IX_QUIET {
     eprintln!(
-      "[compile_env] setup 1/7 build_ref_graph: {:.2}s",
+      "[compile_env] setup 1/7 setup_scan (graph+ground+groups): {:.2}s",
       phase_start.elapsed().as_secs_f32()
     );
   }
 
-  // Grounding pass: identify constants whose transitive Const-refs can't all
-  // be resolved. These are collected into `stt.ungrounded` and filtered from
-  // the SCC input so they don't clog the scheduler. Callers (e.g. the kernel
-  // check FFI) inspect `stt.ungrounded` per-constant to report them as
-  // compile-side rejections without aborting the whole batch.
+  // Grounding: constants whose transitive Const-refs can't all be
+  // resolved are collected into `stt.ungrounded` and filtered from the
+  // SCC input so they don't clog the scheduler. Callers (e.g. the
+  // kernel check FFI) inspect `stt.ungrounded` per-constant to report
+  // them as compile-side rejections without aborting the whole batch.
   let phase_start = Instant::now();
-  let ungrounded = ground_consts(lean_env.as_ref(), &graph.in_refs);
+  let ungrounded =
+    proliferate_ungrounded(scan.immediate_ungrounded, &graph.in_refs);
   if !*IX_QUIET {
     eprintln!(
-      "[compile_env] setup 2/7 ground_consts: {:.2}s",
+      "[compile_env] setup 2/7 proliferate_ungrounded: {:.2}s",
       phase_start.elapsed().as_secs_f32()
     );
   }
+  // Pin the highest-in-degree constants in the lazy env: the ref
+  // graph gives exact reference counts, and the distribution is
+  // heavily skewed, so a small never-evicted set absorbs repeat
+  // decodes of foundational constants that otherwise churn through
+  // the bounded cache. At this size the overlay costs ≤0.3 GiB on
+  // every measured env and wall time is Lean −15 %, FLT −4 %,
+  // InitStd/Mathlib neutral (24-core box); larger sets bought RAM,
+  // not speed, on the same sweep.
+  const PIN_HOT_CONSTANTS: usize = 16384;
+  if !graph.in_refs.is_empty() {
+    let mut by_deg: Vec<(&Name, usize)> =
+      graph.in_refs.iter().map(|(n, refs)| (n, refs.len())).collect();
+    let k = PIN_HOT_CONSTANTS.min(by_deg.len());
+    by_deg.select_nth_unstable_by(k - 1, |a, b| b.1.cmp(&a.1));
+    lean_env.pin(by_deg[..k].iter().map(|(n, _)| (*n).clone()));
+  }
+
   let ungrounded_map: DashMap<Name, String> =
     ungrounded.iter().map(|(n, e)| (n.clone(), format!("{e:?}"))).collect();
   if !ungrounded.is_empty() && !*IX_QUIET {
@@ -179,9 +236,11 @@ pub fn compile_env_with_options(
     );
   }
 
-  // Domain restriction: reject environments with non-canonical inductive flags
+  // Domain restriction: reject environments with non-canonical inductive
+  // flags. Groups come from the fused scan; only inductive families are
+  // re-read here.
   let phase_start = Instant::now();
-  validate_lean_ind_flags(lean_env.as_ref())?;
+  validate_ind_groups(&scan.ind_groups, lean_env.as_ref())?;
   if !*IX_QUIET {
     eprintln!(
       "[compile_env] setup 4/7 validate_ind_flags: {:.2}s",
@@ -467,6 +526,7 @@ pub fn compile_env_with_options(
     for _ in 0..num_threads {
       s.spawn(move || {
         let mut worker_kctx = crate::compile::KernelCtx::new();
+        let mut worker_blocks_done = 0usize;
         loop {
           // Try to get work from the ready queue
           let work = {
@@ -825,6 +885,12 @@ pub fn compile_env_with_options(
               } else {
                 condvar_ref.notify_one();
               }
+
+              // Bounded per-worker kenv growth (see KENV_CLEAR_EVERY).
+              worker_blocks_done += 1;
+              if worker_blocks_done.is_multiple_of(KENV_CLEAR_EVERY) {
+                worker_kctx.kenv.clear_releasing_memory();
+              }
             },
             None => {
               // No work available - check if we're done
diff --git a/crates/compile/src/compile/mutual.rs b/crates/compile/src/compile/mutual.rs
index 68bbca19b..db478df0d 100644
--- a/crates/compile/src/compile/mutual.rs
+++ b/crates/compile/src/compile/mutual.rs
@@ -617,7 +617,7 @@ pub fn generate_and_compile_aux_recursors(
     let mut source_ctor_counts: Vec<usize> =
       Vec::with_capacity(src_order.len());
     for (head, _) in &src_order {
-      match lean_env.get(head) {
+      match lean_env.get(head).as_deref() {
         Some(LeanConstantInfo::InductInfo(v)) => {
           source_ctor_counts.push(v.ctors.len());
         },
diff --git a/crates/compile/src/compile/surgery.rs b/crates/compile/src/compile/surgery.rs
index de8d70caa..f54b1e784 100644
--- a/crates/compile/src/compile/surgery.rs
+++ b/crates/compile/src/compile/surgery.rs
@@ -294,7 +294,7 @@ pub fn compute_call_site_plans(
   // counts are not included here; they're handled separately below.
   let ctor_counts: Vec<usize> = original_all
     .iter()
-    .map(|n| match lean_env.get(n) {
+    .map(|n| match lean_env.get(n).as_deref() {
       Some(LeanConstantInfo::InductInfo(v)) => v.ctors.len(),
       _ => 0,
     })
@@ -314,7 +314,7 @@ pub fn compute_call_site_plans(
     .iter()
     .find_map(|n| {
       let rec_name = Name::str(n.clone(), "rec".to_string());
-      match lean_env.get(&rec_name) {
+      match lean_env.get(&rec_name).as_deref() {
         Some(LeanConstantInfo::RecInfo(r)) => Some((
           nat_to_usize(&r.num_params),
           nat_to_usize(&r.num_indices),
@@ -428,7 +428,7 @@ pub fn compute_call_site_plans(
     .iter()
     .map(|class| {
       let rep = &class[0];
-      match lean_env.get(rep) {
+      match lean_env.get(rep).as_deref() {
         Some(LeanConstantInfo::InductInfo(v)) => v.ctors.len(),
         _ => 0,
       }
@@ -749,7 +749,7 @@ pub fn compute_call_site_plans(
         }
         let target_rec = Name::str(ext_head.clone(), "rec".to_string());
         let target_ok = matches!(
-          lean_env.get(&target_rec),
+          lean_env.get(&target_rec).as_deref(),
           Some(LeanConstantInfo::RecInfo(r))
             if nat_to_usize(&r.num_motives) == 1
         );
@@ -758,7 +758,7 @@ pub fn compute_call_site_plans(
         }
         // Index count comes from the aux recursor itself (the external
         // inductive's indices), not the block-wide default.
-        let rec_n_indices = match lean_env.get(&rec_name) {
+        let rec_n_indices = match lean_env.get(&rec_name).as_deref() {
           Some(LeanConstantInfo::RecInfo(r)) => nat_to_usize(&r.num_indices),
           _ => n_indices,
         };
@@ -847,7 +847,7 @@ pub fn adapt_split_minor(
   }
 
   let rec_info = lean_env.get(rec_name)?;
-  let rec = match rec_info {
+  let rec = match &*rec_info {
     LeanConstantInfo::RecInfo(rec) => rec,
     _ => return None,
   };
@@ -948,14 +948,14 @@ fn source_ctor_for_minor(
   let mut offset = 0usize;
   for (source_pos, ind_name) in rec.all.iter().enumerate() {
     let ind_info = lean_env.get(ind_name)?;
-    let ind = match ind_info {
+    let ind = match &*ind_info {
       LeanConstantInfo::InductInfo(ind) => ind,
       _ => return None,
     };
     let n_ctors = ind.ctors.len();
     if src_minor_idx < offset + n_ctors {
       let ctor_name = &ind.ctors[src_minor_idx - offset];
-      let ctor = match lean_env.get(ctor_name)? {
+      let ctor = match &*lean_env.get(ctor_name)? {
         LeanConstantInfo::CtorInfo(ctor) => ctor.clone(),
         _ => return None,
       };
@@ -967,14 +967,14 @@ fn source_ctor_for_minor(
   // order. The ctor list is the external inductive's own (the aux is the
   // external applied at spec args, so field counts match).
   for sig in aux_sigs {
-    let Some(LeanConstantInfo::InductInfo(ind)) = lean_env.get(&sig.ext_name)
-    else {
+    let ext_entry = lean_env.get(&sig.ext_name);
+    let Some(LeanConstantInfo::InductInfo(ind)) = ext_entry.as_deref() else {
       return None;
     };
     let n_ctors = ind.ctors.len();
     if src_minor_idx < offset + n_ctors {
       let ctor_name = &ind.ctors[src_minor_idx - offset];
-      let ctor = match lean_env.get(ctor_name)? {
+      let ctor = match &*lean_env.get(ctor_name)? {
         LeanConstantInfo::CtorInfo(ctor) => ctor.clone(),
         _ => return None,
       };
@@ -1042,7 +1042,7 @@ fn aux_motive_sigs(
             let (head, t_args) = decompose_apps(&t);
             if let ExprData::Const(ext_name, _, _) = head.as_data()
               && let Some(LeanConstantInfo::InductInfo(ind)) =
-                lean_env.get(ext_name)
+                lean_env.get(ext_name).as_deref()
             {
               let ext_n_params = nat_to_usize(&ind.num_params);
               if t_args.len() >= ext_n_params {
@@ -1081,7 +1081,8 @@ pub fn derive_head_rewrite_app(
   motives: &[LeanExpr],
   lean_env: &LeanEnv,
 ) -> Result<(Vec<Level>, Vec<LeanExpr>), String> {
-  let Some(LeanConstantInfo::RecInfo(rec)) = lean_env.get(rec_name) else {
+  let rec_entry = lean_env.get(rec_name);
+  let Some(LeanConstantInfo::RecInfo(rec)) = rec_entry.as_deref() else {
     return Err(format!("'{}' is not a recursor", rec_name.pretty()));
   };
   let sigs = aux_motive_sigs(rec, rec_levels, params, motives, lean_env);
@@ -1135,8 +1136,8 @@ pub fn derive_head_rewrite_app(
       _ => return Err("major type head is not a constant".into()),
     }
   };
-  let Some(LeanConstantInfo::RecInfo(target)) = lean_env.get(&hr.target_rec)
-  else {
+  let target_entry = lean_env.get(&hr.target_rec);
+  let Some(LeanConstantInfo::RecInfo(target)) = target_entry.as_deref() else {
     return Err(format!(
       "target recursor '{}' missing from env",
       hr.target_rec.pretty()
@@ -1261,7 +1262,7 @@ fn find_source_rec_target(
     return None;
   };
   if let Some(source_pos) = original_all.iter().position(|n| n == target_name) {
-    let target_n_params = match lean_env.get(target_name)? {
+    let target_n_params = match &*lean_env.get(target_name)? {
       LeanConstantInfo::InductInfo(ind) => nat_to_usize(&ind.num_params),
       _ => return None,
     };
@@ -1436,7 +1437,7 @@ fn dump_plan_state(
   // Dump Lean's source recursor telescope, labelled per binder section.
   let first_rec = original_all.iter().find_map(|n| {
     let rec_name = Name::str(n.clone(), "rec".to_string());
-    match lean_env.get(&rec_name) {
+    match lean_env.get(&rec_name).as_deref() {
       Some(LeanConstantInfo::RecInfo(r)) => {
         Some((rec_name, r.cnst.typ.clone()))
       },
diff --git a/crates/compile/src/decompile.rs b/crates/compile/src/decompile.rs
index 56a7ab62b..536b13816 100644
--- a/crates/compile/src/decompile.rs
+++ b/crates/compile/src/decompile.rs
@@ -1609,9 +1609,8 @@ fn decompile_inductive(
             // structure (e.g., alpha-collapsed with fewer motives) than the
             // expression being decompiled. The original metadata matches the
             // un-collapsed block structure.
-            n.original
-              .as_ref()
-              .map_or_else(|| n.meta.clone(), |(_, m)| m.clone())
+            n.original()
+              .map_or_else(|| (*n.meta()).clone(), |(_, m)| (*m).clone())
           })
           .unwrap_or_default()
       } else {
@@ -1707,7 +1706,8 @@ fn decompile_projection(
   dstt: &DecompileState,
 ) -> Result<(), DecompileError> {
   // Build ctx from metadata's ctx field
-  let ctx_addrs = get_ctx_from_meta(&named.meta);
+  let named_meta = named.meta();
+  let ctx_addrs = get_ctx_from_meta(&named_meta);
   let ctx_names: Vec<Name> = ctx_addrs
     .iter()
     .map(|a| decompile_name(a, stt))
@@ -1727,7 +1727,7 @@ fn decompile_projection(
   // every `_sizeOf_N` — which is a DPrj into its mutual block and
   // whose body's `.rec` surgery produces `Collapsed` entries under
   // alpha-collapse — would fail with shape mismatches on decompile.
-  cache.load_meta_extensions(&named.meta);
+  cache.load_meta_extensions(&named_meta);
 
   // Each projection variant must land on the matching `MutConst` kind
   // at its block index. A silent fall-through would leave `name`
@@ -1737,7 +1737,7 @@ fn decompile_projection(
     ConstantInfo::DPrj(proj) => match mutuals.get(proj.idx as usize) {
       Some(MutConst::Defn(def)) => {
         let info =
-          decompile_definition(def, &named.meta, &mut cache, stt, dstt)?;
+          decompile_definition(def, &named_meta, &mut cache, stt, dstt)?;
         dstt.env.insert(name.clone(), info);
       },
       other => {
@@ -1755,7 +1755,7 @@ fn decompile_projection(
     ConstantInfo::IPrj(proj) => match mutuals.get(proj.idx as usize) {
       Some(MutConst::Indc(ind)) => {
         let (ind_val, ctors) =
-          decompile_inductive(ind, &named.meta, &mut cache, stt, dstt)?;
+          decompile_inductive(ind, &named_meta, &mut cache, stt, dstt)?;
         dstt.env.insert(name.clone(), LeanConstantInfo::InductInfo(ind_val));
         for ctor in ctors {
           dstt
@@ -1777,7 +1777,7 @@ fn decompile_projection(
 
     ConstantInfo::RPrj(proj) => match mutuals.get(proj.idx as usize) {
       Some(MutConst::Recr(rec)) => {
-        let info = decompile_recursor(rec, &named.meta, &mut cache, stt, dstt)?;
+        let info = decompile_recursor(rec, &named_meta, &mut cache, stt, dstt)?;
         dstt.env.insert(name.clone(), info);
       },
       other => {
@@ -1812,8 +1812,7 @@ fn projection_mismatch_error(
 ) -> DecompileError {
   let has_addr = stt.name_to_addr.contains_key(name);
   let has_aux = stt.aux_name_to_addr.contains_key(name);
-  let has_original =
-    stt.env.named.get(name).is_some_and(|n| n.original.is_some());
+  let has_original = stt.env.named.get(name).is_some_and(|n| n.has_original());
   DecompileError::BadConstantFormat {
     msg: format!(
       "{kind} '{}' idx={idx} landed on {:?} (mutuals.len={mutuals_len}, \
@@ -1834,7 +1833,8 @@ fn decompile_const(
   let cnst = read_const(&named.addr, stt)?;
 
   // Build ctx from metadata's all field
-  let all_addrs = get_all_from_meta(&named.meta);
+  let named_meta = named.meta();
+  let all_addrs = get_all_from_meta(&named_meta);
   let all_names: Vec<Name> = all_addrs
     .iter()
     .map(|a| decompile_name(a, stt))
@@ -1852,8 +1852,8 @@ fn decompile_const(
         current_const: current_const.clone(),
         ..Default::default()
       };
-      cache.load_meta_extensions(&named.meta);
-      let info = decompile_definition(def, &named.meta, &mut cache, stt, dstt)?;
+      cache.load_meta_extensions(&named_meta);
+      let info = decompile_definition(def, &named_meta, &mut cache, stt, dstt)?;
       dstt.env.insert(name.clone(), info);
     },
 
@@ -1871,8 +1871,8 @@ fn decompile_const(
       // Defn branch above — omitting this desyncs
       // `CallSiteEntry::Collapsed.sharing_idx` from the intended
       // `meta_sharing` slot.
-      cache.load_meta_extensions(&named.meta);
-      let info = decompile_recursor(rec, &named.meta, &mut cache, stt, dstt)?;
+      cache.load_meta_extensions(&named_meta);
+      let info = decompile_recursor(rec, &named_meta, &mut cache, stt, dstt)?;
       dstt.env.insert(name.clone(), info);
     },
 
@@ -1887,8 +1887,8 @@ fn decompile_const(
       };
       // Axioms have only a type (no body), so no surgery today — but
       // load extensions for consistency with the other branches.
-      cache.load_meta_extensions(&named.meta);
-      let info = decompile_axiom(ax, &named.meta, &mut cache, stt, dstt)?;
+      cache.load_meta_extensions(&named_meta);
+      let info = decompile_axiom(ax, &named_meta, &mut cache, stt, dstt)?;
       dstt.env.insert(name.clone(), info);
     },
 
@@ -1903,8 +1903,8 @@ fn decompile_const(
       };
       // Quotient types have only a type signature — same story as
       // axioms. Load extensions for consistency.
-      cache.load_meta_extensions(&named.meta);
-      let info = decompile_quotient(quot, &named.meta, &mut cache, stt, dstt)?;
+      cache.load_meta_extensions(&named_meta);
+      let info = decompile_quotient(quot, &named_meta, &mut cache, stt, dstt)?;
       dstt.env.insert(name.clone(), info);
     },
 
@@ -2024,7 +2024,7 @@ fn build_block_env(all_names: &[Name], lean_env: &LeanEnv) -> LeanEnv {
   for ind_name in all_names {
     if let Some(ci) = lean_env.get(ind_name) {
       env.insert(ind_name.clone(), ci.clone());
-      if let LeanConstantInfo::InductInfo(v) = ci {
+      if let LeanConstantInfo::InductInfo(v) = &*ci {
         for ctor_name in &v.ctors {
           if let Some(ctor_ci) = lean_env.get(ctor_name) {
             env.insert(ctor_name.clone(), ctor_ci.clone());
@@ -2200,7 +2200,7 @@ fn print_const_comparison(
 ) {
   let Some(orig_env) = orig_env else { return };
   let Some(lean_ci_ref) = orig_env.get(name) else { return };
-  let lean_ci = lean_ci_ref;
+  let lean_ci = &*lean_ci_ref;
   if std::mem::discriminant(decompiled) != std::mem::discriminant(lean_ci) {
     eprintln!(
       "[aux_gen diff] {}: kind decompiled={} original={}",
@@ -2680,8 +2680,8 @@ fn roundtrip_block(
     let orig_addr = if singleton {
       // Singleton: compare directly against the constant's original address.
       stt.env.named.get(&first_name).map(|named| {
-        if let Some((ref orig_a, _)) = named.original {
-          orig_a.clone()
+        if let Some((orig_a, _)) = named.original() {
+          orig_a
         } else {
           named.addr.clone()
         }
@@ -2690,12 +2690,12 @@ fn roundtrip_block(
       // Mutual block: compare against the original block address.
       // The original block addr is stored in the projection's block field.
       stt.env.named.get(&first_name).and_then(|named| {
-        let addr = if let Some((ref orig_a, _)) = named.original {
+        let addr = if let Some((orig_a, _)) = named.original() {
           orig_a
         } else {
-          &named.addr
+          named.addr.clone()
         };
-        stt.env.get_const(addr).map(|c| match &c.info {
+        stt.env.get_const(&addr).map(|c| match &c.info {
           ConstantInfo::RPrj(p) => p.block.clone(),
           ConstantInfo::DPrj(p) => p.block.clone(),
           ConstantInfo::IPrj(p) => p.block.clone(),
@@ -2741,7 +2741,7 @@ fn roundtrip_block(
           if let Some(orig_env) = orig_env
             && let Some(lean_ci_ref) = orig_env.get(&nm)
           {
-            let lean_ci = lean_ci_ref;
+            let lean_ci = &*lean_ci_ref;
             eprintln!("  -- lean  {} --", nm.pretty());
             eprintln!("    type: {}", lean_ci.get_type().pretty());
             if let Some(v) = get_value(lean_ci) {
@@ -2762,7 +2762,7 @@ fn roundtrip_block(
           if let Some(orig_env) = orig_env
             && let Some(ci) = orig_env.get(&nm)
           {
-            match ci {
+            match &*ci {
               LeanConstantInfo::RecInfo(rv) => eprintln!(
                 "  -- lean  {} RecInfo: k={} unsafe={} lvls={} params={} \
                  indices={} motives={} minors={} rule_fields={:?}",
@@ -2807,7 +2807,7 @@ fn roundtrip_block(
         //     divergence is contextual, not a regen defect.
         if singleton && let Some(oenv) = orig_env {
           let nm = consts[0].name();
-          let omc: Option<LeanMutConst> = match oenv.get(&nm) {
+          let omc: Option<LeanMutConst> = match oenv.get(&nm).as_deref() {
             Some(LeanConstantInfo::RecInfo(rv)) => {
               Some(LeanMutConst::Recr(rv.clone()))
             },
@@ -2929,15 +2929,16 @@ fn roundtrip_block(
       // Look up original metadata from compile_const_no_aux. If not
       // available, fall back to Phase A metadata from the current compilation.
       let orig_meta = match stt.env.named.get(&name) {
-        Some(ref named) if named.original.is_some() => {
+        Some(ref named) if named.has_original() => {
+          let (orig_addr, orig_meta) = named.original().unwrap();
           if std::env::var_os("IX_ROUNDTRIP_DEBUG").is_some() {
             eprintln!(
               "[orig_meta] {}: using named.original (addr={:.12})",
               name.pretty(),
-              named.original.as_ref().unwrap().0.hex(),
+              orig_addr.hex(),
             );
           }
-          named.original.as_ref().unwrap().1.clone()
+          (*orig_meta).clone()
         },
         s => {
           if std::env::var_os("IX_ROUNDTRIP_DEBUG").is_some() {
@@ -2991,12 +2992,18 @@ fn roundtrip_block(
             let (mut iv, cvs) =
               decompile_inductive(ind, &orig_meta, &mut dec_cache, stt, dstt)?;
             // Recompute the lean flags, which are not stored by Ixon
-            let flags = compute_lean_ind_flags(&iv.all, generated_consts)
-              .map_err(|e| DecompileError::BadConstantFormat {
-                msg: format!(
-                  "roundtrip ind-flags for '{}': {e}",
-                  name.pretty()
-                ),
+            let flags_env: LeanEnv = generated_consts
+              .iter()
+              .map(|(k, v)| (k.clone(), v.clone()))
+              .collect();
+            let flags =
+              compute_lean_ind_flags(&iv.all, &flags_env).map_err(|e| {
+                DecompileError::BadConstantFormat {
+                  msg: format!(
+                    "roundtrip ind-flags for '{}': {e}",
+                    name.pretty()
+                  ),
+                }
               })?;
             iv.num_nested = Nat::from(flags.num_nested);
             iv.is_rec = flags.is_rec;
@@ -3035,7 +3042,7 @@ fn roundtrip_block(
               && let Some(lean_ci_ref) = orig.get(&n)
               && ci.get_hash() != lean_ci_ref.get_hash()
             {
-              let lean_ci = lean_ci_ref;
+              let lean_ci = &*lean_ci_ref;
               if std::env::var_os("IX_ROUNDTRIP_DEBUG").is_some() {
                 eprintln!(
                   "[lean hash mismatch] {}: generated_ci_hash={:x?} lean_ci_hash={:x?}",
@@ -3125,7 +3132,7 @@ fn roundtrip_block(
             if is_primary
               && !is_aux_gen_suffix(&n)
               && let Some(ref named) = stt.env.named.get(&n)
-              && let Some((ref orig_addr, _)) = named.original
+              && let Some((orig_addr, _)) = named.original()
             {
               let proj_addr = match cnst {
                 LeanMutConst::Recr(_) => {
@@ -3151,14 +3158,14 @@ fn roundtrip_block(
                   ixon_content_address(&proj)
                 },
               };
-              if &proj_addr != orig_addr {
+              if proj_addr != orig_addr {
                 // The original might be a singleton (bare constant, not
                 // Muts-wrapped projection) while roundtrip always wraps in
                 // Muts. Skip the mismatch if the original is a singleton
                 // (non-projection) or not stored (compile_const_no_aux
                 // with aux=false doesn't store singleton constants).
                 let orig_is_singleton =
-                  stt.env.get_const(orig_addr).is_none_or(|c| {
+                  stt.env.get_const(&orig_addr).is_none_or(|c| {
                     !matches!(
                       &c.info,
                       ConstantInfo::IPrj(_)
@@ -3174,7 +3181,7 @@ fn roundtrip_block(
                   // `eprintln!` and swallowed; now propagated so callers
                   // don't silently commit a mismatched constant.
                   let orig_detail =
-                    stt.env.get_const(orig_addr).map(|c| match &c.info {
+                    stt.env.get_const(&orig_addr).map(|c| match &c.info {
                       ConstantInfo::RPrj(p) => format!(
                         "RPrj(idx={}, block={:.12})",
                         p.idx,
@@ -3244,7 +3251,7 @@ fn print_rec_comparison(
 ) {
   let Some(orig_env) = orig_env else { return };
   let orig_ci = orig_env.get(rec_name);
-  let Some(LeanConstantInfo::RecInfo(lean_rv)) = orig_ci else {
+  let Some(LeanConstantInfo::RecInfo(lean_rv)) = orig_ci.as_deref() else {
     return;
   };
 
@@ -3376,7 +3383,7 @@ fn print_rec_comparison(
 /// Decompile a single named constant (non-aux_gen) into the decompile state.
 ///
 /// Dispatches on the constant kind (definition, recursor, axiom, quotient,
-/// projection). Constants with `named.original.is_some()` and a recognized
+/// projection). Constants with `named.has_original()` and a recognized
 /// aux_gen suffix are skipped — they'll be regenerated by `decompile_block_aux_gen`.
 fn decompile_named_const(
   name: &Name,
@@ -3385,7 +3392,7 @@ fn decompile_named_const(
   dstt: &DecompileState,
 ) -> Result<(), DecompileError> {
   // Skip aux_gen constants (regenerated separately)
-  if named.original.is_some() && is_aux_gen_suffix(name) {
+  if named.has_original() && is_aux_gen_suffix(name) {
     return Ok(());
   }
 
@@ -3484,7 +3491,8 @@ fn rehydrate_aux_perms_from_env(stt: &CompileState) {
   // number of mutual blocks in the env, not their sizes.
   for muts_entry in stt.env.named.iter() {
     let muts_named = muts_entry.value();
-    let (muts_all, aux_layout) = match &muts_named.meta.info {
+    let muts_meta = muts_named.meta();
+    let (muts_all, aux_layout) = match &muts_meta.info {
       ConstantMetaInfo::Muts { all, aux_layout: Some(layout) } => {
         n_muts += 1;
         n_muts_with_layout += 1;
@@ -3518,7 +3526,8 @@ fn rehydrate_aux_perms_from_env(stt: &CompileState) {
     // version whose Indc.all is also source-order; we prefer the
     // canonical-entry `Indc.all` since it's the same source-order list
     // under spec §10.2.)
-    let source_all: Option<&[Address]> = match &rep_named.meta.info {
+    let rep_meta = rep_named.meta();
+    let source_all: Option<&[Address]> = match &rep_meta.info {
       ConstantMetaInfo::Indc { all, .. } => Some(all.as_slice()),
       _ => None,
     };
@@ -3554,7 +3563,8 @@ fn block_mut_consts_from_env(
 ) -> Result<Vec<LeanMutConst>, DecompileError> {
   let mut cs = Vec::with_capacity(all_names.len());
   for name in all_names {
-    let Some(LeanConstantInfo::InductInfo(ind)) = env.get(name) else {
+    let ind_entry = env.get(name);
+    let Some(LeanConstantInfo::InductInfo(ind)) = ind_entry.as_deref() else {
       return Err(DecompileError::BadConstantFormat {
         msg: format!(
           "decompile aux plan: block member '{}' is not an inductive",
@@ -3564,7 +3574,7 @@ fn block_mut_consts_from_env(
     };
     let mut ctors = Vec::with_capacity(ind.ctors.len());
     for ctor_name in &ind.ctors {
-      match env.get(ctor_name) {
+      match env.get(ctor_name).as_deref() {
         Some(LeanConstantInfo::CtorInfo(ctor)) => ctors.push(ctor.clone()),
         _ => {
           return Err(DecompileError::BadConstantFormat {
@@ -3598,7 +3608,7 @@ fn names_from_addrs(
 
 fn indc_source_all(name: &Name, stt: &CompileState) -> Option<Vec<Name>> {
   let named = stt.env.named.get(name)?;
-  match &named.meta.info {
+  match &named.meta().info {
     ConstantMetaInfo::Indc { all, .. } => names_from_addrs(all, stt),
     _ => None,
   }
@@ -3613,9 +3623,8 @@ fn stored_plan_blocks_for_original_all(
   let mut seen: FxHashSet<Vec<Name>> = FxHashSet::default();
 
   for muts_entry in stt.env.named.iter() {
-    let ConstantMetaInfo::Muts { all, aux_layout } =
-      &muts_entry.value().meta.info
-    else {
+    let muts_meta = muts_entry.value().meta();
+    let ConstantMetaInfo::Muts { all, aux_layout } = &muts_meta.info else {
       continue;
     };
 
@@ -3808,14 +3817,14 @@ fn recover_aux_from_original(
   dstt: &DecompileState,
 ) -> bool {
   let original = match stt.env.named.get(name) {
-    Some(named) => named.original.clone(),
+    Some(named) => named.original(),
     None => None,
   };
   let Some((orig_addr, orig_meta)) = original else {
     return false;
   };
   let had_entry = dstt.env.contains_key(name);
-  let synthetic = Named { addr: orig_addr, meta: orig_meta, original: None };
+  let synthetic = Named::new(orig_addr, (*orig_meta).clone());
   if decompile_named_const(name, &synthetic, stt, dstt).is_err() {
     return false;
   }
@@ -3888,7 +3897,7 @@ fn decompile_block_aux_gen(
     use crate::graph::get_constant_info_references;
     for ind_name in all_names {
       if let Some(ci) = env.get(ind_name) {
-        for ref_name in get_constant_info_references(ci) {
+        for ref_name in get_constant_info_references(&ci) {
           expr_utils::ensure_in_kenv_of(&ref_name, env, stt, kctx);
         }
       }
@@ -4013,16 +4022,18 @@ fn decompile_block_aux_gen(
 
   // Sync generated .rec constants into env and dstt.env so later phases can find them.
   for (n, rv) in &canonical_recs {
-    env
-      .entry(n.clone())
-      .or_insert_with(|| LeanConstantInfo::RecInfo(rv.clone()));
+    if !env.contains_key(n) {
+      env.insert(n.clone(), LeanConstantInfo::RecInfo(rv.clone()));
+    }
     dstt
       .env
       .entry(n.clone())
       .or_insert_with(|| LeanConstantInfo::RecInfo(rv.clone()));
   }
   for (n, ci) in &generated_consts {
-    env.entry(n.clone()).or_insert_with(|| ci.clone());
+    if !env.contains_key(n) {
+      env.insert(n.clone(), ci.clone());
+    }
     dstt.env.entry(n.clone()).or_insert_with(|| ci.clone());
   }
 
@@ -4046,7 +4057,7 @@ fn decompile_block_aux_gen(
         _ => continue,
       };
       let rec_name = Name::str(ind_name.clone(), "rec".to_string());
-      let rec_val = match env.get(&rec_name) {
+      let rec_val = match env.get(&rec_name).as_deref() {
         Some(LeanConstantInfo::RecInfo(rv)) => rv.clone(),
         _ => {
           // Try dstt.env (may have been inserted above)
@@ -4143,7 +4154,7 @@ fn decompile_block_aux_gen(
         _ => continue,
       };
       let rec_name = Name::str(ind_name, "rec".to_string());
-      let rec_val = match env.get(&rec_name) {
+      let rec_val = match env.get(&rec_name).as_deref() {
         Some(LeanConstantInfo::RecInfo(rv)) => rv.clone(),
         _ => match dstt.env.get(&rec_name).as_deref() {
           Some(LeanConstantInfo::RecInfo(rv)) => rv.clone(),
@@ -4279,7 +4290,9 @@ fn decompile_block_aux_gen(
 
   // Sync generated constants into env and dstt.env for subsequent phases.
   for (n, ci) in &generated_consts {
-    env.entry(n.clone()).or_insert_with(|| ci.clone());
+    if !env.contains_key(n) {
+      env.insert(n.clone(), ci.clone());
+    }
     dstt.env.entry(n.clone()).or_insert_with(|| ci.clone());
   }
 
@@ -4371,7 +4384,7 @@ fn decompile_block_aux_gen(
       if std::env::var_os("IX_ROUNDTRIP_DEBUG").is_some()
         && let Some(ref lean_env) = stt.lean_env
       {
-        let lean_all = match lean_env.get(&d.name) {
+        let lean_all = match lean_env.get(&d.name).as_deref() {
           Some(LeanConstantInfo::DefnInfo(v)) => Some(v.all.clone()),
           Some(LeanConstantInfo::ThmInfo(v)) => Some(v.all.clone()),
           Some(LeanConstantInfo::OpaqueInfo(v)) => Some(v.all.clone()),
@@ -4379,7 +4392,7 @@ fn decompile_block_aux_gen(
         };
         let orig_info: Option<(String, String)> =
           stt.env.named.get(&d.name).and_then(|named| {
-            let (addr, _) = named.original.as_ref()?.clone();
+            let (addr, _) = named.original()?;
             let kind = stt
               .env
               .get_const(&addr)
@@ -4528,7 +4541,9 @@ fn decompile_block_aux_gen(
 
   // Sync generated constants (below, below.rec) into env and dstt.env for brecOn.
   for (n, ci) in &generated_consts {
-    env.entry(n.clone()).or_insert_with(|| ci.clone());
+    if !env.contains_key(n) {
+      env.insert(n.clone(), ci.clone());
+    }
     dstt.env.entry(n.clone()).or_insert_with(|| ci.clone());
   }
 
@@ -4641,7 +4656,8 @@ fn decompile_block_aux_gen(
   if let Some(orig) = orig_env {
     for (name, generated_ci) in &generated_consts {
       if let Some(orig_ci) = orig.get(name)
-        && let Err(e) = crate::congruence::const_alpha_eq(generated_ci, orig_ci)
+        && let Err(e) =
+          crate::congruence::const_alpha_eq(generated_ci, &orig_ci)
       {
         aux_gen_errors.push((
           name.clone(),
@@ -4753,7 +4769,7 @@ pub fn decompile_env(
 
   for entry in stt.env.named.iter() {
     let (name, named) = (entry.key(), entry.value());
-    if named.original.is_none() {
+    if !named.has_original() {
       continue;
     }
     let Some((kind, root)) = classify_aux_gen(name) else {
@@ -4873,7 +4889,7 @@ pub fn decompile_env(
       }
       expr_utils::ensure_in_kenv_of(&name, &work_env, stt, &mut kctx);
       if let Some(ci) = work_env.get(&name) {
-        for ref_name in get_constant_info_references(ci) {
+        for ref_name in get_constant_info_references(&ci) {
           if !ingressed.contains(&ref_name) {
             stack.push(ref_name);
           }
@@ -4996,7 +5012,7 @@ pub fn check_decompile(
     if is_aux_gen_suffix(name) {
       return Ok::<(), DecompileError>(());
     }
-    match original.get(name) {
+    match original.get(name).as_deref() {
       Some(orig_info) if orig_info.get_hash() == info.get_hash() => {
         matches.fetch_add(1, Ordering::Relaxed);
         Ok::<(), DecompileError>(())
diff --git a/crates/compile/src/graph.rs b/crates/compile/src/graph.rs
index e10bd777a..50acfa2a7 100644
--- a/crates/compile/src/graph.rs
+++ b/crates/compile/src/graph.rs
@@ -5,7 +5,7 @@
 //! compute SCCs (strongly connected components) for mutual block detection.
 //! Construction is parallelized via rayon.
 
-use rayon::iter::{IntoParallelRefIterator, ParallelIterator};
+use rayon::iter::{IntoParallelIterator, ParallelIterator};
 use rustc_hash::{FxHashMap, FxHashSet};
 use std::collections::hash_map::Entry;
 
@@ -47,6 +47,106 @@ pub struct RefGraph {
 ///
 /// For each constant, extracts the set of names it references (from types, values, constructors,
 /// and recursor rules), then assembles both the forward and reverse edge maps.
+/// Everything the compile-env setup needs from a whole-env pass: the
+/// reference graph, the immediately-ungrounded set (before transitive
+/// proliferation), and the inductive mutual-block groups
+/// (`all[0] → all`, for flag validation).
+pub struct SetupScan {
+  pub graph: RefGraph,
+  pub immediate_ungrounded: FxHashMap<Name, crate::ground::GroundError>,
+  pub ind_groups: FxHashMap<Name, Vec<Name>>,
+}
+
+/// Fused whole-env setup pass: one decode per constant feeding the ref
+/// graph, the groundedness check, and inductive-group collection.
+/// One pass instead of separate `build_ref_graph` /
+/// `ground_consts`' scan, `validate_lean_ind_flags`' scan) — under
+/// (the compile path'''s default) decodes a constant per access, so
+/// visiting the whole env once instead of three times cuts the setup
+/// decode count to a third. Outputs are identical to the separate passes.
+pub fn setup_scan(env: &Env) -> SetupScan {
+  #[derive(Default)]
+  struct Acc {
+    out_refs: RefMap,
+    in_refs: RefMap,
+    ungrounded: FxHashMap<Name, crate::ground::GroundError>,
+    ind_groups: FxHashMap<Name, Vec<Name>>,
+  }
+
+  let names: Vec<&Name> = env.keys().collect();
+  let acc = names
+    .into_par_iter()
+    .filter_map(|name| {
+      let constant = env.get(name)?;
+      let deps = get_constant_info_references(&constant);
+      let mut acc = Acc {
+        in_refs: mk_in_refs(name, &deps),
+        out_refs: RefMap::from_iter([(name.clone(), deps)]),
+        ..Acc::default()
+      };
+      if let Err(err) = crate::ground::ground_const_check(&constant, env) {
+        acc.ungrounded.insert(name.clone(), err);
+      }
+      // Members of one mutual family share the same `all`, so
+      // first-wins insertion is value-identical regardless of which
+      // member lands first.
+      if let ConstantInfo::InductInfo(v) = &*constant
+        && let Some(first) = v.all.first()
+      {
+        acc.ind_groups.entry(first.clone()).or_insert_with(|| v.all.clone());
+      }
+      Some(acc)
+    })
+    .reduce(Acc::default, |mut l, r| {
+      l.out_refs = merge_ref_maps(l.out_refs, r.out_refs);
+      l.in_refs = merge_ref_maps(l.in_refs, r.in_refs);
+      l.ungrounded.extend(r.ungrounded);
+      for (k, v) in r.ind_groups {
+        l.ind_groups.entry(k).or_insert(v);
+      }
+      l
+    });
+
+  SetupScan {
+    graph: RefGraph { out_refs: acc.out_refs, in_refs: acc.in_refs },
+    immediate_ungrounded: acc.ungrounded,
+    ind_groups: acc.ind_groups,
+  }
+}
+
+/// `name → {name} ∪ deps`-shaped reverse-edge fragment for one
+/// constant, merged across the parallel scan.
+fn mk_in_refs(name: &Name, deps: &NameSet) -> RefMap {
+  let mut in_refs = RefMap::from_iter([(name.clone(), NameSet::default())]);
+  for dep in deps {
+    match in_refs.entry(dep.clone()) {
+      Entry::Vacant(entry) => {
+        entry.insert(NameSet::from_iter([name.clone()]));
+      },
+      Entry::Occupied(mut entry) => {
+        entry.get_mut().insert(name.clone());
+      },
+    }
+  }
+  in_refs
+}
+
+/// Size-aware map union (drain the smaller side into the bigger).
+fn merge_ref_maps(l: RefMap, r: RefMap) -> RefMap {
+  let (smaller, mut bigger) = if l.len() < r.len() { (l, r) } else { (r, l) };
+  for (name, set) in smaller {
+    match bigger.entry(name) {
+      Entry::Vacant(entry) => {
+        entry.insert(set);
+      },
+      Entry::Occupied(mut entry) => {
+        entry.get_mut().extend(set);
+      },
+    }
+  }
+  bigger
+}
+
 pub fn build_ref_graph(env: &Env) -> RefGraph {
   let mk_in_refs = |name: &Name, deps: &NameSet| -> RefMap {
     let mut in_refs = RefMap::from_iter([(name.clone(), NameSet::default())]);
@@ -78,14 +178,15 @@ pub fn build_ref_graph(env: &Env) -> RefGraph {
     bigger
   };
 
-  let (out_refs, in_refs) = env
-    .par_iter()
-    .map(|entry| {
-      let (name, constant) = entry;
-      let deps = get_constant_info_references(constant);
+  let names: Vec<&Name> = env.keys().collect();
+  let (out_refs, in_refs) = names
+    .into_par_iter()
+    .filter_map(|name| {
+      let constant = env.get(name)?;
+      let deps = get_constant_info_references(&constant);
       let in_refs = mk_in_refs(name, &deps);
       let out_refs = RefMap::from_iter([(name.clone(), deps)]);
-      (out_refs, in_refs)
+      Some((out_refs, in_refs))
     })
     .reduce(
       || (RefMap::default(), RefMap::default()),
diff --git a/crates/compile/src/ground.rs b/crates/compile/src/ground.rs
index c854a3117..18f973f20 100644
--- a/crates/compile/src/ground.rs
+++ b/crates/compile/src/ground.rs
@@ -5,7 +5,7 @@
 //! propagates through the reference graph: if A references ungrounded B, then A
 //! is also ungrounded.
 
-use rayon::iter::{IntoParallelRefIterator, ParallelIterator};
+use rayon::iter::{IntoParallelIterator, ParallelIterator};
 use rustc_hash::{FxHashMap, FxHashSet};
 use std::collections::hash_map::Entry;
 
@@ -47,21 +47,38 @@ pub fn ground_consts(
   in_refs: &RefMap,
 ) -> FxHashMap<Name, GroundError> {
   // Collect immediate ungrounded constants.
-  let mut ungrounded: FxHashMap<_, _> = env
-    .par_iter()
-    .filter_map(|entry| {
-      let (name, constant) = entry;
-      let univs = const_univs(constant);
-      let mut stt = GroundState::default();
-      if let Err(err) = ground_const(constant, env, univs, 0, &mut stt) {
-        Some((name.clone(), err))
-      } else {
-        None
+  let names: Vec<&Name> = env.keys().collect();
+  let ungrounded: FxHashMap<_, _> = names
+    .into_par_iter()
+    .filter_map(|name| {
+      let constant = env.get(name)?;
+      match ground_const_check(&constant, env) {
+        Err(err) => Some((name.clone(), err)),
+        Ok(()) => None,
       }
     })
     .collect();
+  proliferate_ungrounded(ungrounded, in_refs)
+}
 
-  // Proliferate ungroundedness through in-refs.
+/// Per-constant groundedness check, for callers that already hold a
+/// decoded constant and check as part of a wider pass.
+pub fn ground_const_check(
+  constant: &ConstantInfo,
+  env: &Env,
+) -> Result<(), GroundError> {
+  let univs = const_univs(constant);
+  let mut stt = GroundState::default();
+  ground_const(constant, env, univs, 0, &mut stt)
+}
+
+/// Spread ungroundedness from the immediately-ungrounded set through
+/// the reverse-reference graph: anything referencing an ungrounded
+/// constant is itself ungrounded.
+pub fn proliferate_ungrounded(
+  mut ungrounded: FxHashMap<Name, GroundError>,
+  in_refs: &RefMap,
+) -> FxHashMap<Name, GroundError> {
   let mut stack: Vec<_> = ungrounded.keys().cloned().collect();
   while let Some(popped) = stack.pop() {
     let Some(in_ref_set) = in_refs.get(&popped) else {
@@ -74,7 +91,6 @@ pub fn ground_consts(
       }
     }
   }
-
   ungrounded
 }
 
@@ -125,7 +141,7 @@ fn ground_const(
     },
     ConstantInfo::InductInfo(val) => {
       for ctor in &val.ctors {
-        let ci = env.get(ctor).cloned();
+        let ci = env.get(ctor).map(|e| e.cloned());
         match ci.as_ref() {
           Some(ConstantInfo::CtorInfo(_)) => (),
           _ => {
diff --git a/crates/compile/src/kernel_egress.rs b/crates/compile/src/kernel_egress.rs
index a0ba4184e..fba24c421 100644
--- a/crates/compile/src/kernel_egress.rs
+++ b/crates/compile/src/kernel_egress.rs
@@ -790,15 +790,15 @@ fn build_mut_const(
 /// the original's `meta` and `original` (aux_gen regeneration hint) fields
 /// but with an updated `addr`.
 ///
-/// Decompile's Pass 2 relies on `named.original.is_some()` to decide which
+/// Decompile's Pass 2 relies on `named.has_original()` to decide which
 /// entries are aux_gen-regenerated — we MUST copy that field over, or
 /// otherwise every `.brecOn*` / `.below` / `.brecOn_N.eq` gets dropped.
 fn rebuild_named(addr: Address, original: &Named) -> Named {
-  Named {
-    addr,
-    meta: original.meta.clone(),
-    original: original.original.clone(),
+  let mut named = Named::new(addr, (*original.meta()).clone());
+  if let Some((orig_addr, orig_meta)) = original.original() {
+    named.set_original(orig_addr, (*orig_meta).clone());
   }
+  named
 }
 
 /// Register a member `Named` pointing at the appropriate address:
@@ -976,7 +976,7 @@ fn egress_muts_block(
 
   // Register the synthetic Muts Named entry at the new block_addr. Preserve
   // the original `meta` / `original` fields — decompile's Pass 2 keys off
-  // `named.original.is_some()` to identify aux_gen entries.
+  // `named.has_original()` to identify aux_gen entries.
   out.register_name(
     muts_name.clone(),
     rebuild_named(block_addr.clone(), muts_named),
@@ -1198,7 +1198,7 @@ pub fn ixon_egress(
   for entry in original_env.named.iter() {
     let name = entry.key().clone();
     let named = entry.value().clone();
-    match &named.meta.info {
+    match &named.meta().info {
       ConstantMetaInfo::Muts { .. } => muts_entries.push((name, named)),
       _ => {
         let orig_const = original_env.get_const(&named.addr);
@@ -1229,7 +1229,8 @@ pub fn ixon_egress(
   let t_muts = std::time::Instant::now();
   muts_entries.par_iter().try_for_each(
     |(muts_name, muts_named)| -> Result<(), String> {
-      let all: &[Vec<Address>] = match &muts_named.meta.info {
+      let muts_meta = muts_named.meta();
+      let all: &[Vec<Address>] = match &muts_meta.info {
         ConstantMetaInfo::Muts { all, .. } => all.as_slice(),
         _ => unreachable!("partitioned above"),
       };
@@ -1691,7 +1692,7 @@ mod tests {
     assert_eq!(le.len(), 3);
     for name in ["A", "B", "C"] {
       let ci = le.get(&mk_name(name)).expect("missing name");
-      assert!(matches!(ci, LeanCI::AxiomInfo(..)));
+      assert!(matches!(&*ci, LeanCI::AxiomInfo(..)));
     }
   }
 }
diff --git a/crates/ffi/src/compile.rs b/crates/ffi/src/compile.rs
index cf9285114..23fb3f74b 100644
--- a/crates/ffi/src/compile.rs
+++ b/crates/ffi/src/compile.rs
@@ -1,7 +1,7 @@
 //! FFI bridge between Lean and Rust for the Ixon compilation/decompilation pipeline.
 //!
 //! Provides `extern "C"` functions callable from Lean via `@[extern]`:
-//! - `rs_compile_env_full` / `rs_compile_env`: compile a Lean environment to Ixon
+//! - `rs_compile_env` / `rs_compile_env_full`: compile a Lean environment to Ixon
 //! - `rs_compile_phases`: run individual pipeline phases (canon, condense, graph, compile)
 //! - `rs_decompile_env`: decompile Ixon back to Lean environment
 //! - `rs_roundtrip_*`: roundtrip FFI tests for Lean↔Rust type conversions
@@ -38,7 +38,6 @@ use lean_ffi::object::{
 
 use crate::builder::LeanBuildCache;
 use crate::lean::LeanIxAddress;
-use crate::lean_env::decode_env;
 use crate::lean_ixon::env::decoded_to_ixon_env;
 
 #[cfg(feature = "test-ffi")]
@@ -195,7 +194,7 @@ pub extern "C" fn rs_compile_env_full(
 ) -> LeanIOResult<LeanOwned> {
   {
     // Phase 1: Decode Lean environment
-    let rust_env = decode_env(env_consts_ptr);
+    let rust_env = crate::lean_env::decode_env(env_consts_ptr);
     let env_len = rust_env.len();
     let rust_env = Arc::new(rust_env);
 
@@ -284,100 +283,59 @@ pub extern "C" fn rs_compile_env_full(
   }
 }
 
-/// FFI function to compile a Lean environment to serialized Ixon.Env bytes.
+/// FFI: compile a Lean environment and stream the serialized Ixon.Env
+/// straight to `out_path` (see `Env::put_file`) — no env-sized `Vec` or
+/// Lean `ByteArray` is built. Writes `<out_path>.tmp`, then renames, so
+/// a crash cannot leave a truncated file. Returns bytes written (Nat).
+/// The file is the canonical `Env::put` encoding (see `put_file`'s
+/// equivalence test).
 #[unsafe(no_mangle)]
 pub extern "C" fn rs_compile_env(
   env_consts_ptr: LeanList<LeanBorrowed<'_>>,
+  out_path: LeanString<LeanBorrowed<'_>>,
 ) -> LeanIOResult<LeanOwned> {
-  {
-    let quiet = std::env::var("IX_QUIET").is_ok();
-    let rust_env = decode_env(env_consts_ptr);
-    let rust_env = Arc::new(rust_env);
+  let rust_env = crate::lean_env::decode_env_for_compile(env_consts_ptr);
+  let rust_env = Arc::new(rust_env);
 
-    let compile_stt =
-      match compile_env_with_options(&rust_env, CompileOptions::default()) {
-        Ok(stt) => stt,
-        Err(e) => {
-          let msg = format!("rs_compile_env: Rust compilation failed: {:?}", e);
-          return LeanIOResult::error_string(&msg);
-        },
-      };
+  let compile_stt =
+    match compile_env_with_options(&rust_env, CompileOptions::default()) {
+      Ok(stt) => stt,
+      Err(e) => {
+        let msg = format!("rs_compile_env: Rust compilation failed: {:?}", e);
+        return LeanIOResult::error_string(&msg);
+      },
+    };
 
-    // Serialize the compiled Env to bytes
-    if !quiet {
-      eprintln!("[rs_compile_env] starting serialization");
-    }
-    let ser_start = std::time::Instant::now();
-    let mut buf = Vec::new();
-    if let Err(e) = compile_stt.env.put(&mut buf) {
-      let msg = format!("rs_compile_env: Env serialization failed: {}", e);
+  let path = std::path::PathBuf::from(out_path.as_str());
+  let tmp = {
+    let mut s = path.clone().into_os_string();
+    s.push(".tmp");
+    std::path::PathBuf::from(s)
+  };
+  let written = match compile_stt.env.put_file(&tmp) {
+    Ok(n) => n,
+    Err(e) => {
+      std::fs::remove_file(&tmp).ok();
+      let msg = format!("rs_compile_env: serialization failed: {e}");
       return LeanIOResult::error_string(&msg);
-    }
-    if !quiet {
-      eprintln!(
-        "[rs_compile_env] serialization done in {:.1}s: {} bytes",
-        ser_start.elapsed().as_secs_f64(),
-        buf.len(),
-      );
-    }
-
-    // Build Lean ByteArray
-    if !quiet {
-      eprintln!(
-        "[rs_compile_env] building Lean ByteArray ({} bytes)",
-        buf.len()
-      );
-    }
-    let ba_start = std::time::Instant::now();
-    let ba = LeanByteArray::from_bytes(&buf);
-    if !quiet {
-      eprintln!(
-        "[rs_compile_env] ByteArray built in {:.1}s",
-        ba_start.elapsed().as_secs_f64(),
-      );
-    }
-
-    // Skip destructors on the CLI path. `rs_compile_env` is called from
-    // one-shot commands (lake exe ix compile, serve/connect init) where the
-    // process exits shortly after returning the ByteArray. Running ~millions
-    // of Arc<NameData> chain-drops serially across DashMap shards costs 70+
-    // seconds of wall time on Mathlib and accomplishes nothing — the OS
-    // reclaims the allocations instantly at process exit.
-    //
-    // Safety: `mem::forget` on `Arc<T>` leaks one strong refcount; the
-    // underlying allocation is never freed but also never accessed. The
-    // `LeanEnv` inside `rust_env` was decoded into owned Rust data (no
-    // borrow lifetimes from Lean), so there's no UB risk from leaking it.
-    //
-    // Escape hatch: set `IX_SKIP_DROPS=0` to run destructors (for tests
-    // that assert clean teardown; not used by any production path).
-    if std::env::var("IX_SKIP_DROPS").ok().as_deref() != Some("0") {
-      if !quiet {
-        eprintln!("[rs_compile_env] skipping destructors (IX_SKIP_DROPS)");
-      }
-      std::mem::forget(compile_stt);
-      std::mem::forget(rust_env);
-      std::mem::forget(buf);
-    } else {
-      if !quiet {
-        eprintln!("[rs_compile_env] running destructors (IX_SKIP_DROPS=0)");
-      }
-      let drop_start = std::time::Instant::now();
-      drop(buf);
-      drop(compile_stt);
-      drop(rust_env);
-      if !quiet {
-        eprintln!(
-          "[rs_compile_env] destructors done in {:.2}s",
-          drop_start.elapsed().as_secs_f64(),
-        );
-      }
-    }
-    if !quiet {
-      eprintln!("[rs_compile_env] returning ByteArray to Lean");
-    }
-    LeanIOResult::ok(ba)
+    },
+  };
+  if let Err(e) = std::fs::rename(&tmp, &path) {
+    std::fs::remove_file(&tmp).ok();
+    let msg = format!(
+      "rs_compile_env: rename {} -> {}: {e}",
+      tmp.display(),
+      path.display()
+    );
+    return LeanIOResult::error_string(&msg);
   }
+
+  // Skip destructors: the compile CLI is a one-shot process, the OS
+  // reclaims at exit, and dropping the maps costs tens of seconds at
+  // Mathlib scale.
+  std::mem::forget(compile_stt);
+  std::mem::forget(rust_env);
+  LeanIOResult::ok(LeanOwned::from_nat_u64(written))
 }
 
 /// Round-trip a RawEnv: decode from Lean, re-encode via builder.
@@ -397,7 +355,7 @@ pub extern "C" fn rs_compile_phases(
   env_consts_ptr: LeanList<LeanBorrowed<'_>>,
 ) -> LeanIOResult<LeanOwned> {
   {
-    let rust_env = decode_env(env_consts_ptr);
+    let rust_env = crate::lean_env::decode_env(env_consts_ptr);
     let env_len = rust_env.len();
     let rust_env = Arc::new(rust_env);
 
@@ -442,7 +400,7 @@ pub extern "C" fn rs_compile_phases(
       .collect();
     let named_arr = LeanArray::alloc(named.len());
     for (i, (name, n)) in named.iter().enumerate() {
-      named_arr.set(i, build_raw_named(&mut cache, name, &n.addr, &n.meta));
+      named_arr.set(i, build_raw_named(&mut cache, name, &n.addr, &n.meta()));
     }
 
     let blobs: Vec<_> = compile_stt
@@ -501,7 +459,7 @@ pub extern "C" fn rs_compile_env_to_ixon(
   env_consts_ptr: LeanList<LeanBorrowed<'_>>,
 ) -> LeanIOResult<LeanOwned> {
   {
-    let rust_env = decode_env(env_consts_ptr);
+    let rust_env = crate::lean_env::decode_env(env_consts_ptr);
     let rust_env = Arc::new(rust_env);
 
     let compile_stt =
@@ -538,7 +496,7 @@ pub extern "C" fn rs_compile_env_to_ixon(
       .collect();
     let named_arr = LeanArray::alloc(named.len());
     for (i, (name, n)) in named.iter().enumerate() {
-      named_arr.set(i, build_raw_named(&mut cache, name, &n.addr, &n.meta));
+      named_arr.set(i, build_raw_named(&mut cache, name, &n.addr, &n.meta()));
     }
 
     let blobs: Vec<_> = compile_stt
@@ -591,7 +549,7 @@ pub extern "C" fn rs_canonicalize_env_to_ix(
   env_consts_ptr: LeanList<LeanBorrowed<'_>>,
 ) -> LeanIOResult<LeanOwned> {
   {
-    let rust_env = decode_env(env_consts_ptr);
+    let rust_env = crate::lean_env::decode_env(env_consts_ptr);
     let mut cache = LeanBuildCache::with_capacity(rust_env.len());
     let raw_env = LeanIxRawEnvironment::build(&mut cache, &rust_env);
     LeanIOResult::ok(raw_env)
@@ -618,7 +576,7 @@ pub extern "C" fn rs_canonicalize_env_to_ix(
 pub extern "C" fn rs_leon_hashes(
   env_consts_ptr: LeanList<LeanBorrowed<'_>>,
 ) -> LeanIOResult<LeanOwned> {
-  let rust_env = decode_env(env_consts_ptr);
+  let rust_env = crate::lean_env::decode_env(env_consts_ptr);
   let mut cache = LeanBuildCache::with_capacity(rust_env.len());
 
   let arr = LeanArray::alloc(rust_env.len());
@@ -673,7 +631,7 @@ extern "C" fn rs_compile_env_rust_first(
   env_consts_ptr: LeanList<LeanBorrowed<'_>>,
 ) -> *mut RustCompiledEnv {
   // Decode Lean environment
-  let lean_env = decode_env(env_consts_ptr);
+  let lean_env = crate::lean_env::decode_env(env_consts_ptr);
   let lean_env = Arc::new(lean_env);
 
   // Compile with Rust
diff --git a/crates/ffi/src/ix/env.rs b/crates/ffi/src/ix/env.rs
index 3800bc614..ccaef3dc6 100644
--- a/crates/ffi/src/ix/env.rs
+++ b/crates/ffi/src/ix/env.rs
@@ -147,7 +147,7 @@ impl LeanIxRawEnvironment<LeanOwned> {
     for (i, entry) in consts.iter().enumerate() {
       let (name, info) = entry;
       let key_obj = LeanIxName::build(cache, name);
-      let val_obj = LeanIxConstantInfo::build(cache, info);
+      let val_obj = LeanIxConstantInfo::build(cache, &info);
       // Build pair (Name × ConstantInfo)
       let pair = LeanProd::new(key_obj, val_obj);
       consts_arr.set(i, pair);
diff --git a/crates/ffi/src/kernel.rs b/crates/ffi/src/kernel.rs
index d7d1c2577..41c1dbade 100644
--- a/crates/ffi/src/kernel.rs
+++ b/crates/ffi/src/kernel.rs
@@ -754,7 +754,7 @@ pub extern "C" fn rs_prim_addrs_canonical() -> LeanIOResult<LeanOwned> {
 fn all_checkable_ixon_names(ixon_env: &IxonEnv) -> Vec<Name> {
   let mut names = Vec::with_capacity(ixon_env.named_count());
   for entry in ixon_env.named.iter() {
-    if matches!(entry.value().meta.info, ConstantMetaInfo::Muts { .. }) {
+    if matches!(entry.value().meta().info, ConstantMetaInfo::Muts { .. }) {
       continue;
     }
     names.push(entry.key().clone());
@@ -984,7 +984,7 @@ fn check_schedule_block_addr(
     return None;
   }
   let named = ixon_env.lookup_name(name)?;
-  if matches!(named.meta.info, ConstantMetaInfo::Muts { .. }) {
+  if matches!(named.meta().info, ConstantMetaInfo::Muts { .. }) {
     return None;
   }
   let constant = ixon_env.get_const(&named.addr)?;
@@ -3673,7 +3673,7 @@ fn compare_envs(
             find_diff(orig_ci.get_type(), egressed_ci.get_type(), "type");
           errors.push(format!("{name}: {diff}"));
         }
-        match (orig_ci, egressed_ci) {
+        match (&*orig_ci, &*egressed_ci) {
           (LCI::DefnInfo(a), LCI::DefnInfo(b))
             if a.value.get_hash() != b.value.get_hash() =>
           {
diff --git a/crates/ffi/src/lean_env.rs b/crates/ffi/src/lean_env.rs
index 776070f63..a053ee737 100644
--- a/crates/ffi/src/lean_env.rs
+++ b/crates/ffi/src/lean_env.rs
@@ -81,14 +81,14 @@ fn build_aux_perm_ctx(
   use ix_compile::congruence::perm::{PermCtx, RecHeadInfo, RecHeadKind};
 
   let first = all.first()?;
-  let n_params = match env.get(first) {
+  let n_params = match env.get(first).as_deref() {
     Some(LeanCI::InductInfo(v)) => v.num_params.to_u64().unwrap_or(0) as usize,
     _ => return None,
   };
   let n_primary = all.len();
   let primary_ctor_counts: Vec<usize> = all
     .iter()
-    .map(|n| match env.get(n) {
+    .map(|n| match env.get(n).as_deref() {
       Some(LeanCI::InductInfo(v)) => v.ctors.len(),
       _ => 0,
     })
@@ -99,7 +99,7 @@ fn build_aux_perm_ctx(
   };
   let source_aux_ctor_counts: Vec<usize> = source_aux_order
     .iter()
-    .map(|(head, _)| match env.get(head) {
+    .map(|(head, _)| match env.get(head).as_deref() {
       Some(LeanCI::InductInfo(v)) => v.ctors.len(),
       _ => 0,
     })
@@ -122,7 +122,7 @@ fn build_aux_perm_ctx(
     source_aux_ctor_counts: source_aux_ctor_counts.clone(),
     aux_perm: perm.to_vec(),
   };
-  let n_indices_for = |rec_name: &Name| match env.get(rec_name) {
+  let n_indices_for = |rec_name: &Name| match env.get(rec_name).as_deref() {
     Some(LeanCI::RecInfo(r)) => r.num_indices.to_u64().unwrap_or(0) as usize,
     _ => 0,
   };
@@ -175,7 +175,7 @@ fn build_aux_perm_ctx(
     for suffix in ["rec", "casesOn", "recOn", "below", "brecOn"] {
       add_addr(&Name::str(member.clone(), suffix.to_string()));
     }
-    if let Some(LeanCI::InductInfo(v)) = env.get(member) {
+    if let Some(LeanCI::InductInfo(v)) = env.get(member).as_deref() {
       for ctor in &v.ctors {
         add_addr(ctor);
       }
@@ -308,7 +308,7 @@ fn build_collapse_const_map(
     // Constructors: positional mapping. Both members are alpha-collapsed,
     // so they have the same number of constructors in the same order.
     if let (Some(LeanCI::InductInfo(m_ind)), Some(LeanCI::InductInfo(r_ind))) =
-      (env.get(member), env.get(rep))
+      (env.get(member).as_deref(), env.get(rep).as_deref())
       && m_ind.ctors.len() == r_ind.ctors.len()
     {
       for (m_ctor, r_ctor) in m_ind.ctors.iter().zip(r_ind.ctors.iter()) {
@@ -543,7 +543,7 @@ fn build_aux_compare_contexts(
   let mut by_name = FxHashMap::default();
   let mut seen_blocks: FxHashSet<Vec<Name>> = FxHashSet::default();
   for (name, ci) in env.iter() {
-    let all = match ci {
+    let all = match &*ci {
       LeanCI::InductInfo(v) => &v.all,
       _ => continue,
     };
@@ -1124,6 +1124,73 @@ fn decode_name_constant_info(
   (name, constant_info)
 }
 
+/// Resident-decoded-constant bound for [`decode_env_lazy`]'s cache.
+///
+/// Sized by sweep, not by hit rate: on FLT (511k consts) wall time is
+/// flat from 4096 through 1M entries (60–67 s; misses hide in the
+/// scheduler's dependency-stall slack) while peak RSS climbs from
+/// 11.5 GiB (4k) → 13.0 (64k) → 24.7 (1M); Mathlib (737k consts)
+/// confirms parity at this size (87.5 s / 17.0 GiB vs 87.3 s /
+/// 18.3 GiB at 64k). So the cache buys RAM, not speed, and the bound
+/// sits at the small end with headroom over the 4k floor measured to
+/// still not thrash.
+const LAZY_ENV_CACHE_ENTRIES: usize = 16384;
+
+/// Decode for the production compile FFI entries: an on-demand view
+/// that avoids materializing the full Rust copy of the environment —
+/// the eager copy is the single largest memory term at scale. The
+/// on-demand decode costs a few percent of wall (per-constant fetches
+/// vs one batched decode); `IX_COMPILE_EAGER=1` buys that back on
+/// machines with RAM to spare. Measured on FLT: −8 % wall for
+/// +13 GiB peak; Mathlib eager exceeds a 56 GB machine outright
+/// (the copy sits alongside the Lean-held env). Test and roundtrip
+/// entries keep [`decode_env`] (they re-read the env structurally
+/// throughout).
+pub fn decode_env_for_compile(list: LeanList<LeanBorrowed<'_>>) -> Env {
+  if std::env::var("IX_COMPILE_EAGER").as_deref() == Ok("1") {
+    return decode_env(list);
+  }
+  decode_env_lazy(list, LAZY_ENV_CACHE_ENTRIES)
+}
+
+/// Lazy variant of [`decode_env`]: decode only the *names* eagerly,
+/// keep a per-constant `LeanShared` handle, and decode `ConstantInfo`s
+/// on demand through `Env`'s bounded cache.
+///
+/// Thread-safety is identical to the eager path, which already decodes
+/// in parallel: `lean_mark_mt` (via `LeanShared::new`) transitions the
+/// reachable graph to atomic refcounting, structural reads through
+/// `LeanBorrowed` accessors are refcount-silent, and each element's
+/// owned handle keeps its Lean objects alive for the `Env`'s lifetime
+/// regardless of what the Lean side does after the FFI call.
+pub fn decode_env_lazy(
+  list: LeanList<LeanBorrowed<'_>>,
+  cache_entries: usize,
+) -> Env {
+  let shared_list = LeanShared::new(list.inner().to_owned_ref());
+  let objs = collect_list_shared(shared_list.borrow().as_list());
+  let global = Arc::new(GlobalCache::with_capacity(objs.len() * 3));
+
+  // Name index (parallel; bodies untouched). Each element is a
+  // `Prod (Name × ConstantInfo)` ctor — field 0 is the name.
+  let named: Vec<(Name, LeanShared)> = objs
+    .into_par_iter()
+    .map(|o| {
+      let name = decode_name(o.borrow().as_ctor().get(0), &global);
+      (name, o)
+    })
+    .collect();
+  let names: Vec<Name> = named.iter().map(|(n, _)| n.clone()).collect();
+  let handles: FxHashMap<Name, LeanShared> = named.into_iter().collect();
+
+  let fetch = move |name: &Name| {
+    let obj = handles.get(name)?;
+    let mut cache = Cache::new(&global);
+    Some(decode_constant_info(obj.borrow().as_ctor().get(1), &mut cache))
+  };
+  Env::new_lazy(names, Box::new(fetch), cache_entries)
+}
+
 // Decode a Lean environment in parallel with hybrid caching.
 pub fn decode_env(list: LeanList<LeanBorrowed<'_>>) -> Env {
   // Phase 1: Mark entire list graph as MT, then collect elements as LeanShared.
@@ -1226,7 +1293,7 @@ extern "C" fn rs_tmp_decode_const_map(
       use ix_compile::congruence::perm::{PermCtx, RecHeadInfo, RecHeadKind};
 
       let first = all.first()?;
-      let n_params = match env.get(first) {
+      let n_params = match env.get(first).as_deref() {
         Some(LeanCI::InductInfo(v)) => {
           v.num_params.to_u64().unwrap_or(0) as usize
         },
@@ -1235,7 +1302,7 @@ extern "C" fn rs_tmp_decode_const_map(
       let n_primary = all.len();
       let primary_ctor_counts: Vec<usize> = all
         .iter()
-        .map(|n| match env.get(n) {
+        .map(|n| match env.get(n).as_deref() {
           Some(LeanCI::InductInfo(v)) => v.ctors.len(),
           _ => 0,
         })
@@ -1246,7 +1313,7 @@ extern "C" fn rs_tmp_decode_const_map(
       };
       let source_aux_ctor_counts: Vec<usize> = source_aux_order
         .iter()
-        .map(|(head, _)| match env.get(head) {
+        .map(|(head, _)| match env.get(head).as_deref() {
           Some(LeanCI::InductInfo(v)) => v.ctors.len(),
           _ => 0,
         })
@@ -1269,7 +1336,7 @@ extern "C" fn rs_tmp_decode_const_map(
         source_aux_ctor_counts: source_aux_ctor_counts.clone(),
         aux_perm: perm.to_vec(),
       };
-      let n_indices_for = |rec_name: &Name| match env.get(rec_name) {
+      let n_indices_for = |rec_name: &Name| match env.get(rec_name).as_deref() {
         Some(LeanCI::RecInfo(r)) => {
           r.num_indices.to_u64().unwrap_or(0) as usize
         },
@@ -1323,7 +1390,7 @@ extern "C" fn rs_tmp_decode_const_map(
         for suffix in ["rec", "casesOn", "recOn", "below", "brecOn"] {
           add_addr(&Name::str(member.clone(), suffix.to_string()));
         }
-        if let Some(LeanCI::InductInfo(v)) = env.get(member) {
+        if let Some(LeanCI::InductInfo(v)) = env.get(member).as_deref() {
           for ctor in &v.ctors {
             add_addr(ctor);
           }
@@ -1409,7 +1476,7 @@ extern "C" fn rs_tmp_decode_const_map(
     let mut seen_blocks: FxHashSet<Vec<Name>> = FxHashSet::default();
 
     for (name, ci) in env.iter() {
-      let all = match ci {
+      let all = match &*ci {
         LeanCI::InductInfo(v) => &v.all,
         _ => continue,
       };
@@ -1428,8 +1495,9 @@ extern "C" fn rs_tmp_decode_const_map(
       // longer required at this call site. Still verify the block has at
       // least one ingress-able inductive so we don't waste work on
       // broken envs.
-      let has_indc =
-        all.iter().any(|n| matches!(env.get(n), Some(LeanCI::InductInfo(_))));
+      let has_indc = all
+        .iter()
+        .any(|n| matches!(env.get(n).as_deref(), Some(LeanCI::InductInfo(_))));
       if !has_indc {
         continue;
       }
@@ -1530,7 +1598,7 @@ extern "C" fn rs_tmp_decode_const_map(
         let Some(orig_ci_ref) = env.get(patch_name) else {
           continue;
         };
-        let orig_ci: &LeanCI = orig_ci_ref;
+        let orig_ci: &LeanCI = &orig_ci_ref;
         let eq_result = match &perm_ctx_1b {
           Some(ctx) => ix_compile::congruence::perm::const_alpha_eq_with_perm(
             &gen_ci, orig_ci, ctx,
@@ -1811,7 +1879,8 @@ extern "C" fn rs_compile_validate_aux(
     let fails = AtomicUsize::new(0);
     let fail_msgs: Mutex<Vec<String>> = Mutex::new(Vec::new());
 
-    env.par_iter().for_each(|(name, _)| {
+    let env_names: Vec<&Name> = env.keys().collect();
+    env_names.par_iter().for_each(|&name| {
       if stt.ungrounded.contains_key(name) {
         return;
       }
@@ -1870,7 +1939,7 @@ extern "C" fn rs_compile_validate_aux(
     let work: Vec<(Name, Vec<Name>, Vec<MutConst>)> = env
       .iter()
       .filter_map(|(name, ci)| {
-        let all = match ci {
+        let all = match &*ci {
           LeanCI::InductInfo(v) => v.all.clone(),
           _ => return None,
         };
@@ -1884,7 +1953,7 @@ extern "C" fn rs_compile_validate_aux(
         }
         let original_cs: Vec<MutConst> = all
           .iter()
-          .filter_map(|n| match env.get(n) {
+          .filter_map(|n| match env.get(n).as_deref() {
             Some(LeanCI::InductInfo(v)) => {
               Some(MutConst::Indc(mk_indc(v, &env).ok()?))
             },
@@ -1939,7 +2008,7 @@ extern "C" fn rs_compile_validate_aux(
             continue;
           }
           if let Some(ci) = env.get(&name) {
-            for ref_name in get_constant_info_references(ci) {
+            for ref_name in get_constant_info_references(&ci) {
               if !p2_ingressed.contains(&ref_name) {
                 stack.push(ref_name);
               }
@@ -1985,7 +2054,7 @@ extern "C" fn rs_compile_validate_aux(
       use rustc_hash::FxHashMap;
 
       let first = all.first()?;
-      let n_params = match env.get(first) {
+      let n_params = match env.get(first).as_deref() {
         Some(LeanCI::InductInfo(v)) => {
           v.num_params.to_u64().unwrap_or(0) as usize
         },
@@ -1994,7 +2063,7 @@ extern "C" fn rs_compile_validate_aux(
       let n_primary = all.len();
       let primary_ctor_counts: Vec<usize> = all
         .iter()
-        .map(|n| match env.get(n) {
+        .map(|n| match env.get(n).as_deref() {
           Some(LeanCI::InductInfo(v)) => v.ctors.len(),
           _ => 0,
         })
@@ -2006,7 +2075,7 @@ extern "C" fn rs_compile_validate_aux(
       };
       let source_aux_ctor_counts: Vec<usize> = source_aux_order
         .iter()
-        .map(|(head, _)| match env.get(head) {
+        .map(|(head, _)| match env.get(head).as_deref() {
           Some(LeanCI::InductInfo(v)) => v.ctors.len(),
           _ => 0,
         })
@@ -2047,7 +2116,7 @@ extern "C" fn rs_compile_validate_aux(
       // Helper: look up `n_indices` for a specific recursor, falling
       // back to 0 when the rec isn't in env (e.g., if Lean didn't
       // generate it for this aux — the entry is benign in that case).
-      let n_indices_for = |rec_name: &Name| match env.get(rec_name) {
+      let n_indices_for = |rec_name: &Name| match env.get(rec_name).as_deref() {
         Some(LeanCI::RecInfo(r)) => {
           r.num_indices.to_u64().unwrap_or(0) as usize
         },
@@ -2118,7 +2187,7 @@ extern "C" fn rs_compile_validate_aux(
         for suffix in ["rec", "casesOn", "recOn", "below", "brecOn"] {
           add_addr(&Name::str(member.clone(), suffix.to_string()));
         }
-        if let Some(LeanCI::InductInfo(v)) = env.get(member) {
+        if let Some(LeanCI::InductInfo(v)) = env.get(member).as_deref() {
           for ctor in &v.ctors {
             add_addr(ctor);
           }
@@ -2345,7 +2414,7 @@ extern "C" fn rs_compile_validate_aux(
           let Some(orig_ci_ref) = env.get(patch_name) else {
             continue; // Synthetic name — no Lean original.
           };
-          let orig_ci: &LeanCI = orig_ci_ref;
+          let orig_ci: &LeanCI = &orig_ci_ref;
 
           let eq_result = match &perm_ctx {
             Some(ctx) => {
@@ -2410,7 +2479,7 @@ extern "C" fn rs_compile_validate_aux(
 
     stt.env.named.par_iter().for_each(|entry| {
       let named = entry.value();
-      if let Some((orig_addr, _)) = &named.original {
+      if let Some((orig_addr, _)) = &named.original() {
         if *orig_addr != named.addr
           && stt.env.consts.contains_key(orig_addr)
           && !canonical_addrs.contains(orig_addr)
@@ -3560,7 +3629,7 @@ extern "C" fn rs_compile_validate_aux(
       let eq_result = aux_congruence_result(
         name,
         dec_ci.value(),
-        orig_ci,
+        &orig_ci,
         aux_compare_contexts.get(name),
       );
       match eq_result {
@@ -3703,7 +3772,7 @@ extern "C" fn rs_compile_validate_aux(
           fresh_stt
             .name_to_addr
             .insert(entry.key().clone(), entry.value().addr.clone());
-          if entry.value().original.is_some() {
+          if entry.value().has_original() {
             n_original += 1;
           }
         }
@@ -3780,67 +3849,73 @@ extern "C" fn rs_compile_validate_aux(
     // present). Aux-generated constants get an alpha-collapse-aware
     // semantic fallback when exact source-shape comparison fails.
     // `get_hash()` reads are pure — ok to run concurrently.
-    orig.par_iter().for_each(|(name, orig_ci)| match dstt2.env.get(name) {
-      Some(dec_entry) => {
-        let dec_ci = dec_entry.value();
-        let type_ok =
-          dec_ci.get_type().get_hash() == orig_ci.get_type().get_hash();
-        let val_ok = match (dec_ci.get_value(), orig_ci.get_value()) {
-          (Some(d), Some(o)) => d.get_hash() == o.get_hash(),
-          (None, None) => true,
-          _ => false,
-        };
-        let aux_eq_result = if ix_compile::decompile::is_aux_gen_suffix(name)
-          && !(type_ok && val_ok)
-        {
-          Some(aux_congruence_result(
-            name,
-            dec_ci,
-            orig_ci,
-            aux_compare_contexts.get(name),
-          ))
-        } else {
-          None
-        };
-        let ok = match aux_eq_result.as_ref() {
-          Some(Ok(())) => true,
-          Some(Err(_)) => false,
-          None => type_ok && val_ok,
-        };
-        if ok {
-          passes.fetch_add(1, Ordering::Relaxed);
-        } else {
+    let orig_names: Vec<&Name> = orig.keys().collect();
+    orig_names.par_iter().for_each(|&name| {
+      let Some(orig_ci) = orig.get(name) else { return };
+      match dstt2.env.get(name) {
+        Some(dec_entry) => {
+          let dec_ci = dec_entry.value();
+          let type_ok =
+            dec_ci.get_type().get_hash() == orig_ci.get_type().get_hash();
+          let val_ok = match (dec_ci.get_value(), orig_ci.get_value()) {
+            (Some(d), Some(o)) => d.get_hash() == o.get_hash(),
+            (None, None) => true,
+            _ => false,
+          };
+          let aux_eq_result = if ix_compile::decompile::is_aux_gen_suffix(name)
+            && !(type_ok && val_ok)
+          {
+            Some(aux_congruence_result(
+              name,
+              dec_ci,
+              &orig_ci,
+              aux_compare_contexts.get(name),
+            ))
+          } else {
+            None
+          };
+          let ok = match aux_eq_result.as_ref() {
+            Some(Ok(())) => true,
+            Some(Err(_)) => false,
+            None => type_ok && val_ok,
+          };
+          if ok {
+            passes.fetch_add(1, Ordering::Relaxed);
+          } else {
+            fails.fetch_add(1, Ordering::Relaxed);
+            let mut msgs = fail_msgs.lock().unwrap();
+            if msgs.len() < 20 {
+              let mut parts = Vec::new();
+              match aux_eq_result {
+                Some(Err(e)) => parts.push(format!("aux congruence: {e}")),
+                _ => {
+                  if !type_ok {
+                    parts.push(format!(
+                      "type: dec={} orig={}",
+                      dec_ci.get_type().pretty(),
+                      orig_ci.get_type().pretty(),
+                    ));
+                  }
+                  if !val_ok {
+                    parts.push("value hash mismatch".to_string());
+                  }
+                },
+              }
+              msgs.push(format!("{}: {}", name.pretty(), parts.join("; ")));
+            }
+          }
+        },
+        None => {
           fails.fetch_add(1, Ordering::Relaxed);
           let mut msgs = fail_msgs.lock().unwrap();
           if msgs.len() < 20 {
-            let mut parts = Vec::new();
-            match aux_eq_result {
-              Some(Err(e)) => parts.push(format!("aux congruence: {e}")),
-              _ => {
-                if !type_ok {
-                  parts.push(format!(
-                    "type: dec={} orig={}",
-                    dec_ci.get_type().pretty(),
-                    orig_ci.get_type().pretty(),
-                  ));
-                }
-                if !val_ok {
-                  parts.push("value hash mismatch".to_string());
-                }
-              },
-            }
-            msgs.push(format!("{}: {}", name.pretty(), parts.join("; ")));
+            msgs.push(format!(
+              "{}: missing from roundtripped env",
+              name.pretty(),
+            ));
           }
-        }
-      },
-      None => {
-        fails.fetch_add(1, Ordering::Relaxed);
-        let mut msgs = fail_msgs.lock().unwrap();
-        if msgs.len() < 20 {
-          msgs
-            .push(format!("{}: missing from roundtripped env", name.pretty(),));
-        }
-      },
+        },
+      }
     });
 
     p7b.pass = passes.load(Ordering::Relaxed);
@@ -3919,9 +3994,9 @@ extern "C" fn rs_compile_validate_aux(
         original_strs.iter().map(|s| mk_name(s)).collect();
 
       // Skip if any name is missing from the env (fixture not compiled).
-      let all_present = originals
-        .iter()
-        .all(|n| matches!(env.get(n), Some(ConstantInfo::InductInfo(_))));
+      let all_present = originals.iter().all(|n| {
+        matches!(env.get(n).as_deref(), Some(ConstantInfo::InductInfo(_)))
+      });
       if !all_present {
         continue;
       }
@@ -4165,7 +4240,7 @@ fn compute_const_size_breakdown(
 
   // Metadata size
   let meta_size = if let Some(named) = stt.env.named.get(name) {
-    serialized_meta_size(&named.meta, name_index)
+    serialized_meta_size(&named.meta(), name_index)
   } else {
     0
   };
@@ -4181,7 +4256,7 @@ fn serialized_meta_size(
 ) -> usize {
   let mut buf = Vec::new();
   meta
-    .put_indexed(name_index, &mut buf)
+    .put_with(ixon::metadata::NamePut::Indexed(name_index), &mut buf)
     .expect("metadata serialization failed");
   buf.len()
 }
diff --git a/crates/ffi/src/lean_ixon/env.rs b/crates/ffi/src/lean_ixon/env.rs
index 398ada44e..edac79ad2 100644
--- a/crates/ffi/src/lean_ixon/env.rs
+++ b/crates/ffi/src/lean_ixon/env.rs
@@ -359,7 +359,7 @@ pub fn ixon_env_to_decoded(env: &IxonEnv) -> Result<DecodedRawEnv, String> {
     .map(|e| DecodedRawNamed {
       name: e.key().clone(),
       addr: e.value().addr.clone(),
-      const_meta: e.value().meta.clone(),
+      const_meta: (*e.value().meta()).clone(),
     })
     .collect();
   let blobs = env
diff --git a/crates/ffi/src/lean_ixon/meta.rs b/crates/ffi/src/lean_ixon/meta.rs
index 13db8ec0e..5c8af7c00 100644
--- a/crates/ffi/src/lean_ixon/meta.rs
+++ b/crates/ffi/src/lean_ixon/meta.rs
@@ -686,7 +686,11 @@ impl<R: LeanRef> LeanIxonNamed<R> {
         tag => panic!("Invalid Option tag for Named.original: {tag}"),
       }
     };
-    Named { addr, meta, original }
+    let mut named = Named::new(addr, meta);
+    if let Some((orig_addr, orig_meta)) = original {
+      named.set_original(orig_addr, orig_meta);
+    }
+    named
   }
 }
 
@@ -774,5 +778,6 @@ pub extern "C" fn rs_roundtrip_ixon_named(
   obj: LeanIxonNamed<LeanBorrowed<'_>>,
 ) -> LeanIxonNamed<LeanOwned> {
   let named = obj.decode();
-  LeanIxonNamed::build(&named.addr, &named.meta, &named.original)
+  let original = named.original().map(|(a, m)| (a, (*m).clone()));
+  LeanIxonNamed::build(&named.addr, &named.meta(), &original)
 }
diff --git a/crates/ixon/src/env.rs b/crates/ixon/src/env.rs
index 425d9b976..3a5f46f58 100644
--- a/crates/ixon/src/env.rs
+++ b/crates/ixon/src/env.rs
@@ -13,27 +13,117 @@ use super::lazy::LazyConstant;
 use super::map::IxonMap;
 use super::metadata::{ConstantMeta, ConstantMetaInfo};
 
+/// Metadata representation inside [`Named`]: structured, or demoted to
+/// its self-contained serialized form ([`ConstantMeta::put_raw`]),
+/// which costs a fraction of the pointer-rich structured DAG and is
+/// decoded on demand. The demoted form is chosen at registration under
+/// [`DEMOTE`] (the default).
+#[derive(Clone, Debug)]
+enum MetaRepr {
+  Structured(Arc<ConstantMeta>),
+  Bytes(Arc<[u8]>),
+}
+
+impl MetaRepr {
+  fn structured(meta: ConstantMeta) -> Self {
+    MetaRepr::Structured(Arc::new(meta))
+  }
+
+  fn demoted(meta: &ConstantMeta) -> Self {
+    let mut buf = Vec::new();
+    meta
+      .put_raw(&mut buf)
+      .expect("ConstantMeta::put_raw cannot fail on in-memory metadata");
+    MetaRepr::Bytes(buf.into())
+  }
+
+  /// Materialize. Cheap `Arc` clone for `Structured`; a fresh decode per
+  /// call for `Bytes` (nothing is cached — mirroring `LazyConstant`).
+  fn decode(&self) -> Arc<ConstantMeta> {
+    match self {
+      MetaRepr::Structured(m) => m.clone(),
+      MetaRepr::Bytes(b) => {
+        let mut slice: &[u8] = b;
+        Arc::new(
+          ConstantMeta::get_raw(&mut slice)
+            .expect("Named meta bytes produced by put_raw failed to decode"),
+        )
+      },
+    }
+  }
+}
+
 /// A named constant with metadata.
 #[derive(Clone, Debug)]
 pub struct Named {
   /// Address of the constant (in consts map)
   pub addr: Address,
-  /// Typed metadata for this constant (includes mutual context in `all` field)
-  pub meta: ConstantMeta,
+  /// Typed metadata for this constant (includes mutual context in `all`
+  /// field). Private repr: structured, or demoted to serialized bytes —
+  /// read through [`Self::meta`].
+  meta: MetaRepr,
   /// For aux_gen-rewritten constants: the original Lean constant's compiled
   /// form (address + metadata). Ingress uses `addr`/`meta` (the canonical
   /// aux_gen form). Decompile uses `original` for faithful roundtrip of
   /// binder names and other cosmetic metadata.
-  pub original: Option<(Address, ConstantMeta)>,
+  original: Option<(Address, MetaRepr)>,
 }
 
 impl Named {
   pub fn new(addr: Address, meta: ConstantMeta) -> Self {
-    Named { addr, meta, original: None }
+    Named { addr, meta: MetaRepr::structured(meta), original: None }
   }
 
   pub fn with_addr(addr: Address) -> Self {
-    Named { addr, meta: ConstantMeta::default(), original: None }
+    Named {
+      addr,
+      meta: MetaRepr::structured(ConstantMeta::default()),
+      original: None,
+    }
+  }
+
+  /// The constant's metadata. Cheap (`Arc` clone) for structured
+  /// entries; a fresh decode per call for demoted ones.
+  pub fn meta(&self) -> Arc<ConstantMeta> {
+    self.meta.decode()
+  }
+
+  /// The aux_gen original form, if recorded (see field docs).
+  pub fn original(&self) -> Option<(Address, Arc<ConstantMeta>)> {
+    self.original.as_ref().map(|(a, m)| (a.clone(), m.decode()))
+  }
+
+  pub fn has_original(&self) -> bool {
+    self.original.is_some()
+  }
+
+  /// Record the aux_gen original form. Stored in the same repr as
+  /// `self.meta`, so demoted entries stay fully demoted.
+  pub fn set_original(&mut self, addr: Address, meta: ConstantMeta) {
+    let repr = match &self.meta {
+      MetaRepr::Structured(_) => MetaRepr::structured(meta),
+      MetaRepr::Bytes(_) => MetaRepr::demoted(&meta),
+    };
+    self.original = Some((addr, repr));
+  }
+
+  pub fn clear_original(&mut self) {
+    self.original = None;
+  }
+
+  /// Convert both metadata slots to the serialized-bytes repr.
+  pub fn demote(&mut self) {
+    if let MetaRepr::Structured(m) = &self.meta {
+      self.meta = MetaRepr::demoted(m);
+    }
+    if let Some((a, MetaRepr::Structured(m))) = &self.original {
+      self.original = Some((a.clone(), MetaRepr::demoted(m)));
+    }
+  }
+
+  /// Whether the primary metadata slot holds structured metadata.
+  pub fn is_meta_structured(&self) -> bool {
+    matches!(self.meta, MetaRepr::Structured(_))
   }
 }
 
@@ -83,6 +173,20 @@ pub struct LazyNamed {
   pub hint: Option<ReducibilityHints>,
 }
 
+/// `IX_COMPILE_DEMOTE` (default **on**; set `0` to disable): store the
+/// compile accumulator's constants and registered names' metadata as
+/// serialized bytes instead of keeping the structured forms resident.
+/// The structured forms cost a large multiple of their encodings
+/// (~20× measured) and compilation never reads them back; the `.ixe`
+/// output is byte-identical either way. Disabling trades that RAM for
+/// materialized-on-store caches, which only helps in-process flows
+/// that re-read the env structurally after compiling (`ix check` /
+/// `ix validate`).
+#[cfg(not(target_arch = "riscv64"))]
+pub static DEMOTE: std::sync::LazyLock<bool> = std::sync::LazyLock::new(|| {
+  std::env::var("IX_COMPILE_DEMOTE").as_deref() != Ok("0")
+});
+
 /// Result of [`Env::parse_lazy_index`]: a metadata-light, zero-copy view of an
 /// `.ixe` buffer suitable for the anon/lazy check path. Constants are byte
 /// windows (offsets), `named` is `name → addr` + hint, and `blobs` are copied
@@ -165,14 +269,42 @@ impl Env {
 
   /// Store a structured constant under `addr`.
   ///
-  /// Serializes the constant once and pre-populates the
-  /// [`LazyConstant`] cache so subsequent `Env::put` is a memcpy and
-  /// the first `get_const` call is free.
+  /// Serializes the constant once. With demotion disabled,
+  /// the [`LazyConstant`] cache is pre-populated so `get_const` is
+  /// free; under [`DEMOTE`] (the default) the structured value is
+  /// dropped and the entry costs only its bytes (`get_const` re-parses
+  /// per access). Compilation never reads stored constants back, so the
+  /// modes differ only in memory footprint and later readers' CPU cost.
   ///
   /// Host-only — see `store_blob`.
   #[cfg(not(target_arch = "riscv64"))]
   pub fn store_const(&self, addr: Address, constant: Constant) {
-    self.consts.insert(addr, LazyConstant::from_constant(constant));
+    self.store_const_demoted(addr, constant, *DEMOTE);
+  }
+
+  /// `store_const` with an explicit demotion choice, bypassing
+  /// `IX_COMPILE_DEMOTE`. Exists so tests can drive both reprs without
+  /// process-global env-var races.
+  #[cfg(not(target_arch = "riscv64"))]
+  pub fn store_const_demoted(
+    &self,
+    addr: Address,
+    constant: Constant,
+    demote: bool,
+  ) {
+    if demote {
+      // A re-store of an existing address is a no-op: content
+      // addressing guarantees identical bytes. (Alpha-collapsed blocks
+      // re-store the shared address once per member.) The cached mode
+      // keeps insert-overwrite: there a re-store can upgrade a
+      // cache-less lazy-loaded entry to a cached one.
+      if self.consts.contains_key(&addr) {
+        return;
+      }
+      self.consts.insert(addr, LazyConstant::from_constant_uncached(&constant));
+    } else {
+      self.consts.insert(addr, LazyConstant::from_constant(constant));
+    }
   }
 
   /// Store an already-serialized constant under `addr` (lazy load path).
@@ -221,9 +353,16 @@ impl Env {
     self.consts.get(addr).map(|r| Arc::from(r.value().raw_bytes()))
   }
 
-  /// Register a named constant. Host-only — see `store_blob`.
+  /// Register a named constant. Under [`DEMOTE`] (the default) the
+  /// entry's metadata is stored in its serialized-bytes form (see
+  /// [`Named::demote`]) — the structured DAG costs a large multiple of
+  /// its encoding and compilation never reads it back.
+  /// Host-only — see `store_blob`.
   #[cfg(not(target_arch = "riscv64"))]
-  pub fn register_name(&self, name: Name, named: Named) {
+  pub fn register_name(&self, name: Name, mut named: Named) {
+    if *DEMOTE {
+      named.demote();
+    }
     self.named.insert(name, named);
   }
 
@@ -273,7 +412,9 @@ impl Env {
     self
       .named
       .iter()
-      .filter(|e| !matches!(e.value().meta.info, ConstantMetaInfo::Muts { .. }))
+      .filter(|e| {
+        !matches!(e.value().meta().info, ConstantMetaInfo::Muts { .. })
+      })
       .map(|e| e.value().addr.clone())
       .collect()
   }
@@ -420,6 +561,85 @@ mod tests {
     assert_eq!(*got, constant);
   }
 
+  /// Distinct axiom per `lvls` so each store gets its own address.
+  fn axiom_with_lvls(lvls: u64) -> Constant {
+    Constant::new(ConstantInfo::Axio(Axiom {
+      is_unsafe: false,
+      lvls,
+      typ: Arc::new(Expr::Sort(0)),
+    }))
+  }
+
+  /// Preset an Active spill state with a tiny segment so a handful of
+  /// stores force seals (bypasses the env-var-driven `SpillState::create`).
+  #[test]
+  fn store_const_demoted_roundtrips_uncached() {
+    let env = Env::new();
+    let mut stored = Vec::new();
+    for i in 0..64 {
+      let c = axiom_with_lvls(i);
+      let (addr, _) = c.commit();
+      env.store_const_demoted(addr.clone(), c.clone(), true);
+      stored.push((addr, c));
+    }
+    for (addr, c) in &stored {
+      let entry = env.consts.get(addr).unwrap();
+      assert!(entry.value().verify_address(addr));
+      assert!(!entry.value().is_materialized());
+      drop(entry);
+      assert_eq!(*env.get_const(addr).unwrap(), *c);
+    }
+  }
+
+  #[test]
+  fn demoted_named_roundtrips_and_serializes_identically() {
+    let addr = Address::hash(b"demoted-named-target");
+    // Empty metadata: no name references, so `Env::put` needs no name
+    // index entries. Name-ref-rich raw/indexed equivalence is covered
+    // by `metadata::tests::test_constant_meta_indexed_roundtrip`.
+    let meta = ConstantMeta::default();
+    let mut structured = Named::new(addr.clone(), meta.clone());
+    structured.set_original(addr.clone(), meta.clone());
+    let mut demoted = structured.clone();
+    demoted.demote();
+
+    assert!(structured.is_meta_structured());
+    assert!(!demoted.is_meta_structured());
+    // Accessors agree between reprs.
+    assert_eq!(*structured.meta(), *demoted.meta());
+    assert!(demoted.has_original());
+    let (sa, sm) = structured.original().unwrap();
+    let (da, dm) = demoted.original().unwrap();
+    assert_eq!(sa, da);
+    assert_eq!(*sm, *dm);
+
+    // Envs whose named entries differ only in repr serialize identically.
+    let mk_env = |named: &Named| {
+      let env = Env::new();
+      env.register_name(n("target"), named.clone());
+      let mut buf = Vec::new();
+      env.put(&mut buf).unwrap();
+      buf
+    };
+    assert_eq!(mk_env(&structured), mk_env(&demoted));
+  }
+
+  #[test]
+  fn env_put_identical_across_demotion() {
+    let build = |demote: bool| {
+      let env = Env::new();
+      for i in 0..32 {
+        let c = axiom_with_lvls(i);
+        let (addr, _) = c.commit();
+        env.store_const_demoted(addr, c, demote);
+      }
+      let mut buf = Vec::new();
+      env.put(&mut buf).unwrap();
+      buf
+    };
+    assert_eq!(build(false), build(true));
+  }
+
   #[test]
   fn register_and_lookup_name() {
     let env = Env::new();
diff --git a/crates/ixon/src/lazy.rs b/crates/ixon/src/lazy.rs
index f08330e1a..edfa356d4 100644
--- a/crates/ixon/src/lazy.rs
+++ b/crates/ixon/src/lazy.rs
@@ -140,6 +140,17 @@ impl LazyConstant {
     }
   }
 
+  /// Like [`Self::from_constant`] but drops the structured value after
+  /// serializing (`cache: None`), so the entry costs only its bytes and
+  /// `get()` re-parses per access — the same policy as
+  /// [`Self::from_bytes`]. The demoted accumulator repr (see
+  /// `env::DEMOTE`).
+  pub fn from_constant_uncached(c: &Constant) -> Self {
+    let mut buf = Vec::new();
+    c.put(&mut buf);
+    LazyConstant { bytes: BytesSource::Heap(buf.into()), cache: None }
+  }
+
   /// Materialize the `Constant`.
   ///
   /// If this entry was built via [`Self::from_constant`], returns the
@@ -294,6 +305,20 @@ mod tests {
     assert!(!lazy.is_materialized());
   }
 
+  #[test]
+  fn from_constant_uncached_roundtrips_without_cache() {
+    let c = defn_constant();
+    let (addr, bytes) = c.commit();
+    let lazy = LazyConstant::from_constant_uncached(&c);
+    assert!(!lazy.is_materialized());
+    // Same serialized form as the cached constructor / commit().
+    assert_eq!(lazy.raw_bytes(), &bytes[..]);
+    assert!(lazy.verify_address(&addr));
+    assert_eq!(*lazy.get().unwrap(), c);
+    // get() parses fresh and does not populate a cache.
+    assert!(!lazy.is_materialized());
+  }
+
   #[test]
   fn from_constant_clones_share_cache() {
     let c = axiom_constant();
diff --git a/crates/ixon/src/metadata.rs b/crates/ixon/src/metadata.rs
index e76992672..c126fafb0 100644
--- a/crates/ixon/src/metadata.rs
+++ b/crates/ixon/src/metadata.rs
@@ -254,12 +254,12 @@ impl ConstantMeta {
 
   /// Delegate indexed serialization to the inner enum, then serialize
   /// extension tables.
-  pub fn put_indexed(
+  pub fn put_with(
     &self,
-    idx: &NameIndex,
+    idx: NamePut<'_>,
     buf: &mut Vec<u8>,
   ) -> Result<(), String> {
-    self.info.put_indexed(idx, buf)?;
+    self.info.put_with(idx, buf)?;
     // Extension tables (backward-compatible: 0-length for old constants)
     put_vec_len(self.meta_sharing.len(), buf);
     for expr in &self.meta_sharing {
@@ -276,13 +276,23 @@ impl ConstantMeta {
     Ok(())
   }
 
+  /// Self-contained encoding: name references as raw 32-byte addresses,
+  /// no index required. This is the demoted in-memory form
+  /// (see `env::DEMOTE`), NOT the `.ixe` named-section encoding —
+  /// `Env::put` re-encodes through the name index.
+  pub fn put_raw(&self, buf: &mut Vec<u8>) -> Result<(), String> {
+    self.put_with(NamePut::Raw, buf)
+  }
+
+  /// Decode the [`Self::put_raw`] encoding.
+  pub fn get_raw(buf: &mut &[u8]) -> Result<Self, String> {
+    Self::get_with(buf, NameGet::Raw)
+  }
+
   /// Delegate indexed deserialization, then deserialize extension tables.
-  pub fn get_indexed(
-    buf: &mut &[u8],
-    rev: &NameReverseIndex,
-  ) -> Result<Self, String> {
-    let info = ConstantMetaInfo::get_indexed(buf, rev)?;
-    // Extension tables: always present (put_indexed always writes them,
+  pub fn get_with(buf: &mut &[u8], rev: NameGet<'_>) -> Result<Self, String> {
+    let info = ConstantMetaInfo::get_with(buf, rev)?;
+    // Extension tables: always present (put_with always writes them,
     // even when empty — three zero-length vectors).
     let sharing_len = get_vec_len(buf)?;
     let mut meta_sharing = Vec::with_capacity(sharing_len);
@@ -631,36 +641,65 @@ pub type NameIndex = HashMap<Address, u64>;
 /// Reverse name index for deserialization: position -> Address
 pub type NameReverseIndex = Vec<Address>;
 
+/// How name references are written: compressed through the env-level
+/// name index (the `.ixe` named-section form), or as raw 32-byte
+/// addresses — a self-contained encoding that needs no index, used by
+/// the demoted in-memory metadata form (see `env::DEMOTE`).
+#[derive(Clone, Copy)]
+pub enum NamePut<'a> {
+  Indexed(&'a NameIndex),
+  Raw,
+}
+
+/// Decoding counterpart of [`NamePut`].
+#[derive(Clone, Copy)]
+pub enum NameGet<'a> {
+  Indexed(&'a NameReverseIndex),
+  Raw,
+}
+
 pub(super) fn put_idx(
   addr: &Address,
-  idx: &NameIndex,
+  idx: NamePut<'_>,
   buf: &mut Vec<u8>,
 ) -> Result<(), String> {
-  let i = idx.get(addr).copied().ok_or_else(|| {
-    format!(
-      "put_idx: address {:?} not in name index (index has {} entries)",
-      addr,
-      idx.len()
-    )
-  })?;
-  put_u64(i, buf);
-  Ok(())
+  match idx {
+    NamePut::Indexed(map) => {
+      let i = map.get(addr).copied().ok_or_else(|| {
+        format!(
+          "put_idx: address {:?} not in name index (index has {} entries)",
+          addr,
+          map.len()
+        )
+      })?;
+      put_u64(i, buf);
+      Ok(())
+    },
+    NamePut::Raw => {
+      put_address_raw(addr, buf);
+      Ok(())
+    },
+  }
 }
 
 pub(super) fn get_idx(
   buf: &mut &[u8],
-  rev: &NameReverseIndex,
+  rev: NameGet<'_>,
 ) -> Result<Address, String> {
-  let i = get_u64(buf)? as usize;
-  rev
-    .get(i)
-    .cloned()
-    .ok_or_else(|| format!("invalid name index {i}, max {}", rev.len()))
+  match rev {
+    NameGet::Indexed(v) => {
+      let i = get_u64(buf)? as usize;
+      v.get(i)
+        .cloned()
+        .ok_or_else(|| format!("invalid name index {i}, max {}", v.len()))
+    },
+    NameGet::Raw => get_address_raw(buf),
+  }
 }
 
 fn put_idx_vec(
   addrs: &[Address],
-  idx: &NameIndex,
+  idx: NamePut<'_>,
   buf: &mut Vec<u8>,
 ) -> Result<(), String> {
   put_vec_len(addrs.len(), buf);
@@ -672,7 +711,7 @@ fn put_idx_vec(
 
 fn get_idx_vec(
   buf: &mut &[u8],
-  rev: &NameReverseIndex,
+  rev: NameGet<'_>,
 ) -> Result<Vec<Address>, String> {
   let len = get_vec_len(buf)?;
   let mut v = Vec::with_capacity(len);
@@ -687,9 +726,9 @@ fn get_idx_vec(
 // ===========================================================================
 
 impl DataValue {
-  pub fn put_indexed(
+  pub fn put_with(
     &self,
-    idx: &NameIndex,
+    idx: NamePut<'_>,
     buf: &mut Vec<u8>,
   ) -> Result<(), String> {
     match self {
@@ -723,10 +762,7 @@ impl DataValue {
     Ok(())
   }
 
-  pub fn get_indexed(
-    buf: &mut &[u8],
-    rev: &NameReverseIndex,
-  ) -> Result<Self, String> {
+  pub fn get_with(buf: &mut &[u8], rev: NameGet<'_>) -> Result<Self, String> {
     match get_u8(buf)? {
       0 => Ok(Self::OfString(get_address_raw(buf)?)),
       1 => Ok(Self::OfBool(get_bool(buf)?)),
@@ -745,32 +781,32 @@ impl DataValue {
 
 fn put_kvmap_indexed(
   kvmap: &KVMap,
-  idx: &NameIndex,
+  idx: NamePut<'_>,
   buf: &mut Vec<u8>,
 ) -> Result<(), String> {
   put_vec_len(kvmap.len(), buf);
   for (k, v) in kvmap {
     put_idx(k, idx, buf)?;
-    v.put_indexed(idx, buf)?;
+    v.put_with(idx, buf)?;
   }
   Ok(())
 }
 
 fn get_kvmap_indexed(
   buf: &mut &[u8],
-  rev: &NameReverseIndex,
+  rev: NameGet<'_>,
 ) -> Result<KVMap, String> {
   let len = get_vec_len(buf)?;
   let mut kvmap = Vec::with_capacity(len);
   for _ in 0..len {
-    kvmap.push((get_idx(buf, rev)?, DataValue::get_indexed(buf, rev)?));
+    kvmap.push((get_idx(buf, rev)?, DataValue::get_with(buf, rev)?));
   }
   Ok(kvmap)
 }
 
 fn put_mdata_stack_indexed(
   mdata: &[KVMap],
-  idx: &NameIndex,
+  idx: NamePut<'_>,
   buf: &mut Vec<u8>,
 ) -> Result<(), String> {
   put_vec_len(mdata.len(), buf);
@@ -782,7 +818,7 @@ fn put_mdata_stack_indexed(
 
 fn get_mdata_stack_indexed(
   buf: &mut &[u8],
-  rev: &NameReverseIndex,
+  rev: NameGet<'_>,
 ) -> Result<Vec<KVMap>, String> {
   let len = get_vec_len(buf)?;
   let mut mdata = Vec::with_capacity(len);
@@ -805,9 +841,9 @@ impl ExprMetaData {
   // Tag 8: Prj { struct_name_idx, child: u32 }
   // Tag 9: Mdata { kvmap_count, kvmaps..., child: u32 }
 
-  pub fn put_indexed(
+  pub fn put_with(
     &self,
-    idx: &NameIndex,
+    idx: NamePut<'_>,
     buf: &mut Vec<u8>,
   ) -> Result<(), String> {
     match self {
@@ -883,10 +919,7 @@ impl ExprMetaData {
     Ok(())
   }
 
-  pub fn get_indexed(
-    buf: &mut &[u8],
-    rev: &NameReverseIndex,
-  ) -> Result<Self, String> {
+  pub fn get_with(buf: &mut &[u8], rev: NameGet<'_>) -> Result<Self, String> {
     match get_u8(buf)? {
       0 => Ok(Self::Leaf),
       1 => {
@@ -972,26 +1005,23 @@ impl ExprMetaData {
 // ===========================================================================
 
 impl ExprMeta {
-  pub fn put_indexed(
+  pub fn put_with(
     &self,
-    idx: &NameIndex,
+    idx: NamePut<'_>,
     buf: &mut Vec<u8>,
   ) -> Result<(), String> {
     put_vec_len(self.nodes.len(), buf);
     for node in &self.nodes {
-      node.put_indexed(idx, buf)?;
+      node.put_with(idx, buf)?;
     }
     Ok(())
   }
 
-  pub fn get_indexed(
-    buf: &mut &[u8],
-    rev: &NameReverseIndex,
-  ) -> Result<Self, String> {
+  pub fn get_with(buf: &mut &[u8], rev: NameGet<'_>) -> Result<Self, String> {
     let len = get_vec_len(buf)?;
     let mut nodes = Vec::with_capacity(len);
     for _ in 0..len {
-      nodes.push(ExprMetaData::get_indexed(buf, rev)?);
+      nodes.push(ExprMetaData::get_with(buf, rev)?);
     }
     Ok(ExprMeta { nodes })
   }
@@ -1018,9 +1048,9 @@ fn get_u64_vec(buf: &mut &[u8]) -> Result<Vec<u64>, String> {
 // ===========================================================================
 
 impl ConstantMetaInfo {
-  pub fn put_indexed(
+  pub fn put_with(
     &self,
-    idx: &NameIndex,
+    idx: NamePut<'_>,
     buf: &mut Vec<u8>,
   ) -> Result<(), String> {
     match self {
@@ -1041,7 +1071,7 @@ impl ConstantMetaInfo {
         hints.put_ser(buf);
         put_idx_vec(all, idx, buf)?;
         put_idx_vec(ctx, idx, buf)?;
-        arena.put_indexed(idx, buf)?;
+        arena.put_with(idx, buf)?;
         put_u64(*type_root, buf);
         put_u64(*value_root, buf);
       },
@@ -1049,14 +1079,14 @@ impl ConstantMetaInfo {
         put_u8(1, buf);
         put_idx(name, idx, buf)?;
         put_idx_vec(lvls, idx, buf)?;
-        arena.put_indexed(idx, buf)?;
+        arena.put_with(idx, buf)?;
         put_u64(*type_root, buf);
       },
       Self::Quot { name, lvls, arena, type_root } => {
         put_u8(2, buf);
         put_idx(name, idx, buf)?;
         put_idx_vec(lvls, idx, buf)?;
-        arena.put_indexed(idx, buf)?;
+        arena.put_with(idx, buf)?;
         put_u64(*type_root, buf);
       },
       Self::Indc { name, lvls, ctors, all, ctx, arena, type_root } => {
@@ -1066,7 +1096,7 @@ impl ConstantMetaInfo {
         put_idx_vec(ctors, idx, buf)?;
         put_idx_vec(all, idx, buf)?;
         put_idx_vec(ctx, idx, buf)?;
-        arena.put_indexed(idx, buf)?;
+        arena.put_with(idx, buf)?;
         put_u64(*type_root, buf);
       },
       Self::Ctor { name, lvls, induct, arena, type_root } => {
@@ -1074,7 +1104,7 @@ impl ConstantMetaInfo {
         put_idx(name, idx, buf)?;
         put_idx_vec(lvls, idx, buf)?;
         put_idx(induct, idx, buf)?;
-        arena.put_indexed(idx, buf)?;
+        arena.put_with(idx, buf)?;
         put_u64(*type_root, buf);
       },
       Self::Rec {
@@ -1093,7 +1123,7 @@ impl ConstantMetaInfo {
         put_idx_vec(rules, idx, buf)?;
         put_idx_vec(all, idx, buf)?;
         put_idx_vec(ctx, idx, buf)?;
-        arena.put_indexed(idx, buf)?;
+        arena.put_with(idx, buf)?;
         put_u64(*type_root, buf);
         put_u64_vec(rule_roots, buf);
       },
@@ -1125,10 +1155,7 @@ impl ConstantMetaInfo {
     Ok(())
   }
 
-  pub fn get_indexed(
-    buf: &mut &[u8],
-    rev: &NameReverseIndex,
-  ) -> Result<Self, String> {
+  pub fn get_with(buf: &mut &[u8], rev: NameGet<'_>) -> Result<Self, String> {
     match get_u8(buf)? {
       255 => Ok(Self::Empty),
       0 => Ok(Self::Def {
@@ -1137,20 +1164,20 @@ impl ConstantMetaInfo {
         hints: ReducibilityHints::get_ser(buf)?,
         all: get_idx_vec(buf, rev)?,
         ctx: get_idx_vec(buf, rev)?,
-        arena: ExprMeta::get_indexed(buf, rev)?,
+        arena: ExprMeta::get_with(buf, rev)?,
         type_root: get_u64(buf)?,
         value_root: get_u64(buf)?,
       }),
       1 => Ok(Self::Axio {
         name: get_idx(buf, rev)?,
         lvls: get_idx_vec(buf, rev)?,
-        arena: ExprMeta::get_indexed(buf, rev)?,
+        arena: ExprMeta::get_with(buf, rev)?,
         type_root: get_u64(buf)?,
       }),
       2 => Ok(Self::Quot {
         name: get_idx(buf, rev)?,
         lvls: get_idx_vec(buf, rev)?,
-        arena: ExprMeta::get_indexed(buf, rev)?,
+        arena: ExprMeta::get_with(buf, rev)?,
         type_root: get_u64(buf)?,
       }),
       3 => Ok(Self::Indc {
@@ -1159,14 +1186,14 @@ impl ConstantMetaInfo {
         ctors: get_idx_vec(buf, rev)?,
         all: get_idx_vec(buf, rev)?,
         ctx: get_idx_vec(buf, rev)?,
-        arena: ExprMeta::get_indexed(buf, rev)?,
+        arena: ExprMeta::get_with(buf, rev)?,
         type_root: get_u64(buf)?,
       }),
       4 => Ok(Self::Ctor {
         name: get_idx(buf, rev)?,
         lvls: get_idx_vec(buf, rev)?,
         induct: get_idx(buf, rev)?,
-        arena: ExprMeta::get_indexed(buf, rev)?,
+        arena: ExprMeta::get_with(buf, rev)?,
         type_root: get_u64(buf)?,
       }),
       5 => Ok(Self::Rec {
@@ -1175,7 +1202,7 @@ impl ConstantMetaInfo {
         rules: get_idx_vec(buf, rev)?,
         all: get_idx_vec(buf, rev)?,
         ctx: get_idx_vec(buf, rev)?,
-        arena: ExprMeta::get_indexed(buf, rev)?,
+        arena: ExprMeta::get_with(buf, rev)?,
         type_root: get_u64(buf)?,
         rule_roots: get_u64_vec(buf)?,
       }),
@@ -1282,10 +1309,22 @@ mod tests {
     });
 
     let mut buf = Vec::new();
-    meta.put_indexed(&idx, &mut buf).unwrap();
+    meta.put_with(NamePut::Indexed(&idx), &mut buf).unwrap();
     let recovered =
-      ConstantMeta::get_indexed(&mut buf.as_slice(), &rev).unwrap();
+      ConstantMeta::get_with(&mut buf.as_slice(), NameGet::Indexed(&rev))
+        .unwrap();
     assert_eq!(meta, recovered);
+
+    // Raw (self-contained) encoding roundtrips the same value without
+    // any index, and re-encoding the recovered value through the index
+    // matches the indexed bytes exactly.
+    let mut raw = Vec::new();
+    meta.put_raw(&mut raw).unwrap();
+    let from_raw = ConstantMeta::get_raw(&mut raw.as_slice()).unwrap();
+    assert_eq!(meta, from_raw);
+    let mut reindexed = Vec::new();
+    from_raw.put_with(NamePut::Indexed(&idx), &mut reindexed).unwrap();
+    assert_eq!(buf, reindexed);
   }
 
   #[test]
@@ -1307,8 +1346,9 @@ mod tests {
     let _ = mdata;
 
     let mut buf = Vec::new();
-    arena.put_indexed(&idx, &mut buf).unwrap();
-    let recovered = ExprMeta::get_indexed(&mut buf.as_slice(), &rev).unwrap();
+    arena.put_with(NamePut::Indexed(&idx), &mut buf).unwrap();
+    let recovered =
+      ExprMeta::get_with(&mut buf.as_slice(), NameGet::Indexed(&rev)).unwrap();
     assert_eq!(arena, recovered);
   }
 }
diff --git a/crates/ixon/src/serialize.rs b/crates/ixon/src/serialize.rs
index 2e2fd9b86..08ee0856e 100644
--- a/crates/ixon/src/serialize.rs
+++ b/crates/ixon/src/serialize.rs
@@ -1019,7 +1019,9 @@ fn get_name_component(
 // ============================================================================
 
 use super::env::{AuxLayout, Named};
-use super::metadata::{ConstantMeta, NameIndex, NameReverseIndex};
+use super::metadata::{
+  ConstantMeta, NameGet, NameIndex, NamePut, NameReverseIndex,
+};
 
 /// Serialize an `AuxLayout` side-table entry.
 ///
@@ -1059,14 +1061,17 @@ pub fn put_named_indexed(
   buf: &mut Vec<u8>,
 ) -> Result<(), String> {
   put_address(&named.addr, buf);
-  named.meta.put_indexed(idx, buf)?;
+  // Demoted entries decode here and re-encode through the name index —
+  // the raw and indexed encodings share the wire format, differing only
+  // in how name references are written.
+  named.meta().put_with(NamePut::Indexed(idx), buf)?;
   // Serialize original as Option: 0 = None, 1 = Some(addr, meta)
-  match &named.original {
+  match named.original() {
     None => buf.push(0),
     Some((addr, meta)) => {
       buf.push(1);
-      put_address(addr, buf);
-      meta.put_indexed(idx, buf)?;
+      put_address(&addr, buf);
+      meta.put_with(NamePut::Indexed(idx), buf)?;
     },
   }
   Ok(())
@@ -1078,17 +1083,18 @@ pub fn get_named_indexed(
   rev: &NameReverseIndex,
 ) -> Result<Named, String> {
   let addr = get_address(buf)?;
-  let meta = ConstantMeta::get_indexed(buf, rev)?;
-  let original = match get_u8(buf)? {
-    0 => None,
+  let meta = ConstantMeta::get_with(buf, NameGet::Indexed(rev))?;
+  let mut named = Named::new(addr, meta);
+  match get_u8(buf)? {
+    0 => {},
     1 => {
       let orig_addr = get_address(buf)?;
-      let orig_meta = ConstantMeta::get_indexed(buf, rev)?;
-      Some((orig_addr, orig_meta))
+      let orig_meta = ConstantMeta::get_with(buf, NameGet::Indexed(rev))?;
+      named.set_original(orig_addr, orig_meta);
     },
     x => return Err(format!("Named.original: invalid tag {x}")),
-  };
-  Ok(Named { addr, meta, original })
+  }
+  Ok(named)
 }
 
 // ============================================================================
@@ -1367,6 +1373,144 @@ impl Env {
     Ok(())
   }
 
+  /// Serialize the environment directly to a file, streaming entry by
+  /// entry through a reusable staging buffer — nothing proportional to
+  /// env size is allocated (contrast [`Env::put`], whose output `Vec`
+  /// is ~env size). Returns the byte count written.
+  ///
+  /// MUST remain byte-identical with [`Env::put`] — checked by the
+  /// `put_file_matches_put` test. Any format
+  /// change lands in both or not at all.
+  #[cfg(not(target_arch = "riscv64"))]
+  pub fn put_file(&self, path: &std::path::Path) -> Result<u64, String> {
+    use rayon::prelude::*;
+    use std::io::Write;
+    let file = std::fs::File::create(path)
+      .map_err(|e| format!("Env::put_file: create {}: {e}", path.display()))?;
+    let mut w = std::io::BufWriter::with_capacity(8 * 1024 * 1024, file);
+    let mut written: u64 = 0;
+    let mut buf: Vec<u8> = Vec::with_capacity(64 * 1024);
+    // Drain the staging buffer to the writer. Large constant bodies
+    // bypass staging and go straight to the writer.
+    macro_rules! emit {
+      () => {
+        if !buf.is_empty() {
+          w.write_all(&buf)
+            .map_err(|e| format!("Env::put_file: write: {e}"))?;
+          written += buf.len() as u64;
+          buf.clear();
+        }
+      };
+    }
+
+    // Header: Tag4 + canonical merkle root over consts.keys().
+    Tag4::new(Self::FLAG, 0).put(&mut buf);
+    let mut const_addrs: Vec<Address> =
+      self.consts.iter().map(|e| e.key().clone()).collect();
+    const_addrs.par_sort_unstable();
+    let root = merkle_root_canonical(&const_addrs).unwrap_or_else(zero_address);
+    put_address(&root, &mut buf);
+
+    // Section 1: Blobs
+    let mut blob_addrs: Vec<Address> =
+      self.blobs.iter().map(|e| e.key().clone()).collect();
+    blob_addrs.par_sort_unstable();
+    put_u64(blob_addrs.len() as u64, &mut buf);
+    for addr in &blob_addrs {
+      if let Some(entry) = self.blobs.get(addr) {
+        let bytes = entry.value();
+        put_address(addr, &mut buf);
+        put_u64(bytes.len() as u64, &mut buf);
+        buf.extend_from_slice(bytes);
+        emit!();
+      }
+    }
+
+    // Section 2: Consts — the dominant bytes; raw_bytes stream straight
+    // through with no intermediate copy of the constant bodies
+    put_u64(const_addrs.len() as u64, &mut buf);
+    for addr in &const_addrs {
+      if let Some(entry) = self.consts.get(addr) {
+        put_address(addr, &mut buf);
+        let bytes = entry.value().raw_bytes();
+        Tag0::new(bytes.len() as u64).put(&mut buf);
+        emit!();
+        w.write_all(bytes)
+          .map_err(|e| format!("Env::put_file: write const: {e}"))?;
+        written += bytes.len() as u64;
+      }
+    }
+    // Section 3: Names (topologically sorted; builds the name index the
+    // Named section encodes through).
+    let sorted_names = topological_sort_names(&self.names);
+    let mut name_index: NameIndex = NameIndex::new();
+    put_u64(sorted_names.len() as u64, &mut buf);
+    for (i, (addr, name)) in sorted_names.iter().enumerate() {
+      name_index.insert(addr.clone(), i as u64);
+      put_address(addr, &mut buf);
+      put_name_component(name, &mut buf);
+      emit!();
+    }
+
+    // Section 4: Named — the largest per-entry section, and the only
+    // one whose per-entry encode is CPU-heavy (demoted entries decode
+    // and re-encode through the name index). Chunks encode in parallel
+    // into per-entry buffers and drain to the writer in order; the
+    // chunk size bounds staged memory to a few MiB.
+    let mut named_keys: Vec<Name> =
+      self.named.iter().map(|e| e.key().clone()).collect();
+    named_keys.par_sort_unstable_by(|a, b| {
+      a.get_hash().as_bytes().cmp(b.get_hash().as_bytes())
+    });
+    put_u64(named_keys.len() as u64, &mut buf);
+    emit!();
+    for chunk in named_keys.chunks(4096) {
+      let encoded: Vec<Vec<u8>> = chunk
+        .into_par_iter()
+        .map(|name| {
+          let mut b = Vec::new();
+          if let Some(entry) = self.named.get(name) {
+            put_bytes(name.get_hash().as_bytes(), &mut b);
+            put_named_indexed(entry.value(), &name_index, &mut b)?;
+          }
+          Ok::<_, String>(b)
+        })
+        .collect::<Result<_, _>>()?;
+      for b in &encoded {
+        w.write_all(b).map_err(|e| format!("Env::put_file: write: {e}"))?;
+        written += b.len() as u64;
+      }
+    }
+    // Section 5: Comms
+    let mut comm_addrs: Vec<Address> =
+      self.comms.iter().map(|e| e.key().clone()).collect();
+    comm_addrs.par_sort_unstable();
+    put_u64(comm_addrs.len() as u64, &mut buf);
+    for addr in &comm_addrs {
+      if let Some(entry) = self.comms.get(addr) {
+        put_address(addr, &mut buf);
+        entry.value().put(&mut buf);
+        emit!();
+      }
+    }
+
+    // Optional trailing anon_hints section — same condition as `put`.
+    if !self.anon_hints.is_empty() {
+      let mut hint_addrs: Vec<Address> =
+        self.anon_hints.keys().cloned().collect();
+      hint_addrs.sort_unstable();
+      put_u64(hint_addrs.len() as u64, &mut buf);
+      for addr in &hint_addrs {
+        put_address(addr, &mut buf);
+        self.anon_hints[addr].put_ser(&mut buf);
+      }
+    }
+
+    emit!();
+    w.flush().map_err(|e| format!("Env::put_file: flush: {e}"))?;
+    Ok(written)
+  }
+
   /// Deserialize an Env from bytes.
   pub fn get(buf: &mut &[u8]) -> Result<Self, String> {
     // Header
@@ -1598,7 +1742,7 @@ impl Env {
       let name = names_lookup.get(&name_addr).cloned().ok_or_else(|| {
         format!("parse_lazy_index: missing name for addr {:?}", name_addr)
       })?;
-      let hint = match &named.meta.info {
+      let hint = match &named.meta().info {
         super::metadata::ConstantMetaInfo::Def { hints, .. } => Some(*hints),
         _ => None,
       };
@@ -1736,7 +1880,7 @@ impl Env {
       let _name_addr = get_address(buf)?;
       let named = get_named_indexed(buf, &name_reverse_index)?;
       if let super::metadata::ConstantMetaInfo::Def { hints, .. } =
-        &named.meta.info
+        &named.meta().info
       {
         env.anon_hints.insert(named.addr.clone(), *hints);
       }
@@ -1939,7 +2083,7 @@ impl Env {
       let _name_addr = get_address(&mut buf)?;
       let named = get_named_indexed(&mut buf, &name_reverse_index)?;
       if let super::metadata::ConstantMetaInfo::Def { hints, .. } =
-        &named.meta.info
+        &named.meta().info
       {
         env.anon_hints.insert(named.addr.clone(), *hints);
       }
@@ -2141,6 +2285,23 @@ mod tests {
     bools == unpack_bools(bools.len(), pack_bools(bools.clone()))
   }
 
+  #[test]
+  fn put_file_matches_put() {
+    let mut g = Gen::new(24);
+    for i in 0..8 {
+      let env = gen_env(&mut g);
+      let mut buf = Vec::new();
+      env.put(&mut buf).unwrap();
+      let path = std::env::temp_dir()
+        .join(format!("ixon_put_file_test_{}_{i}.ixe", std::process::id()));
+      let written = env.put_file(&path).unwrap();
+      let from_file = std::fs::read(&path).unwrap();
+      std::fs::remove_file(&path).ok();
+      assert_eq!(written as usize, from_file.len());
+      assert_eq!(buf, from_file, "put and put_file bytes diverge");
+    }
+  }
+
   #[test]
   fn test_pack_bools_specific() {
     assert_eq!(pack_bools([true, false, true]), 0b101);
@@ -2271,7 +2432,10 @@ mod tests {
         } else {
           None
         };
-        let named = Named { addr: addr.clone(), meta, original };
+        let mut named = Named::new(addr.clone(), meta);
+        if let Some((orig_addr, orig_meta)) = original {
+          named.set_original(orig_addr, orig_meta);
+        }
         env.named.insert(name, named);
       }
     }
diff --git a/crates/ixvm-codegen/src/env_handle.rs b/crates/ixvm-codegen/src/env_handle.rs
index d92c546cd..f2c0354e0 100644
--- a/crates/ixvm-codegen/src/env_handle.rs
+++ b/crates/ixvm-codegen/src/env_handle.rs
@@ -41,7 +41,7 @@ impl EnvHandle {
       .iter()
       .filter_map(|entry| {
         let named = entry.value();
-        if let ConstantMetaInfo::Def { hints, .. } = &named.meta.info {
+        if let ConstantMetaInfo::Def { hints, .. } = &named.meta().info {
           Some((named.addr.clone(), *hints))
         } else {
           None
diff --git a/crates/kernel/src/ingress.rs b/crates/kernel/src/ingress.rs
index 5b17aa012..b7349bd0b 100644
--- a/crates/kernel/src/ingress.rs
+++ b/crates/kernel/src/ingress.rs
@@ -1895,8 +1895,9 @@ fn ingress_muts_inductive<M: KernelMode>(
       )
     })?;
 
+    let ctor_named_meta = ctor_named.meta();
     let (ctor_lvl_params, ctor_arena, ctor_type_root) =
-      match &ctor_named.meta.info {
+      match &ctor_named_meta.info {
         ConstantMetaInfo::Ctor { lvls, arena, type_root, .. } => {
           (resolve_level_params(lvls, names), arena, *type_root)
         },
@@ -1998,7 +1999,7 @@ fn ingress_muts_block<M: KernelMode>(
       format!("Muts member '{member_name}' not found in named entries")
     })?;
     let member_addr = &member_named.addr;
-    let member_meta = &member_named.meta;
+    let member_meta = &member_named.meta();
 
     let self_id: KId<M> =
       KId::new(member_addr.clone(), M::meta_field(member_name.clone()));
@@ -2586,8 +2587,9 @@ pub fn ingress_compiled_names(
     let mut stats = ConvertStats::default();
 
     // Check if this is a Muts entry (mutual block) — handle differently
-    if matches!(&named.meta.info, ConstantMetaInfo::Muts { .. }) {
-      if let ConstantMetaInfo::Muts { all, .. } = &named.meta.info
+    let named_meta = named.meta();
+    if matches!(&named_meta.info, ConstantMetaInfo::Muts { .. }) {
+      if let ConstantMetaInfo::Muts { all, .. } = &named_meta.info
         && let Ok(entries) = ingress_muts_block(
           name,
           &named.addr,
@@ -2630,7 +2632,7 @@ pub fn ingress_compiled_names(
       name,
       &named.addr,
       &constant,
-      &named.meta,
+      &named_meta,
       ixon_env,
       name_map,
       addr_map,
@@ -2714,7 +2716,7 @@ pub fn build_leon_addr_map(lean_env: &LeanEnv) -> DashMap<Name, Address> {
   // phase from `src/ix/compile/aux_gen.rs:823`. Splitting the two into
   // different types would propagate a signature change through ~5
   // functions with no matching perf win.
-  let entries: Vec<(&Name, &LeanCI)> = lean_env.iter().collect();
+  let entries: Vec<_> = lean_env.iter().collect();
   let map = DashMap::with_capacity(lean_env.len());
   entries.par_iter().for_each(|(name, ci)| {
     map.insert((*name).clone(), Address::from_blake3_hash(ci.get_hash()));
@@ -2975,7 +2977,7 @@ pub fn lean_ingress(lean_env: &LeanEnv) -> KEnv<Meta> {
   let t = Instant::now();
   for (name, ci) in lean_env.iter() {
     let kid = KId::new(leon_addr_of(name, &n2a), name.clone());
-    let kc = lean_const_to_kconst(name, ci, &mut kenv, &n2a);
+    let kc = lean_const_to_kconst(name, &ci, &mut kenv, &n2a);
     kenv.insert(kid, kc);
   }
   if !quiet {
@@ -3049,12 +3051,12 @@ pub fn lean_ingress(lean_env: &LeanEnv) -> KEnv<Meta> {
   let t = Instant::now();
   let mut seeded: FxHashSet<KId<Meta>> = FxHashSet::default();
   for (name, ci) in lean_env.iter() {
-    let block_id = block_rep(name, ci);
+    let block_id = block_rep(name, &ci);
     if !seeded.insert(block_id.clone()) {
       continue;
     }
     let all =
-      lean_constant_all(ci).cloned().unwrap_or_else(|| vec![name.clone()]);
+      lean_constant_all(&ci).cloned().unwrap_or_else(|| vec![name.clone()]);
     let members: Vec<KId<Meta>> =
       all.iter().map(|n| KId::new(leon_addr_of(n, &n2a), n.clone())).collect();
     kenv.blocks.insert(block_id, members);
@@ -3073,9 +3075,9 @@ pub fn lean_ingress(lean_env: &LeanEnv) -> KEnv<Meta> {
   // (`find_peer_recursors` for recs).
   let t = Instant::now();
   for (name, ci) in lean_env.iter() {
-    match ci {
+    match &*ci {
       LeanCI::InductInfo(v) => {
-        let block_id = block_rep(name, ci);
+        let block_id = block_rep(name, &ci);
         for ctor_name in &v.ctors {
           let ctor_kid: KId<Meta> =
             KId::new(leon_addr_of(ctor_name, &n2a), ctor_name.clone());
@@ -3083,7 +3085,7 @@ pub fn lean_ingress(lean_env: &LeanEnv) -> KEnv<Meta> {
         }
       },
       LeanCI::RecInfo(_) => {
-        let block_id = block_rep(name, ci);
+        let block_id = block_rep(name, &ci);
         let self_kid = KId::new(leon_addr_of(name, &n2a), name.clone());
         kenv.blocks.entry(block_id).or_default().push(self_kid);
       },
@@ -3160,7 +3162,7 @@ pub fn build_ixon_ingress_lookups(ixon_env: &IxonEnv) -> IxonIngressLookups {
       .addr_to_name
       .entry(named.addr.clone())
       .or_insert_with(|| name.clone());
-    if let ConstantMetaInfo::Muts { all, .. } = &named.meta.info {
+    if let ConstantMetaInfo::Muts { all, .. } = &named.meta().info {
       lookups
         .muts_by_addr
         .entry(named.addr.clone())
@@ -3364,7 +3366,7 @@ fn ingress_addr_set_into_kenv<M: KernelMode>(
             const_name,
             &addr,
             &constant,
-            &named.meta,
+            &named.meta(),
             ixon_env,
             &lookups.names,
             &lookups.name_to_addr,
@@ -3684,7 +3686,9 @@ fn drop_ixon_env(ixon_env: IxonEnv, quiet: bool) {
   // `anon_hints` is a small FxHashMap (one entry per Def from the .ixe's
   // Named metadata); dropping it inline alongside the bookkeeping below
   // is negligible compared to the DashMap dropdance.
-  let IxonEnv { consts, named, blobs, names, comms, anon_hints: _ } = ixon_env;
+  // `..` covers the env's private fields.
+  let IxonEnv { consts, named, blobs, names, comms, anon_hints: _, .. } =
+    ixon_env;
   let consts_len = consts.len();
   let named_len = named.len();
   let names_len = names.len();
@@ -3797,7 +3801,7 @@ fn ixon_ingress_inner<M: KernelMode>(
   for entry in ixon_env.named.iter() {
     let const_name = entry.key().clone();
     let named = entry.value();
-    match &named.meta.info {
+    match &named.meta().info {
       ConstantMetaInfo::Muts { .. } => {
         work_items.push(IngressWorkItem::Muts(const_name));
       },
@@ -3895,7 +3899,7 @@ fn ixon_ingress_inner<M: KernelMode>(
           &const_name,
           &named.addr,
           &constant,
-          &named.meta,
+          &named.meta(),
           ixon_env,
           &names,
           &name_to_addr,
@@ -3931,7 +3935,8 @@ fn ixon_ingress_inner<M: KernelMode>(
           timing.lookup_ns += elapsed_ns(lookup_start);
         }
 
-        let all = match &named.meta.info {
+        let named_meta = named.meta();
+        let all = match &named_meta.info {
           ConstantMetaInfo::Muts { all, .. } => all,
           _ => {
             timing.convert_stats = convert_stats;
diff --git a/sp1/guest/src/main.rs b/sp1/guest/src/main.rs
index 1ebee5aa8..48b91c16f 100644
--- a/sp1/guest/src/main.rs
+++ b/sp1/guest/src/main.rs
@@ -105,7 +105,7 @@ pub fn main() {
         .named
         .iter()
         .filter(|e| {
-          !matches!(e.value().meta.info, ConstantMetaInfo::Muts { .. })
+          !matches!(e.value().meta().info, ConstantMetaInfo::Muts { .. })
         })
         .map(|e| KId::<Meta>::new(e.value().addr.clone(), e.key().clone())),
     );