Function require_recorded 

pub fn require_recorded(
    ledger: &Ledger,
    handles: &[String],
) -> Result<Vec<String>>

Theorem 7’s recording obligation, adopted literally (PSP-9 system 14): the kernel refuses to commit any transition that depends on an unrecorded observation. Returns the observation hashes on success so the transition record can content-address them.