Method validate_const_well_scoped

crates/kernel/src/check.rs:428–433

Validate declaration expressions before inference. This is the Ix equivalent of Lean's declaration-admission closure and universe-param checks: declarations must be closed at the top level, and every `Param(idx)` in their type/value/rules must refer to one of the declaration's own universe parameters.

(
    &mut self,
    c: &KConst<M>,
  )

        // `check_recursor` runs the full kernel-driven verification:
        // coherence (major inductive passes A1–A4, K-target flag matches),
        // plus generated-canonical-vs-stored rule comparison via
        // `is_def_eq`. The rule generator is shared between the kernel and
        // the compile-time aux_gen, with the nested-aux ordering selected
        // by `KEnv::recursor_aux_order`, so the syntactic compare is sound
        // against the canonical aux-restored env produced by `ixon_ingress`.
        self.check_recursor_member(id)?;
        Ok(())
      },