Function derive_recursor_universe_poly 

pub fn derive_recursor_universe_poly(
    ctx: &Context,
    ind: &str,
) -> KernelResult<(Vec<String>, Term, Term)>

Build I_rec.{u} — the UNIVERSE-POLYMORPHIC eliminator, Π(P : I → Sort u). … → Π(x). P x with u an explicit level PARAMETER. Returns (level_params, recursor_type, recursor_term).

This is the other half of the motive-sort rule (see motive_target): monomorphic and polymorphic are two DECLARATIONS, not two spellings of one. derive_recursor gives an inductive an eliminator at its own concrete sort — the one a Type 1 inductive needs to recover the Type 0 its constructor stores — and this gives Lean’s Nat.rec.{u}, the one a Type 1-valued family built by recursion over Nat needs. A single artefact cannot be both: a level variable in the motive’s target makes Type 0 ⋠ u (a variable ranges over Prop), so the concrete instance is lost the moment the polymorphic one is claimed.

Register it either way and both reference forms work:

• Context::add_universe_poly + Term::Const { name, levels } — Lean’s explicit Nat.rec.{1}; the level telescope is checked positionally by term::resolve_const_levels.
• Context::add_definition + a bare Term::Global — the application rule turns the free level variable into a metavariable and solves it from the motive actually supplied (type_checker.rs::implicit_levels_for_head).

The soundness gates are NOT parameterised: a non-subsingleton Prop still targets Prop, a subsingleton Prop still targets Type 0, SProp still targets SProp, and an inductive whose own sort is already a level variable keeps that variable rather than gaining a second, independently-instantiable one. A sort provably above Prop (including symbolic successors/maxima) gets an independent motive level.

The returned telescope COVERS the eliminator’s type, in Lean’s order (Eq.rec.{u, u_1}): the motive’s own level first, then the inductive’s levels — its declared universe parameters, in order and including any unused one, or else the levels its arity auto-binds, in first-occurrence order — then any level the type still mentions (a mutual sibling’s). The explicit door refuses a level variable no parameter binds, so only a covering telescope keeps the promise that both reference forms above work.