Function emit_lrat 

pub fn emit_lrat(
    num_vars: usize,
    original: &[Vec<Lit>],
    steps: &[ProofStep],
) -> Result<String, EmitError>

Emit an LRAT proof: each RUP addition as <id> <clause> 0 <hints> 0, deletions as <id> d <deleted-id> 0, and a final empty-clause line. Returns EmitError::PrInRupOnlyFormat for any Pr step (LRAT proper carries no PR witness).