6.3. Dual registry🔗

Two parallel registries, both populated by a single LeanBench.register call emitted by the setup_benchmark macro:

• Compile-time (SimplePersistentEnvExtension): used by anything that needs to inspect the catalogue at elaboration / build time. Stored in the .olean; survives import.

• Runtime (IO.Ref (Std.HashMap Name RuntimeEntry)): used at runtime. Populated at module init via the initialize block the macro emits. The child looks up runner here for dispatch; the parent looks up complexity (to compute ratios) and spec (to drive the ladder).

The dual is unavoidable — env extensions are an elaboration-time concept and the runtime needs callable closures — but the macro emits exactly one LeanBench.register call so the duality stays out of user code.