Function normalize_checked_at 

pub fn normalize_checked_at(
    ctx: &Context,
    term: &Term,
    tr: Transparency<'_>,
) -> Result<Term, (Term, Unreduced)>

The δ-transparency axis (Lean’s TransparencyMode): normalize_at/normalize_checked_at keep an @[irreducible] constant folded with its body intact, while normalize stays the kernel’s own always-unfolding setting. normalize_checked at a chosen transparency — the honest face of normalize_at.