| 388 | /// `ingress_muts_inductive`) pull addresses out of `ConstantMetaInfo::*::{all, |
| 389 | /// ctx, ctors}`. Those fields store **name-hash** addresses (they were written |
| 390 | /// by compile via `compile_name`), but each KConst is stored in `KEnv` under |
| 391 | /// its **projection** address (the content hash of the `IPrj` / `CPrj` / `RPrj` |
| 392 | /// / `DPrj` struct, or `block_addr` for singleton Muts classes). The two |
| 393 | /// address spaces are different, so we have to round-trip through the Lean |
| 394 | /// name to recover the projection address: |
| 395 | /// |
| 396 | /// name-hash-addr → Lean Name → `ixon_env.named[name].addr` → projection |
| 397 | /// |
| 398 | /// If the `name_to_addr` lookup misses, that means the Named entry we expected |
| 399 | /// the compile pipeline to register is missing — bailing with an error is far |
| 400 | /// better than guessing (the prior behavior synthesized a name-hash address as |